From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 2 May 2018 08:20:49 -0700 (PDT) From: Russell O'Connor To: Homotopy Type Theory Message-Id: In-Reply-To: <161ab0f5-32a6-4868-b9fc-901f0df147b8@googlegroups.com> References: <161ab0f5-32a6-4868-b9fc-901f0df147b8@googlegroups.com> Subject: Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_18264_142105909.1525274450160" ------=_Part_18264_142105909.1525274450160 Content-Type: multipart/alternative; boundary="----=_Part_18265_1207113230.1525274450160" ------=_Part_18265_1207113230.1525274450160 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable The claim that Coq proves PA is consistent, is formally speaking, simply a= =20 statement that a particular type (on line 18 of PAconsistent.v=20 )=20 is inhabited. You can chase the definitions used in constructing that type= =20 through folProof.v=20 =20 and so forth. How you choose to interpret the fact that this type is inhabited is up to= =20 you. However, since we are dealing with type theory here, I might suggest= =20 that there is at least one obvious interpretation, which is that this=20 inhabitant is a pair of a value of type Formula (which in this case is the= =20 Formula (notH LNT (equal LNT (var LNT 0) (var LNT 0)))) and a typed=20 function. The typed function is such that if you ever fulfill its=20 argument, it will produce a value belonging to an empty type. I believe the description of this value as a "proof of the completeness of= =20 PA" is a fair description, and if you dislike that description that you are= =20 welcome to analyze the type and its inhabitant and come up with a better=20 description of what it means. That said, proving the consistency of PA is= =20 hardly supernatural and is, in fact, a fairly pedestrian result by today's= =20 mathematical standards. As Carl Mummert notes on stack exchange=20 : There are (at least) three proofs of the consistency of PA that are=20 > important:=20 > =20 > -=20 > =20 > The proof in ZFC, which proceeeds by just verifying that N is a model= =20 > of PA.=20 > -=20 > =20 > The proof by Gentzen. Here consistency is proved in a much weaker=20 > theory than ZFC (but of course the theory is not included in PA).=20 > -=20 > =20 > The proof by G=C3=B6del using what is now called the *Dialectica*=20 > interpretation. This proof uses a completely different method than=20 > Gentzen's proof, but obtains the same result. It is also conducted in = a=20 > weak system, but a different weak system than Gentzen's proof.=20 > =20 > The consistently of PA isn't a magical result; it is a well studied=20 theorem that is equivalent to a combinatorial problem that roughly states= =20 that there is always a strategy to win at the Hydra game=20 (see Laurie Kirby and Jeff= =20 Paris. "Accessible independence results for Peano arithmetic"). (Turns out= =20 that it is the case that every strategy wins the Hydra game.) The paper "Essential Incompleteness of Arithmetic Verified by Coq" isn't=20 novel for its mathematical result. No one doubted that the consistency of= =20 PA could be deduced in Coq in principle. The only novel result of that=20 paper is that such a deduction could be carried out in practice (arguably= =20 even this isn't all that novel of a result either). I also want to point out that proving that PA is consistent doesn't by=20 itself mean that there isn't a proof that PA is inconsistent. To go from= =20 the existence of a deduction of some sentence S in some formal system T to= =20 the claim that S is actually true relies the assumption that the formal=20 system T is sound, and to go from the existence of a deduction of some=20 sentence S in some formal system T to the claim that there is no deduction= =20 of =C2=ACS in T relies the assumption that the formal system T is consisten= t. =20 In our case S is the sentence that "PA is consistent" and T is Coq. I=20 don't explicitly claim that Coq is consistent as a logic. Of course the=20 same issue holds for deductions in ZFC; however mathematicians don't=20 generally go around prefacing every mathematical paper with a note saying= =20 that "this result of our deduction is only true under the assumption that= =20 ZFC is sound", although perhaps we should. ;) I personally think there are good reasons to believe Martin-Lof style type= =20 theory (which I mean to cover systems such as CIC) is consistent. If we=20 believe that Coq is normalizing then of course we cannot provide arguments= =20 to the function defined as the second component of the value that denotes= =20 the proof of the consistency of PA. Otherwise we could execute said=20 function and normalize it to produce a constructor of the empty type, and= =20 there are no such constructors. The argument that terms in type theory are= =20 normalizing and amounts to another combinatorial problem that is going to= =20 be equivalent to finding a winning strategy against a hydra that is even=20 more difficult to slay than Kirby and Paris's hydra. You can prove Martin-Lof type theory is consistent using ZFC, and you can= =20 prove CIC is consistent using ZFC with some large cardinal assumptions. ------=_Part_18265_1207113230.1525274450160 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
The claim that Coq proves PA is consistent, is formally sp= eaking, simply a statement that a particular type (on line 18 of PAconsistent.v) is inhabited.=C2=A0 You = can chase the definitions used in constructing that type through folProof.v and so forth.

How you cho= ose to interpret the fact that this type is inhabited is up to you.=C2=A0 H= owever, since we are dealing with type theory here, I might suggest that th= ere is at least one obvious interpretation, which is that this inhabitant i= s a pair of a value of type Formula (which in this case is the Formula (not= H LNT (equal LNT (var LNT 0) (var LNT 0)))) and a typed function.=C2=A0 Th= e typed function is such that if you ever fulfill its argument, it will pro= duce a value belonging to an empty type.

I believe the description o= f this value as a "proof of the completeness of PA" is a fair des= cription, and if you dislike that description that you are welcome to analy= ze the type and its inhabitant and come up with a better description of wha= t it means.=C2=A0 That said, proving the consistency of PA is hardly supern= atural and is, in fact, a fairly pedestrian result by today's mathemati= cal standards.=C2=A0 As = Carl Mummert notes on stack exchange:

There are (at least) three proofs of the co= nsistency of PA that are important:

  • The proof in ZFC, which proc= eeeds by just verifying that N is a model = of PA.

  • The proof by Gentzen. Here consistency is proved in = a much weaker theory than ZFC (but of course the theory is not included in PA).

  • The proof by G=C3=B6del using what is now called the Dialectica= interpretation. This proof uses a completely different method than=20 Gentzen's proof, but obtains the same result. It is also conducted in a= =20 weak system, but a different weak system than Gentzen's proof.

The consistently of PA isn't a magical result; it= is a well studied theorem that is equivalent to a combinatorial problem th= at roughly states that there is always a strategy to win at the Hydra game (see Laurie K= irby and Jeff Paris. "Accessible independence results for Peano arithm= etic"). (Turns out that it is the case that every strategy wins the Hy= dra game.)


The paper "Essential Incompleteness of= Arithmetic Verified by Coq" isn't novel for its mathematical resu= lt. No one doubted that the consistency of PA could be deduced in Coq in pr= inciple.=C2=A0 The only novel result of that paper is that such a deduction= could be carried out in practice (arguably even this isn't all that no= vel of a result either).


