[FOM] 461: Reflections on Vienna Meeting

[Timothy Y. Chow]

On Thu, 16 Jun 2011, Richard Heck wrote:
> I am still a bit puzzled why some people think we do not know that PA is 
> consistent. I do not say we do know; as I've said in previous posts, I 
> think there are complex issues here related to the closure of knowledge 
> (or justification) under (known) logical consequence. But I also think 
> there are some other, more logical issues in the neighborhood.  So I'd 
> like to ask for some clarification about this.

I think that part of the key to understanding people's objections to the 
consistency of PA is the concept of *obviousness*.  Obviousness is not a 
formal concept, but I think that it plays an important role in the 
practice of mathematics.  Specifically, I believe that mathematicians 
tacitly see themselves as establishing less obvious statements from more 
obvious statements.

"Obvious" here could mean "self-evident," but in practice, known theorems 
are also granted this status.  That is, if you show that something follows 
from a known theorem, your work is done.

Since the day-to-day practice of mathematical theorem-proving requires 
only the ability to check logical correctness "locally" (i.e., from 
whatever body of knowledge is currently taken as given, to whatever new 
statement is under scrutiny), questions about the ultimate status of any 
of the statements can usually be ignored.  You can be a closet formalist, 
believing that local checking is all there really is to mathematics, or 
you can be a closet Platonist, believing that you're mapping out actual 
truths, and nobody will be able to tell the difference.

Now, what does this have to do with consistency proofs?  Though f.o.m. 
experts are accustomed to treating statements such as "PA is consistent" 
on an equal footing with any other mathematical statement, that is not how 
many mathematicians think.  The term "consistency," as applied to some 
theory T that purports to be some kind of "foundation for [a large part 
of] mathematics," signals to some people that we are now going to take a 
step back from our day-to-day activity of local checking, and ask some 
questions about "ultimate status."  Therefore, we are no longer going to 
allow people to take for granted the entirety of the body of "obvious" 
statements that we conventionally accept.  Only things that are somehow 
deemed to be *more obvious than the consistency of PA* will be allowed.

Now we can see why the fights start.  What sorts of statements are more 
obvious than the consistency of PA?  Different people are going to give 
different answers to this question.  May will say that the consistency, 
and a fortiori the truth, of the axioms of ZF is *less* obvious than the 
consistency of PA.  Similarly, if you take any of the other proofs of the 
consistency of PA, you can still find people who will identify some step 
in the proof that they regard as less obvious than the consistency of PA.

At this point, we might object that the skeptic is making unreasonable 
demands.  For example, as Richard Heck says:

> Is the worry that the principles needed to prove Con(T) must themselves
> be "as dubious" as the claim Con(T) itself? There is a sense in which
> that is true, but it is a trivial one. If the principles in question
> entail Con(T), then, of course, if T is inconsistent, some of those
> principles must be false. But if we cannot prove Con(T) for this reason,
> then we cannot prove anything. Premises that logically imply a
> conclusion are, by definition, logically at least as strong as that
> conclusion.

*Logically at least as strong*, yes.  But what about *at least as 
obvious*?  Then the answer is no.  Mathematicians routinely deduce less 
obvious statements from more obvious ones.  Thus, a priori, the skeptic 
isn't being totally unreasonable in asking for a proof of the consistency 
of PA from statements that are more obvious than the consistency of PA.

> A more sophisticated worry would be that the "consistency strength" of 
> the principles needed to prove Con(T) must be at least that of T itself, 
> meaning: If you have some principles that prove Con(T), and if T is 
> itself inconsistent, then those principles will themselves be (not just 
> false but) inconsistent. This is true, but, first, you do not need 
> anything close to Goedel's Second to prove it.

I think that Goedel's Second functions as a whipping boy simply because 
it's famous.  It demonstrates one particular intrinsic obstacle to any 
consistency proof.  To some people, it apparently suggests that it is 
hopeless to prove the consistency of PA from assumptions that are more 
obvious than the consistency of PA.  To Voevodsky, it apparently suggests 
that PA is inconsistent.  After all, what better explanation could there 
be for a stubborn obstacle to proving X than the falsity of X?

> Finally, strong versions of Goedel's Second apply also to Q. The form of
> argument being considered would imply, therefore, that we do not know
> that Q is consistent either. One can swallow this pill if one likes, but
> it does not seem a happy result to me

Happy for whom?  For you?  But you don't have any qualms about the 
consistency of PA either.  My guess is that a sizable proportion of the 
people who object strenuously to the consistency of PA would be quite 
happy swallowing this pill.

Tim