<p>First a correction. The statement
$$\forall P \,.\, (P(0) \Rightarrow (\forall n . P(n) \Rightarrow P(S n)) \Rightarrow \forall m . P(m)),$$
is <em>not</em> the schema of induction, but rather induction written in second-order arithmetic.
To get the <em>schema</em> 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 <em>formula</em> $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$.</p>

<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 <em>type family</em> or <em>dependent type</em>. 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.</p>

<p>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)$$</p>

<p>What are these types inhabited by? In the case of schema, they are inhabited by <em>primitive recursors</em> $\mathsf{rec}_P$ which satisfy the equations
\begin{align*}
\mathsf{rec}_P \; z \; f \; 0 &amp;= z \\
\mathsf{rec}_P \; z \; f \; (S n) &amp;= 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$.</p>

<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 &amp;= z \\
\mathsf{rec} \; P \; z \; f \; (S n) &amp;= f \; n \; (\mathsf{rec} \;P \; z \; f \; n)
\end{align*}</p>

<p>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 <em>polymorphic</em> $\mathsf{rec}$.</p>

CC BY-SA 3.0
2014-07-28T10:22:29.177Z
2014-07-28T12:22:02.003Z
2014-07-28T12:22:02.003Z
Andrej Bauer
<p>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 <a href="http://ncatlab.org/nlab/show/type+theory" rel="nofollow">nLab entry on type theory</a> and the <a href="http://en.wikipedia.org/wiki/Calculus_of_constructions" rel="nofollow">Wikipedia entry on the calculus of constructions</a> contain a host of references which you may find interesting.  Also, the <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385" rel="nofollow">lecture notes by Sørensen and Urzyczyn</a> are an excellent starting place for learning about the Curry-Howard isomorphism, independently of type theory.</p>

<p>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 <em>Proofs and Types</em> and Krivine's book <em>Lambda-calculus, Types and Models</em> for a formal justification of the above "trick".</p>

CC BY-SA 3.0
2014-07-26T18:46:03.133Z
Thanks! I corrected the question - I am learning Haskell so that was on my mind when I was thinking about this...
Holden Lee
CC BY-SA 3.0
2014-07-26T17:17:08.500Z
2014-07-26T20:24:05.297Z
2014-07-26T20:24:05.297Z
Damiano Mazza
<p>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.</p>

<p>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]$.</p>

<p>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)
$</p>

<p>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.</p>

CC BY-SA 3.0
2014-07-26T17:20:26.570Z
I am not sure this is research level, but I am equally unsure how this would be answered at cs.stackexchange, so I gave an answer below (actually, mostly references).
Damiano Mazza
CC BY-SA 3.0
2014-07-28T10:09:20.190Z
It would be answered on cs.stackexchange, and it is not research-level.
Andrej Bauer
<type-theory><dependent-type>
How to translate the axiom schema of induction by Curry-Howard?
Holden Lee
# How to translate the axiom schema of induction by Curry-Howard?

(Asked by: username_0 on 2014-07-26)

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.

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: I am not sure this is research level, but I am equally unsure how this would be answered at cs.stackexchange, so I gave an answer below (actually, mostly references).  
> **username_2**: It would be answered on cs.stackexchange, and it is not research-level.  

---

## 2 answers

### Answer by username_2 on 2014-07-28. Score: 6 | Accepted answer

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 by username_1 on 2014-07-26. Score: 1

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](http://ncatlab.org/nlab/show/type+theory) and the [Wikipedia entry on the calculus of constructions](http://en.wikipedia.org/wiki/Calculus_of_constructions) contain a host of references which you may find interesting. Also, the [lecture notes by Sørensen and Urzyczyn](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385) 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".

> **Comments:**
> **username_0**: Thanks! I corrected the question - I am learning Haskell so that was on my mind when I was thinking about this...  

---

