FOM: Re: SOL confusion

[Harvey Friedman]

Reply to Davis 3:57PM 9/8/00 (and to Shipman down below where indicated):

>Here we go again.

I started this exchange with you because there has been so many confused
postings about SOL and FOL, and that your postings did a lot to clear up
some of the confusion, but wasn't sharp enough about some points.

> In any case,  please change in my
>previous messages the term "relation symbol" to "relation variable". The
>crucial point is that these are symbols; as such they range over nothing
>until an interpretation is provided.

Good, we agree on that!

>>The semantic SOL is obviously robust, noncontentious, clear, well
>>motivated, etcetera. You are talking about some sort of experimental
>>deductive SOL, which should be labeled as such.
>
>This is work that has been going on for a century. You may think that it is
>bad work,  but it is certainly not experimental.

It is experimental in comparison to semantic SOL, in that because of the
strength of SOL semantics, it is not at all clear what deductive structure
should ultimately be associated with SOL. E.g., should one just have a
comprehension scheme, or should it involve choice? And also the ultimate
goal of the investigations are not so clear. Perhaps you would prefer
characterizations like "open ended". In any case, it is sharply different
in such respsects from semantic SOL.

>> (some things I said)

>Of course.

Good, we agree on that!

>> (some things I said)

>I'm not trying to disagree.

Good, we agree on that!

>> >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) <=> S(y,x,z)]
>
>How wicked of me! I've quantified a relation symbol!
>
>> >
>> >Without specifying an interpretation, each of these expresses a
>> >proposition, the first true, the second false.
>>
>>In these cases, the interpretation is just a nonempty domain, since there
>>are no constant, relation, or function symbols appearing in the sentences.
>
>"The interpretation???" Why is any interpretation needed to understand the
>clear content of these sentences?

There is still a confusion, here. Consider the two sentences of SOL,

(ES)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)]

(AS)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)]

S ranges over ternary relations on what domain? S does not range over
arbitrary ternary relations. That is not a feature of SOL semantics. If the
domain is D, then S ranges over ternary relations on D. Depending on just
what nonempty set D is, we get a true or a false statement.

We can also consider the following two assertions that do not depend on any
choice of domain:

(ES)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)] is valid

(AS)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)] is valid

The first of these assertions is true. The second of these assertions is
false.

(ES)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)] is satisfiable

(AS)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)] is satisfiable

Both of these assertions are true.

To illustrate the power of semantic SOL, there is a sentence phi of SOL
with no constant, relation, or function symbols, such that

phi holds in domain D if and only if D is countably infinite.

And another phi such that

phi holds in domain D if and only if D has cardinality aleph-one.

And another phi such that

phi holds in domain D if and only if D has cardinality a strongly inaccessible.

But no phi such that

phi holds in domain D if and only if D has cardinality a measurable cardinal.

This latter result is provable in ZFC + there exists a measurable cardinal.

However there is a phi in TOL (third order logic) such that

phi holds in domain D if and only if D has cardinality a measurable cardinal.

>>If SOL is taken as a deductive calculus, then there are plenty of senses in
>>which it is entirely reducible to FOL.
>
>Yes certainly. I gave an hour address to the ASL something like 20 years
>ago in which I made that point. Also on FOM a year or so ago. More recently
>(maybe 5 years ago) I gave a talk to computer science audiences called IN
>DEFENSE OF FIRST ORDER LOGIC in which I explained that very fact (among
>other things).

Good, we agree on that!

>>However, if SOL is taken in its more robust, unproblematic, semantic sense,
>>then I know of no sense in which it is reducible to FOL.
>>
>>This stark difference makes it all the more important to distinguish SOL as
>>a semantic system, versus SOL as a deductive system.
>
>This we agree on. I've been saying this over and over.
>
>However I refuse to dismiss work on deductive SOL. The work of Boolos et al
>I've mentioned is quite interesting although the semantics is obscure.
>Likewise the proof theoretic work is difficult and studied by serious logians.

I did not dismiss work on deductive SOL. It must be clearly distinguished
from semantic SOL in order to avoid confusion.

Reply to Shipman 8:06PM 9/8/00:

>Because of SOL's incompleteness, there is no obvious choice for a deductive
>calculus (deductive calculus=algorithm for generating validities, or,
>alternatively, satisfiabilities).

Agreed.

>However, there are some standard deductive
>calculi for SOL, for example the ones given in chapter II of Manzano's book,
>which are sound for standard semantics.  Furthermore, these calculi allow for
>the development of "ordinary mathematics" without the standard
>set-theoretical apparatus, using an interpretation where the first-order
>variables are integers, the unary relations are sets of integers, etc.  (The
>development can proceed further either by coding, as in Simpson's "Subsystems
>of Second-Order Arithmetic", or by introducing higher types, since we know
>the validities of HOL are recursively equivalent to the validities of SOL.)

There cannot be a development of ordinary mathematics within SOL, which is
sound for standard semantics, unless that development uses proper SOL
axioms. This is precisely the same situation as with FOL, which also cannot
formalize mathematics without proper FOL axioms.

One can obviously do this, even with the introduction of no constant,
relation, or function symbols. One can write down SOL statements asserting
that there exists relations giving what amounts to the first omega + omega
levels of the cumulative hierarchy, or what amounts to the first omega
levels of the cumulative hierarchy over a natural number system. This is
straightforward. And with the standard comprehension axiom scheme for
deductive SOL, one gets a deductive system that is more or less equivalent
to Zermelo set theory, or Zermelo set theory with natural numbers as
urelements. But so what? One has essentially lifted the usual set theoretic
foundations into another equivalent notation.

On the other hand, no matter what set of SOL statements you take as axioms
in whatever deductive SOL you are considering, one can consider the purely
semantic question of just what are the semantic SOL consequences of those
SOL statements. I.e., just what SOL statements are true in all SOL
interpretations of the SOL statements. You typically wind up with
intersting but answers that are uninformative about mathematical reasoning.

>Questions: Is there a canonical "most complete" deductive calculus for SOL
>other than the "ZFC-calculus"

Obviously there is not any "most complete" deductive calculus for SOL.

ZFC is not a deductive calculus for SOL. I don't know what you are talking
about.

"generate proofs in ZFC that sentences of SOL
>are second-order-validities in the standard semantics"?

Obviously, there are plenty of sentences phi of SOL such that

phi is SOL valid

is provable in ZFC but not in any standard deductive calculus for SOL.

>I expect that none of the standard calculi for SOL generate any validities
>not generated by the ZFC-calculus.

Obviously.

>So it appears that FOL+ZFC is "stronger" than SOL with respect to any of its
>usual calculi.

Of course.

>But is this greater strength too high up to matter in
>ordinary mathematics?

Any arithmetic sentence provable in ZFC but not in 2nd order arithmetic
corresponds to an SOL validity that is provable in ZFC but not in any
standard deductive SOL. In fact, the same can be said of any Pi-1-infinity
sentence.

Maybe somebody will claim a standard deductive SOL that corresponds to
Zermelo set theory. In that case, any arithmetic, or even Pi-1-infinity
sentence provable in ZFC but not in Zermelo set theory corresponds to an
SOL valdity that is provable in ZFC but not in such a deductive SOL.