8
$\begingroup$

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!

Improve this question
$\endgroup$
10
  • 3
    $\begingroup$ In what sense does CR imply consistency? Consider the relation $x \rightarrow y$ whenever $x, y \in X$. $\endgroup$
    – Martin Berger
    Commented Dec 31, 2015 at 3:39
  • $\begingroup$ @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. $\endgroup$
    – StudentType
    Commented Dec 31, 2015 at 6:27
  • 5
    $\begingroup$ I know nothing about CIC, but the obvious possibility would be that it doesn't prove its own Church-Rosser property. $\endgroup$
    – Emil Jeřábek
    Commented Dec 31, 2015 at 12:34
  • 2
    $\begingroup$ 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 $\endgroup$
    – daniel gratzer
    Commented Dec 31, 2015 at 20:00
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Kaveh
    Commented Jan 1, 2016 at 15:26

1 Answer 1

Reset to default
13
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ +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? $\endgroup$
    – StudentType
    Commented Jan 1, 2016 at 13:28
  • $\begingroup$ 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$. $\endgroup$
    – Damiano Mazza
    Commented Jan 1, 2016 at 19:03
  • $\begingroup$ @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$. $\endgroup$
    – cody
    Commented Jan 4, 2016 at 17:59
  • $\begingroup$ 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!). $\endgroup$
    – Damiano Mazza
    Commented Jan 7, 2016 at 7:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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