FOM: second-order logic is a sterile myth

[Stephen G Simpson]

Pat Hayes 23 Mar 1999 12:11:26 writes:

 > I wonder if you would tell us how you reconcile yourself to the
 > fact that every consistent first-order theory (including, one
 > hopes, ZFC) has a countable model?

This is a fundamental theorem of mathematical logic.  It's basic to my
thinking on f.o.m.  I assume that it's also basic to the thinking of
every other modern f.o.m. researcher.

 > There seems to be a central snag with the idea of choosing any
 > formal language as the foundation for mathematics

I don't think a formal language by itself can be the foundation of
anything.

You seem to think I'm advocating ZFC as *the* foundation of
mathematics.  That's not at all what I advocate; or at least, it's not
my bed-rock position.  I am only trying to bring the experience of
modern f.o.m. research to bear on the ongoing discussion of
second-order logic.  The overwhelming weight of that experience is
that second-order logic with standard semantics is a dead end for
f.o.m., while ZFC (including countable models of ZFC, as in Cohen's
work) and other foundationally motivated first-order systems
(e.g. subsystems of second-order arithmetic such as WKL_0 etc) are the
framework that leads to f.o.m. advances and insights.

If you're interested in something closer to a serious, bed-rock,
philosophical position on f.o.m., have a look at my recent postings on
interpreting PRA in the real world, 3 Mar 1999 19:23:38 and 17 Mar
1999 18:29:38, as well as my paper on Hilbert's program
<http://www.math.psu.edu/simpson/papers/hilbert/> and my recent book
`Subsystems of Second Order Arithmetic'
<http://www.math.psu.edu/simpson/sosoa/>.

Now, I've tried to answer your question, so why don't you try to
answer mine.  What are the significant proof-theoretic differences
that you seemed to be alluding to, between formalisms for second-order
logic with quantifiers versus those with lambda abstraction etc?

-- Steve