<p>The short answer to your question 1 is <em>no</em>, but for perhaps subtle reasons.</p>

<p>First of all, System $F$ and $F_\omega$ <strong>cannot express the first-order theory of arithmetic</strong>, and even less the consistency of $\mathrm{PA}$.</p>

<p>Secondly, and this is really surprising, $\mathrm{PA}$ can actually prove consistency of both those systems! This is done using the so-called <strong>proof-irrelevant model</strong>, which interprets types as sets $\in\{\varnothing,\{\bullet\}\}$, where $\bullet$ is some dummy element representing an inhabitant of a non-empty type. Then one can write down simple rules for the operation of $\rightarrow$ and $\forall$ on such types rather easily to get a model for system $F$, in which the type $\forall X.X$ is interpreted by $\varnothing$. One can do a similar thing for $F_\omega$, using a bit more care to interpret higher kinds as finite functions spaces.</p>

<p>There's an apparent paradox here, where $\mathrm{PA}$ can prove consistency of these seemingly powerful systems, but not (as I'll show in a moment) normalization.</p>

<p>The missing ingredient here is <strong>realizability</strong>. Realizability is a way to make certain programs correspond to certain propositions, typically in arithmetic. I won't go into the details here, but if a program $p$ realizes a proposition $\phi$, written $p\Vdash \phi$, then we have a certain piece of evidence for $\phi$, in particular if $p$ is normalizing, then $p\not\Vdash\bot$. We have:</p>

<blockquote>
  <p>Theorem: If $\phi$ is a theorem of 2nd order arithmetic $\mathrm{PA}_2$, then there is some closed term $t$ of system $F$ such that $$ t\Vdash\phi$$</p>
</blockquote>

<p><em>This</em> theorem can be proven in $\mathrm{PA}$, and so we have
$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}_2$ is consistent} $$
and Gödel's argument applies (and $\mathrm{PA}$ cannot prove normalization of system $F$). It's useful to note that the reverse implication holds as well, so we have an exact characterization of the proof-theoretic power needed to prove normalization of system $F$.</p>

<p>There is a similar story for system $F_\omega$, which, I believe, corresponds to higher arithmetic $\mathrm{PA}_\omega$.</p>

<hr>

<p>Finally, we have the tricky case of MLTT with inductive types. Here again a somewhat subtle issue arises. Certainly here we can express the consistency of $\mathrm{PA}$, so that isn't an issue, and there is no proof-irrelevant model, as we can prove that the type $\mathrm{Nat}$ has at least 2 elements (an infinite amount of distinct elements, in fact).</p>

<p>However we run into a surprising fact of higher-order intuitionistic theories: $\mathrm{HA}_\omega$, the higher-order version of Heyting Arithmetic is <strong>conservative</strong> over $\mathrm{HA}$! In particular, we cannot prove consistency of $\mathrm{PA}$, (which is equivalent to that of $\mathrm{HA}$). An intuitive reason for this is that intuitionistic function spaces do not allow you to quantify over arbitrary subset of $\mathbb{N}$, since all definable functions $\mathbb{N}\rightarrow \mathbb{N}$ must be computable.</p>

<p>In particular, I don't think you can prove consistency of $\mathrm{PA}$ if you add only natural numbers to MLTT without universes. I do believe adding either universes or "stronger" inductive types (like ordinal types) will give you enough power though, but I'm afraid I have no reference for this. With universes, the argument seems quite simple though, since you have enough set theory to build a model of $\mathrm{HA}$.</p>

<hr>

<p>Finally, references for the proof theory of type systems: there's really a gap in the literature here I think, and I would relish a clean treatment of all these subjects (in fact, I dream of writing it myself some day!). In the meantime:</p>

<ul>
<li><p>The proof-irrelevant model is explained <a href="http://www.lix.polytechnique.fr/Labo/Benjamin.Werner/publis/cc.pdf" rel="noreferrer">here</a> by Miquel and Werner, though they do it for the Calculus of Constructions, which complicates matters somewhat.</p></li>
<li><p>The realizability argument is sketched in the classic <a href="http://www.paultaylor.eu/stable/prot.pdf" rel="noreferrer">Proofs and Types</a> of Girard, Taylor and Lafont. I think they also sketch the proof-irrelevant model, and a great deal of useful things besides. It's probably the first reference to read.</p></li>
<li><p>The conservativity argument of higher-order Heyting arithmetic can be found in the elusive second volume of <em>Constructivism in Mathematics</em> by Troelstra &amp; van Dalen (see <a href="http://store.elsevier.com/Constructivism-in-Mathematics-Vol-2/A_S_-Troelstra/isbn-9780080955100/" rel="noreferrer">here</a>). Both volumes are extremely informative, but quite difficult to read for a novice, IMHO. It also somewhat avoids "modern" type theory subjects, which is unsurprising given the books' age.</p></li>
</ul>

