14
$\begingroup$

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, 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?
$\endgroup$
  • $\begingroup$ In System F you won't get an induction principle for your Church numerals so they're out of the equations. $\endgroup$ – gallais Nov 21 '16 at 10:37
17
$\begingroup$

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 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 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). 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.

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

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – fhyve Nov 21 '16 at 19:43
  • $\begingroup$ And should it read "if $p$ is normalizing, then $p\not\Vdash\emptyset$? $\endgroup$ – fhyve Nov 21 '16 at 19:46
  • 1
    $\begingroup$ Why do you mean by "in $\mathrm{HA}_\omega$ all functions must be computable"? Certainly not, consider the set-theoretic model. $\endgroup$ – Andrej Bauer Nov 21 '16 at 19:50
  • 1
    $\begingroup$ @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. $\endgroup$ – cody Nov 21 '16 at 20:22
  • 1
    $\begingroup$ Then you should have said something like "definable functions in $\mathrm{HA}_\omega$ are computable". Saying "must be computable" is at least misleading. $\endgroup$ – Andrej Bauer Nov 22 '16 at 7:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.