[FOM] Provability of Consistency

[Artemov, Sergei]

> By Artemov's principle, it follows that Goldbach's conjecture is 
> finitarily provable.

A good joke, thank you. Actually, it does not. “Artemov’s principle” has not been formulated yet publicly in a general form covering the Goldbach case. In PoC, we consider a specific finitary proof of a specific scheme ConS(PA). For that example, in Section 4.3, PoC explains that the standard “soundness-in-the-standard-model” argument does not count as a finitary proof of consistency, but the partial truth definitions construction from PoC does. Please expect this kind of distinction for the Goldbach scheme as well.  

Since this is, supposedly, my last posting on this thread, I list PoC findings and suggestions in a nutshell, for reader’s convenience.  

1. Boxing Hilbert’s consistency into a single formula like Con(PA) does not appear to be defensible. Even the most basic notions of finitary reasoning, like “induction,” or “axioms of PA” cannot be finitarily certified in this format. We need to consider schemes of formulas as well.

2. We consider a scheme ConS(T) with parameter S ranging over finite sequences of formulas, “S is not a T-proof of a contradiction,” as a legitimate representation of mathematical consistency of T, along with the traditional consistency formula Con(T). We argue that for a general mathematician, these formalizations of consistency are basically equivalent.

3. ConS(PA) is finitarily provable and this revives Hilbert’s consistency program. Goedel’s Second Incompleteness Theorem offers a useful analysis of provability of consistency by ruling out special “uniform” kind of consistency proofs of PA in PA, but not all finitary consistency proofs.   

4. Each of these two formalizations of consistency, Con(T) and ConS(T), has its own area of applications. Right now it looks like we can use ConS(T) for analysis of Hilbert’s consistency program, and Con(T) for virtually “all other” proof-theoretical tasks.  

I am taking this opportunity to sincerely thank all the contributors and readers of this FOM thread for their interest and stimulating discussions. This is very helpful in further editing the PoC text. 

________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Timothy Y. Chow [tchow at math.princeton.edu]
Sent: Tuesday, April 2, 2019 2:53 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

This is my final contribution to the Artemov thread.

Sergei Artemov wrote:
> A scheme is finitarily provable if each instance of S is.

It would appear to follow from the above principle that if anyone ever
proves Goldbach's conjecture by any means, then Goldbach's conjecture will
be finitarily provable.

We can write down a scheme

   "exists prime p1 : exists prime p2 : p1 + p2 = E"

where in each instance of the scheme we insert a different even number E.

Under the assumption that Goldbach has been proved, every instance of the
scheme is certainly finitarily provable.

By Artemov's principle, it follows that Goldbach's conjecture is
finitarily provable.

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwICAg&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=L9q8j7JsbTMfpmlvjVKrJ6tKt95wRaXKRoLggfQbRG8&s=dulEfJR2ZxMK01nT9hhjH3oejDB3jfZ_ipEfAl2E3nY&e=