<hr>

<p>An additional question in the comments was about the exact consistency strength/normalization strength of MLTT+Inductives. I don't have a precise answer here, but certainly the answer depends on the number of universes and the nature of the inductive families allowed. Rathjen explores this question in the excellent paper <a href="https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf" rel="noreferrer"><em>The Strength of some Martin-Lof Type theories</em></a>.</p>

<p>Wrt normalization, the basic idea is that if, for 2 theories $\cal{T}$ and $\cal{U}$, we have
$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U}) $$</p>

<p>then, <strong>generally</strong></p>

<p>$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U}) $$</p>

<p>where 1-$\mathrm{Con}$ is <a href="https://en.wikipedia.org/wiki/%CE%A9-consistent_theory" rel="noreferrer">1-consistency</a> and $\mathrm{Norm}$ is (weak) normalization.</p>

<p>MLTT + the type of natural numbers (and recursion) is a conservative extension of $\mathrm{HA}_\omega$, which is proven in Besson <a href="http://ac.els-cdn.com/0003484382900031/1-s2.0-0003484382900031-main.pdf" rel="noreferrer"><em>Recursive Models for Constructive Set Theories</em></a>.</p>

<p>As far as MLTT with induction-recursion or induction-induction, I don't know what the situation is, and AFAIK, the problem of exact consistency strength is still open.</p>

CC BY-SA 3.0
2016-11-21T19:43:04.460Z
So in a sense, system F is a very weak theory, but it has this combinatorial problem which requires a very strong theory to prove? If that's the case, then shouldn't its proof theoretic ordinal be known, and less than $\epsilon_0$, contradicting the question that I linked?
fhyve
CC BY-SA 3.0
2016-11-21T19:46:08.013Z
And should it read "if $p$ is normalizing, then $p\not\Vdash\emptyset$?
fhyve
CC BY-SA 3.0
2016-11-21T19:50:12.147Z
Why do you mean by "in $\mathrm{HA}_\omega$ all functions *must* be computable"? Certainly not, consider the set-theoretic model.
Andrej Bauer
CC BY-SA 3.0
2016-11-21T20:14:54.480Z
@fhyve: I meant $p\not\Vdash\bot$ rather than $p\not\Vdash\phi$. Corrected
cody
CC BY-SA 3.0
2016-11-21T20:18:32.667Z
@fhyve System F doesn't have a proof theoretic ordinal, *per se*, since it isn't even a theory of arithmetic, just a quantified propositional logic. In this sense it is indeed a very weak theory. It's strength comes from the fact that as a *programing language*, it may serve as a language of realizers for higher-order arithmetic.
cody
CC BY-SA 3.0
2016-11-21T20:22:55.447Z
@AndrejBauer certainly, all functions $\mathbb{N}\rightarrow\mathbb{N}$ which can be proven to exist within $\mathrm{HA}_\omega$ are computable (from the "outside"). Of course, from the "inside", it is consistent to assume that there are non-computable functions, unless further fun axioms are added.
cody
CC BY-SA 3.0
2016-11-22T07:33:41.933Z
Then you should have said something like "definable functions in $\mathrm{HA}_\omega$ are computable". Saying "must be computable" is at least misleading.
Andrej Bauer
CC BY-SA 3.0
2016-11-22T12:40:13.227Z
Fair enough, I'll amend the post.
cody
CC BY-SA 3.0
2016-11-22T21:15:55.920Z
You don't say much about what it takes to prove normalization of MLTT + inductive types. Do you know much about that? If not, I can accept your answer and ask that in a separate question
fhyve
CC BY-SA 3.0
2016-11-22T22:42:30.497Z
I'm mostly concerned with MLTT +/- Nat, W-types, and 1 or n universes. After that, then maybe $\omega$ or more universes, induction-induction, and the like.
fhyve
CC BY-SA 3.0
2016-11-21T13:45:02.910Z
2016-11-23T17:19:42.433Z
2016-11-23T17:19:42.433Z
cody
<p>For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F_\omega$ are consistent. MLTT + inductive types also has a normalization proof. However, these should all be powerful enough to construct a model of PA, which proves that PA is consistent from these theories. System $F$ is <a href="https://cstheory.stackexchange.com/questions/8623/can-we-prove-weak-normalization-for-system-f-by-induction-on-a-transfinite-ordin">quite powerful</a>, so I expect it to be able to prove the consistency of PA by constructing a model using Church numerals. MLTT + IT has a natural numbers inductive type and should prove consistency as well.</p>

