Proof strength of Calculus of (Inductive) Constructions - MathOverflow

Proof strength of Calculus of (Inductive) Constructions

2011-07-01T05:08:41Z

This is a follow-on from this question, where I pondered the consistency strength of Coq. This was too broad a question, so here is one more focussed. Rather, two more focussed questions:

I've read that CIC (the Calculus of Inductive Constructions) is interpretable in set theory (IZFU - intuitionistic ZF with universes I believe). Is there a tighter result?

And

What is the general consensus of the relative consistency of constructive logics anyway?

I am familiar, in a rough-and-ready way, with the concept of consistency strength in set theory, but more so of the 'logical strength' one has in category theory, where one considers models of theories in various categories. Famously, intuitionistic logic turns up as the internal logic of a topos, but perhaps this is an entirely different dimension of logical strength.

I guess one reason for bringing this up is the recent discussion on the fom mailing list about consistency of PA - Harvey Friedman tells us that $Con(PA)$ is equivalent to 15 (or so) completely innocuous combinatorial statements (none of which were detailed - if someone could point me to them, I'd be grateful), together with a version of Bolzano-Weierstrass for $\mathbb{Q}_{[0,1]} = \mathbb{Q} \cap [0,1]$ every sequence in $\mathbb{Q}_{[0,1]}$ has a Cauchy subsequence with a specified sequence of 'epsilons', namely $1/n$). A constructive proof of this result would be IMHO very strong evidence for the consistency of PA, if people are worried about that.

Answer by Neel Krishnaswami for Proof strength of Calculus of (Inductive) Constructions

2011-07-01T10:56:31Z

IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles -- see Benjamin Werner's "Sets in Types, Types in Sets". (This is because of the presence of a universe hierarchy in the CIC.)

As I understand it, the homotopy type theory project does not need (or want?) the full consistency strength of Coq; they make use of it simply because it is one of the better implementations of type theory. Instead, what makes this work interesting is not its consistency strength, but its focus on a wholly new dimension of logical complexity: the complexity of equality (which, utterly amazingly, they relate to homotopy type). It puts me in mind of a famous quotation of Rota:

“What can you prove with exterior algebra that you cannot prove without it?” Whenever you hear this question raised about some new piece of mathematics, be assured that you are likely to be in the presence of something important. In my time, I have heard it repeated for random variables, Laurent Schwartz’ theory of distributions, ideles and Grothendieck’s schemes, to mention only a few. A proper retort might be: “You are right. There is nothing in yesterday’s mathematics that could not also be proved without it. Exterior algebra is not meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds is as worthwhile a mathematical enterprise as proving old conjectures.” (Indiscrete Thoughts, 48)

(This is not meant as criticism of your question, but just as a caution not to let old battles cause us to lose sight of the new innovations brought to us.)

That said, as a sometime constructivist, I do not find consistency to be a primary philosophical notion. If PA is consistent, so is PA+$\lnot$Con(PA). That is, systems can lie despite being consistent, and so I hesitate to build my foundations on consistency. Instead, I prefer a proof-theoretic justification for logical systems, such as Gentzen's proof of cut-elimination. This guarantees that a system is not merely consistent, but that theorems actually have proper proofs. For a good introduction to these ideas, you can hardly do better than Per Martin-Lof's Siena lectures, "On the Meaning of the Logical Constants and the Justification of the Logical Laws".

I should be clear that these are more stringent conditions than consistency, and hence offer no way at all of avoiding the obstacles that the halting/incompleteness theorems pose. Heyting and Peano arithmetic are equi-consistent: there is no reason to trust constructivism more, if consistency strength is all that you are interested in. It is other logical qualities that make constructivism attractive.

Answer by Andrej Bauer for Proof strength of Calculus of (Inductive) Constructions

2011-07-01T21:27:12Z

I would just like to point out that there is no constructive proof of

"Every sequence or rationals in $[0,1]$ has a $1/n$-convergent subsequence."

because in the effective topos this is false. Consider a Specker sequence which has no accumulation point in a strong sense, so it cannot have a convergent subsequence.

Moreover, I heard it claimed that IZF (intuotionistic Zermelo-Fraenkel) does not prove consistency of PA. Can someone confirm this?

Answer by Daniel Mehkeri for Proof strength of Calculus of (Inductive) Constructions

2011-07-10T23:15:57Z

As Neel Krishnaswami says, Heyting arithmetic and Peano arithmetic are equiconsistent. However this does not necessarily hold at the level of set theory or type theory. So, while consistency strength cannot motivate constructive arithemtic, it can indeed motivaite constructive set theory or type theory.

As for type theory, the flavour of CIC you are referring to contains some impredicative features, not often used in practice. My understanding is that as of version 8, unless explictly told otherwise, Coq by default uses the predicative calculus of inductive constructions (pCIC). This should have vastly lower proof theoretic strength.

As for set theory, CZF is consistent, provably so by transfinite recursion up to the Bachmann Howard ordinal, while IZF is equiconsistent with ZF, whose proof-theoretic ordinal is unknown, perhaps non-existent. Adding classical logic to either CZF or IZF recovers ZF.

Answer by Gro-Tsen for Proof strength of Calculus of (Inductive) Constructions

2012-12-08T17:07:12Z

I just stumbled upon this old question by chance, and I thought maybe you should have a look at Alexandre Miquel's thesis if you haven't already done so (and if you can read French). Conjecture 9.7.12 on page 329 (331 of PDF) suggests that the Calculus of Constructions with universes should be equiconsistent with Zermelo set theory with universes (assuming I'm not misreading—I'm easily confused between all these theories), which at least gives some lower bound.