[FOM] FOM Digest, Vol 169, Issue 11

[tchow]

Thomas Klimpel wrote:

>> (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.
[...]
> 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.

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.

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."  The typical FOM
subscriber, of course, recognizes that the independence from ZFC of the
continuum hypothesis or V=L or whatever does not automatically "settle
its status," but that is not how the mathematician in the street thinks.
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.

Tim