FW: firts and rdf:rest as functional property

[Originally private discussion between Chris Mungall and me, but Chris
agreed to forward this to the list. Chris' original mail is quoted.]


Hi, Chris!

Thanks for this interesting example! See below for my answer.

>-----Original Message-----
>From: Chris Mungall [mailto:cjm@berkeleybop.org]
>Sent: Friday, March 20, 2009 7:37 PM
>To: Michael Schneider
>Subject: Re: firts and rdf:rest as functional property
>
>
>On Mar 20, 2009, at 10:43 AM, Pat Hayes wrote:
>
>>>>>
>>>>> (2) Lists should not be cyclic, though this is possible with RDF
>>>>> lists:
>>>>>
>>>>>     A -> B
>>>>>     ^    |
>>>>>     |    v
>>>>>     D <- C
>>>
>>> Try to express such a general cycle prohibition axiom! This would
>>> roughly
>>> need to say something like:
>>>
>>> For any non-negative integer n:
>>>   there must not be nodes x1,...,xn
>>>   such that
>>>      x1 rdf:rest x2
>>>      x2 rdf:rest x3
>>>      ...
>>>      xn rdf:rest x1
>>>
>>> If the cycle size would be restricted, one could express this by a
>>> finite
>>> set of axioms (I'm not necessarily talking about OWL here). But the
>>> cycles
>>> may be arbitrarily large, so this is not possible.
>
>possibly missing something, 
>but would this not work (OWL Full issues
>not withstanding, just taking 'rest' as a standard object property)?
>
>SubPropertyOf(rest,restT)
>Transitive(restT)
>SubClassOf(HasSelf(restT),owl:Nothing)
>
>I thought the main point of HasSelf was to to express simple cyclic
>structures, e.g. carbon rings

Ok, in principle, this does the job, however...

Here is, how I would prove this.

Claim: Any ontology that is consistent with these axioms does not have
"rest" cycles.

Assume the contrary:

There exist individuals x1 ... xn such that        (***) 

  x1 rest x2 rest ... rest xn rest x1 .

Since rest is a sub property of restT, we also have

  x1 restT x2 restT ... restT xn restT x1 . 

Via transitivity of restT, we have

  x1 restT x1

Hence, HasSelf(restT) is non-empty. Contradiction to the third axiom! Q.E.D.

But what have I done? Look at "(***)" above! There is an existential
assumption about /n/ variables, with non-fixed "n", which means there are in
fact n existence quantors. This is not a "normal" first order logic proof.
Instead, one can see this proof in different ways:

(1) As in fact infinitely many different proofs, one for each fixed natural
number n.

(2) The proof can be seen as saying: "There exists a finite set X =
{x1,...,xn} of variables...", which means that the existential quantor
refers to a set --> Second Order Logic!  

(3) Alternatively, one can see it to be a single quantor refering to a
variable of type "finite sequence" <x1,...,xn>. --> Sort of extended First
Order Logic with arbitrary length tuple-variables.

Dealing with infinitely many proofs (1) is a bit "inconvenient", to say the
least :). And I think, regarding this as an application of full Second Order
Logic (2) would be too much, because we only deal with finite enumeration
sets here. So seeing the proof under the third view is my favorite. I think
this is what Pat talks about in his earlier mail (I had once a look at
Common Logic, and found this "sequences as variables" idea there, I
believe).

Now, after all, it isn't classical first order logic. So something must be
"wrong" here, because this cannot be expected to be working with at least
OWL 2 DL. My first guess was that some of the "global restrictions" of OWL 2
DL are hurt by this example. And, indeed, that's the case:

Look at 

 
<http://www.w3.org/2007/OWL/wiki/Syntax#Global_Restrictions_on_Axioms_in_OWL
_2_DL>

(That's the current Editor's Draft of the "OWL 2 Structural Specification",
soon to be published as a 2nd Last Call Working Draft).

You can see in Section 11.2, in the paragraph "Restriction on Simple Roles",
that the constructor "ObjectHasSelf" is listed there. This means that a
HasSelf restriction may only be applied to so called "simple properties".
And when you read Section 11.1 (not easy!!!), then you will find out that a
/transitive/ property is NOT a simple property. So the (non-obvious!) error
is: You have defined restT to be transitive AND have used it in a HasSelf
expression. Puh! :)

Interestingly, your axioms are valid OWL 2 Full, because the global
restrictions do not hold for OWL 2 Full. Interesting for me to see that one
falls out of FOL by doing this.

Cheers,
Michael

--
Dipl.-Inform. Michael Schneider
Research Scientist, Dept. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: michael.schneider@fzi.de
WWW  : http://www.fzi.de/michael.schneider
=======================================================================
FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts, Az 14-0563.1, RP Karlsruhe
Vorstand: Prof. Dr.-Ing. Rüdiger Dillmann, Dipl. Wi.-Ing. Michael Flor,
Prof. Dr. Dr. h.c. Wolffried Stucky, Prof. Dr. Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus
=======================================================================