[FOM] PA inconsistencies

[Harvey Friedman]

On Sat, Aug 18, 2018 at 2:04 PM, Sam Sanders <sasander at me.com> wrote:
> Dear Harvey,
>
>> FOM Readership: what are the main references for "mathematics without
>> exponentiation" and how far has it gotten?
>
> A major contribution is Nelson’s book “predicative arithmetic” and outgrowths.
>
> However, this approach has its problems: there exist (fairly natural) statements A, B
> such that both A and B are acceptable acceptable in Nelson’s framework, but A AND B
> is not acceptable.

Of course, this is prima facie FATAL for the kind of thing I have in mind.

>From the foundational point of view, here is the kind of thing I want
to get at. Suppose you immerse yourself in some corner of say
undergraduate mathematics. There often will not be any explicit
mention of any exponential or other super polynomial function in front
of you. The subject matter might be very different. You are just going
about your basic math in your merry way, assuming that when you buckle
down and give PROOFS, that all of high school and introductory basic
material is freely available to you. Is there a way of saying that you
are working without the exponential function, when you are not
involving the exponential function or anything like it in the
statements of the theorems you are making, which are not even on the
topic of "slightly high growth rates of natural number or real number
functions"?

Of course, you can interpret this as a big ad for SRM = strict reverse
mathematics. Whether I can deliver on this ad is an interesting
question.

> Also, there are a number of people that have done “feasible reverse math”, i.e. reverse
> math over a base theory weaker than EFA.

A couple of references for "feasible reverse math" of this kind would
be appreciated by me and perhaps FOM readers.
>
> Finally, when one does “mathematics without exponentiation”, I believe statements become
> very sensitive to coding.
>
This suggests to me that one needs a developed form of SRM = Strict
Reverse Mathematics to really effectively deal with "mathematics
without exponentiation".

Harvey Friedman