4
$\begingroup$

Wikipedia says that

The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies inconsistency.

Why is it impossible to prove within CoC that it is strongly normalizing?

Probably strong normalization property within CoC implies proof of consistency within CoC. Then we can use the second Gödel's incompleteness theorem. If so,

How does strong normalization property within CoC imply proof of consistency within Coc?

UPDATE:

In other words, why there can not exist a term of CoC that is a proof of CoC's proposition that CoC has normalization property. My guess is that such a term could be used to construct a term that proves a proposition of CoC that expresses consistency of CoC which is impossible by the second Gödel's incompleteness theorem. How to construct a proof of consistency within CoC given a proof of normalization property?

$\endgroup$
  • $\begingroup$ I think that it's something like this: if 1) you have weak normalization and 2) you know that False has no normal forms, then you get consistency. Indeed, if you could prove False, then you could normalize that proof and get an impossible normal form for False. $\endgroup$ – chi Nov 14 '16 at 23:47
  • $\begingroup$ @chi: Thank you. I am probably not educated enough to understand your explanation. What does it mean that False has no normal form? Do you refer Πα.α by False? If so, it's a type, and 'has normal form' applies to terms. What do I miss? $\endgroup$ – amakarov Nov 15 '16 at 0:45
  • $\begingroup$ Yes, let False = Πα.α. Of course, False is a term in normal form. Being inconsistent means that there is some proof for that type, i.e. some term $t : \sf False$. Then you take $t$ and normalize it. This should produce a term $t' = \lambda \alpha:*. p$ where $p$ is a normal form such that, for each type $T$ in NF we have $p\{T/\alpha\} : T$ in NF. This is impossible, since e.g. a normal form for $T= A\rightarrow A \rightarrow A \ldots \rightarrow A$ must have that many lambdas inside, but $p$ is fixed and $T$ can be taken arbitrarily large. $\endgroup$ – chi Nov 15 '16 at 8:57
  • $\begingroup$ @chi: You showed that inconsistency prevents strong normalization. As far as I can see this can not help with my question. I asked why we can not proof that CoC has strong normalization property within CoC. Or, in other words, why there can not exist a term of CoC that is a proof of CoC's proposition that CoC has normalization property. My guess is that such a term could be used to construct a term that proves a proposition of CoC that expresses consistency of CoC which is impossible by the second Gödel's incompleteness theorem. $\endgroup$ – amakarov Nov 15 '16 at 11:23
  • $\begingroup$ Yes, that's it. If you can prove within CoC that CoC is normalizing, then you can prove, within CoC, that CoC is consistent. Then you conclude by Gödel that CoC must be inconsistent. $\endgroup$ – chi Nov 15 '16 at 11:32
6
$\begingroup$

I'll summarize the comments from chi, and sketch the proof that

  1. There can be no proof of $\mathrm{False}:=\forall X:*.X$ in the CoC in head normal form. Furthermore, this fact can be proven in a weak theory, say Peano Arithmetic (though the excluded middle is not required).

  2. This fact implies that if the CoC is normalizing, then it is consistent, and furthermore this implication does not use classical logic.

for 1., you proceed by induction on the term structure of a hypothetical closed term $t$ of type $\mathrm{False}$. Actually terms in normal form must be in the form: $$ \lambda x_1:T_1\ldots\lambda x_n:T_n.y\ t_1\ldots t_m$$

where $n$ and $m$ may be $0$. If $n$ is zero, then $t=y\ t_1\ldots t_m$, which is not possible since $t$ is closed (typed in the empty context).

Otherwise, we may apply inversion and conclude that $T_1=*$ (and $x_1=X$), and we get $$ X:*\vdash\lambda x_2\ldots\lambda x_n.y\ t_1\ldots t_m\ :\ X$$ to be derivable in the CoC. Now since $X$ is not a $\Pi$, we can apply inversion again to conclude that $n=1$ and in fact the above term is simply $$ X:*\vdash y\ t_1\ldots t_m\ :\ X$$ Inversion yet again shows that $$X:*\vdash y\ :\ \Pi y_1:U_1\ldots\Pi y_m:U_m.X $$ but $y$ must be $X$, since it is the only variable around! Therefore $m=0$, and $X=*$, which is impossible, contradiction.

Now all this reasoning is intuitionistic, as I've proven a negative (there can be no proof of...) and proofs of negations are always constructive. I do rely heavily on inversion, and you'll just have to take it on faith that this also can be proven in arithmetic, without the excluded middle, which is non-trivial.

Now for 2. we define consistency to mean "does not prove $\mathrm{False}$"! Again a negative statement. Now if the CoC is normalizing, one can take any normal form of a proof of $\mathrm{False}$ and use the above argument to get a contradiction. Again a constructive argument!

Finally to tie it all together. Now suppose you had enough arithmetic to carry out the above arguments in CoC. Note that this is almost possible: you actually need to add the axiom $0\neq 1$ to get anything off the ground. You can then prove that normalization implies consistency within the CoC, and you also have enough arithmetic for the second incompleteness theorem to apply. Therefore you cannot (if CoC is consistent!) prove normalization, as then you would have a full proof of consistency within CoC.

$\endgroup$
  • 1
    $\begingroup$ I think you abused my blog post there a bit. Proofs of negation are not "always constructive". It's just that the usual rule for proving a negation is constructive. And your proof happens to be of this sort. $\endgroup$ – Andrej Bauer Nov 16 '16 at 23:46
  • $\begingroup$ @AndrejBauer you're right, thanks for clarifying that. In general, I believe that proofs of $\Pi^0_1$ statements can always be made constructive, and this happens to be an instance of such a statement (but perhaps this is a digression). $\endgroup$ – cody Nov 17 '16 at 3:08

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.