The Coq mailing list

[ikdc <ikdc AT mit.edu>]

On 05/02/2018 07:35 PM, Jose Manuel Rodriguez Caballero wrote:
> Russell said:
>
> "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”
>
> Ok, we are not talking the same language. In my world: PA is consistent means that 
> there isn't a proof that PA is inconsistent (a proof that 1=0 formalized inside 
> PA). I’m following Hilbert’s metamathematical standards: 
> https://plato.stanford.edu/entries/hilbert-program/ 
> <https://plato.stanford.edu/entries/hilbert-program/>


I think the point was that "proving X doesn't mean X is true" if you 
don't believe that the metalogic you did the proof in is consistent. 
You are not going to find a proof of the consistency of PA that you 
like, because all such proofs must be done in a stronger system than PA. 
 In other words, all of them are what you call "begging the question". 
The only way you will find one which isn't "begging the question" is if 
PA is inconsistent.  This is (informally) Gödel's second incompleteness 
theorem.


Y: This is begging the question.

G: You cannot escape begging this question.


Nonetheless, a proof of PA's consistency is useful: not necessarily 
because it increases our confidence that PA is consistent---but rather 
because it's interesting in itself to study which proof systems are 
stronger or weaker than others.

(Please correct me if I said something wrong.)