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.

  • $\begingroup$ What's $\sigma$? $\endgroup$ – Asaf Karagila Oct 5 '18 at 6:19
  • $\begingroup$ @AsafKaragila, sorry, it is the successor function. edited. $\endgroup$ – user600670 Oct 5 '18 at 6:21
  • $\begingroup$ Ah, okay, that's what I thought. Note that you need access to second-order logic in order to prove that $(\Bbb N,\sigma)$ is a model of PA. Even if you only want it to be a model of first-order PA. $\endgroup$ – Asaf Karagila Oct 5 '18 at 6:22
  • $\begingroup$ @AsafKaragila, but even the first-order part of the PA cannot be proven to hold for $(\mathbb N,\sigma,0)$ using (first order formal logic + sequent calculus) right? we need to go "outside" of formal logic to do it, right? My guess is that that's not necessary in type theory. Also we can express second order logic in type theory using CHI can we not? $\endgroup$ – user600670 Oct 5 '18 at 6:24
  • $\begingroup$ A remark (I don't have an answer to your question): Peano arithmetic is based on classical logic. The Curry-Howard isomorphism can be extended to classical logic, but via some extensions of the $\lambda$-calculus such as the $\lambda\mu$-calculus. The axiomatization of arithmetic in accordance with intuitionistic logic (and then with the $\lambda$-calculus via Curry-Howard isomorphism) is Heyting arithmetic. $\endgroup$ – Taroccoesbrocco Oct 5 '18 at 11:23

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.

  • $\begingroup$ "Of course you need a specific axiom to get the existance of this initial/inductive structure." Why do we need an axiom? an axiom is a logical statement. My question is about whether we can simply define the natural numbers, define the successor function, without using any axioms (logical propositions), and then prove the truth of the axioms merely from the definition of $\mathbb N$ and $\sigma$ (without using any axioms). Maybe I've misunderstood your answer though. $\endgroup$ – user600670 Oct 9 '18 at 9:22
  • $\begingroup$ @user600670 Sorry I have probably used to much the term axiom. I have edited the answer to make ammends. $\endgroup$ – Giorgio Mossa Oct 9 '18 at 9:37
  • $\begingroup$ @user600670use I have also added two little paragraphs tell me if they address your concerns. $\endgroup$ – Giorgio Mossa Oct 9 '18 at 9:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.