[FOM] Provability of Consistency

Till Mossakowski till at iks.cs.ovgu.de
Fri Mar 29 12:19:56 EDT 2019

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


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
> 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,
> 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://cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list