[FOM] Concerning Con(PA)

[Timothy Y. Chow]

Harvey Friedman wrote:

> BWQ. Every bounded infinite sequence from Q has an infinite Cauchy 
> subsequence.
> BWQ'. Every strictly increasing infinite sequence from Q[0,1] has an
> infinite 1/n Cauchy subsequence.
>
> The following is well known (I think I am usually cited for this or
> this kind of thing):
>
> BWQ and BWQ' are provably equivalent to ACA_0 over RCA_0.
>
> COROLLARY. PA is interpretable in RCA_0 + BWQ and RCA_0 + BWQ'..

I've seen you mention this before, but I don't know how the argument goes. 
Have you written it up anywhere, or alternatively, can you sketch the 
argument?

> So the idea is that BWQ, BWQ' is an essential component of mathematics 
> that is readily accepted and used or conceptually used by all of the 
> Nelsons, Voevodskys, etcetera of this world. Hence Con(PA) is not an 
> issue.
>
> The obvious weakness in this line of argument is the use of RCA_0.

I like this line of argument.  However, I think that there is a way that 
"Nelson" (again I use his name figuratively) can potentially dodge it, 
that doesn't have to do with the logical strength of RCA_0 (at least not 
in the sense that "logical strength" is classically understood).

When I talk with "Nelson" I sometimes get the feeling that he is tacitly 
using something like the following algorithm to field my questions about 
mathematical statements.

0. Consider a mathematical statement to be "directly meaningful" if it 
asserts the existence of some finite feasible object.  Thus, "tic-tac-toe 
is a draw" and "45*55 = 2475" and "there is a proof of Con(PA) in ZFC" are 
all directly meaningful.

1. When confronted with a directly meaningful mathematical statement S,
affirm S if convinced that the finite feasible object in question has 
been constructed or could actually be constructed if desired.

2. When confronted with a mathematical statement S that is not directly 
meaningful, first assess whether S appears to have anything to do with the 
foundations of mathematics.  If not, then affirm S if a proof of S in ZFC 
has been constructed or could be constructed if desired.  Issue no warning 
that what is really being affirmed is not S itself but rather "there is a 
proof of S in ZFC," unless the context of the discussion involves the 
foundations of mathematics.

3. If, in step 2, S *does* appear to have something to do with the 
foundations of mathematics, then generate an ad hoc response depending on 
the specific S in question.

If I adopt an algorithm of this sort, then I am able to masquerade as an 
ordinary mathematician most of the time.  If someone asks me, for example, 
whether every differentiable function is continuous, then I do not need to 
launch into a philosophical tirade that the reals don't actually exist in 
any direct sense, but that I happily accept that "every differentiable 
function is continuous" has been proved.  Instead, in accordance with step 
2 above, I simply say, "Yes" and move on.

Similarly, if I am confronted with BWQ, then *in accordance with step 2*, 
I simply affirm it.  I can even nod in affirmation as you walk me through 
a proof of BWQ => Con(PA).  But at the end, when you cry, "Gotcha!" I lay 
my cards on the table and maintain that all I have *really* been affirming 
all along is that the discussion we have been having can be formalized in 
ZFC (or some other foundational system).  I am not affirming that BWQ is 
directly meaningful.  It might look that way, because under normal 
circumstances, I issue no warning in step 2, but if you force me into 
"verbose mode" then I will reveal what I'm really thinking.

It's not so easy to corner someone who is using an algorithm of this sort, 
where by "this sort" I mean having some dichotomy (not necessarily exactly 
the one above) between "directly meaningful" statements and other 
mathematical assertions.  I think the first step is to try to pin down 
exactly what sorts of statements are being accepted as "directly 
meaningful" and are not being silently transformed from "S" to "S is 
provable in T" under the hood.  My previous FOM post can be viewed as 
asking whether "PA is consistent" is a directly meaningful statement. 
One might think so, but it's not as clear as you might think.  If "PA is 
consistent" is not regarded as directly meaningful then I don't think that 
a demonstration of BWQ => Con(PA) will carry much weight, no matter how 
elementary the demonstration is.

Tim