Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?

From: Ralph Hartley (hartley_at_aic.nrl.navy.mil)
Date: 01/14/05 

Date: Fri, 14 Jan 2005 12:16:11 -0500

tchow@lsa.umich.edu wrote:
> In article <cs6ep3$lso$1@ra.nrl.navy.mil>, Ralph Hartley
> <hartley@aic.nrl.navy.mil> wrote:
>
>> But you are presumably a mathematician, and when mathematicians make
>> unqualified statements, with no other context, they usually *mean* "In
>> ZFC ...".
>
> As a matter of sociological fact, this is definitely false. For a
> trivial counterexample, consider:
>
> (*) "sqrt(2) is irrational" is provable in ZFC.
>
> When mathematicians assert (*), they mean (*). They don't mean
>
> (**) `"sqrt(2) is irrational" is provable in ZFC' is provable in ZFC.
>
> They couldn't, obviously, because this would instantly lead to an
> infinite regress.

I did say "usually".

The most obvious exception is most statements about ZFC.

But (*) doesn't need that exception because it is not an "unqualified"
statement.

I could argue that when they say (*) they really mean

(***) `"sqrt(2) is irrational" is provable in ZFC' is provable in V.

Where V is the much weaker system used to verify proofs.

Are there any cases where you need the axiom of choice to prove that
something is provable in ZFC? (That's different from a proof that uses AC)
It would be odd, the normal way to prove something is a theorem is to
exhibit a proof, and checking a proof is a finite thing.

Only in such a rare case of a non-constructive proof of theoremhood would
someone say (or mean) "'A is provable in ZFC' is provable in ZFC". I have
seen statements of the form '"A is not provable in ZFC" is not provable in
ZFC'.

I *could* argue that, but I don't think I will, because then the question
of in what theory (***) is provable might come up.

You are the the final arbiter of what you mean by a statement, but when *I*
say something like "sqrt(2) is irrational", I think I might mean something
like:

I^1 have seen and verified a proof^2 in ZFC^3 of "sqrt(2) is irrational".

1) Someone I *really* trust has, in this case I have myself, but I don't
even trust myself completely.

2) Actually a summary. I don't think I have seen (much less verified) a
proof of every single step from the axioms of ZFC, but I am confident that
there is one, and that I could produce one if I really needed one. In this
case I think I even know where to find one.

3) I only mean "ZFC" by default. The proof may not have used every axiom of
ZFC (in this case I know it didn't) so it is really a proof in a weaker
system. I am (intentionally or not) making a slightly ambiguous statement,
because it is impractical to always specify exactly what my conclusions
depend on.

If pressed, I would surely have to add even more footnotes. Most of the
time it is enough to say (and think) "sqrt(2) is irrational."

> Even you seem comfortable with asserting (*) flat out; that is, it isn't
> a white lie or a shorthand for something like (**)---it is meaningful on
> its own.

Maybe it's a *little* bit of a white lie, since I *ought* to note that it
really depends on V, and I don't. But V is so minimal that I feel justified
ignoring it completely. If you start with nothing, and trust no
assumptions, it is impossible to think at all.

> So we have at least one class of examples of mathematical statements
> that are meaningful on their own. Mathematicians typically include
> "sqrt(2) is irrational" and "every differentiable function is
> continuous" and so forth among the mathematical statements that are
> meaningful on their own, and that are *true* in an absolute sense, just
> as (*) is true in an absolute sense.

Just as they once included the Parallel Postulate.

(*) is dependent on fewer assumptions than "sqrt(2) is irrational", so one
might say that (*) is *more* absolutely true, if one could do so without
cruelly abusing words.

Except on Usenet :-), I could convince a finitist of (*), but not of
"sqrt(2) is irrational".

> There's another way to see that ZFC doesn't, in practice, have the
> status that you assign it. Suppose that someone were to find a
> contradiction in ZFC. Would this make any difference to mathematics?
> It would depend on the specific contradiction, but in general, it
> wouldn't make any difference.

