[FOM] Aaronson's Summary of Incompleteness

[Harvey Friedman]

These are all legitimate and interesting points. However, Independence
Results is such a limited part of Aaronson's major essay on P ? NP
that I cannot fault him for omitting these finer points.

However, I do think that Aaronson could simply say that we as of yet
do not even know how to show that P = NP is independent of much weaker
systems than PA, and in particular of EFA = exponential function
arithmetic https://en.wikipedia.org/wiki/Elementary_function_arithmetic
which is the weakest intensively studied formal system directly
incorporating exponentiation.

Harvey Friedman

On Tue, Jan 10, 2017 at 8:56 PM, Thomas Klimpel
<jacques.gentzen at gmail.com> wrote:
>> (1)  Independence of statements that are themselves about formal systems: ... This is the class produced by Gödel's incompleteness theorems.
>
> But not every independence result falling under category (1) is
> produced in such a way. For example, Friedman's exponential function
> arithmetic (https://en.wikipedia.org/wiki/Elementary_function_arithmetic)
> does not prove the consistency of Robinson arithmetic.
....
>> (3) Independence from “weak” systems, which don’t encompass all accepted mathematical reasoning. ..., but not within Peano arithmetic.
>
> I find the bar implicitly set by Scott Aaronson for independence
> results too high. Peano arithmetic is not a weak system.
...
> According to this dividing line, Friedman's exponential function
> arithmetic (EFA) is a weak fragment of arithmetic. But if the question
> is whether independence results for P != NP can be proved, then EFA
> feels like a really interesting candidate, precisely because it cannot
> prove cut-elimination. It would cast an interesting light on the role
> of higher-order reasoning.
...
> Another reason why I find EFA interesting is because it might be the
> limit of what is still acceptable to some styles of ultrafinitism. And
> in my opinion, there should be some connection between ultrafinitism
> and complexity theory.