[Scl] Re: Report on Common Logic

[pat hayes]

>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.

Pat is working on that right now, in his (maniacal laughter) spare time.

>
>>  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.

One needs to have faith in the semantics, not in axioms. The core of 
SCL is the model theory.

>  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.

Well, actually, you don't need to hear that, as far as this group is 
concerned. What is NEEDED is for us as a group to reach a decision, 
which I believe we did at the meeting in January at Santa Fe, where 
this issue was discussed at some length. If we continually revisit 
old decisions because one person did not like the decision, we will 
never make progress. I do not have time to re-visit the arguments 
against what you call option 1 in detail, but they can be briefly 
summarized by the observation that since there is not, and cannot 
possibly be, any finite axiomatization in any compact and complete 
logic of the notion of a finite sequence, that option is simply 
incoherent as stated.  The secondary argument is that the seq vars in 
fact add virtually no extra complexity to the syntax and none 
whatsoever to the semantics. (I agree that the style of Chris' 
document is forbidding, but this has no bearing on the point at 
issue.) The point you make about wanting to have lists in an ontology 
is a nice one, but I believe that if you take the responsibility 
seriously of providing a semantics for those lists you will discover 
that your axioms are inadequate to the task. Simply going through the 
motions of recursive definitions in a first-order framework does not 
get lists axiomatized. Chris and I have gone into the matter in some 
detail, and shown that a subset of Lw1w is required. If you would 
want to propose that we adopt infinitary logic as an ISO standard 
then I suggest you start another group :-)

Pat

>John
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes