[FOM] Concerning 1st and 2nd order "logic"

[Harvey Friedman]

There are a number of confusing points to be made about these
"logics". If looked at from a proper perspectives, there are
definitely some promising research programs that need to be explored.

First of all, both 1st and 2nd order "logic" are perfectly legitimate
semantic systems. I.e., there is a clear notion of structure - the
same for both - and a clear notion of formula and satisfiability.
Although there are some interesting and important variants that need
to be considered.

The 1st and 2nd order semantic systems both require prima facie
substantial set theoretic commitments. Namely, to the notion of
arbitrary set.

However, as is well known, in the case of the 1st order semantic
system, there is a tremendous stability. With tiny set theoretic
commitments, one sees that validity is r.e. So there is a presentation
of 1st order logic as a semantic system, with essentially no set
theoretic commitments, which can be proved to be equivalent to the
standard presentation via tiny set theoretic commitments. This is from
Goedel's Completeness Theorem.

The situation with regard to 2nd order logic as a semantic system is
completely different. We can effectively transform any set theoretic
sentence A, subject to certain restrictions, to a sentence A* in
second order logic and a proof in ZFC that A is true if and only if A*
is valid. We can also do this with "satisfiability" instead of
"validity*. Here the restriction can be taken to be, e.g.,

that a given first order sentence holds of V(omega + omega)
that a given first order sentence holds of V(kappa), where kappa is
the least fixed point of the beth function.
and so forth.

In fact, we can go further. For validity, we can use sentences in set
theory that begin with a universal quantifier over all sets, followed
by any set theoretic formula where the quantifiers are bounded to the
power set of a set. In fact, we can use the form

1) (for all sets x)(phi holds in (POW(x) union x,epsilon).)

where phi is first order.

Then we get a kind of equivalence between validity in 2nd order logic
and 1). There is an effective map from sentences in 2nd order logic to
sentences in 1) such that, provably in ZFC, the given sentence is
valid if and only if its value is true. And there is an effective map
from sentences in 1) to sentences in 2nd order logic such that,
provably in ZFC, the given sentence is true if and only if its value
is valid in 2nd order logic. NOTE: What fragment of ZFC suffices for
this? NOTE: What about a bijection between sentences in 1) and
sentences of 2nd order logic?

All of this is very well known, or very well essentially known.

But we see a very stark contrast between 1st and 2nd order logic here.
Validity in 1st order logic is always in principle finitely
verifiable. Whereas this is very much not the case for validity in 2nd
order logic.

Higher order logic is in a sense equivalent to 2nd order logic, as a
semantic system, in the following sense. There is an effective map
from the sentences of higher order logic to sentences in 2nd order
logic such that, provably in Z, the given sentence is valid in higher
order logic if and only if its value is valid in 2nd order logic.
Again, very well known.

Now a "logic" is not just a semantic system, but also is a proof
system. I.e., we want to treat deductions. Deducibility must at least
imply validity.

In the case of 1st order logic, there is an obvious necessary
criterion for the proof system. That deducibility be equivalent to
validity. I am including relative deducibility and relative validity,
of course. And there are quite a lot of nice ones from many points of
view.

In the case of 2nd order logic, this is impossible. Therefore what has
developed is some deduction systems which are not complete. I.e., do
not correspond to validity in 2nd order logic.

We are now ready to confront the proposed research program. In what
sense are any of the various usual deduction systems for 2nd order
logic complete or in some interesting sense special?

For the weak ones based first order comprehension, we can derive
completeness if we modify the semantics of 2nd order logic. There are
some objections and defenses of this. This kind of move is yet more
problematic and awkward in the case of second order comprehension.
Much more satisfactory would be a way to justify the choice of having
just the comprehension principles on the grounds of simplicity and
naturally. Of course, the situation is more delicate in that on those
grounds, why not have choice like versions of comprehension, as is
used in variants of deductive 2nd order logic?

Harvey Friedman