<p>First, you are confusing consistency of CIC <em>as an equational theory</em> with consistency of CIC <em>as a logical theory</em>. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second.  This, as has been pointed out in the comments, is implied instead by (weak) normalization. The prototypical example of this situation is the pure $\lambda$-calculus: it is equationally consistent (CR holds) but, if you consider it as a logical system (as Alonzo Church orginally intended) it is inconsistent (indeed, it does not normalize).</p>

<p>Second, as Emil pointed out, even if CIC has a given property (CR or normalization) it is perfectly possible that CIC cannot itself prove that property. In this case, I do not see any inconsistency in the fact that CIC is able to prove its own CR property, and I guess that this is indeed the case (elementary combinatorial arguments usually suffice for CR, and such arguments definitely fall within the huge logical power of CIC).  However, CIC certainly does not prove its own normalization property, precisely because of the second incompleteness theorem.</p>

CC BY-SA 3.0
2016-01-01T13:28:01.377Z
+1 Thanks! Could you just elaborate a little bit how is that (weak) normalization property implies consistency (of a logical theory)? i.e. how is that the fact that every term has a normal form implies that $\bot$ is inhabited?
StudentType
CC BY-SA 3.0
2016-01-01T19:03:31.130Z
Of course!  It is essentially the fact that cut-elimination implies consistency.  More in detail: since normalization preserves types, weak normalization implies that if $\bot$ is inhabited, then it is inhabited by a normal term.  But it is (usually) a trivial consequence of the definition of the logical system (such as CIC or any of the calculi of the $\lambda$-cube) that there is no normal inhabitant of $\bot$.
Damiano Mazza
CC BY-SA 3.0
2016-01-04T17:59:13.617Z
@StudentType: it is a relatively straightforward lemma (by induction over derivations) that a term of inductive type in normal form **in the empty context** has to be a constructor applied to arguments. $\bot$ is an inductive type with no constructors. Similar proofs work with alternate definitions of $\bot$.
cody
CC BY-SA 3.0
2016-01-07T07:31:44.610Z
Yes, you're right @cody!  I should have said that (in traditional systems) there is no *closed* normal inhabitant of $\bot$ (there are lots of normal inhabitants of $\bot$ which are not closed!).
Damiano Mazza
CC BY-SA 3.0
2016-01-01T13:13:03.777Z
2016-01-01T13:13:03.777Z
Damiano Mazza
<p>On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the other hand, the Church-Rosser's property of a formal (rewriting) system tells us that it is consistent, in the sense that not all equations are derivable, for example, <strong>K</strong>$\neq$<strong>I</strong>, since they don't have the same normal form.</p>

<p>Then the Calculus of Inductive Constructions (CIC) clearly statisfies both conditions. It is strong enough to represent arithmetical propositions (indeed, the $\lambda\beta\eta$-calculus alone is already able to encode the Church numerals and represent all primitive recursive functions). Moreover, CIC also has the confluence or Church-Rosser property. But:</p>

<blockquote>
  <p>shouldn't CIC be unable to prove its own consistency by the Second Incompleteness theorem?</p>
</blockquote>

<p>Or it just states that the CIC can't prove its own consistency inside the system, and somehow the confluence property is a meta-theorem? Or maybe the confluence property of CIC does not guarantee its consistency?</p>

<p>I would highly appreciate  if someone could shed some light on those issues!</p>

<p>Thanks!</p>

CC BY-SA 3.0
2015-12-31T03:39:43.670Z
In what sense does CR imply consistency? Consider the relation $x \rightarrow y$ whenever $x, y \in X$.
Martin Berger
CC BY-SA 3.0
2015-12-31T06:27:10.630Z
@MartinBerger So you are saying that CR doesn't imply consistency in the CIC? Because it does in the $\lambda$-calculus, e.g. **K** $\neq$ **I**. And sorry, I don't understand you point in considering the above relation.
StudentType
CC BY-SA 3.0
2015-12-31T12:34:08.777Z
I know nothing about CIC, but the obvious possibility would be that it doesn't prove its own Church-Rosser property.
Emil Jeřábek
CC BY-SA 3.0
2015-12-31T20:00:14.997Z
Strong normalization would be closer to consistency for a type theory no? CR implies that there are unequal terms, but that doesn't exclude an inhabitant of void. Strong normalization isn't internally provable to cic so Godels theorem still holds
daniel gratzer
CC BY-SA 3.0
2016-01-01T13:30:48.270Z
@jozefg Interesting, thanks! Btw, do you know any good textbook that addresses directly these subjects?
StudentType
CC BY-SA 3.0
2016-01-01T13:33:44.347Z
@MartinBerger So, in your notation, $x \rightarrow y$ means '$x$ reduces to $y$'? I thought it was something like the function type. I don't understand what it would be inconsistent, so if you could develop your argument a little bit it would be great! :)
StudentType
CC BY-SA 3.0
2016-01-01T13:47:38.867Z
I think looking at Girard's system F might be helpful for you to understand why consistency is not provable inside the system: the system is not strong enough to prove normalization of its terms. The complexity of normalization dominates the complexity of any function that the system can prove to be total.
Kaveh
CC BY-SA 3.0
2016-01-01T13:54:17.820Z
Also, for Godel's theorem you need arithmetic consistency, e.g. unprovability of 0=1. For any other notion of consistency you need to show that it implies the interpretation of the authentic statement 0=1 is not provable in the system.
Kaveh
CC BY-SA 3.0
2016-01-01T14:06:08.503Z
@Kaveh "The complexity of normalization dominates the complexity of any function that the system can prove to be total." Oh, that's an interesting argument! Could you give me any reference I could look for it? :)
StudentType
CC BY-SA 3.0
2016-01-01T15:26:02.713Z
The intuition is that typically it is easy to show that there is no bad normal object inside the system. Now if we can provably show that all terms have normal form we are done. The normalization algorithm is easy to formalize. The hard part is to show that it terminates. If we have functions which grow fast enough inside the system then we can use them to prove an upper bound on the termination of the normalization algorithm. I think Girard's old book should have these. Proofs and Types may also. (Any good proof theory book which discusses probable total functions of a theory should have it.)
Kaveh
<lo.logic><type-theory><lambda-calculus>
Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?
StudentType
# Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