<p>This all implies that the normalization proofs for these theories can't be internalized in PA. So:</p>

<ol>
<li>Can system $F$, system $F_\omega$, and MLTT + IT actually prove the consistency of PA?</li>
<li>If they can, then what metatheory is needed to prove normalization for system $F$, $F_\omega$, and MLTT+IT?</li>
<li>Is there a good reference for the proof theory of type theories in general, or for some of these type theories in particular?</li>
</ol>

CC BY-SA 3.0
2016-11-21T10:37:03.590Z
In System F you won't get an induction principle for your Church numerals so they're out of the equations.
gallais
<type-theory><proof-theory>
Relative consistency of PA and some type theories
fhyve
# Relative consistency of PA and some type theories

(Asked by: username_0 on 2016-11-21)

For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F\_\omega$ are consistent. MLTT + inductive types also has a normalization proof. However, these should all be powerful enough to construct a model of PA, which proves that PA is consistent from these theories. System $F$ is [quite powerful](https://cstheory.stackexchange.com/questions/8623/can-we-prove-weak-normalization-for-system-f-by-induction-on-a-transfinite-ordin), so I expect it to be able to prove the consistency of PA by constructing a model using Church numerals. MLTT + IT has a natural numbers inductive type and should prove consistency as well.

This all implies that the normalization proofs for these theories can't be internalized in PA. So:

1. Can system $F$, system $F\_\omega$, and MLTT + IT actually prove the consistency of PA?
2. If they can, then what metatheory is needed to prove normalization for system $F$, $F\_\omega$, and MLTT+IT?
3. Is there a good reference for the proof theory of type theories in general, or for some of these type theories in particular?

**Tags:** type-theory, proof-theory

> **Comments:**
> **username_1**: In System F you won't get an induction principle for your Church numerals so they're out of the equations.  

---

## 1 answers

### Answer by username_2 on 2016-11-21. Score: 20 | Accepted answer

The short answer to your question 1 is *no*, but for perhaps subtle reasons.

First of all, System $F$ and $F\_\omega$ **cannot express the first-order theory of arithmetic**, and even less the consistency of $\mathrm{PA}$.

Secondly, and this is really surprising, $\mathrm{PA}$ can actually prove consistency of both those systems! This is done using the so-called **proof-irrelevant model**, which interprets types as sets $\in\{\varnothing,\{\bullet\}\}$, where $\bullet$ is some dummy element representing an inhabitant of a non-empty type. Then one can write down simple rules for the operation of $\rightarrow$ and $\forall$ on such types rather easily to get a model for system $F$, in which the type $\forall X.X$ is interpreted by $\varnothing$. One can do a similar thing for $F\_\omega$, using a bit more care to interpret higher kinds as finite functions spaces.

There's an apparent paradox here, where $\mathrm{PA}$ can prove consistency of these seemingly powerful systems, but not (as I'll show in a moment) normalization.

The missing ingredient here is **realizability**. Realizability is a way to make certain programs correspond to certain propositions, typically in arithmetic. I won't go into the details here, but if a program $p$ realizes a proposition $\phi$, written $p\Vdash \phi$, then we have a certain piece of evidence for $\phi$, in particular if $p$ is normalizing, then $p\not\Vdash\bot$. We have:

> Theorem: If $\phi$ is a theorem of 2nd order arithmetic $\mathrm{PA}\_2$, then there is some closed term $t$ of system $F$ such that $$ t\Vdash\phi$$

*This* theorem can be proven in $\mathrm{PA}$, and so we have
$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}\_2$ is consistent} $$
and Gödel's argument applies (and $\mathrm{PA}$ cannot prove normalization of system $F$). It's useful to note that the reverse implication holds as well, so we have an exact characterization of the proof-theoretic power needed to prove normalization of system $F$.

There is a similar story for system $F\_\omega$, which, I believe, corresponds to higher arithmetic $\mathrm{PA}\_\omega$.

---

Finally, we have the tricky case of MLTT with inductive types. Here again a somewhat subtle issue arises. Certainly here we can express the consistency of $\mathrm{PA}$, so that isn't an issue, and there is no proof-irrelevant model, as we can prove that the type $\mathrm{Nat}$ has at least 2 elements (an infinite amount of distinct elements, in fact).

However we run into a surprising fact of higher-order intuitionistic theories: $\mathrm{HA}\_\omega$, the higher-order version of Heyting Arithmetic is **conservative** over $\mathrm{HA}$! In particular, we cannot prove consistency of $\mathrm{PA}$, (which is equivalent to that of $\mathrm{HA}$). An intuitive reason for this is that intuitionistic function spaces do not allow you to quantify over arbitrary subset of $\mathbb{N}$, since all definable functions $\mathbb{N}\rightarrow \mathbb{N}$ must be computable.

