- From: Dan Connolly <connolly@w3.org>
- Date: Sat, 14 Apr 2001 08:29:30 -0500
- To: Miles Sabin <MSabin@interx.com>
- CC: www-rdf-logic@w3.org
Miles Sabin wrote:
>
> Ken Baclawski wrote,
> > We suggest that this axiom be changed to:
> >
> > Ax8. (<=> (Type ?fp FunctionalProperty)
> > (and (Type ?fp Property)
> > (forall (?s ?v1 ?v2)
> > (=> (and (PropertyValue ?fp ?s ?v1)
> > (PropertyValue ?fp ?s ?v2))
> > (= ?v1 ?v2)))))
>
> Unless I'm missing something this is equivalent to the original.
> All of s, v1, and v2 are free in the LHS of the conjunction and
> in the LHS of the biconditional, so the forall can be pushed to
> the outermost scope. Then it can be dropped altogether because
> KIF treats free variables in quantifier free sentences as
> implicitly universally quantified.
That universal quantifiers can be pushed out is true
as a rule of thumb, but it doesn't always apply in the "if" part
of a conditional. That is:
(=> (=> (in ?x ?set) (inOrder ?y ?x))
(min ?set ?y))
is very different from
(= (forall (?x)
(=> (in ?x ?set) (inOrder ?y ?x)) )
(min ?set ?y))
> Can you give a sketch of the generated proof that all properties
> are functional and the role that this axiom plays in it?
Given the original formulation of the axiom...
(<=> (Type ?fp FunctionalProperty)
(and (Type ?fp Property)
(=> (and (PropertyValue ?fp ?s ?v1)
(PropertyValue ?fp ?s ?v2))
(= ?v1 ?v2))))
Take any old property... say... rdf:type
and any of its subject/object pairs... say
Adam and Person. Then we have
(Type rdf:type Property)
of course and we have
(= Person Person)
and
(and (PropertyValue rdf:type Adam Person)
(PropertyValue rdf:type Adam Person))
now we can conclude
(=> (and (PropertyValue rdf:type Adam Person)
(PropertyValue rdf:type Adam Person))
(= Person Person))
from which we can conclude
(Type rdf:type FunctionalProperty)
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Saturday, 14 April 2001 09:29:34 UTC