FOM: SOL confusion

[Harvey Friedman]

Reply to Roger Jones 11:38AM 9/7/00:

>1. The word "semantics" does not appear in the phrase for which SOL is an
>acronym.

The failure to explicitly distinguish SOL as a semantic system (the usual)
and as a deductive system (less usual) causes the confusion. Its role as a
semantic system is well motivated as a powerful language for expressing
statements where one is not committed to a particular framework like the
cumulative hierarchy or the ring of integers, or the like. Any associated
deductive structure is more problematic and its importance is less clear.
In contrast, the deductive structure normally associated with FOL is of
crucial importance for f.o.m. and has a lot of vital robustness properties,
etcetera.

>2. The acronyms FOL and HOL have established usage in computer science
>referring respectively to first order and w-order logic, not specifically to
>the semantics of these logics.

The constructions originated long before computer science. Yet the
distinctions I am drawing are important to make in any computer science
context as well.

>4. Your usage does not seem to be well established, since at least half a
>dozen people have been engaged in a discussion in which its use has been
>broader without anyone raising objection until now.

Many people I know who understand these issues perfectly well would be very
wary of discussing SOL versus FOL in a forum such as this because so many
people are confused about their relationship, and past experience shows
that no amount of discussion will help clear up the confusions.

>"SOL is not a deductive system" or "SOL does not encompass a deductive
>system" would do the trick.

I am happy with this way of stating it if you prefer it.

>> Comparing SOL and FOL is inappropriate since they have virtually no common
>> purposes.

>Whether you think it appropriate or not, comparing SOL and FOL is what we
>have been doing recently in some of the threads on fom.

These threads appear to me to be based on confusions.

>The point has been made that it is possible to express in SOL propositions
>which cannot be expressed in FOL (under its usual semantics).

When expressed entirely in terms of the usual semantics, this has been
realized, at least in some form, for over 100 years. The machinery to
demonstrably refute is more recent, perhaps 70 years ago.

But the confusion enters in when semantics is confused with deduction. For
example, one might really mean

"it is possible to formalize some mathematics using SOL that you can't
formalize using FOL."

This is either trivially true, trivially false, or meaningless. It
certainly has no readily apparent interesting interpretation.

>Though I am surprised that this point should cause much debate, I am under
>the impression that it has not yet been conceded by all parties.

Not all parties are making the proper distinctions in order to be assured
that they are talking about remotely the same thing.

>Though I am curious as to whether you consider this comparison
>"appropriate", I am much more interested to know whether you think it true.

I think I have given an informative answer.