In particular, I don't think you can prove consistency of $\mathrm{PA}$ if you add only natural numbers to MLTT without universes. I do believe adding either universes or "stronger" inductive types (like ordinal types) will give you enough power though, but I'm afraid I have no reference for this. With universes, the argument seems quite simple though, since you have enough set theory to build a model of $\mathrm{HA}$.

---

Finally, references for the proof theory of type systems: there's really a gap in the literature here I think, and I would relish a clean treatment of all these subjects (in fact, I dream of writing it myself some day!). In the meantime:

* The proof-irrelevant model is explained [here](http://www.lix.polytechnique.fr/Labo/Benjamin.Werner/publis/cc.pdf) by Miquel and Werner, though they do it for the Calculus of Constructions, which complicates matters somewhat.
* The realizability argument is sketched in the classic [Proofs and Types](http://www.paultaylor.eu/stable/prot.pdf) of Girard, Taylor and Lafont. I think they also sketch the proof-irrelevant model, and a great deal of useful things besides. It's probably the first reference to read.
* The conservativity argument of higher-order Heyting arithmetic can be found in the elusive second volume of *Constructivism in Mathematics* by Troelstra & van Dalen (see [here](http://store.elsevier.com/Constructivism-in-Mathematics-Vol-2/A_S_-Troelstra/isbn-9780080955100/)). Both volumes are extremely informative, but quite difficult to read for a novice, IMHO. It also somewhat avoids "modern" type theory subjects, which is unsurprising given the books' age.

---

An additional question in the comments was about the exact consistency strength/normalization strength of MLTT+Inductives. I don't have a precise answer here, but certainly the answer depends on the number of universes and the nature of the inductive families allowed. Rathjen explores this question in the excellent paper [*The Strength of some Martin-Lof Type theories*](https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf).

Wrt normalization, the basic idea is that if, for 2 theories $\cal{T}$ and $\cal{U}$, we have
$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U}) $$

then, **generally**

$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U}) $$

where 1-$\mathrm{Con}$ is [1-consistency](https://en.wikipedia.org/wiki/%CE%A9-consistent_theory) and $\mathrm{Norm}$ is (weak) normalization.

MLTT + the type of natural numbers (and recursion) is a conservative extension of $\mathrm{HA}\_\omega$, which is proven in Besson [*Recursive Models for Constructive Set Theories*](http://ac.els-cdn.com/0003484382900031/1-s2.0-0003484382900031-main.pdf).

As far as MLTT with induction-recursion or induction-induction, I don't know what the situation is, and AFAIK, the problem of exact consistency strength is still open.

> **Comments:**
> **username_0**: So in a sense, system F is a very weak theory, but it has this combinatorial problem which requires a very strong theory to prove? If that's the case, then shouldn't its proof theoretic ordinal be known, and less than $\epsilon_0$, contradicting the question that I linked?  
> **username_0**: And should it read "if $p$ is normalizing, then $p\not\Vdash\emptyset$?  
> **username_3**: Why do you mean by "in $\mathrm{HA}_\omega$ all functions *must* be computable"? Certainly not, consider the set-theoretic model.  
> **username_2**: @username_0: I meant $p\not\Vdash\bot$ rather than $p\not\Vdash\phi$. Corrected  
> **username_2**: @username_0 System F doesn't have a proof theoretic ordinal, *per se*, since it isn't even a theory of arithmetic, just a quantified propositional logic. In this sense it is indeed a very weak theory. It's strength comes from the fact that as a *programing language*, it may serve as a language of realizers for higher-order arithmetic.  
> **username_2**: @AndrejBauer certainly, all functions $\mathbb{N}\rightarrow\mathbb{N}$ which can be proven to exist within $\mathrm{HA}_\omega$ are computable (from the "outside"). Of course, from the "inside", it is consistent to assume that there are non-computable functions, unless further fun axioms are added.  
> **username_3**: Then you should have said something like "definable functions in $\mathrm{HA}_\omega$ are computable". Saying "must be computable" is at least misleading.  
> **username_2**: Fair enough, I'll amend the post.  
> **username_0**: You don't say much about what it takes to prove normalization of MLTT + inductive types. Do you know much about that? If not, I can accept your answer and ask that in a separate question  
> **username_0**: I'm mostly concerned with MLTT +/- Nat, W-types, and 1 or n universes. After that, then maybe $\omega$ or more universes, induction-induction, and the like.  

---

