FOM: second-order logic is a myth

[Stephen G Simpson]

John Mayberry 11 Mar 1999 16:28:35 writes:
 > In the controversy over second order logic, everyone seems to 
 > agree about the basic mathematical facts

Maybe not -- see below.

 > first order logic doesn't provide a model of reasoning either:
 ...
 > it works for some such definitions (e.g. the definition of "group")
 > but not for others (e.g. the definition of "complete ordered field"
 > or "topological space").

I disagree.  All of this reasoning, including the definitions of
complete ordered field and topological space, is captured in
first-order logic.  More generally, almost all of mathematics is
formalizable in ZFC, and ZFC is a first-order system.  These
mathematical facts are well known, but you (and other advocates of
second-order logic, such as Shapiro) don't seem to fully accept them.

 > logic - formal, mathematical logic - is part of set theory. 

This is historically incorrect.  Logic existed long before set theory.
Logic goes back to Aristotle; set theory goes back to Cantor.

It's also scientifically incorrect.  The correct view of the matter is
that logic is a framework or common background for all scientific
theories.  Set theory is one of those theories.  All of the set
theories commonly considered in set theory textbooks (ZF, ZFC, ZF+V=L,
ZF+DC+AD, etc etc) are in this framework, the underlying logic being
first-order logic.

 > Without set theory you cannot motivate your systems of formal,
 > first order proof, because you can't formulate completeness in a
 > natural way, or establish it.

I'm pretty sure this remark is historically incorrect.  The axioms and
rules of first-order logic were expounded and motivated in logic
textbooks (early editions of Hilbert-Ackermann?) earlier than the
formulation or proof of G"odel's completeness theorem.

The remark is also scientifically incorrect.  First-order logic (it's
better to call it predicate calculus) can and should be motivated
independently of set theory, as a general framework for reasoning
about any subject whatsoever.  For instance, if you want to reason
about cars and trucks, you lay down primitive predicates Cx (`x is a
car') and Tx (`x is a truck') and maybe Vx (`x is a vehicle') and go
from there.  If you want to also reason about sets of vehicles, you
will probably also want an additional predicate Sx (`x is a set of
vehicles') but you can go a long way without this.

Incidentally, nothing like the power of ZF set theory is needed to
state or prove G"odel's completeness theorem.  In fact, the
completeness theorem is provable in WKL_0.  (See my book `Subsystems
of Second Order Arithmetic',
<http://www.math.psu.edu/simpson/sosoa/>.)

-- Steve