FOM: second-order logic is a sterile myth
Stephen G Simpson
simpson at math.psu.edu
Tue Mar 23 14:41:15 EST 1999
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
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'
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?
More information about the FOM