# Can we prove the Peano axioms from a type theoretic construction of the natural numbers?

Here are two quotes that, while not literally contradictory, reach conclusions that are opposite in spirit.

The first one states that the Peano axioms can be proven to hold for an explicit construction of the Natural numbers in set theory: Wikipedia states:

The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.

The second one states that at least one of the axioms (induction) cannot be proven to hold for an explicit construction of the natural numbers in type theory. Nederpelt & Geuvers (Type theory and formal proof, an introduction. p. 306) state:

It has been shown that induction, one of the most fundamental proof principles of natural numbers, cannot be derived by means of the (polymorphic) Church numerals. Hence, we need an extra axiom to represent it.

What explains this difference?

Set theory and type theory are both proposed as a "foundation of mathematics". Based on my naive perspective, these two quotes seem to suggest that there is an important difference between the two, as foundations of mathematics. Is this intuition correct?

Is there a way to "solve" this, by somehow extending type theory, or something like that, so that the peano axioms can be proven true for some construction of the naturals in type theory?

• Have you read the Wikipedia article Peano axioms? The problematic axiom is indeed the induction axiom. What is your source for "type theory as a foundations of mathematics"? – Somos Apr 24 at 21:58
• I don't think your intuition is correct. The axiom system ZF needs the axiom of infinity to justify the construction of the set of natural numbers and to prove the induction principle. Likewise type theory needs a boost of some sort to justify the construction and prove the induction principle. – Rob Arthan Apr 24 at 22:16
• @RobArthan Your comment could be interpreted as saying that ZF doesn't include the axiom of infinity, so I just wanted to clarify that it does include this axiom. Of course, the point is a good one: if we remove this axiom, we can't construct $\omega$ in the resulting system. – Alex Kruckman Apr 26 at 17:46
• @Alex: yes. What I wrote was intended to mean "The axiom system ZF includes the axiom of infinity because it is needed to justify ...". – Rob Arthan Apr 27 at 23:16

The quote from Nederpelt & Geuvers in the question has been abridged. They actually write:

Firstly, it has been shown that induction, one of the most fundamental proof principles of natural numbers, cannot be derived by means of the polymorphic Church numerals, not in λ2 or λP2 (Geuvers, 2001), and also not in λD. Hence, we need an extra axiom to represent it.

A key point here is that the authors are discussing Church numerals in particular. The second half of p. 305 and the top half of p. 306 are devoted to explaining why the natural numbers should not be formalized as Church numerals in the systems they have described. After that discussion, they go on to formalize the integers and natural numbers in a different way.

On p. 313, after formalizing the naturals and integers, they write:

Again, it is not necessary to formulate [induction for the natural numbers] as an extra axiom, because it is a theorem: it can be derived from our axioms for integers and the definition of N.

There is no contradiction. On one hand, they don't use Church numerals. The more important point is that they assume various axioms about the integers, in their Figure 14.3, and construct the natural numbers as predicate on the integers.

There are interesting differences between type theory and set theory. They approach mathematics from almost opposite perspectives (essentially: highly typed versus completely untyped). But both type theory and set theory can produce foundational systems strong enough for practical use in formalizing everyday mathematics, including the Peano postulates.

Of course it is necessary to include enough axioms in either kind of theory to prove the results that you are interested in. In set theory, this assumption takes the form of the "axiom of infinity", without which ZFC set theory cannot prove there is any infinite set. In type theory, we will also need an axiom showing there is a type with an infinite number of elements, and with appropriate functions. The axioms in Figure 14.3 are one way to achieve this.

As a follow up: the OP is asking why is appears that type theory "explicitly" assumes the induction principle for $$N$$, while set theory "proves" it. However, this is just an artifact of the way that set theory and type theory quantify over predicates. If we use a somewhat unnatural definition of $$N$$ in type theory, we can mimic the same kind of definition as in set theory.

