[FOM] Aaronson's Summary of Incompleteness

[Thomas Klimpel]

> (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. This was proved
(as theorem 3.5) in

A. J. Wilkie and J. B. Paris, On the scheme of induction for bounded
arithmetic formulas, Annals of Pure and Applied Logic, 35 (1987), pp.
261–302.

A modified version of that proof is contained in chapter 2
"First-Order Theory of Arithmetic." by Samuel R. Buss at
http://www.math.ucsd.edu/~sbuss/ResearchWeb/HandbookProofTheory/index.html
This chapter also contains a good explanation in which way the quoted
result is different from the results produced by Gödel's
incompleteness theorems:
"One way to strengthen this incompleteness theorem is by working with
two theories, S and T, such that S is a subtheory of T: in some cases,
one can establish that T cannot prove the consistency of its subtheory
S."


> (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. For example,
Tennenbaum's theorem
(https://en.wikipedia.org/wiki/Tennenbaum's_theorem) states that no
countable nonstandard model of Peano arithmetic can be computable.

At least for fragments of arithmetic, a more explicit dividing line
between weak and strong systems has been used (in the cited chapter
2):
"The line between strong and weak fragments is somewhat arbitrarily
drawn between those theories which can prove the arithmetized version
of the cut-elimination theorem and those which cannot; in practice,
this is equivalent to whether the theory can prove that the
superexponential function is total."

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. Whether those independence result would
take the form "P = NP is not provable in EFA" or rather "Assuming that
..., then P != NP is not provable in EFA" is hard to say. Not that I
believe that this is achievable, but it would be a huge success if it
could be achieved. You could object that EFA is laughably weak and
doesn't encompass all of mathematical reasoning. But that is a
different question, i.e. whether P != NP is unprovable (by
mathematical reasoning), which is different from the question whether
P != NP can be shown unprovable (in a specific given system).

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. (I know that some ultrafinitists will reject
axiomatic systems by principle, but ultrafinitism is not the topic
here anyway.)


Thomas Klimpel