FOM: Re: SOL confusion
martin at eipye.com
Fri Sep 8 15:50:42 EDT 2000
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
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)
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
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.
Visiting Scholar UC Berkeley
Professor Emeritus, NYU
martin at eipye.com
(Add 1 and get 0)
More information about the FOM