FOM: Re: SOL confusion

[Harvey Friedman]

Reply to Davis 1:54PM 9/7/00:

>I want to inject some history. In fact, second order logic made its first
>appearance precisely as a deductive system. For example, in
>Hilbert-Ackermann's influential textbook of 1928 and in Church' textbook.
>The key rule of inference was a complicated substitution rule for predicate
>symbols that tended to be stated incorrectly. Henkin introduced (in his
>dissertation 1949) what came to be called Henkin semantics with respect to
>which these rules were complete. Later Henkin published a paper in the JSL
>"Banishing the Rule of Substitution" in which he proved that the
>substitution rule is equivalent to a simple comprehension scheme. It
>followed readily (though he didn't make that connection explicit) that his
>completeness theorem was an easy consequence of Goedel's completeness
>theorem for FOL.

This seems to me to be a case where the move to thinking of SOL as a
semantic system - unless a deductive system is specifically referred to -
may differ from original usage, mainly as a result of trying to clarify
confusion, and fixing on the most productive aspect of SOL. I maintain that
this is the most common usage in the mathematical logic community taken as
a whole.

E.g., from what you wrote above:

>The key rule of inference was a complicated substitution rule for predicate
>symbols that tended to be stated incorrectly.

My understanding of what SOL ought to mean - I was under the impression
that it was standard - seems to be at odds with what you write below:

>Now let us consider the assertion: "there are propositions that can be
>stated in SOL that can not be stated in FOL." This is true and for a
>trivial reason. Because the sentences of FOL contain symbols for predicates
>(and/or functions) that have no specific reference, these sentences do not
>express any propositions. [This statement is for FOL without equality. If,
>as is often the case, FOL is formulated to include equality, then there are
>sentences that provide lower bounds on the size of the universe; but that's
>all.] So of course the quoted assertion is true.

In particular, the sentences of SOL also contain symbols for predicates
(and/or functions) that have no specific reference.

Therefore, I am going to state explicity what I think SOL is.

SOL and FOL both use equality, and infinitely many constant, relation, and
function symbols. In both systems, these remain uninterpreted until one
specifies a relational structure, which in both cases, consists of a
nonempty domain (set), an interpretation of the constant symbols as
elements from the domain, interpretation of the relation symbols as
relations on the domain, and interpretation of the function symbols as
functions on the domain. All relations and functions are of arbitrary arity
>= 1.

FOL uses connectives, equality between domain elements, variables over
domain elements, and quantifiers over domain elements.

SOL uses connectives, equality between domain elements, variables over
domain elements, quantifiers over domain elements, variables over relations
on the domain, and quantifiers over relations on the domain. In the case of
variables over relations on the domain, there is a separate infinite list
of variables for each arity of relations considered.

It is now obvious how to define, following Tarski (who did it for FOL), the
notion of a relational structure satisfying an FOL formula at an assignment
of domain elements to domain variables. And also, the notion of a
relational structure satisfying an SOL formula at an assignment of domain
elements to domain variables, and an assignment of relations to relation
variables (respecting arity).

Then the notions of validity and satisfiability are defined as usual.

This modern setup is by no means due to me, and I believe I have seen it
spelled out like this in a number of places.

With this (I thought) totally standard setup in mind, I repeat the answer I
gave to Roger Jones in my previous posting:

There is a sentence in second order logic with only equality whose models
are exactly the domains that are finite. There is no sentence in first
order logic with only equality whose models are exactly the domains that
are finite.