[FOM] PA inconsistencies

[Harvey Friedman]

Sam Sanders https://cs.nyu.edu/pipermail/fom/2018-August/021165.html wrote

>  In my modest case, I take the infinitely large strictly decreasing sequence of ordinals as a property of ZFC or CIC, but not as something factually true.

As it happens, Voevodsky’s lecture, and esp. his comment on the
consistency of PA, was discussed here on FOM; this discussion included
(IIRC) a question of Harvey Friedman along the following lines:

In your own papers, you have used axioms/theorems that imply (dwarf is
perhaps a better word) the consistency of PA, and far stronger
systems.  Why single out the consistency of PA? Why is the
latter questionable, while the rest of math that implies it is left alone?

*****************

Yes, specifically I wrote concerning what kinds of mathematics would
have to be discarded if an inconsistency in PA was found.

Basically,

BW (Bolzano Weierstrass). Every sequence of real numbers from [0,1]
has an infinite 2^-n convergent subsequence.

would have to be discarded, and therefore also the many proofs that
use BW, mainly in classical analysis. (I proved RCA_0 + BW is
equivalent to ACA_0, and therefore implies PA). But also, prima facie,
even the current proofs of FLT that have been cleansed of Grothendieck
universes need to be intensively reworked - maybe also discarded.

There is the question of what statements in classical analysis can be
proved without BW. Actually a fair amount, as many of them have
constructive proofs, and usually those don't rely on BW.

NOW WAIT A MINUTE. The reason BW would have to be discarded is that
any inconsistency in PA can be converted, I think even by hand, to an
inconsistency in RCA_0 + BW.

However, a criticism of this is that RCA_0 is not so obviously a
necessary part of the kind of mathematics we are talking about.

HOWEVER, when my foundational papers on Strict Reverse Mathematics
come out, we will see how to show that any proof of 1 = 0 in PA can be
converted to a proof of 1 = 0 from

T + BW

where T is a collection of absolutely essential statements in
mathematics like, e.g., the ordered ring axioms for integers. Then the
argument that an inconsistency in PA will then destroy BW and a lot of
classical analysis and other theorems will be significantly
strengthened.

Another even more fundamental place where inconsistencies in formal
systems will have to destroy large portions of mathematics is the
following.

Suppose we have an inconsistency in EFA (exponential function
arithmetic), the name I used for the (synonymous) system that is often
now called ISigma_0(exp). Then using SRM = Strict Reverse Mathematics,
in a more powerful and extensive way, a very large amount of pure
mathematics should be destroyed, rigorously. Such would be some fruits
from the proper foundation of SRM expected to be available in 2019.

Informally, this corresponds to the question: just how much
mathematics can be done without any supposing of integer
exponentiation? What does "mathematics without exponentiation" look
like?

FOM Readership: what are the main references for "mathematics without
exponentiation" and how far has it gotten?

I have been very busy with #108 and reversals: see
http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/b
and this delays the foundational papers on SRM = Strict Reverse
Mathematics, as well as many other promises made on the FOM and
elsewhere.

Harvey Friedman