Can we prove that the peano axioms are true for $(\mathbb N, \sigma)$ in type theory?

Question

In mathematical logic that I'm used to (i.e. we have first-order formulas and a sequent calculus to derive formula's from axioms), we never prove that the peano axioms are true for the natural numbers, simply because the proof calculus is "at a completely different level" than the structure $(\mathbb N,\sigma,0)$ or $(\mathbb N,+,0,1)$, where $\sigma$ is the successor function.

But in type theory using the curry-howard isomorphism, we treat proofs as "first class citizens" (quote from wikipedia). That is, we define the underlying structures about which we want to talk as types, but the propositions themselves are also types.

That means that both the peano axioms and the $\sigma$ are $\lambda$-functions in the same "program", and therefore could potentially "talk to each other". i.e. the structure $(\mathbb N,\sigma,0)$ is defined in the same language as the peano axioms.

This made me conjecture: Even though we cannot prove that the peano axioms are true for $(\mathbb N, \sigma,0)$ using (formal logic + sequent calculus), could we prove it using (type theory + curry howard isomorphism)?

• Is my understanding correct, that in (formal logic + sequent calculus), it is the case that $(\mathbb N, \sigma,0)$ and PA are objects within different universes that cannot talk to eachother, but that in (Type theory + CHI) they are in the same universe and can talk to eachother?

• is it correct that we can prove the correctness of the peano axioms from the definition of $(\mathbb N,\sigma,0)$ in (type theory + CHI)? How do we show this?

edit: practically, I'd want to implement this in the Lean theorem prover if possible.

Answer 1

First of all as Asaf Karaglia pointed out you would need to use an higher order logic to talk about structures such as $(\mathbb N,\sigma,0)$ but that is fair considering that even the simply typed $\lambda$-calculus is a form of higher order-logic.

With that in mind we can define $(\mathbb N,\sigma,0)$ as a structure with a given signature satisfying an induction principle, it does not have to be the classical induction principle for natural numbers, for instance it could be an initiality condition.

Of course you need a specific axiom principle-inference rule in your logic-type theory to get the existance of this initial/inductive structure.

Note that you need an induction principle in type theory as well: natural numbers need the induction principle to be able to define functions out of $\mathbb N$ via recursion.

Once you have the inductive structure you easily get the classical induction principle for natural numbers and from that you can easily derive all the other axioms of Peano Arithmetic as is usually done in basic courses of mathematical logic and set theory.

Addendum. Without an induction principle, which must be part of your logic-type theory, and it isnnot part of classical logic and type theories without inductive types you shouldn't be able to get a structure of natural numbers.

In the case of logic it should follow easily by interpreting higher order-logic inside an elementary (boolean) topos without natural number object (which if I remember correctly should exist). I suppose that a similar argument should apply to dependent type theories.

I hope this helps, if you need any additional details feel free to ask.