FOM: Re: SOL confusion

[Martin Davis]

Here we go again.

At 05:03 PM 9/8/00 -0400, Harvey Friedman wrote:
>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.

I used the term "relation symbol" to mean what you call "relation 
variable". This should have been clear from our previous discussion when 
you criticized my speaking of relation symbols as "free variables" not by 
telling me that they were not variables at all, but by telling me that 
their intended range was too large. In any case,  please change in my 
previous messages the term "relation symbol" to "relation variable". The 
crucial point is that these are symbols; as such they range over nothing 
until an interpretation is provided.

> >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.

This is work that has been going on for a century. You may think that it is 
bad work,  but it is certainly not experimental.



> >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.

Of course.

> >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.

I'm not trying to disagree.


> >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.

Yes I am. See below.


> >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.

Note that S is a "relation symbol."

> >
> >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)]

How wicked of me! I've quantified a relation symbol!

> >
> >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 interpretation???" Why is any interpretation needed to understand the 
clear content of these sentences?


>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.

Yes certainly. I gave an hour address to the ASL something like 20 years 
ago in which I made that point. Also on FOM a year or so ago. More recently 
(maybe 5 years ago) I gave a talk to computer science audiences called IN 
DEFENSE OF FIRST ORDER LOGIC in which I explained that very fact (among 
other things).


>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.

This we agree on. I've been saying this over and over.

However I refuse to dismiss work on deductive SOL. The work of Boolos et al 
I've mentioned is quite interesting although the semantics is obscure. 
Likewise the proof theoretic work is difficult and studied by serious logians.

Martin




                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com