De Jongh’s Theorem for Type Theory
Daniël D. Otten
Abstract:
We investigate the relation between arithmetic and type theory, in particular, we will consider: a constructive axiomatisation of the natural numbers known as Second-order Heyting Arithmetic (HA2), and a version of type theory known as Second-order Propositional Lambda Calculus (λP2). We give an embedding of HA2 in λP2, as well as an interpretation of λP2 in HA2. This will allow us to prove our main result: λP2 + ind + funext + uip proves exactly the same first-order arithmetical formulas as HA2. We will use this result to analyse the logic of λP2. De Jongh’s Theorem shows us that the propositional logic of HA2 is constructive, and we can translate this result to show that the propositional logic of λP2 is also constructive.