[Scl] Re: Report on Common Logic

[John F. Sowa]

Bill,

The issue depends on whether the sequences are part
of the logic or part of the ontology:

 > Well, maybe it's been that I have been away too long,
 > but I do remember the semantics for seq vars being somewhat,
 > but not too, complicated.

I wouldn't say that it's "too complicated", but the current
SCL document is not easy to read, especially by non-
mathematicians (who are our major customers).  If Chris
can find a way to make the SCL document substantially
more palatable, that would be good.

 > Correct me if I'm wrong, but we *use* FOL all the time
 > without having to include the axioms of set theory
 > in every ontology we write with it.

You don't have to include the axioms for anything,
as long as you are willing to take it on faith that
somebody competent has written them carefully and
deposited them in a safe place suitable for future
reference.  But if we are the ones who are proposing
SCL, we are responsible for making sure that all the
definitions and axioms for anything we use are carefully
written and deposited with the appropriate authorities,
such as ISO.

 > Why are we forced to include a theory (ontology) of sequences
 > explicitly when we wish to *use* seqvars.  Is not such a theory
 > of sequences simply part of the background theory of the semantics?

There are two options:

  1. Have a very simple semantics for basic SCL, write or copy
     some axioms for a suitable theory of sequences, and assume
     those axioms as part of the built-in ontology that goes
     with SCL.

  2. Avoid any built-in ontology in pure SCL, and define the
     sequence variables as part of the SCL syntax and semantics
     without assuming the existence of entities of type "Sequence".

The advantage of Option #1 is that sequences become first-class
entities, and sequence variables are no different from any other
kind of variables.  You can quantify over them and do all the
things that languages like Lisp and Prolog do with lists.  The
disadvantage is that you don't have a clean separation of logic
and ontology, since SCL has a built-in ontology of sequences.

The advantage of Option #2 is that sequences are not true
entities that can allow quantification.  Therefore, you don't
have a built-in ontology as part of SCL.  The disadvantage is
that there are two kinds of variables:  ordinary variables and
sequence variables.  Another disadvantage is that if you want
to do list processing, you still have to add axioms for sequences
to the ontology, and then you have ordinary variables that can
represent sequences as first-class entities and sequence variables
represent sequences, but not as first-class entities.

I believe that both options can be defined in a consistent way.
However, I prefer Option #1 for the following reasons:

  1. I do want to do list processing, and I would rather not have
     two different kinds of variables that both represent sequences,
     but not in exactly the same way.

  2. There are a lot of other commonly used things that I don't
     believe any well-dressed kn. rep. language should leave
     home without:  sets, bags, sequences, and integers.
     Z puts all of them into its "workbench", which is nicely
     axiomatized.  I would like to adopt the Z workbench (which
     is already an ISO standard) as a recommended companion
     to be used with SCL for anyone who wants it.

  3. If you have the Z workbench, then you can use true sequences
     as seqvars and do "real" list processing with them.

Pat and Chris have been arguing in favor of Option #2.  I am
willing to be convinced that Option #2 is better, but I need
to hear some good reasons why.

John