[FOM] Provability of Consistency

[Artemov, Sergei]

Dear Anton, 

The mathematical world, from the foundationalist’s point of view, is full of circularities. How can we speak of a theory of natural numbers without having some grasp of the concept of a natural number? How can we develop a concept of a natural number as an element of the standard model without having a good list of principles, a theory, of natural numbers?  This is a noble subject, deep and interesting, which usually produces an infinite regress of notions yielding a famous mathematicians’ joke “if you assume nothing, you prove nothing.” 

Mathematicians deal with this problem in a consciously practical way: they assume certain mathematical universe of structures and facts, and study them thus leaving studying infinite regressing chains of notions to special interested scholars. 

My position here is close to this mathematical tradition: assume the world of logic as described in the mainstream university course of mathematical logic: symbols-terms-formulas-theories, evaluations-truth-models-mathematical structures as models of theories, natural numbers as individual objects and as a set, computability, derivability, completeness theorem, etc. If you want to discuss or question these foundations, you need a separate arrangement, probably with different people, not because I am not interested, I actually am, but rather because I don’t really have time for such kind of discussions, sorry. So, I will gladly comment on the basis of a mainstream course of mathematical logic, if you don’t mind. 

> (1) The formula \forall x. S(x)\neq 0 is an appropriate formalization of
> ”no number is both a successor and equal to zero", even though we are only
> interested in standard numbers and the quantifier is not restricted to
> these.

The formula \forall x.S(x)\neq 0 is an appropriate formalization of ”no number is both a successor and equal to zero" in any structure with the successor function and 0. In particular, on the standard natural numbers with S and 0. 

The analogue of the Con(PA) sin for the successor would be the following: 

i) formalize the property “no NATURAL number is both a successor and equal to zero" as \forall x.S(x)\neq 0; 
ii) evaluate this formalization without domain condition on the set Z of all integers positive and negative; 
iii) notice that \forall x.S(x)\neq 0 fails on Z;
iv) announce that the theory of integers cannot prove that “no NATURAL number is both a successor and equal to zero.”

This reasoning is obviously a crime against humanity since the theory of integers can easily prove a proper formalization of “no NATURAL number is both a successor and equal to zero" which incorporates the domain condition:  \forall x.[x\geq 0 -> S(x)\neq 0]. 
BTW, thank you for this example, I hope it is as convincing for you as it is for me.  

> (2) The formula Con(PA) is no appropriate formalization of "no number
> codes a proof of 0=1", because we are only interested in standard numbers
> and the quantifier is not restricted to these.

The formula Con(PA) is an appropriate formalization of "no number codes a proof of 0=1" in any model of PA, provided the “appropriateness” for us is compliance with properties of consistency provable in PA. However, the formula Con(PA) is no appropriate formalization of "no STANDARD number codes a proof of 0=1” in the same way as \forall x.S(x)\neq 0 is no appropriate formalization of ”no NATURAL number is both a successor and equal to zero,” cf. the previous example.

> you claim that consistency-as-a-scheme captures Hilbert's original intention.

Not exactly, I am not having here any specific historic stand. “Hilbert’s consistency” refers to the exact formulation of consistency taken from the SEP article “Hilbert’s Program”, see the reference on page 1 of the PoC paper. I have no reasons to doubt this article in historical questions. With this exact reference, "Hilbert’s consistency" is just a name tag of the specific definition in the PoC paper. Strictly speaking, it has the same connection to Hilbert as "George Washington Bridge" to George Washington as a person. Well, a more tight connection actually, stated in the reference to the SEP article. 

However, since you feel a terminological pressure coming from this usage, absolutely not intended, I will take a second look at PoC terminology. 

Thank you as always for a meaningful discussion.

Best,
Sergei
________________________________________
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: Sunday, March 31, 2019 6:09 AM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

Dear Sergei,

Thank you very much for your explanation! I am sorry to insist, but it
appears to me that your justification of the Peano axioms is somewhat
circular. You write:

> domain condition in axioms is redundant since axioms are ex officio true
in all models of PA and hence are always equivalent to their relativized
forms.

However, the formula

\forall x. S(x)\neq 0

is only true in all models of PA *if* we have already accepted it as an
axiom of Peano arithmetic. I do not yet understand how this resolves the
apparent incoherence between the two following positions:

(1) The formula \forall x. S(x)\neq 0 is an appropriate formalization of
"no number is both a successor and equal to zero", even though we are only
interested in standard numbers and the quantifier is not restricted to
these.

(2) The formula Con(PA) is no appropriate formalization of "no number
codes a proof of 0=1", because we are only interested in standard numbers
and the quantifier is not restricted to these.

Maybe your position is that the formula \forall x. S(x)\neq 0 is no
appropriate formalization of "no number is both a successor and equal to
zero", but should be accepted as a Peano axiom nevertheless. I do not see
why: Why should we accept a statement about non-standard numbers, when we
are only interested in standard ones?

I would also like to comment on your use of the expression "Hilbert’s
consistency": As far as I understand, you claim that
consistency-as-a-scheme captures Hilbert's original intention. I
understand your argument about non-standard models (even though I do not
agree with its conclusion), but I do not see enough support for the claim
that this captures Hilbert's own position. In my opinion this claim could
only be justified by a close analysis of Hilbert's writing (not single
quotations, but a comprehensive study of his position at different stages
of his career, his own reaction to Gödel's theorem, the reception of
Hilbert's program by his contemporaries...). As long as such a study has
not been conducted, I personally find the expression "Hilbert's
consistency" problematic, because it suggests a historic fact that has -
in my view - not been established.

Very best,
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=DwIFAw&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=MaTj2WGvnlJM5JtMRNKzTEefVru0fr7yf59NfP-8e30&s=RNW57WoMhLXY5kmy0491ftEcOPZtZPRpAOFit2Mox8I&e=