[FOM] Aaronson's Summary of Incompleteness

[Thomas Klimpel]

On Thu, Jan 12, 2017 at 3:14 AM, Harvey Friedman wrote:
> 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.

You are right. But it would be nice to expand point (1) to more than
three lines to do more justice to the effort involved in obtaining
independence of concrete statements that are themselves about formal
systems.

How about:
(1) Independence of statements that are themselves about formal
systems: for example, that assert their own unprovability in a given
system, or the system’s consistency. This class includes the results
produced by Gödel’s incompleteness theorems. More effort is needed for
concrete results like that EFA(^1) proves neither the consistency of
Robinson arithmetic nor the cut-elimination theorem. Despite the huge
effort, even the beautiful independence results of the reverse
mathematics program fall into this class, since the separation between
the systems follows from Gödel's incompleteness theorem.

(^1) EFA is the weak fragment of Peano Arithmetic based on the usual
quantifier free axioms for 0, 1, +, x, exp, together with the scheme
of induction for all formulas in the language all of whose quantifiers
are bounded. The quoted result is from Wilkie and Paris [1], a
modified version of their proof is contained in [2].

[1] 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.
[2] "well formed entry in the Reference section equivalent to:"
chapter 2 "First-Order Theory of Arithmetic." by Samuel R. Buss at
http://www.math.ucsd.edu/~sbuss/ResearchWeb/HandbookProofTheory/index.html


> 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.

I thought about this now whether he really should. In his previous
more extensive survey of the same question, he decided to avoid such
explicit statements, and deferred to existing surveys [10, 46, 49]
(and discussions like
http://cs.nyu.edu/pipermail/fom/2001-August/004996.html). Since he
deferred to his previous survey this time, I think he could just leave
it like that.

[10]  S. Buss. Bounded arithmetic and propositional proof complexity,
in Logic of Computation (H. Schwichtenberg, ed.), pp. 67–122,
Springer-Verlag, 1997.
https://www.math.ucsd.edu/~sbuss/ResearchWeb/marktoberdorf95/
[46]  R. Raz. P ̸= NP, propositional proof complexity, and resolution
lower bounds for the weak pigeonhole principle, in Proceedings of
ICM’2002 (International Congress of Mathematicians), Vol. III, pp.
685–693, 2002. http://www.wisdom.weizmann.ac.il/~ranraz/publications/Pchina.ps
[49]  A. A. Razborov. Lower bounds for propositional proofs and
independence results in bounded arithmetic, in Proceedings of
ICALP’1996, pp. 48–62, 1996.
http://people.cs.uchicago.edu/~razborov/files/icalp.ps.


Thomas Klimpel