FOM: Re: SOL confusion

[Martin Davis]

At 11:38 AM 9/7/00 +0100, Roger Bishop Jones wrote:
>In response to: Harvey Friedman Thursday, September 07, 2000 3:32 AM
>
>
> > SOL is a semantic system, not a deductive system. It is an interesting
> > semantic system for some purposes, and is a lot weaker than set theory in
> > its role as a semantic system. Both SOL and set theory can be made into
> > deductive systems, the latter being much stronger and far more suitable
>for
> > the formalization of mathematics.
>
>Thankyou for this clarification of your use of the term SOL, which greatly
>helps in understanding your previous message.

I want to inject some history. In fact, second order logic made its first 
appearance precisely as a deductive system. For example, in 
Hilbert-Ackermann's influential textbook of 1928 and in Church' textbook. 
The key rule of inference was a complicated substitution rule for predicate 
symbols that tended to be stated incorrectly. Henkin introduced (in his 
dissertation 1949) what came to be called Henkin semantics with respect to 
which these rules were complete. Later Henkin published a paper in the JSL 
"Banishing the Rule of Substitution" in which he proved that the 
substitution rule is equivalent to a simple comprehension scheme. It 
followed readily (though he didn't make that connection explicit) that his 
completeness theorem was an easy consequence of Goedel's completeness 
theorem for FOL.

Here's an example of how these things were seen circa 1950. In my 
dissertation I proved the (embarrassingly weak) theorem that what came to 
be called the hyperarithmetic sets are definable in second order arithmetic 
(that is they are analytic). When Church, my advisor read the manuscript, 
he objected that second order definability was not a well-defined notion 
and insisted that I add explicitly the semantic rules.

This history is why it can be confusing to speak of SOL without specifying 
whether one has in mind this traditional textbook system or (what only came 
to be discussed considerably later) full blown SOL semantics.

First order logic was also introduced as a system of axioms and rules of 
inference, extracted in Hilbert-Ackermann from the systems of Frege and 
Whitehead-Russell. It had also been studied semantically, but in a very 
different spirit deriving from the tradition of Boole and Schroeder. The 
question of the equivalence of the syntactic with the semantic formulations 
was made explicit in this same book of Hilbert-Ackermann and, famously, 
Goedel proved this equivalence in his dissertation.

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.

Martin



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