FOM: Re: SOL confusion

[Harvey Friedman]

Reply to Davis 12:50PM 9/8/00:

>>Yes. But constant symbols, relation symbols, and function symbols are not
>>free variables in FOL, and they are not free variables in SOL.
>
>"Free variable" is a syntatctic notion. It is a symbol to which a
>quantifier can be applied.

Second order logic does not apply quantifiers to relation symbols. It only
applies quantifiers to relation variables, and these relation variables
range over the relations on the domain.

If SOL where to apply quantifiers to relation symbols, then it would in
effect have quantifiers over arbitrary sets, something that nobody intends.
Of course, such quantification is inherent in asking about validity and
satisfiability.  E.g., you are confusing sentences in SOL - which always
depend on an interpretation, even if that interpretation is only a matter
of a choice of domain - with assertions that sentences in SOL are or are
not valid.

The only natural way that any sentence phi of SOL can be construed as a
proposition about the world is to consider the allied proposition

phi is valid

or the allied  proposition

phi is satisfiable.

Similarly, and exactly analogously, the only natural way that any sentence
phi of FOL can be construed as a proposition about the world is to consider
the allied proposition

phi is valid

or the allied  proposition

phi is satisfiable.

I was expecting that all of this would be apparent from my detailed account
of the standard semantics for SOL that I gave in my last posting. I take it
that you do not adhere to that detailed account?

>This usage is so well established with respect
>to SOL and the theory of types (Frege, Russell - bur Russell used "real"
>and "apparent" for "free" and "bound" respectively), that I can't imagine
>your questioning it.

The relation, constant, and function symbols in SOL are not variables, and
so cannot be quantified over. Nor should they be variables. In SOL, one
does not fix a domain in advance any more than one would in FOL. And you
certainly don't quantify over all domains in SOL any more than you would in
FOL.

>In particular there is now a huge literature, starting
>with Boolos, on rescuing Frege's system. What is studied is Frege's system
>minus his calamitous comprehension principle plus what  these folks call
>Hume's Principle (very roughly: sets in one-one correspondence have the
>same cardinalities).  These folks say they are working in SOL and they are
>working in a system with axioms and rules of inference.

The semantic SOL is obviously robust, noncontentious, clear, well
motivated, etcetera. You are talking about some sort of experimental
deductive SOL, which should be labeled as such.

>When computer
>scientists talk about HOL, they're also talking about a system for drawing
>inferences.

Again, a comparatively experimental form involving deductions, types, or
what have you, that should, and is, labeled as such to distinguish it from
the icon of semantic SOL.

>In addition (as I'm reminded by a posting just in from Walter
>Felscher) there is a long line of work on Gentzen style systems for SOL and
>HOL where the interest is in obtaining cut-free versions. Are you telling
>all of these folks that unless they stick strictly to the semantical
>version you provide, they have no right to use the terms SOL, HOL?

That it should be made very clear from the outset that they are talking
about deductive forms of SOL, HOL, etcetera. The need for clear labeling is
important largely because of the horribly confused things that are
routinely said about SOL versus FOL, and the like.

>Because of completeness, in the case of FOL, one can, for many purposes,
>safely conflate the syntactic proof-theoretic and the semantic
>model-theoretic versions. In the case of SOL, one can't do this, and
>confusion can readily arise. But the way to resolve it is to be clear about
>what one is talking about, not by proposing to banish a mode of discourse
>occurring in a long line of work.

You say,

>But the way to resolve it is to be clear about
>what one is talking about Which is exactly what I said. Glad you agree
>with me.

which is exactly what I said. Glad you agree with me.

>In any case, when I say "free variable" I simply
>mean one not in the scope of a quantifier. Since in an arbitrary formula of
>SOL, in general some predicate letters will be in such scopes and others
>will not, surely I may use some term to distinguish them.

You are failing to distinguish between relation symbols and relation
variables. No relation symbol is a variable.

>This is a matter of terminology.

No.

>The way I would say it is that a sentence
>of FOL containing function, constant, or relation symbols other than
>equality does not express a definite proposition, because by choosing
>different interpretations, different propositions are expressed. However, a
>sentence of SOL (i.e., a formula in which all variables are in the scope of
>quantifiers) has the property that it expresses a unique proposition,
>regardless of interpretations.

This is wrong. And your example below is wrong.

>Here's an example: (Ax,y,z)[S(x,y,z) <=> S(y,x,z)]
>
>If we take the domain to be the natural numbers, and interpret S as the
>relation of sum (i.e., informally, z=x+y), this formula expresses the true
>proposition that addition of natural numbers is commutative. If the domain
>is the quarternions with integer components and S is interpreted as
>multiplication then the formula expresses the false proposition that
>multiplication of integer quaternions is commutative.
>
>Now, in SOL we can form the sentences:
>
>             (ES)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)],  (AS)(Ax,y,z)[S(x,y,z)
><=> S(y,x,z)]
>
>Without specifying an interpretation, each of these expresses a
>proposition, the first true, the second false.

In these cases, the interpretation is just a nonempty domain, since there
are no constant, relation, or function symbols appearing in the sentences.
The first sentence is valid. The second sentence is also satisfiable, but
not valid. The second sentence is true in all domains of cardinality 1 and
false in all domains of cardinality greater than 1.

If you want a domain independent interpretation of a SOL sentence phi, or
an FOL sentence phi for that matter, then you should take

phi is valid.

An interesting, and well studied question is: what statements can be
expressed in the form

phi is valid

where phi is a sentence in SOL, or phi is a sentence in FOL.

And what statements can be expressed in the form

phi is satisfiable

where phi is a sentence in SOL, or phi is a sentence in FOL.

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

I now come to the main point.

If SOL is taken as a deductive calculus, then there are plenty of senses in
which it is entirely reducible to FOL.

However, if SOL is taken in its more robust, unproblematic, semantic sense,
then I know of no sense in which it is reducible to FOL.

This stark difference makes it all the more important to distinguish SOL as
a semantic system, versus SOL as a deductive system.