[FOM] first/second order logic

[Harvey Friedman]

In some offline correspondence with a student, the question of first
order versus second order logic arose, and I wrote something about it
which may be of interest or educational interest for the FOM
readership. Here it is.

Traditionally, this has been a bit of a murky subject with a lot of
misunderstandings. What I write below is nowhere near good enuf to
dispel all of the controversies and misunderstanding. It may still
help and be useful to student readers.

Is there anything new below? Not directly, but I did notice the
following interesting issue that may really lead to something new. I
say below that there is no completeness theorem for second order
logic.

QUESTION. Is there an interesting completeness theorem for nontrivial
fragments of second order logic? Obviously, first order logic is a
nontrivial fragment that does have a completeness theorem. But what if
we look at SIMPLE fragments of second order logic. Maybe there are
really interesting such with a completeness theorem. Or if there has
been a good start on this, then how far can it be pushed?

**************************

There has been a lot of confusion about the use of first order logic,
and second order logic, in f.o.m. (foundations of mathematics), or
even what second order logic is.

First of all about ZFC. ZFC usually refers to a first order system,
and there are models of ZFC of every infinite cardinality by the
downward and upward Skolem Lowenheim theorems.

There is also something called second order ZFC.It is formulated in
second order logic, and according to the usual semantics for second
order logic, all models of second order ZFC the models of second order
logic have cardinalities the strongly inaccessible cardinals.

First order logic has syntax and semantics. The syntax includes most
importantly the notion of rigorous proof. This is meant as an
idealized model of mathematical practice. Mathematicians "adhere" to
rigorous proof in first order logic from ZFC and any rigorous proof in
ZFC is supposed to represent rigorous mathematical thinking.

The completeness of first order logic is viewed as a response to the
question: can we extend the notion of rigorous proof in first order
logic? Is it too restrictive? The answer is no. Because we first argue
that every rigorous proof in first order logic is in fact valid
according to the semantics of first order logic. In fact that is the
main purpose of the usual semantics of first order logic. To make this
self evident.

Then there is the famous Godel Completeness Theorem, a really very
good mathematical result, that every sentence in first order logic
that is semantically valid has a rigorous proof.

So how does second order logic fit into this picture? When working in
ZFC mathematicians will of course single out certain constructions in
order to even make sense of what they do for a living. One of them is
the notion of subset of a set. This can be treated a just another
concept handled in the usual way like any other - expand it out with a
universal quantifier and implication. Every element of A is an element
of B. There are uncountably many subsets of B (assuming B is infinite)
and so in any countable model of ZFC with a point B, the points A that
are satisfied to be subsets of B in the model, are going to be very
very impoverished. There will be only countably many points A that are
satisfied to be a subset of B because even the whole model is only
countable

So in a sense we really want to work with second order models of ZFC
if we are concerned about working with models of ZFC that better
reflect set theoretic reality. The essence of second order logic is to
take "subset of" as primitive and require that, in the semantics of
second order logic, models fully reflect it.

So why not move to second order logic instead of first order logic?

Well let's back up. What is the syntax of second order logic? What do
we mean by a rigorous proof in second order logic? There are some
standard proof systems of second order logic, but there are more than
one standard natural one reasonably well studied. The difference
between first order and second order logic is that SECOND ORDER LOGIC
HAS NO COMPLETENESS THEOREM to guide as to when to stop adding logical
axioms or proof methods.

Furthermore, all of the standard natural proof systems of second order
logic can be appropriately viewed as systems in first order logic.

So if you care about modeling mathematical thinking then first order
logic is essentially the only game in town. If you care more about
modeling mathematical reality (not merely accepting that there is
exactly one such) then you naturally gravitate towards second order
logic. But you always bear in mind that second order logic syntax is
extremely open ended with no completeness theorem to guide you, and
also that mathematicians working in second order logic is still
properly modeled by first order logic.

Harvey Friedman