[FOM] Provability of Consistency

[Artemov, Sergei]

Dear Anton, thank you for this clever and civilized discussion. 

> Would you say that the domain condition is missing in the Peano axioms as well? 

No, 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. We don’t have to sacrifice the pleasures of the first-oder language in PA. The same holds for all provable in PA formulas. 

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

Of course, I agree: "the formula Con(PA) is not provable in PA" is both meaningful and true. It just different from “unprovability of Hilbert’s consistency.”

The mainstream logic has two wings, syntax and semantics, we use both to fly. Models provide an insightful analysis of G2 and expose a logical error in interpreting G2 as “unprovability of Hilbert’s consistency”. Such analysis could probably not be given by syntactic methods only, since the claim itself is about connection between syntactic ams semantic realms. However, I would love to see another analysis of G2 vs. H-consistency, more syntactic, if you wish. 

Very 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: Friday, March 29, 2019 12:21 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

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

_______________________________________________
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=BgCfoCBAg6qzL01zkI2h1XYN9zUO0PSV5vt-8IrL89k&s=DwbkNCjWEv5kICG9Z18GRf2CJ3Oy1Z7GfEm3eawTZHA&e=