FOM: second-order logic is a myth

[Stephen G Simpson]

Perhaps I expressed myself in a misleading way.  Robert Black 23 Feb
1999 17:22:56 thinks I'm a formalist, but I'm not one.  Black said

 > ...  Of course Steve's entitled to his
 > neoformalist view, and I dare say it's widely shared, but ....

 > .... if Steve's right, is there any such thing as 'the intended
 > interpretation' of second-order logic?

but actually I wasn't intending to take any particular stand on these
issues.  The remarks in my original `second-order logic is a myth'
posting (22 Feb 1999 16:16:41) were certainly not intended as an
attack on the standard `Platonist' or realist view of sets, `the
intended interpretation' of second-order quantifiers in terms of
arbitrary subsets of the domain of individuals, etc.  I actually favor
the `Platonist' or realist view in many contexts.  

My only purpose in 22 Feb 1999 16:16:41 was to explain or summarize
the current understanding of second- and higher-order logic.  Such an
explanation seemed worth-while, because much of this hard-won
understanding dates from 1939 and later, and some FOM subscribers may
be unaware of it.

Since my earlier attempt fell flat, let me try again.

It's all very well to posit the set V_2 of second-order validities,
i.e., sentences that are true in all structures of the form (A, P(A),
s) where A is an arbitrary set, P(A) is the power set of A, and s is a
finite sequence of relations on A.  The main point that I wanted to
make in 22 Feb 1999 16:16:41 is that it has not proved fruitful to try
to study the structure of V_2 as a whole, or to try to correlate V_2
to some `logic'.  In particular, we know that V_2 cannot be generated
in any reasonable way by axioms and rules of inference.  Furthermore,
we know how to find particular sentences such that the question of
whether they belong to V_2 is not absolute in the sense of G"odel
1939.  For example, we can straightforwardly construct a sentence S
such that S belongs to V_2 if and only if the continuum hypothesis
holds, and another sentence S' such that S' belongs to V_2 if and only
if there exists a well ordering of the reals.  This is what I intended
when I said that V_2 depends on the underlying set theory.  (I
apologize for this somewhat inaccurate formulation.)  Thus the study
of V_2 turns out to be tantamount to the study of set-theoretic
independence a la G"odel 1939, Cohen 1962, Solovay, Jensen, Shelah,
..., to the point where V_2 can scarcely be considered as a separate
object of study.

When I said that second-order logic is a myth, this was simply my
provacative way of making the point that the study of V_2 as a whole
is fruitless and hopelessly intractable.  (I'm apologize if some
people were confused or offended by this formulation.)

Although V_2 itself is intractable, there is another, more `logical'
approach in which one studies certain first-order, two-sorted theories
with axioms of extensionality, comprehension, etc.  The two sorts may
be called individuals and sets, and the axioms are motivated by V_2.
Thus one studies what amounts to fragments of V_2 formulated as
theories in a two-sorted predicate calculus.  Letting x, y, ... be
individuals and X, Y, ... be sets, the general comprehension scheme is
something like

     (forall ...) (exists X) (forall x) (x in X <==> F(x,...))

where F(x,...) is an arbitrary formula in which X does not occur.  One
can also consider various choice schemes, etc.  The study of such
predicate calculus schemes and their proof theory and model theory is
what one means by second-order logic nowadays.  This approach also
extends to higher-order logics.  The G"odel/Henkin completeness
theorem holds for all of these logics.

This predicate calculus approach has been *much* more fruitful than
the study of V_2, V_3, ....  In particular, the predicate calculus
line is the one that I follow in my book `Subsystems of Second Order
Arithmetic' <http://www.math.psu.edu/simpson/sosoa/> as the framework
for reverse mathematics, etc.  Hilbert's second-order axioms for
geometry can also be viewed in this way, and categoricity can be
proved.  The proof-theorists have also obtained interesting
cut-elimination results, etc., for some of these second- and
higher-order logics.

With this clarification, let's return to the discussion of the
continental philosophers' claim that geometrical reasoning is
irreducible to logical reasoning.  To be continued ....

-- Steve