How to translate the axiom schema of induction by Curry-Howard?

Question

I'm trying to understand the Curry-Howard correspondence. I am comfortable with it for propositional logic, but get confused when $\forall, \exists$ quantifiers come in the picture.

The axiom schema of induction (in second-order logic) is $\forall P. \left[(P(0) \implies \forall k\in \mathbb N. (P(k)\implies P(k+1)))\implies \forall n\in \mathbb N. P(n)\right]$.

To my understanding, via Curry-Howard every statement gets translated to a type. Proving a statement means showing that the type is inhabited. For example, +, = are dependent types taking two parameters of type nat; every $\forall k\in A$ gets translated into a dependent product $\prod_{k::A}$. So the axiom schema should become something like $ \left[\prod_{P::?} \left((P\, 0) \rightarrow \left(\prod_{k::\mathbb N} (P \, k)\rightarrow P \, (+\, k\, 1) \right)\right)\right]\rightarrow \prod_{n::\mathbb N}(P \,n) $

A difficulty arises when translating $\forall P$: what is the type of $P$? The problem is that, in order for the above to make sense, $(P\, k)$ is supposed to be a type for all $k::\mathbb N$ (so we are allowed to say $(P\, 0) \rightarrow \cdots$, for instance). So $P$ seems to me like a (dependent) type constructor taking a nat as parameter. But then we are taking a product over $P$, so we must be able to treat $P$ as an element of a type! The problem seems to boil down to, are type constructors themselves of some type? Can we write this statement without having to refer to such a type? Perhaps higher-order logic translates to higher-order type theory, but I do not know the latter. References would also be appreciated.

Answer 1

First a correction. The statement $$\forall P \,.\, (P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m)),$$ is not the schema of induction, but rather induction written in second-order arithmetic. To get the schema you need to avoid $\forall P$. This is done by saying that there are infinitely many axioms of the form $$P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m),$$ one for each formula $P(x)$. That is, whereas in your axiom $P$ refers to arbitrary subsets of $\mathbb{N}$, in the schema it refers to sytnactic entities, namely formulas with parameter $x$. It is called a "schema" because it prescribes a shape from which infinitely many axioms may be generated by plugging in all possible syntactic entities $P$.

To answer your question, we just have to look at the Curry-Howard correspondence to see what a predicate $P(x)$ correspond to. The answer is type family or dependent type. Because you wrote your axiom in second-order arithmetic, it became unclear how to quantify over dependent types. This is possible by using universes, for instance Daimano in his answer used $\mathsf{Prop}$, the universe of propositions. However, under the pure Curry-Howard there is no $\mathsf{Prop}$, there are only types.

We have two options. If we translate the schema, then it is this: for every dependent type $$x : \mathbb{N} \vdash P(x) \, \mathsf{type}$$ we get the type $$\textstyle P(0) \to (\prod_{n:\mathbb{N}} P(n) \to P(S n)) \to \prod_{m:\mathbb{N}} P(m)$$ If we translate the second-order formulation of induction, we need to use a type universe $\mathsf{Type}$, and then we get $$\textstyle \prod_{P : \mathbb{N} \to \mathsf{Type}} P(0) \to (\prod_{n:\mathbb{N}} P(n) \to P(S n)) \to \prod_{m:\mathbb{N}} P(m)$$

What are these types inhabited by? In the case of schema, they are inhabited by primitive recursors $\mathsf{rec}_P$ which satisfy the equations \begin{align*} \mathsf{rec}_P \; z \; f \; 0 &= z \\ \mathsf{rec}_P \; z \; f \; (S n) &= f \; n \; (\mathsf{rec}_P \; z \; f \; n) \end{align*} Depending on the details of your formalism we may be able to drop the subscript $P$ on $\mathsf{rec}_P$, and just write $\mathsf{rec}$ -- but secretly there is a different $\mathsf{rec}$ for each $P$.

In the case of the second-order induction we would get a single primitive recursor $\mathsf{rec}$ satisfying \begin{align*} \mathsf{rec} \; P \; z \; f \; 0 &= z \\ \mathsf{rec} \; P \; z \; f \; (S n) &= f \; n \; (\mathsf{rec} \;P \; z \; f \; n) \end{align*}

If I spoke to a Haskell programmer I would say that in the case of schema each $\mathsf{rec}$ was obtained from $P$ using a "deriving" clause, whereas in the second-order case there is a single polymorphic $\mathsf{rec}$.

Answer 2

Yes, in type theory second order variables do have a type, it may be called $Prop$ (the type of propositions) or $Set$ (the type of sets) depending on the context. In your case, I would write $P:\mathbb N\rightarrow Prop$. The nLab entry on type theory and the Wikipedia entry on the calculus of constructions contain a host of references which you may find interesting. Also, the lecture notes by Sørensen and Urzyczyn are an excellent starting place for learning about the Curry-Howard isomorphism, independently of type theory.

An additional note: if you are interested in second order Peano arithmetic and Curry-Howard, you may also want to look into System F before type theory. System F, which corresponds to propositional second order, has an enormous expressive power (precisely related to second order Peano arithmetic) and data types representing inductive structures may be obtained by the following "trick": take the second order formula describing the desired induction principle and "erase" all first order information. In particular, from usual induction (the formula you consider), you get $\forall P.(P\Rightarrow (P\Rightarrow P)\Rightarrow P)$, whose normal forms are exactly the Church integers. See Girard, Lafont and Taylor's book Proofs and Types and Krivine's book Lambda-calculus, Types and Models for a formal justification of the above "trick".