FOM: Re: SOL confusion
Martin Davis
martin at eipye.com
Thu Sep 7 16:54:18 EDT 2000
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
More information about the FOM
mailing list