The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

Hi Russell,

While your statement (a "proof" always refers to a proof within a certain 
formal system) is correct looked at in an isolated way,
I find it problematic as it overlooks that the formal systems (deduction 
systems) in discussion here are designed to represent mathematics.

Of course, this is the standard use of the terminology ("Now we prove the 
theorem MUIIU." - p. 179),
even in toy systems such as the MIU system, cf. pp. 177 ff. at
        http://us.metamath.org/downloads/metamath.pdf

But all the systems in discussion here (e.g., ZFC) implicitly or explicitly 
claim to represent (significant parts of) mathematics,
making it difficult to follow a pure relativism (denying provability "in any 
absolute sense").
For example, if one of the systems mentioned previously would be shown to be 
inconsistent (or otherwise not sound), it would be discarded.

Moreover, I would even argue that some of these formal systems are better 
than others in representing mathematics,
e.g., type theory is superior to (axiomatic) set theory, and the ideal system 
should follow the concept of expressiveness of Q0
by Peter B. Andrews, who regularly emphasizes that mathematics should be 
expressed "naturally".

Hence, there should be an ideal formal system for representing mathematics, 
and proofs in it would be proofs in an "absolute sense".

I still owe Randy an answer in the HOL mailing list, which I hope to finish 
soon.

Best regards,

Ken

____________________________________________________


Ken Kubota
http://doi.org/10.4444/100



> Am 03.05.2018 um 02:57 schrieb 
> roconnor AT theorem.ca:
> 
> On Thu, 3 May 2018, 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/

> Firstly, your statement is incomplete.  There isn't a proof according to 
> what system?  Please, if you are going to dive into logic like this, don't 
> use the term "proof" unaddorned like this.  Mathematical statements are not 
> provable in any absolute sense.  Mathematical statements are only provable 
> or not within some deduction system.  Coq can prove something, or ZFC can 
> prove something or PA can prove something, and these different systems form 
> completely different classes of statements of what they can or cannot prove.

> Let me reiterate again that "Essential Incompleteness of Arithmetic 
> Verified by Coq" is only claiming that "PA is consistent" is provable in 
> Coq (and this is just a side remark within that paper).  This is a claim 
> that you can directly verify yourself by downloading the development and 
> checking it in Coq and seeing for yourself that Coq indeed considers the 
> deduction valid.  The paper does not directly claim that "PA is consistent" 
> is true; that would only follow if you assume that Coq is sound, and the 
> paper doesn't discuss the soundness of Coq.