# How is induction justified in intuitionistic logic?

This question might be extremely naïve for which I apologise in advance.

The induction principle can be stated as:

If $A ⊂ ℕ$ such that

1. $1 ∈ A$, and
2. $ν(A) ⊂ A$ (where $ν\colon ℕ → ℕ$ is the successor function),

then $A = ℕ$.

It can be proven as follows:

If $ℕ\setminus A$ was non-empty, it would have a least element (which again can be proven from the axiom of regularity using a set-theoretic definition of naturals and using contradiction), say $x ∈ ℕ\setminus A$: By 1.) $x ≠ 1$, so there is a $y ∈ ℕ$ with $x = ν(y)$. By assumption, $y ∈ A$, and by 2.) $x = ν(y) ∈ A$ which cannot be.

This proof uses contradiction. But it is, of course, assuming (other) axioms from ZF.

But how is this handled with intuitionistic logic where contradiction isn’t allowed? Is induction an axiom on its own?

• Bourbaki also uses contradiction in Théorie des ensembles, III.32. – Watson Aug 21 '16 at 12:19

The answer depends on the formal system you are working in. Here are some examples - and indeed, as you speculated it might be the case, in all of them we have induction directly built into the axiomatics or the definition of ${\mathbb N}$:

In Constructive Set Theory like Intuitionistic Zermelo Fraenkel (IZF) you need to find a replacement for the Axiom of Foundation since it implies the Law of Excluded Middle (for a proposition $\phi$, consider a $\in$-minimal element of $\{\emptyset\ |\ \phi\}\cup\{\{\emptyset\}\}$). The (classically equivalent) alternative one uses is the following:

$$\text{(Law of Set Induction):}\quad\quad\forall x ((\forall y\in x: A(y))\Rightarrow A(x))\Rightarrow \forall z: A(z)$$

Thus, inductive proofs of statements parametrized over ${\mathbb N}$ are realized directly through the axiomatics.

In topos theory, which one can also view of an intuitionistic foundation of mathematics, one uses the notion of a natural number object, which is by definition the initial pointed object with an endomorphism. Hence, it is the definition of ${\mathbb N}$ there that maps with domain ${\mathbb N}$ are constructed inductively.

In type theory, ${\mathbb N}$ is an example of an inductive type which usually comes directly with the corresponding induction scheme.

In System F, for example, the natural numbers could be implemented as the polymorphic type ${\mathbb N}:\equiv\forall X: X \to (X\to X)\to X$ which reads as: An element of ${\mathbb N}$ is a uniform procedure to associate to any type $X$, any element $x_0:X$ and any rule $X\to X$ an element of $X$. Indeed it turns out that these are, up to normalization, the Church presentations $\lambda X.\lambda (x_0:X) (f:X\to X). f(f(...(f(x))...))$ of the naturals.

In Coq the definition of an inductive type such as

Inductive Nat := | O : Nat | succ : Nat -> Nat.

automatically results in the implementation of induction schemes such as

Nat_ind: forall P : Nat -> Prop, P O -> (forall n : Nat, P n -> P (succ n)) -> forall n : Nat, P n

allowing the 'inductive' construction of a proof of $\forall n\in{\mathbb N}: P(n)$ out of a proof of $P(0)$ and a rule turning a proof of $P(n)$ into a proof of $P(n+1)$.

• @k.stm: Btw, may I ask, where are you from in Germany? :) – Hanno Jan 27 '15 at 8:11
• Not from Bonn, if you’re hinting at that! ;) Thanks for the elaborate answer. – k.stm Jan 27 '15 at 8:21