<p>I'll summarize the comments from chi, and sketch the proof that</p>
<ol>
<li><p>There can be no proof of <span class="math-container">$\mathrm{False}:=\forall X:*.X$</span> 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).</p>
</li>
<li><p>This fact implies that if the CoC is normalizing, then it is consistent, and furthermore this implication does not use classical logic.</p>
</li>
</ol>
<p>for 1., you proceed by induction on the term structure of a hypothetical closed term <span class="math-container">$t$</span> of type <span class="math-container">$\mathrm{False}$</span>. Actually terms in normal form must be in the form:
<span class="math-container">$$ \lambda x_1:T_1\ldots\lambda x_n:T_n.y\ t_1\ldots t_m$$</span></p>
<p>where <span class="math-container">$n$</span> and <span class="math-container">$m$</span> may be <span class="math-container">$0$</span>. If <span class="math-container">$n$</span> is zero, then <span class="math-container">$t=y\ t_1\ldots t_m$</span>, which is not possible since <span class="math-container">$t$</span> is closed (typed in the empty context).</p>
<p>Otherwise, we may apply inversion and conclude that <span class="math-container">$T_1=*$</span> (and <span class="math-container">$x_1=X$</span>), and we get
<span class="math-container">$$ X:*\vdash\lambda x_2\ldots\lambda x_n.y\ t_1\ldots t_m\ :\ X$$</span>
to be derivable in the CoC. Now since <span class="math-container">$X$</span> is not a <span class="math-container">$\Pi$</span>, we can apply inversion again to conclude that <span class="math-container">$n=1$</span> and in fact the above term is simply
<span class="math-container">$$ X:*\vdash y\ t_1\ldots t_m\ :\ X$$</span>
Inversion yet again shows that
<span class="math-container">$$X:*\vdash y\ :\ \Pi y_1:U_1\ldots\Pi y_m:U_m.X $$</span>
but <span class="math-container">$y$</span> must be <span class="math-container">$X$</span>, since it is the only variable around! Therefore <span class="math-container">$m=0$</span>, and <span class="math-container">$X=*$</span>, which is impossible, contradiction.</p>
<p>Now all this reasoning is intuitionistic, as I've proven a <em>negative</em> (there <em>can be no</em> proof of...) and  <s>proofs of negation are always constructive</s> <a href="http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/" rel="nofollow noreferrer">the logical rule for the proof of a negation is constructive</a>. 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.</p>
<p>Now for 2. we <em>define</em> consistency to mean &quot;does not prove <span class="math-container">$\mathrm{False}$</span>&quot;! Again a negative statement. Now if the CoC is normalizing, one can take any normal form of a proof of <span class="math-container">$\mathrm{False}$</span> and use the above argument to get a contradiction. Again a constructive argument!</p>
<p>Finally to tie it all together. Now suppose you had enough arithmetic to carry out the above arguments in CoC. Note that this is <em>almost</em> possible: you actually need to add the axiom <span class="math-container">$0\neq 1$</span> 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 <em>cannot</em> (if CoC is consistent!) prove normalization, as then you would have a full proof of consistency within CoC.</p>

CC BY-SA 3.0
2016-11-16T23:46:36.773Z
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.
Andrej Bauer
CC BY-SA 3.0
2016-11-17T03:08:12.327Z
@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).
cody
CC BY-SA 4.0
2016-11-15T13:39:32.590Z
2023-01-21T20:32:02.847Z
2023-01-21T20:32:02.847Z
cody
<p><a href="https://en.wikipedia.org/wiki/Calculus_of_constructions" rel="noreferrer">Wikipedia</a> says that</p>

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

<p><em>Why is it impossible to prove within CoC that it is strongly normalizing?</em></p>

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

<p><em>How does strong normalization property within CoC imply proof of consistency within Coc?</em></p>

<p><strong>UPDATE:</strong></p>

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

CC BY-SA 3.0
2016-11-14T23:47:12.423Z
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.
chi
CC BY-SA 3.0
2016-11-15T00:45:04.670Z
@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?
amakarov
CC BY-SA 3.0
2016-11-15T08:57:05.780Z
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.
chi
CC BY-SA 3.0
2016-11-15T11:23:26.027Z
@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.
amakarov
CC BY-SA 3.0
2016-11-15T11:32:35.710Z
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.
chi
CC BY-SA 3.0
2016-11-15T11:55:38.290Z
@chi: But your proof requires tertium not datur within CoC, right?
amakarov
CC BY-SA 3.0
2016-11-15T13:29:14.720Z
I am not completely sure about tertium non datur/law of excluded middle, maybe you don't need it. Also, I am not completely confident about how 2nd Gödel's incompleteness theorem works inside a constructive logic like CoC. I hope some expert can give a proper answer.
chi
<type-theory><calculus-of-constructions><normalization>
Strong normalization property of CoC inside CoC
amakarov
# Strong normalization property of CoC inside CoC

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

[Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions) 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?

**Tags:** type-theory, calculus-of-constructions, normalization

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1: 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?  
> **username_1**: 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.  
> **username_0**: @username_1: 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.  
> **username_1**: 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.  
> **username_0**: @username_1: But your proof requires tertium not datur within CoC, right?  
> **username_1**: I am not completely sure about tertium non datur/law of excluded middle, maybe you don't need it. Also, I am not completely confident about how 2nd Gödel's incompleteness theorem works inside a constructive logic like CoC. I hope some expert can give a proper answer.  

---

## 1 answers

### Answer by username_2 on 2016-11-15. Score: 10 | Accepted answer

I'll summarize the comments from username_1, 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 negation are always constructive~~ [the logical rule for the proof of a negation is constructive](http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/). 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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: @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).  

---

