[FOM] Concerning Con(PA)

[Harvey Friedman]

I will try to get into the substance of what Chow has written in
http://www.cs.nyu.edu/pipermail/fom/2015-May/018749.html in the near
future. In the meantime, I want to clarify a technical point and also
briefly discuss what I consider to be an important proof of Con(PA)
that perhaps some subscribers have forgotten.

I said that PA is interpretable in RCA_0 + BWQ. This shows very
fantastically that Con(RCA_0 + BWQ) implies Con(PA). However, RCA_0 +
BWQ does not prove Con(PA). This is because RCA_0 + BWQ is equivalent
to ACA_0 over RCA_0. See Theorem 1.9.1 of Simpson's SOSOA, where it is
stated for the reals. But it works fine with the rationals, which is
highly preferable for present purposes.

I will be giving a SRM (strict reverse math) treatment of the above.
The devil is entirely contained in the details...

Here is a proof of Con(PA). It does accomplish the following: it shows
that the usual formulation of Con(PA) did not screw up on the
relatively complicated axioms of PA, involving all arithmetic
formulas, and primitive axioms, nor screw up on the axioms and rules
of predicate calculus.

"Obviously" we can define predicates on N by recursion - we do this of
course with addition, multiplication, exponentiation, and various
elementary mathematical contexts. So we use a very specific single
instance of definition of a predicate on N by recursion, involving a
condition which does have one unbounded quantifier. Then we use a
single quantifier free induction involving this defined predicate. All
of this can feasibly be done very explicitly, and we get a proof of
Con(PA).

Harvey Friedman