[FOM] Provability of Consistency

Sat Mar 30 01:00:37 EDT 2019

a typo: "each instance of ConS(PA) is finite"
________________________________________
From: Artemov, Sergei
Sent: Saturday, March 30, 2019 12:54 AM
To: Foundations of Mathematics
Subject: RE: [FOM] Provability of Consistency

> The
> comparison with the PA induction scheme is not valid because the latter
> is finitary: in a finite proof, only finitely many instances of PA
> induction can be used, and each instance itself is finite and its
> correct application can be finitely checked. By contrast, your
> consistency-as-a-scheme requires an infinitary proof.

Dear Till,
Respectfully, the claim “consistency-as-a-scheme requires an infinitary proof” is not correct. Please double check your reasoning. In fact, exactly the same claims as for Ind hold for consistency-as-a-scheme ConS(PA): each instance of Con(PA) is finite and its finite proof can be finitely found and checked. Since the provability of a scheme is provability of each of its instance, ConS(PA) is provable in PA. Som the conclusion
USING FINITARY METHODS, TRUST IN CONSISTENCY CANNOT INCREASE
is not warranted and contradicts the fact that ConS(PA) is provable in PA.

This fact, “ConS(PA) is provable in PA,” does not require a secondary formalization as single formula, so no second order logic is needed.

I appreciate the fact that you agree with “Induction is finitary.”

Best,
Sergei
________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Till Mossakowski [till at iks.cs.ovgu.de]
Sent: Friday, March 29, 2019 12:19 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

The problem is that your consistency-as-a-scheme is not finitary (in the
sense of "arithmetizable" or "implementable on a comupter"). The
comparison with the PA induction scheme is not valid because the latter
is finitary: in a finite proof, only finitely many instances of PA
induction can be used, and each instance itself is finite and its
correct application can be finitely checked. By contrast, your
consistency-as-a-scheme requires an infinitary proof. The better
analogue is with course-of-value induction as a theorem. One can prove
that ordinary induction entails course-of-value induction, but not in PA
in a finitary way (only as a scheme).

If you want your argument to be formalised in a finitary way (and in
particular, if you want to formalise all your model-theoretic
arguments), you need a stronger system. For your consistency-as-a-scheme
proof, probably some form of second-order arithmetic would do (there,
you could also prove that ordinary induction entails course-of-value
induction in a finitary way). You end up in proving the consistency of
PA in a stronger system, and by G2, that stronger system cannot prove
its own consistency. Hence, we end with

USING FINITARY METHODS, TRUST IN CONSISTENCY CANNOT INCREASE

Till Mossakowski

Am 28.03.19 um 03:04 schrieb 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=
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=yHnXaKLkKpOq8OCDsV2jGDfAERQlp5bWKoFOx_SsiUg&s=WMYz16PQmrP0XCNJM4pcxdBluuG3Bbp2ewm0x-U6lBs&e=
>

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwIF-g&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=yHnXaKLkKpOq8OCDsV2jGDfAERQlp5bWKoFOx_SsiUg&s=WMYz16PQmrP0XCNJM4pcxdBluuG3Bbp2ewm0x-U6lBs&e=