A note on arithmetic in finite types

2014/08/15 by Benno van den Berg, Berg, Benno van den
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #Mathematical and Theoretical Analysis #Logic, Reasoning, and Knowledge

paper · pdf · doi:10.48550/arxiv.1408.3557

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.

Related

• Apartness and the elimination of strong forms of extensionality
• Functional interpretation and inductive definitions
• Arithmetical conservation results
• The modal logic of arithmetic potentialism and the universal algorithm
• Arithmetic as a theory modulo