FOM: Re: SOL confusion

[Martin Davis]

At 10:05 PM 9/7/00 -0400, Harvey Friedman wrote:

>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. 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. 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. When computer 
scientists talk about HOL, they're also talking about a system for drawing 
inferences. 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?

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 can't even view them as free variables in SOL since if they were, then
>such free variables would range over all unary predicates defined on the
>entire universe whose extension is setlike. This is not in consonance with
>the spirit of SOL. If you want instead such free variables to range over
>all unary predicates defined on the entire universe, you have something
>with paradoxical overtones that is again not in consonance with the spririt
>of SOL.

I find this comment very strange. The standard semantics for FOL and SOL of 
which you have reminded us in your posting, begins with an *arbitrary set*, 
the domain of the interpretation. Why does this not have the same 
"paradoxical overtones"? 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.


> >And such sentences can indeed express propositions.
>
>No more and no less than sentences in FOL can express propositions. Of
>course, any sentence in FOL has an associated proposition - that it is
>valid. Similarly, any sentence in SOL has an associated proposition- that
>it is valid.

This is a matter of terminology. 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.

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.

> >>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.
>
> >This is often said, but I don't believe that it is true. The notion is at
> >least implicit in earlier work of Skolem and in Hilbert-Bernays. The
> >attribution to Tarski is, I believe, based on his famous paper on the
> >concept of truth in formal languages. But you'll find nothing about FOL in
> >that paper. What Tarski did do in that paper was to emphasize that one
> >should take seriously and formally the semantics of formal languages.
>
>The phrase "Tarski's truth definition" is so ingrained in the math logic
>literature and the philosophy literature that I find it hard to believe
>there isn't a good clean reference to the formal definition attributed to
>Tarski in some of Tarski's papers. Are you trying to tell us that there
>isn't?

To the best of my knowledge: yes that is what I'm saying. (By the way, 
please note my correction: I typed "Hilbert-Bernays" when I meant 
"Hilbert-Ackermann".) I'm no expert on Tarski's work, but I have discussed 
this with others, and I believe that what I said is true. If someone 
disagrees, I'd be grateful for a reference.

Tarski's famous paper THE CONCEPT OF TRUTH IN FORMALIZED LANGUAGES 
(reprinted in his collection LOGIC, SEMANTICS, METAMATHEMATICS) chooses as 
the specific language for which he gives a truth definition, what he calls 
"the calculus of classes." The importance of this paper is well-known, but 
you will not find in it a "good clean reference to the formal definition" 
of the semantics of FOL. What is there, is the idea that the semantics of a 
language should be provided by a recursion on the manner in which the 
expressions of the  language are built up; but applying this to FOL is not 
at all in the spirit of that paper. On the other side, consider that when 
Hilbert-Ackermann (1928) posed the problem of completeness of FOL, the 
problem would not even have made sense without the notion of validity being 
understood on some level, although no recursive definition was provided. 
(They define interpretation as we do today, but say that a formula is VALID 
[German: "identisch"] if making the substitutions of an interpretation in 
the formula, a true proposition ["richtige Aussage"] will always result.

Martin




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