On Fri, 29 Mar 2019, Artemov, Sergei wrote:
> < Do you consider S to be a satisfactory formalization of the statement,
> "the sum of three cubes is never equal to 42"? >
>
> Of course NOT, since in its syntactic form, S allows x,y,z to be
> positive integers, rationals, reals, etc. And this is not a forgotten
> default, but a principal game-changing feature. A better formulation
> would be S* which is S with additional condition "x,y,z are integers"
> (there is also a default that x,y,z are standard integers).
>
> At this very point you are losing your syntactic paradise. Insisting
> that S "as is" is the proper syntactic formulation of the three cubes
> problem would be unprofessional since without specifying the domain of
> x,y,z, S is a plain wrong formulation.
I'm not sure if you recognize how radically you are diverging from the
standard understanding of how mathematical logic works. At the risk of
saying some things that are so basic that they might seem to insult the
intelligence, let me try to articulate some of the differences.
In the standard development of PA, one starts by defining symbols and
strings and syntactic rules for well-formed formulas. These don't have
any meaning. The word "meaning" isn't even standardly used in the
textbooks; instead one talks about interpretations in a model, but even
that is generally deferred until much later since it is not a logically
necessary part of setting up PA.
Well-formed formulas in the first-order language of arithmetic have
nothing that could possibly be construed, even by accident, as a symbol
(or symbols) indicating "are integers" or "are natural numbers." Of
course, in informal mathematical discourse, mathematicians routinely write
things such as "forall x in Z" where Z is supposed to denote the integers.
But as I said, "Z" is not one of the symbols in the first-order language
of arithmetic. Therefore, if I am following the standard development of
PA, I simply *cannot comply* with your demand for a "better formulation"
of S since my alphabet does not contain any symbols that I could put in S
to indicate "x,y,z are integers."
I'll come back to this in a moment, but let's continue with the
development of PA. One develops purely syntactic rules for manipulating
formulas, and also specifies axioms (and/or axiom schemata). Whether S
(or some other well-formed formula) is a theorem of PA is then simply a
syntactic question of whether one can arrive at S starting with the axioms
and applying the syntactic rules.
So far, we're still in what we call a "syntactic paradise." There is no
mention of integers. A mathematician with guilty knowledge might look at
the strings and the syntactic rules and notice a haunting resemblance to
finitistic mathematical proofs of arithmetical statements, but at this
stage---to borrow a phrase one sometimes sees at the beginning of a
fictional work---any resemblance to real mathematics is purely
coincidental.
Now let's return to my S, which you did not like but which I continue to
be emotionally attached to. It is certainly a legitimate question to ask
if S is a formal theorem of PA. This is something I might be interested
in even if I have no interest in arithmetic. I might just like playing
around on my computer with syntactic strings and rules, and might be
curious as to what might emerge.
Okay, finally we're ready to make a philosophically interesting move. I
want to make the following claim (I'm repeating myself from my previous
messages, of course):
(*) Any finitistic mathematical proof that the sum of three cubes
can never be 42 can be mimicked by a formal PA proof of S.
Here, I am finally exposing my guilty conscience to the world and speaking
plainly of integers ("...the sum of three cubes..."). But I wish to
emphasize that I am still *not* inserting any new symbols (such as "Z")
into my formal string S, or even assigning any "meaning" to S. I have not
defined what a "model" or an "interpretation" is. I am simply making the
claim (*) above, no more and no less.
Note that I am not claiming that (*) is a mathematical statement, let
alone something I could prove mathematically. The statement (*) is a
philosophical statement of belief. What motivates me to believe it?
Quite simply, the answer is: mathematical experience. The mathematical
community, most recently with the aid of computerized proof assistants,
but long before that with pencil and paper and chalkboards, has found that
finitistic mathematical proofs can be mimicked by formal PA proofs. They
have learned by experience that when they think of certain
number-theoretic statements, such as "sqrt(2) is irrational", then they
are able to write down corresponding formal strings in the first-order
language of arithmetic such as
S' = "NOT exists x exists y: (x>0) AND x*x = y*y + y*y"
and then mimic the ordinary mathematical proof that sqrt(2) is irrational
by a formal derivation of S' from the axioms of PA. Note carefully, once
again, that S' does *not* contain any "Z" symbol to represent the
integers.
Note also that no claim is being made that these formal manipulations are
being assigned some "real meaning" that includes the assertion that x and
y and z are integers. The statement (*) does not claim that S refers
unambiguously to integers. Maybe some Martian with some strange guilty
knowledge will look at what I'm doing and say, "Hey! Your PA proof of S
is really an argument that there aren't any zorks that gerbaffle in the
wox!" It's a free universe; the Martian can think that if it wants. I
don't care. I just notice that I seem to have developed the skill of
writing down (Z-free) formal strings that have the property that
finitistic proofs of arithmetical statements can be mimicked by formal PA
proofs of the formal string. When I assert (*), I am not demanding that S
be "adequate" or "satisfactory" in any way beyond this. This might seem
very weak to you. You might feel the need to impose additional
requirements, such that S explicitly "say something" about integers. But
I don't. And neither does the rest of the mathematical community.
It is true that doing what you're requesting would take me out of my
syntactic paradise. That's why I don't want to do it. Also, I don't need
to do it. As long as I have (*), I'm able to conclude that if I can show
that S is unprovable in PA then the impossibility of the sum of three
cubes equalling 42 is unprovable finitistically.
Let me conclude with one more direct question: Do you believe (*) above?
Note that I am not asking whether you believe that S is right or wrong or
inadequate or "should" contain a Z symbol or anything like that. I am
simply asking if you believe that (*) is true, given how I have defined S.
If you don't, why not, given that this kind of mimicry is a routine skill
that an increasing number of users of proof assistants are developing on a
daily basis?
Tim