[FOM] Provability of Consistency

[Anton Freund]

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