(Asked by: username_0 on 2015-12-31)

On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the other hand, the Church-Rosser's property of a formal (rewriting) system tells us that it is consistent, in the sense that not all equations are derivable, for example, **K**$\neq$**I**, since they don't have the same normal form.

Then the Calculus of Inductive Constructions (CIC) clearly statisfies both conditions. It is strong enough to represent arithmetical propositions (indeed, the $\lambda\beta\eta$-calculus alone is already able to encode the Church numerals and represent all primitive recursive functions). Moreover, CIC also has the confluence or Church-Rosser property. But:

> shouldn't CIC be unable to prove its own consistency by the Second Incompleteness theorem?

Or it just states that the CIC can't prove its own consistency inside the system, and somehow the confluence property is a meta-theorem? Or maybe the confluence property of CIC does not guarantee its consistency?

I would highly appreciate if someone could shed some light on those issues!

Thanks!

**Tags:** lo.logic, type-theory, lambda-calculus
> **Comments:**
> **username_1**: In what sense does CR imply consistency? Consider the relation $x \rightarrow y$ whenever $x, y \in X$.  
> **username_0**: @MartinBerger So you are saying that CR doesn't imply consistency in the CIC? Because it does in the $\lambda$-calculus, e.g. **K** $\neq$ **I**. And sorry, I don't understand you point in considering the above relation.  
> **username_2**: I know nothing about CIC, but the obvious possibility would be that it doesn't prove its own Church-Rosser property.  
> **username_3**: Strong normalization would be closer to consistency for a type theory no? CR implies that there are unequal terms, but that doesn't exclude an inhabitant of void. Strong normalization isn't internally provable to cic so Godels theorem still holds  
> **username_0**: @jozefg Interesting, thanks! Btw, do you know any good textbook that addresses directly these subjects?  
> **username_0**: @MartinBerger So, in your notation, $x \rightarrow y$ means '$x$ reduces to $y$'? I thought it was something like the function type. I don't understand what it would be inconsistent, so if you could develop your argument a little bit it would be great! :)  
> **username_4**: I think looking at Girard's system F might be helpful for you to understand why consistency is not provable inside the system: the system is not strong enough to prove normalization of its terms. The complexity of normalization dominates the complexity of any function that the system can prove to be total.  
> **username_4**: Also, for Godel's theorem you need arithmetic consistency, e.g. unprovability of 0=1. For any other notion of consistency you need to show that it implies the interpretation of the authentic statement 0=1 is not provable in the system.  
> **username_0**: @Kaveh "The complexity of normalization dominates the complexity of any function that the system can prove to be total." Oh, that's an interesting argument! Could you give me any reference I could look for it? :)  
> **username_4**: The intuition is that typically it is easy to show that there is no bad normal object inside the system. Now if we can provably show that all terms have normal form we are done. The normalization algorithm is easy to formalize. The hard part is to show that it terminates. If we have functions which grow fast enough inside the system then we can use them to prove an upper bound on the termination of the normalization algorithm. I think Girard's old book should have these. Proofs and Types may also. (Any good proof theory book which discusses probable total functions of a theory should have it.)  

---

## 1 answers

### Answer by username_5 on 2016-01-01. Score: 13 | Accepted answer

First, you are confusing consistency of CIC *as an equational theory* with consistency of CIC *as a logical theory*. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent. The second means that the type $\bot$ is not inhabited. CR implies the first kind of consistency, not the second. This, as has been pointed out in the comments, is implied instead by (weak) normalization. The prototypical example of this situation is the pure $\lambda$-calculus: it is equationally consistent (CR holds) but, if you consider it as a logical system (as Alonzo Church orginally intended) it is inconsistent (indeed, it does not normalize).

Second, as Emil pointed out, even if CIC has a given property (CR or normalization) it is perfectly possible that CIC cannot itself prove that property. In this case, I do not see any inconsistency in the fact that CIC is able to prove its own CR property, and I guess that this is indeed the case (elementary combinatorial arguments usually suffice for CR, and such arguments definitely fall within the huge logical power of CIC). However, CIC certainly does not prove its own normalization property, precisely because of the second incompleteness theorem.

> **Comments:**
> **username_0**: +1 Thanks! Could you just elaborate a little bit how is that (weak) normalization property implies consistency (of a logical theory)? i.e. how is that the fact that every term has a normal form implies that $\bot$ is inhabited?  
> **username_5**: Of course!  It is essentially the fact that cut-elimination implies consistency.  More in detail: since normalization preserves types, weak normalization implies that if $\bot$ is inhabited, then it is inhabited by a normal term.  But it is (usually) a trivial consequence of the definition of the logical system (such as CIC or any of the calculi of the $\lambda$-cube) that there is no normal inhabitant of $\bot$.  
> **username_6**: @StudentType: it is a relatively straightforward lemma (by induction over derivations) that a term of inductive type in normal form **in the empty context** has to be a constructor applied to arguments. $\bot$ is an inductive type with no constructors. Similar proofs work with alternate definitions of $\bot$.  
> **username_5**: Yes, you're right @cody!  I should have said that (in traditional systems) there is no *closed* normal inhabitant of $\bot$ (there are lots of normal inhabitants of $\bot$ which are not closed!).  

---