In set theory, we use the axiom of infinity and a set existence axiom to produce a set $$\omega$$ which is the smallest set containing $$0$$ and closed under the operation $$\operatorname{succ}\colon x \mapsto \{x\} \cup x$$. In particular, letting $$I$$ be the set from the axiom of infinity, we define $$\omega = \bigcap \{ S \subseteq I : 0 \in S \land (\forall x)[x \in S \to \operatorname{succ}(x) \in S\}.$$ Here, the quantifier is over all subsets $$S\subseteq I$$, rather than over all "properties". Interestingly, this is a kind of impredicative definition: the set $$\omega$$ itself is one of the candidates for $$S$$ in the intersection.

With this definition, the "second order" induction axiom $$0 \in S \land (\forall n \in N)[n \in S \to n+1 \in S) \to (\forall m)[m \in S]$$ follows immediately from the definition of $$\omega$$.

In type theory, we will similarly need some axioms to assert the existence of a type $$N$$ that contains an initial element $$0$$ and is inductively generated by a function $$s\colon N \to N$$. The issue is how to formalize "is inductively generated by" within type theory. Of course, part of being "inductively generated" is that, for every $$f \colon N \to \{T, F\}$$, if $$f(0)$$ and $$(\forall n:N)[ fn \to f(n+1)]$$ then $$(\forall k:N) fk$$. The authors state this as the 'axiom of induction'.

If we insisted, in type theory we could instead mimic the set theoretic definition of $$N$$ by defining a function $$g \colon N \to \{T,F\}$$ by $$gk \leftrightarrow (\forall f \colon N \to \{T,F\})[f0 \land (\forall m : N)[fm \to f(m+1)] \to fk]$$ This is also an impredicative definition: $$g$$ itself is a candidate for $$f$$. With that definition, we could let $$N'$$ be the subset of $$N$$ defined the predicate $$g$$, and we could prove that induction holds for $$N'$$, immediately from the definition of $$g$$. However, that is not the way that type theory is normally used, because it misses the spirit of type theory.

The axiom of induction for $$N$$ is better viewed as a basic axiom of type theory - it is simply the way that type theory expresses the inductive construction of $$N$$ from $$0$$ and $$s$$. We would have a similar induction axiom for any inductively defined type, so we are not really assuming anything about $$N$$ beyond what would normally be assumed about an inductively defined type.

Analogously, the general set existence axioms in set theory allow us to form subsets of $$N$$, but we don't view them as special assumptions about the natural numbers - the set existence axioms are just part of set theory, just as induction principles for inductively defined types are part of type theory.

• The contents of Figure 14.3 are their construction / formalization of the integers in type theory. They add axioms to their type theory asserting a type $Z$ and a bijection $s$ from $Z$ to $Z$. They then construct the natural numbers as a predicate on the integers. Once they have the natural number $0$, they can indeed define $1 = s 0$, $2 = s 1$, etc. – Carl Mummert Apr 25 at 11:50
• Normally, in foundational contexts, both "construct" and "formalize" mean the same thing: to start with an informal mathematical object, make a formal definition of a formal object within a particular formal theory and then prove within that theory that the newly defined formal object has properties reminiscent of the mathematical object. This is what happens, for example, in the construction of the natural numbers in set theory: we define "formal $N$" to be $\omega$, the set of finite ordinals, and then prove that formal $N$ satisfies the Peano postulates. – Carl Mummert Apr 25 at 11:55
• I think I see what you mean now. – Carl Mummert Apr 25 at 13:15
• @user56834 As Carl Mummert indirectly suggests, you may be attributing too much to "construction" in set theory. In practice, being coy about assuming the existence of naturals (or something clearly more powerful) is silly. In ZFC, the naturals are usually defined as the smallest inductive set, but for this to make sense we need to know that some inductive set exists which is exactly what the Axiom of Infinity states. The Axiom of Infinity is one a step away from just assuming the naturals directly. However, that step is a bit of a doozy. The definition "smallest inductive set" is ... – Derek Elkins Apr 25 at 22:51
• ... impredicative, as Carl Mummert states. Impredicativity has often been seen as logically dubious (and many type theories rule it out) and is pretty powerful. Even if one accepts it, they may not want their notion of the naturals to depend on it. One concern is how meaningful it is to say an impredicative definition "constructs" something. Let's review what ZFC is actually doing to "construct" the naturals. Step 1: Assume a set $I$ that contains the naturals. Step 2: Dig through the (uncountable!) powerset of $I$ (which also just exists by assumption) and (somehow) pick the smallest. – Derek Elkins Apr 25 at 22:51