[FOM] PA Completeness/more

[Harvey Friedman]

The following adds to the growing completeness phenomena for PA. It goes in
a somewhat different direction than the earlier recent postings of mine on
this topic. 

THEOREM. Any universal sentence in 0,S,+,dot that is true in the reals is
provable in PA. Any scheme in 0,S and unary schematic letters is true for
all set interpretations of those letters if and only if every substitution
by formulas in 0,S,+,dot is true in the natural numbers if and only if every
substitution by formulas in 0,S,+,dot is provable in PA.

THEOREM. PA can be axiomatized as follows.
1. All universal sentences in 0,S,+,dot true in the reals.
2. All schemes using only 0,S and unary schematic letters all of whose
substitution instances in 0,S,+,dot are true.

Note that these results do not treat sentences and schemes the same way.

The completeness phenomena for PA will become deeper and deeper through
sustained effort over many years, and will vindicate the idea that

"PA does not miss any fundamental axioms and axiom schemes in its language".

The same efforts will also prove dramatically fruitful for many other axiom
systems that we use in f.o.m.

This kind of paradigm shift is one of many other paradigm shifts that are
needed to make real progress in f.o.m.

Harvey Friedman