[SCL] Re: Formal_Semantics of SCL & Z

John F. Sowa sowa at bestweb.net
Thu Jan 1 12:05:35 CST 2004


Jon,

Those are two very good questions:

JA> If what we really mean by "formal semantics for X" is something like
> the assumption of LOS -- for now let's leave a bit wobbly the latitude
> of saying axiomatic LOS or naive LOS -- as a universal target language
> in the category-theoretic sense, along with the provision of a mapping
> f : X -> LOS, then why not just cut to the chase and work in LOS itself?

First of all, set theory isn't actually a "language".  It is a
particular kind of mathematical structure, which many people
have found to be useful for constructing models of other
kinds of structures.  It is by no means the only such structure.
Mereology, category theory, arithmetic, and Euclidean geometry
are also widely used mathematical structures used to model
other structures.  Many of those systems can be and have been
used to state truth conditions on various formal languages.

Peirce, Tarski, and their followers chose to use sets of individuals
and relations as convenient structures for stating truth conditions
on formalized languages.  For the CL/SCL standard, the simplest
and quickest approach and the one that requires the least amount
of explanation and justification is to follow their lead and adopt
the techniques they have developed and used quite effectively.

That doesn't mean that the other approaches should be ignored.
In fact, I personally prefer mereology + the integers, but
it would require more work and more explanation to use them.
It would not make any improvements to the CL/SCL standard,
but it would require more work to relate the CL/SCL M-T
to the M-T of other systems that use a Tarski-style approach.

JA> Since there are evidently so many "universal languages in principal",
> what further considerations of a practical nature would induce us
> to select one of them over all others?

First-order logic probably has the strongest claim to be
the most "natural" of all universal languages.  However,
there are variations in what FOL actually means.  Those
variations primarily consist in kinds of restrictions
on the range of quantifiers.  For the SCL model theory,
we have deliberately chosen the least restrictive approach
we are able to define (or to find in anyone else's versions).

That enables the less restricted model theory of SCL to include
the model theories of more restricted languages (such as Z,
which has a very strong typing system) as well as much less
restricted languages, such as untyped predicate calculus
or untyped OWL and RDF.

That last paragraph explains why we believe that SCL is
better suited to being an interchange language among
different dialects of FOL than a more restricted
language such as Z:

  1. It is possible to translate a wide range of both
     restrictive and unrestrictive versions of FOL into
     SCL while preserving the same truth conditions.

  2. However, very few versions of FOL have a type theory
     that is as restrictive as Z.  Therefore, the number
     of FOL languages that can be translated into Z is
     very small.  (In fact, I am not aware of *any* other
     commonly used version of FOL that can be translated
     to Z -- primarily because of Z's highly restrictive
     type system.)

John



More information about the SCL mailing list