I also want to point out that= proving that PA is consistent doesn't by itself mean that there isn= 9;t a proof that PA is inconsistent.=C2=A0 To go from the existence of a de= duction of some sentence S in some formal system T to the claim that S is a= ctually true relies the assumption that the formal system T is sound, and t= o go from the existence of a deduction of some sentence S in some=20 formal system T to the claim that there is no deduction of =C2=ACS in T rel= ies the=20 assumption that the formal system T is consistent.=C2=A0 In our case S is t= he sentence that "PA is consistent" and T is Coq.=C2=A0 I don'= ;t explicitly claim that Coq is consistent as a logic.=C2=A0 Of course the = same issue holds for deductions in ZFC; however mathematicians don't ge= nerally go around prefacing every mathematical paper with a note saying tha= t "this result of our deduction is only true under the assumption that= ZFC is sound", although perhaps we should. ;)


I pers= onally think there are good reasons to believe Martin-Lof style type theory= (which I mean to cover systems such as CIC) is consistent.=C2=A0 If we bel= ieve that Coq is normalizing then of course we cannot provide arguments to = the function defined as the second component of the value that denotes the = proof of the consistency of PA.=C2=A0 Otherwise we could execute said funct= ion and normalize it to produce a constructor of the empty type, and there = are no such constructors.=C2=A0 The argument that terms in type theory are = normalizing and amounts to another combinatorial problem that is going to b= e equivalent to finding a winning strategy against a hydra that is even mor= e difficult to slay than Kirby and Paris's hydra.


You = can prove Martin-Lof type theory is consistent using ZFC, and you can prove= CIC is consistent using ZFC with some large cardinal assumptions.

<= /div> ------=_Part_18265_1207113230.1525274450160-- ------=_Part_18264_142105909.1525274450160--