18
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • $\begingroup$ @David Isn't CIC too broad? Voevodsky has a Coq fork reflecting his new theory, so I am inclined to believe Coq and Voevodsky's fork are quite different types of CIC. $\endgroup$
    – joro
    Commented Jul 1, 2011 at 8:35
  • $\begingroup$ @joro - Voevodsky's personal version of Coq is different to the trunk, for sure, but I don't know the depth at which his modification is made. That would be another facet to this line of reasoning. $\endgroup$
    – David Roberts ♦
    Commented Jul 1, 2011 at 9:14
  • $\begingroup$ In response to your motivation, note there are already constructive proofs of Con(PA), such as Gentzen's cut-elimination theorem and Gödel's Dialectica interpretation. However, these can be criticized philosophically as circular, since they rely on principles (e.g., transfinite induction up to $\epsilon_0$ for primitive recursive statements) which are equivalent to Con(PA), albeit in a non-trivial way; indeed, these proofs establish one direction of that equivalence. You can read Tait's FOM posts for a good discussion of this (e.g., cs.nyu.edu/pipermail/fom/2011-June/015556.html). $\endgroup$
    – Noam Zeilberger
    Commented Jul 1, 2011 at 9:25
  • 1
    $\begingroup$ If you need constructive justification for consistency of PA, I guess there are easier ways to do it. I’m not familiar with CIC, but it sounds like some sort of higher-order logic/type theory. Thus, it’s quite likely much stronger than the constructive Heyting arithmetic, which is well-known to be equiconsistent with PA. $\endgroup$
    – Emil Jeřábek
    Commented Jul 1, 2011 at 10:20
  • 1
    $\begingroup$ @David: This is an old result of Gödel. See en.wikipedia.org/wiki/G%C3%B6del-Gentzen_translation for definition of the translation and some references (the verification that the translation works is routine). $\endgroup$
    – Emil Jeřábek
    Commented Jul 1, 2011 at 11:06

4 Answers 4

Reset to default
20
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks, Neel! I had a quick browse of Werner's article while posing this question. But it is the latter part of your answer which is really useful. I was uncertain as to whether restricting one's allowed fragment of logic (to constructive or otherwise) had any bearing on consistency strength. Naively it might have done, but I'm becoming convinced that we are dealing with two separate foundational 'axes' here. $\endgroup$
    – David Roberts ♦
    Commented Jul 2, 2011 at 0:46
11
$\begingroup$

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?

Improve this answer
$\endgroup$
11
  • 3
    $\begingroup$ Oh? I had naively thought that IZF surely proved consistency of Heyting Arithmetic by exhibiting a model (same as ZF proves consistency of PA), and that double-negation translation interpreted Peano Arithmetic into Heyting Arithmetic in such a way that the consistency of PA followed quite simply from the consistency of HA. Where did my naive assumptions falter? $\endgroup$
    – Sridhar Ramesh
    Commented Jul 1, 2011 at 21:43
  • 5
    $\begingroup$ Con(HA) implies Con(PA) intuitionistically (even in ridiculously weak arithmetic like iPV). That IZF cannot prove the existence of a model of arithmetic is quite possible, because (IIRC) it would imply the existence of a completion of arithmetic, contradicting a derivation rule corresponding to the Church thesis (which is admissible in IZF). However, I would be quite surprised if IZF does not prove the consistency of HA (or PA), as it is a $\Pi^0_1$ statement. I’m not sure whether the usual Friedman translation showing $\Pi^0_2$-conservativity of classical over intuitionistic theories ... $\endgroup$
    – Emil Jeřábek
    Commented Jul 2, 2011 at 12:45
  • 3
    $\begingroup$ I’m stupid: Friedman actually gives $\Pi^0_2$-conservativity of ZF over IZF (formulated in the disguise of provably total computable functions) as an application in the very paper where he introduced the Friedman translation: dx.doi.org/10.1007%2FBFb0103100 . So, yes, IZF proves the consistency of PA. $\endgroup$
    – Emil Jeřábek
    Commented Jul 2, 2011 at 17:49
  • 2
    $\begingroup$ For what it's worth, I have proved the consistency of PA in Coq. I am able to do this because I interpret the logical symbols under a double negation translation. After all, constructive logic is a richer language that classical logic. $\endgroup$
    – Russell O'Connor
    Commented Jul 4, 2011 at 15:01
  • 3
    $\begingroup$ Just as a short late addendum: The general completeness theorem, stating that consistency is equivalent to having a model (in $\mathrm{Set}$), is indeed not constructively provable. A simple way to see that is that in the effective topos, there is no model of PA, though PA is still consistent (being equiconsistent to HA, which does have a model, namely the naturals (and somewhat amazingly, has the naturals as its only model [van den Berg--van Oosten])). However, for the fragment of predicate logic without $\exists$ and $\vee$, the completeness theorem [Herberlin--Ilik] is constructive. $\endgroup$
    – Ingo Blechschmidt
    Commented Feb 17, 2019 at 21:45
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Several of your statements are false: Coq still contains impredicative Prop by default, and every (countable) theory has a "proof theoretic ordinal": just take the smallest countable ordinal which cannot be proven to be well-ordered in the theory. For ZF though, no concise self-contained description of this ordinal is known. In addition I'm highly doubtful about CZF+EM = ZF. $\endgroup$
    – cody
    Commented Dec 10, 2015 at 23:18
  • 2
    $\begingroup$ @cody: CZF + EM = IZF + EM = ZF is a standard fact, see for instance Corollary 4.2.8 in Rathjen and Aczel's book draft. $\endgroup$
    – Ingo Blechschmidt
    Commented Feb 17, 2019 at 21:50
  • $\begingroup$ @IngoBlechschmidt Thanks, that's very enlightening! I had no idea the weakness of CZF was tied to intuitionistic logic. $\endgroup$
    – cody
    Commented Feb 18, 2019 at 2:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .