[Top] [All Lists]

Re: [ontac-forum] Re: The world may fundamentally be inexplicable

To: ONTAC-WG General Discussion <ontac-forum@xxxxxxxxxxxxxx>
Cc: guarino@xxxxxxxxxx, CG <cg@xxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Fri, 13 Jan 2006 01:19:36 -0500
Message-id: <43C74678.6050804@xxxxxxxxxxx>
Barry,    (01)

We agree on a number of important points:  the need for clear
distinctions of type/subtype, type/instance, part/whole, and
the use of formal logic for expressing the definitions and
axioms of an ontology.  But there are many issues about how
much to include in the upper levels, how to organize them,
and what version of logic to use.    (02)

JS>> I am trying to keep as much as possible *out* of the core.    (03)

BS> A priori; and drawing conclusions as to what is possible
> on the basis of whose theory of what should be on it?    (04)

Not a priori.  The decisions should be based on fundamental
principles of logic, linguistics, physics, and philosophy
together with considerations of the accumulated wisdom by
the software development community over the past fifty years.    (05)

To keep the ontology as general as possible, I recommend
the following two principles:    (06)

  1. The required core should avoid any commitment that might
     be inconsistent with future scientific discoveries or new
     mathematical, computational, and engineering techniques.    (07)

  2. Detailed methods of analysis and reasoning are the most
     likely to introduce inconsistencies with other detailed
     techniques.  Therefore, they should be kept in optional
     modules that may be used, as needed, for specific problems
     or application areas.    (08)

The recent exchange of notes between Michael Gruninger and
me illustrates the kinds of things that are likely to create
inconsistencies.  Michael wants the Process Specification
Language (PSL) and the associated reasoning method of situation
calculus to be included in the core, but I maintain that it
should not be in the core because it is inconsistent with the
more general pi calculus (and related special cases, which
include Petri nets and UML activity diagrams).    (09)

Although I prefer the pi calculus, I would recommend that my
preference, Michael's preference, and many other versions should
*all* be put in optional modules, *not* in the core.  The reason
for excluding all of them from the core is that any of them could
be a reasonable choice for some problem, but their conjunction
is inconsistent.  Therefore, *none* of them belong in the core.    (010)

Following are some related considerations that we should discuss:    (011)

  1. Adding axioms to a theory makes it more specialized and
     enables more theorems to be proved.  The ability to prove
     more theorems is often useful, but one unfortunate axiom
     can create inconsistencies with entire branches of science.
     The most general upper level would have no axioms at all,
     except perhaps the default, "There exists something."
     More would be useful, but it is always easier to add axioms
     than to delete any that have been in use for some time.
     Therefore, I would suggest, "When in doubt, leave it out."    (012)

  2. For the choice of logic, I recommend the draft ISO standard
     for Common Logic (CL):    (013)

     http://cl.tamu.edu/docs/cl/32N1377T-FCD24707.pdf    (014)

     CL is a very general version of first-order logic, which also
     supports quantification over relations while still preserving
     a first-order model theory (see the document for details).
     It includes the semantics of RDF and OWL as proper subsets, and
     it supports most common versions of FOL, including typed or
     sorted versions, such as Z, conceptual graphs, and many others.    (015)

  3. Although I have been on the committee that developed the CL
     standard and I wrote Appendix B, which maps the CL semantics
     to conceptual graphs, the version of semantics adopted for CL
     was not my first choice.  It was developed by Pat Hayes and
     Chris Menzel, and it's very different from the typed CG semantics
     I had been using for many years.  But after working with the
     CL semantics for some time, I became convinced that both Z and
     something similar to, but more general than my original CG
     semantics could be defined on top of CL.  In Appendix B, I
     defined both a typeless core notation and an extended typed
     version of CGs.  The method used to define typed CGs on top
     of the typeless core could also be used to support Z and many
     other typed or sorted versions of FOL.    (016)

  4. I realize that BFO uses modal logic, and so do the research
     versions of conceptual graphs, which support a rich variety
     of intensional logics for representing natural language
     semantics.  Since those are still research topics, I would
     not suggest that they be included in the CL standard.
     However, it is possible to define a variety of modal and
     intensional logics (in any notation for logic, graphic or
     linear) on top of CL by the methods of the following paper:    (017)

        http://www.jfsowa.com/pubs/laws.htm    (018)

  5. In any case, there are serious questions about how any version
     of modal logic should be incorporated into an ontology.  In
     that laws.htm paper, I adopt a version of Dunn's semantics for
     modal logic, which is formally equivalent to the possible worlds
     semantics of Kripke, Montague, and others, but instead of using
     possible worlds, it partitions the propositions into a set of
     facts and a set of laws, which are a privileged subset of the
     facts.  For any proposition p, (Necessary p) means that p is
     provable from the laws, and (Possible p) means that p is
     consistent with the laws.    (019)

  6. In the KL-ONE predecessor to the modern description logics, there
     was a clear distinction between the T-Box (Terminological component)
     and the A-Box (Assertional component).  In effect, the T-Box used
     an early version of description logics for defining an ontology,
     and the A-Box used the terms (or predicates) defined in the T-Box
     to make assertions.  Many people who talked about description
     logics said that they had a "modal effect", but it was not the
     DLs themselves that introduced modality, but the fact that the
     T-Box had a privileged (or more deeply entrenched) role with
     respect to the A-Box.  In effect, they were using a version of
     Dunn's semantics in which the T-Box specified the laws, and the
     A-Box was required to be consistent with the laws.  Therefore,
     there was an implicit necessity operator in front of every T-Box
     statement.    (020)

  7. I would claim that the distinction between an ontology and any
     application that uses the ontology establishes a distinction of
     the same kind as Dunn's semantics of laws and facts or the KL-ONE
     T-Box and A-Box.  Therefore, every proposition p in an ontology
     has an implicit modal operator (Necessary p) in front of it.
     Adding another operator in the form (Necessary (Necessary p))
     would imply (Necessary p) in all versions of modal logic, and
     it would be exactly equivalent to (Necessary p) in many versions.
     Therefore, I do not believe that there is a need to use explicit
     modal operators in the ontology.  (Although I believe that it
     would be useful to use various modal operators in other areas.)    (021)

There is a lot more to be said about these and other issues, but I'll
stop here for now.    (022)

John Sowa    (023)

Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki: 
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG    (024)
<Prev in Thread] Current Thread [Next in Thread>