[FOM] Provability of Consistency

Timothy Y. Chow tchow at math.princeton.edu
Fri Mar 29 12:15:05 EDT 2019

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 

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 

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?


More information about the FOM mailing list