[FOM] Provability of Consistency

[Anton Freund]

Sergei Artemov wrote:

> a) S is a WRONG formulation of the three cubes problem, since the domain
> condition for x,y,z is missing.

I would like to ask a quick follow-up question: Would you say that the
domain condition is missing in the Peano axioms as well? In other words,
would you say that

\forall x. S(x)\neq 0

should not be counted as a Peano axiom, because Peano was interested in
standard numbers rather than non-standard ones? If we would treat this
parallel to consistency, it seems that we would have to replace the given
axiom by the instances

S(n)\neq 0

for all numbers n. The induction axiom could not be formulated at all,
because it contains quantifiers, which will necessarily range over
non-standard numbers in some models. It seems that Peano arithmetic would
then become a propositional (rather than first order) theory that can only
reason about (in-)equalities between closed terms. I do not mean to
suggest that the previous is your position. I have merely tried to devise
an extreme case that might help me to understand it better.

I also wanted to remark that models are not the only way to give a meaning
to symbols. Symbols can also assume meaning because of the way in which
they are used in conjunction with other symbols. For example, the meaning
of the universal quantifier is determined by the rules which allow us to
introduce it (infer \forall x.\phi(x) from \phi(x), with the usual
variable condition) and to eliminate it (infer \phi(t) from \forall
x.\phi(x)). Similarly, the language of arithmetic assumes meaning when we
decide to use it in order to build proofs from the axioms of Peano
arithmetic. For this reason I would say that the statement

"the formula Con(PA) is not provable in PA"

has meaning and is not a mere play with symbols, even if we do not speak
about models at all. I would be very interested whether you agree. Note
that I am not disputing that models play an important role in logic.

Best,
Anton