[FOM] EFA versus bounded arithmetic (was Aaronson's Summary of Incompleteness)

[Thomas Klimpel]

On Thu, Jan 12, 2017 at 1:34 AM, tchow wrote:
> There are two different questions here.  If we are interested in
> independence results for their own sake, then certainly any independence
> result for P = NP would be interesting.  Even independence from bounded
> arithmetic would be interesting.

The exact meaning of bounded arithmetic (in this context) is not fully
clear to me. It seems that it refers to a class of systems rather than
a single system. Interpreting it as Robinson arithmetic plus induction
for formulas with bounded quantifiers might be possible. But Nelson's
binary function # (defined as m#n=2^(|m| |n|) and pronounced 'smash')
used in fragments of bounded arithmetic could not be proved total in
that case. So this interpretation would be in conflict with the
interpretation (of bounded arithmetic) used in the formulation of
Razborov's independence result and in the titles of related papers:

"The bounded arithmetic theory S_2^2(\alpha) cannot separate
complexity classes P from NP by proving circuit lower bounds unless
hard pseudorandom generators do not exist." (The \alpha refers to a
second-order extension of S_2^2 by adding symbols for countably many
unary predicates \alpha, \beta, ...)

Razborov, A.A.: Unprovability of lower bounds on the circuit size in
certain fragments of bounded arithmetic; Izvestiya of the R.A.N.,
59(1), 1995, pp. 201-224.

Krajíček, J.: Interpolation theorems, lower bounds for proof
systems, and independence results for bounded arithmetic; Journal of
Symbolic Logic, 66(2), 1997, pp. 457-486.


So I would prefer to interpret bounded arithmetic to mean systems that
only have induction for formulas with bounded quantifiers. With this
interpretation, EFA is also a system of bounded arithmetic. It has the
advantage that a normal background in mathematical logic is sufficient
to work with it without running into huge surprises. The only big
surprise is just how much of normal mathematics can be formalized in
EFA. For weaker systems, the surprises already start when "standard"
Gödel coding (based on the Chinese remainder theorem and hence
essentially fixed width) must be replaced with more space efficient
variable length encodings
(https://golem.ph.utexas.edu/category/2011/10/weak_systems_of_arithmetic.html#c039677),
but the surprises don't end there. For example, Robinson arithmetic
plus induction for formulas with bounded quantifiers is still
interpretable in Robinson arithmetic, but (I was told that) it doesn't
have a computable non-standard model.

So I agree that independence results from (fragments of) bounded
arithmetic like Razborov's result are interesting. But I have been
surprised too much by those weak systems in the past, so that I prefer
not to judge whether such independence results would constitute a
major breakthrough or not. (I did quite some reading before writing
this answer, because I knew from past experience just how easy it is
to say wrong things about those weak systems.)


> However, the "mathematician in the street" typically has a different
> view of independence results: An independence result is typically viewed
> as *settling the status* of a mathematical problem by putting into the
> category of "problems that cannot possibly be solved."

Well, Scott Aaronson is a good example of how mathematicians "like to
interpret" independence results. In a certain sense, naïve set theory
is inconsistent, but naïve arithmetic is not. Hence independence of
set theoretic statements from set theory is seen as a sort of fault of
the statement itself, while independence of arithmetic statements from
a given formal system is seen as a fault of the formal system.

This "privileged" status of arithmetic statements is sort of the
reason why I protest that PA is not a weak system. I find EFA much
better in this respect, since the "mathematician in the street" with a
"reasonable" background in mathematical logic (as Scott Aaronson has
without doubts) will be in a much better position to understand the
significance of the independence results for that specific system
(like that it cannot prove cut elimination), what it entails to accept
that system (the allowed computations are no longer "feasible"), and
what it entails to go beyond that system (exponentiation is an
analytic function in complex function theory, but superexponentiation
is not).


> For this purpose, independence from PA isn't good enough.  Goodstein's
> theorem is viewed as a *theorem*, and the fact that it is unprovable in
> PA is viewed as a curiosity.

And the opinions of "logicians" are seen as kind of unpredictable and
difficult to follow, as witnessed by disclaimers like "Or do any
experts want to disagree or add caveats?"
(http://www.scottaaronson.com/blog/?p=2996#comment-1685358). It is
even worse if you don't know whether the "logician" is a "tenured
academic logician", a graduate student, or just an amateur logician.
But I really think that using EFA instead of PA can help reduce the
insecurity in such situations.


Thomas Klimpel