new version of CL

The most recent version of CL has a patch to handle "Horrocks" sentences.  So
both Chris and I were right, just talking about different formalisms.

Here is my short description of my view of how this works in CL.

The basic idea is that there is subset of the universe of reference (which in
FOL would be called the domain of discourse) which is called the universe of
discourse.  Quantification works only over this subset.  Names used as
arguments must map into the universe of discourse.  The syntax can say that
certain names must map outside the universe of discourse.

So, you can define the FOL fragment of CL as follows:

    Predicate, function, and object names are pairwise disjoint.
    Predicate names can only appear as predicates.
    Function names can only appear as functions.
    Object names can only appear as arguments.
    Predicate and function names denote outside the universe of discourse.

Note that object names that get used must denote inside the universe of
discourse.

This means that
     (forall x forall y x=y)
does not have any impact on predicates.

Why?  Quantification only quantifies over elements of the universe of
discourse, and the denotation of predicate names are not in this set.

Therefore

     (forall x forall y x=y) implies (P(a) iff P(b))

is not a theorem of the new CL.  (It was a theorem of the old CL.)

[From here on in there is much less relevance to RIF.]

There is an interesting consequence of the changes.  To determine the
theorems of CL formulae, you may(?) need to know which names have this special
property of not denoting in the universe of discourse.

I believe that there is an error in the 1 December draft, however.  I do not
believe that restricting attention to flat interpretations (where both
universes are the same) for unsegregated dialects (dialects with none of these
non-discourse denoting names) is appropriate.  To see this, consider that in a
flat interpretation Horrocks sentences are true (because predicate names denote
elements of the universe of discourse).  However, this is not necessarily the
case in non-flat interpretations.


Peter F. Patel-Schneider

Received on Friday, 9 December 2005 01:07:34 UTC