I think it would make a huge difference.

I think there are proofs (not in ZFC) that ZFC is consistent. I'm not sure
exactly what those proofs depend on, but if ZFC is inconsistent, then those
proofs must not be sound either.

You couldn't just give up choice or whatever, and continue like nothing
had happened.

For the rest of this post I will assume not that ZFC had been found to be
inconsistent, but instead that mathematicians decided that ZFC does not
capture their intuitive idea of "sets" very well after all, and *decided*
to use something else. I think your arguments apply just as well to that
example, and it could happen.

Someone would have to go back through every proof and make sure it
is still valid (or a valid proof exists). Many would be easy, and some
could be handled in bulk. For some axioms (e.g. choice) it may be customary
to keep track, which would make it easier.

> Logicians would just pick some other foundation for mathematics with no
> known contradiction. ZFC is way too strong for most of ordinary
> mathematics anyway. All the theorems in the books would remain intact,
> except for the few that were affected by the specific contradiction.

It would make a *big* difference where the problem was. Just giving up
choice would be easy.

But suppose the problem were in V.

That would infect *all* proofs, and mathematics would have to start over.
(It is unlikely they would do that voluntarily.)

> What would you say then? That in this new situation, "sqrt(2) is
> irrational" no longer means "`sqrt(2) is irrational' is provable in ZFC"
> but now means "`sqrt(2) is irrational' is provable in X," where X is the
> new foundation? Given that the usual proof of sqrt(2)'s irrationality is
> left unchanged by the discovered contradiction in ZFC, it's a little
> bizarre to think that its meaning has changed.

My footnote 3) above supplies some wiggle room. The meaning of an ambiguous
statement need not be perfectly fixed.

> ... mimicking this proof formally in this or that formal system does not
> yield the "true meaning" of the statements in question.
> In fact, it's almost the other way around; we only accept (as a
> candidate for foundations) formal systems that faithfully mimic what we
> *already* recognize to be correct reasoning. Where do you think ZFC came
> from in the first place?

If you look at axioms as definitions, that makes sense. A formal definition
should match the informal definition as well as is practical, or it is no good.

The formal system does not yield "the true meaning", it yields "an
unambiguous meaning" (or less ambiguous).

When someone says "sqrt(2) is irrational" it may be a bit ambiguous. Is it
a statement about their intuitive (but imprecise) idea of the reals, or
about the much more exactly defined objects of a formal system?

If the definitions provided by the formal system are good enough, those two
meanings (mostly) coincide, and it doesn't matter (much).

Ralph Hartley

Relevant Pages

  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >> But you are presumably a mathematician, and when mathematicians make ... The most obvious exception is most statements about ZFC. ... Given that the usual proof of sqrt's irrationality is ... > bizarre to think that its meaning has changed. ...
    (sci.math)
  • Re: Platonism
    ... Most mathematicians just say "theorem" without referencing a system, ... Retreating to ZFC is unlikely. ... happens in SOME physics classes. ... The set of reals is not hard to construct in ZFC, ...
    (comp.theory)
  • Re: Platonism
    ... Most mathematicians just say "theorem" without referencing a system, ... Retreating to ZFC is unlikely. ... happens in SOME physics classes. ... The set of reals is not hard to construct in ZFC, ...
    (sci.math)
  • Re: Platonism
    ... Retreating to ZFC is unlikely. ... My assessment of the beliefs of mathematicians comes from conversations ... reason to be suspicious of formalism. ... and not a problem with the mathematicians concept of reals or of ...
    (comp.theory)
  • Re: Platonism
    ... Retreating to ZFC is unlikely. ... My assessment of the beliefs of mathematicians comes from conversations ... reason to be suspicious of formalism. ... and not a problem with the mathematicians concept of reals or of ...
    (sci.math)