Two Observations on Intuitionistic Logic and Arithmetic

Explore two key observations on intuitionistic logic and arithmetic in this 36-minute lecture by Benno van den Berg, presented as part of the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into a convenient formalization of arithmetic in finite types, examining both extensional and intensional models with decidable atomic formulas and a version of equality at higher types that includes all congruence laws. Then, investigate negative translations, focusing on the generalization of the Goedel-Gentzen negative translation to arbitrary nuclei and the extension of this concept to the Kuroda negative translation. Gain insights into simple applications of these concepts in the field of intuitionistic logic and arithmetic.