Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[Russell O'Connor <roco...@r6.ca>]

[-- Attachment #1.1: Type: text/plain, Size: 4771 bytes --]

The claim that Coq proves PA is consistent, is formally speaking, simply a 
statement that a particular type (on line 18 of PAconsistent.v 
<https://github.com/coq-contribs/goedel/blob/c3f922cd5cf2345e1be55ba2ec976afcdc6f4b13/PAconsistent.v#L18>) 
is inhabited.  You can chase the definitions used in constructing that type 
through folProof.v 
<https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/folProof.v#L109> 
and so forth.

How you choose to interpret the fact that this type is inhabited is up to 
you.  However, since we are dealing with type theory here, I might suggest 
that there is at least one obvious interpretation, which is that this 
inhabitant is a pair of a value of type Formula (which in this case is the 
Formula (notH LNT (equal LNT (var LNT 0) (var LNT 0)))) and a typed 
function.  The typed function is such that if you ever fulfill its 
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 
PA" is a fair description, and if you dislike that description that you are 
welcome to analyze the type and its inhabitant and come up with a better 
description of what it means.  That said, proving the consistency of PA is 
hardly supernatural and is, in fact, a fairly pedestrian result by today's 
mathematical standards.  As Carl Mummert notes on stack exchange 
<https://math.stackexchange.com/a/56117>:

There are (at least) three proofs of the consistency of PA that are 
> important: 
>    
>    - 
>    
>    The proof in ZFC, which proceeeds 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ödel using what is now called the *Dialectica* 
>    interpretation. This proof uses a completely different method than 
>    Gentzen's proof, but obtains the same result. It is also conducted in a 
>    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 that roughly states 
that there is always a strategy to win at the Hydra game 
<https://www.youtube.com/watch?v=uWwUpEY4c8o> (see Laurie Kirby and Jeff 
Paris. "Accessible independence results for Peano arithmetic"). (Turns out 
that it is the case that every strategy wins the Hydra game.)


The paper "Essential Incompleteness of Arithmetic Verified by Coq" isn't 
novel for its mathematical result. No one doubted that the consistency of 
PA could be deduced in Coq in principle.  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 novel of a result either).


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


I personally think there are good reasons to believe Martin-Lof style type 
theory (which I mean to cover systems such as CIC) is consistent.  If we 
believe 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.  Otherwise we could execute said 
function and normalize it to produce a constructor of the empty type, and 
there are no such constructors.  The argument that terms in type theory are 
normalizing and amounts to another combinatorial problem that is going to 
be equivalent to finding a winning strategy against a hydra that is even 
more 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.

[-- Attachment #1.2: Type: text/html, Size: 6127 bytes --]