[FOM] Provability of Consistency

[Artemov, Sergei]

AF: < (*) What do we gain by establishing that PA is consistent in your sense? >

What a wonderful question! The super-idea of Hilbert’s program was to formalize mathematics and to prove its consistency within a trusted core of mathematical methods (a proper part of whole mathematics). The traditional (erroneous) reading of G2 as prohibiting a consistent theory to prove its Hilbert's consistency suggested a restrictive foundational picture of the world in which 

(**) TRUST IN CONSISTENCY CANNOT INCREASE. 

A consistent theory T cannot prove consistency of any theory S which is greater or equal to T. If you trust T, you cannot even prove your trust in T, let alone stronger theories. 

Within this picture of universe, we can only establish relative trust reductions of X to Y without any hope to actually prove either of X,Y within a trusted core. Your example “if we are convinced that PA is consistent in the usual sense, then we have reason to believe that any \Pi^0_1-statement that is provable in PA (such as Fermat's Last Theorem) is actually true” is within this vein. 

What you call “your formalization of consistency”, i.e.,  consistency schemes, which fit the original mathematical (Hilbert’s) understanding of consistency, change the foundational universe in its most principal point: (**) is no longer valid. Instead we show that, as Hilbert hoped, 

(***) TRUST IN CONSISTENCY CAN INCREASE. 

For example, a fraction of PA sufficient to check the basic combinatorics of partial truth definitions suffices to prove the consistency of the whole PA. We can do “absolute” (finitary) proofs of consistency, we can do proofs in T of consistency of a theory S extending T. The real extent of this phenomenon is not clear because a huge foundational effort was invested into consistency-as-a-formula approach, but not into consistency-as-a-scheme. However, the body of mathematical results in foundations could hopefully be applied to this new understanding of consistency right away. 

It is also true that the consistency-as-a-scheme model cannot do what the traditional consistency-as-a-formula does: build stronger and stronger theories, compare theories, analyze consistency proofs, etc. These two models supplement each other rather than actually compete. However, in the questions of Hilbert’s consistency program, the consistency-as-a-scheme model breaks the G2 impossibility barrier whereas the consistency-as-a-formula does not. 




________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Anton Freund [freund at mathematik.tu-darmstadt.de]
Sent: Tuesday, March 26, 2019 3:33 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

> In summary, Anton Freund's post is mathematically correct, but not quite
> relevant.

I still think that the results that I have mentioned are relevant, so let
me try to condense my point into a single question:

(*) What do we gain by establishing that PA is consistent in your sense?

For the usual formalization of consistency there is a clear answer (which
I sketched in my previous post): If we are convinced that PA is consistent
in the usual sense, then we have reason to believe that any
\Pi^0_1-statement that is provable in PA (such as Fermat's Last Theorem)
is actually true (even if we were not convinced that PA is sound). I would
be genuinely interested whether your formalization of consistency has
similar significance for the foundation of mathematics.

Best wishes,
Anton

_______________________________________________
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=ED0F_xMesye0wOYDuvxOjHBfH6gXuSis0O4fnSs1LeQ&s=J7P1Ia8IeFYekKPxc9GJArF6qhRo0vcLrm7ETz2vN5E&e=