A note on arithmetic in finite types
classification
🧮 math.LO
keywords
typesallowsarithmeticfinitecongruencedeductiondefinitionderivable
read the original abstract
We present a version of arithmetic in all finite types which allows for a definition of equality at higher types for which all congruence are derivable, for which the soundness of the Dialectica interpretation is provable inside the system itself, which allows for both intensional and extensional models and for which the deduction theorem holds.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.