[FOM] Concerning Con(PA)
Timothy Y. Chow
tchow at alum.mit.edu
Thu May 28 17:31:16 EDT 2015
Harvey Friedman wrote:
> BWQ. Every bounded infinite sequence from Q has an infinite Cauchy
> 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
> 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
> 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
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.
More information about the FOM