FOM: Re: SOL confusion

[Harvey Friedman]

>The question is: what is a SENTENCE of SOL? And I take this to be one in
>which there are no free variables of either type. Is this not the standard
>usage?

Yes. But constant symbols, relation symbols, and function symbols are not
free variables in FOL, and they are not free variables in SOL.

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.

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

>For example, for
>any theorem A of second order arithmetic the implication P => A, where P is
>the sentence expressing the second order Peano postulates, expresses a true
>proposition. (Technically: the closure of that sentence; there will be a
>free variable whose intended interpretation is the successor relation, and
>the implication would need to be universally quantified with respect to
>that variable.)

Not directly. There is only the associated sentence asserting that the
implication P arrows A is valid.

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