FOM: Re: SOL confusion

[Martin Davis]

At 07:08 PM 9/7/00 -0400, Harvey Friedman wrote:
>Reply to Davis 1:54PM 9/7/00:
>
>My understanding of what SOL ought to mean - I was under the impression
>that it was standard - seems to be at odds with what you write below:
>
> >Now let us consider the assertion: "there are propositions that can be
> >stated in SOL that can not be stated in FOL." This is true and for a
> >trivial reason. Because the sentences of FOL contain symbols for predicates
> >(and/or functions) that have no specific reference, these sentences do not
> >express any propositions. [This statement is for FOL without equality. If,
> >as is often the case, FOL is formulated to include equality, then there are
> >sentences that provide lower bounds on the size of the universe; but that's
> >all.] So of course the quoted assertion is true.
>
>In particular, the sentences of SOL also contain symbols for predicates
>(and/or functions) that have no specific reference.

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? And such sentences can indeed express propositions. 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.)

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

Martin




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