[FOM] Regarding consistency of PA

[Harvey Friedman]

There is a set of fifteen or so well known essential facts from  
mathematics, A_1,...,A_15, such that the following holds.

There is a direct combinatorial transfer of an inconsistency in PA to  
a refutation of

A_1 and ... and A_15 and "every bounded infinite sequence of rationals  
has a Cauchy subsequence with rate 1/n".

I.e., for all i,j >= n, |q_i - q_j| < 1/n.

This kind of result (mine from the 1960's) is normally stated with  
RCA_0 instead of the conjunction of these A's. This is an innovation  
typical of SRM = strict reverse mathematics.

**********

The "usual" proof of Con(PA) involves looking at formulas of PA in  
detail. But that is expected by any mathematician.

One makes a recursive definition of SAT(A,n_1,n_2,...,n_k), where A is  
a formula of PA with at most the free variables v_1,...,v_k, following  
Tarski.

Then one proves that for every axiom A of PA, including the logical  
axioms of PA, SAT(A,n_1,n_2,...,n_k) holds for al choices of  
n_1,...,n_k, where A has at most the free variables v_1,...,v_k.

Next one proves that this property is preserved under the rules of  
inference of PA (which are just the rules of inference of logic).

Next one proves that this property holds of all theorems of PA.

Obviously this property does not hold of 1 = 0. Therefore PA is  
consistent.

Subscribers can now discuss explicitly why they view the consistency  
of PA problem as a legitimate open problem in mathematics.

Angus MacIntyre asserted explicitly at his talk at the recent Vienna  
meeting, that "consistency of PA is a legitimate open problem in  
mathematics."

Harvey Friedman