[FOM] Provability of Consistency

Sun Mar 31 20:31:19 EDT 2019

Dear Sergei (and Till),

First, a general comment: I believe there is great value in looking for ways to salvage Hilbert's program which was perhaps undeservedly put to sleep because of Goedel's results, and I am following this discussion with interest.

Second, some nitpicking: I agree with Till on his point concerning consistency-as-a-scheme. If one wants to be fully formal in such a way that the made argument can be represented on, and checked by a computer, there is a fundamental difference between the following two statements:
(1) "forall x y, x + y = y + x" is provable in PA.
and
(2) ConS(PA) is provable in PA.
(The following discussion applies in general to single sentences versus schemas; instead of "forall x y, x + y = y + x", at (1) I could have used Con(PA) as an example, but I preferred to pick something that is actually provable in PA.)

For (1), we do not need a "secondary formalization"; it is enough to exhibit a formal proof in PA. For (2), we need to prove that, for all parameters k, the instance ConS(PA)_k is provable in PA. So (1) can be construed as a statement *in PA*, whereas (2) must be construed as a statement *about PA*. And indeed, (2) eventually amounts to a proof by induction on k, which can only be expressed in a "secondary formalization". In my opinion, an interesting question for your foundational pursuit here is: What is the weakest logic required for a proof of (2)?  (As far as I understand, the answer to this would also apply to any theory extending PA.)

Where I disagree with Till is in that I don't see the need of second-order arithmetic for proving (2). Isn't (first-order) PA sufficient? The informal finitistic proof of (2) given in the paper suggests that it can be turned into: PA |- forall x, "PA |- ConS(PA)_x".

A related note on schemas, in the context of the comparison between ConS(PA) and the PA induction schema: I believe we should distinguish between (A) employing a logical system that involves axiom-schemas (which most interesting logical systems do) and (B) proving that a schema is admissible in that system. (A) only requires some mechanical manipulation of symbols (provided the schemas are recursive). By contrast, (B) requires reasoning about the system (a.k.a. meta-reasoning), so its fully rigorous/convincing justification needs an underlying (meta-)logic.

Best wishes,

Andrei

________________________________________
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 ConS(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<https://cs.nyu.edu/mailman/listinfo/fom> [fom-bounces at cs.nyu.edu<https://cs.nyu.edu/mailman/listinfo/fom>] on behalf of Till Mossakowski [till at iks.cs.ovgu.de<https://cs.nyu.edu/mailman/listinfo/fom>]
Sent: Friday, March 29, 2019 12:19 PM
To: fom at cs.nyu.edu<https://cs.nyu.edu/mailman/listinfo/fom>
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<https://cs.nyu.edu/mailman/listinfo/fom> [fom-bounces at cs.nyu.edu<https://cs.nyu.edu/mailman/listinfo/fom>] on behalf of

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

> Anton Freund [freund at mathematik.tu-darmstadt.de<https://cs.nyu.edu/mailman/listinfo/fom>]
> Sent: Tuesday, March 26, 2019 3:33 PM
> To: fom at cs.nyu.edu<https://cs.nyu.edu/mailman/listinfo/fom>

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

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

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

> 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>

FOM
 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM
 is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

> 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 -- Foundations of Mathematics - New York University<https://cs.nyu.edu/mailman/listinfo/fom>
cs.nyu.edu
FOM is an automated e-mail list for discussing foundations of mathematics. It is a closed, moderated list. This means that all subscriptions and postings must be approved by the moderator,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190401/f754182e/attachment-0001.html>