FOM: second order logic not a myth and related issues

[Randall Holmes]

Friedman says:

Despite a lengthy interchange with Holmes, I still cannot tell whether or
not there are any substantive issues worthy of continued discussion! I
believe that Holmes thinks that certain facts and definitions are important
that I don't. And Holmes may think that NFU plays a significant role in
f.o.m. I don't. It might in the future, but so might a large number of
things.

Holmes says:

I agree with the first two sentences.  The relevance of NFU to fom is
a side issue (not really part of this thread); I think that
formalization in NFU is interesting because it is actually possible,
and it is always nice to see an alternative foundation; it helps to
see what foundations do for us.  But I think that the ZFC formulation
is, alas, somewhat better overall.  For one thing, the best intuitive
motivations for NFU (there are some!) are not nearly as convincing as
those for ZFC, and a conviction that NFU is a workable foundation is
likely to rest ultimately on Jensen's and other consistency proofs for
NFU and extensions ... in ZFC.  A new development is that it appears
that some intuitively appealing extensions of NFU give surprisingly
high consistency strength; this may prove interesting eventually.

A subtle point is that I think there is a fairly good argument that
the comprehension criterion for NF(U) is a better resolution of the set
theoretical paradoxes than the comprehension criterion of ZFC -- but I
don't think that the foundations of mathematics really depend in any
essential way on a confrontation with the set theoretical paradoxes
(the paradoxes were avoidable mistakes).

Friedman says:

Perhaps a more interesting disagreement might be that he does not
acknowledge the very important sense in which ZFC is currently accepted as
the complete formalization of mathematics. He keeps emphasizing various
pedestrian senses in which it is not. This seems counterproductive,
backward looking, and totally uninteresting.

Holmes says:

I do not deny that ZFC is the favorite formalization of mathematics.
Fellow NF-istes chide me for referring to it as "the usual set
theory".  But I think that Friedman is making a stronger claim than is
warranted.  

A predicate like "backward-looking" is generally applied to evil
reactionary forces opposed to the right-thinking "progressive"
elements; in what direction does Friedman think we should be making
progress (he might find that I agree with him :-))?

Friedman says:

Of course, I am engaged in a long term project which may ultimately change
the status of ZFC as the currently accepted complete formalization of
mathematics. This in a much deeper sense than Holmes remark that "we
believe in Con(ZFC), which is not provable in ZFC". But we are not there
yet.

Holmes says:

I considered citing this against you.  Results of the kind you are
aiming for are much better examples than Con(ZFC).  The mere
possibility of such a project militates against your apparent views.

Harvey Friedman writes:
>...
>But I am confident that you will join me and many others on the FOM list in
>enthusiastically celebrating this recognition of Turing and Godel!!

Thus Holmes:

I will applaud, even if the recognition is for the wrong reasons :-)

Steve Simpson asks:

However, if 

  "it depends on the metatheory"

is enough to severely irritate Mayberry, then what would 

  "it depends on the real world" 

have done to him?  I could be wrong, but I imagine that the latter
formulation would have been much more irritating.

Holmes comments:

I think that the latter formulation would be much more to the point in
a conversation with me, and the same might be true of Mayberry.  I
like that.

Simpson says:

Let me try to put the point in a broader, more philosophical, more
speculative way.  This will probably irritate Mayberry even more!

The entire concept of `*the* standard semantics' or `absolute standard
semantics' for second-order logic seems to make sense only if you are
a set-theoretic realist or Platonist.  In other words, `absolute
standard semantics' assumes that infinite sets exist, the powerset
operation applied to infinite sets is real and meaningful, the
continuum hypothesis has a definite truth value, etc etc.  These
assumptions have to be part of the metatheory.

Thus it seems that, in order to accept `second-order logic with
standard semantics', you must first take a strong stand on many
questions in the philosophy of mathematics that are prima facie
important.  Thus your logic is not neutral with respect to such
questions.  Instead, your logic carries a lot of realist/Platonist
baggage.  Thus the scope and nature of logic have been severely and
sadly diminished.  Logic is no longer a common meeting ground that all
parties can agree on.  Instead it has become the exclusive instrument
of a particular philosophical faction.

This is another reason why `second-order logic with standard
semantics' is an inappropriate vehicle for philosophical and
foundational studies.

Holmes comments:

Do you engage in philosophical or foundational studies without bringing
your own strong philosophical views to bear?  Is it even possible to do
this?  Logic is a branch of philosophy itself.  The question of what should
properly even be called a logic is philosophical in character!

There is a pragmatic advantage to avoiding the use of controversial
assumptions when you can and flagging their use when you cannot; it
makes a search for common ground with others easier, and it makes it
easier to communicate.  I have never hidden the fact that I am a
realist.

Simpson argues:

I'm not so sure that's a well-known fact [referring to a statement to
the effect that no formal theory can completely formalize mathematics
--Holmes].  Isn't it more of a well-known philosophical assumption?
Extreme formalists might want to argue that arithmetic is *nothing
but* some particular formal system.  Thus your `well-known fact'
appears to be a prejudgement against the extreme formalists.

Holmes comments:

This may be a just criticism.  Are you innocent of making statements
which reflect your own philosophical convictions?  Try making one that
doesn't :-)

Simpson says:

Once again, I am speaking as neither a formalist nor a
realist/Platonist.  I only want all sides to get a fair hearing.

Holmes comments:

All sides are welcome to weigh in with their own opinions.  A
discussion of what kinds of foundations are seen to be appropriate by
what philosophical schools would be very interesting.  I often find
that philosophical viewpoints with which I disagree motivate
fascinating work in the foundations of mathematics.  Looking at the
foundational work often makes it easier to understand the
philosophical viewpoint as well.  For one thing, it is much easier to
talk about the mathematics, where there are generally accepted
principles of reasoning.

Simpson says (in dialogue with Hayes?)

 > He has an agenda: to defend the integrity of mathematics against
 > the dark forces of postmoderism, especially those infidels who
 > misuse G"odel's name.

There is some truth to that.  I am very passionate about foundations
of mathematics.  So is Harvey, and that's why he and I started the FOM
list.  And yes, I do see f.o.m. as part of a struggle against what one
might call forces of darkness (not only postmodernists).

Holmes comments:

Oddly enough, I have similar passionate interests, and similar
concerns about some of the same dark forces :-)

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes