Re: Universal Quantification - common misconception

Hi Bijan,

Thanks for the explanation, it was very helpful. My confusion really stemmed
from the wording in the primer. I could see for myself that the restriction
could be satisfied by a person who has no children, but could not understand
what formal semantics were actually being described or how they could be
used to make such an inference.

I recommend rephrasing that text in the next version of the primer along
similar lines to the  explanation in your reply. My confusion was no doubt
in part due to my lack of experience with formal logics or semantics and
perhaps the intended audience would be a little more informed, but for what
it's worth...

Cheers,
Niall.

On 23 March 2011 09:56, Bijan Parsia <bparsia@cs.man.ac.uk> wrote:

> On 22 Mar 2011, at 11:18, Niall Murphy wrote:
>
> > Hello,
> >
> > I am confused by the statement in the OWL 2 Primer that "any individual
> that is not a “starting point” of the property hasChild is class member of
> any class defined by universal quantification over hasChild.",
>
> That's clumsily put.
>
> Rephrase: In order for *ALL* your children to be happy, it suffices that
> you have NO children at all.
>
> This is sometimes known as "vacuously satisfying the restriction".
>
> > referring to this statement.
> >
> > EquivalentClasses(
> >     :HappyPerson
> >     ObjectAllValuesFrom( :hasChild :HappyPerson )
> > )
>
> The way to see this is to consider the following class:
>
> EquivalentClasses(
>        :ChildlessHappyPerson
>        ObjectAllValuesFrom(:hasChild owl:Nothing)
> )
>
> It follows that ChildlessHappyPerson SubClassOf: HappyPerson.
>
> > My understanding (or attempt thereof) is that the any individual that is
> not not a "starting point" of the property hasChild can be expressed as
> follows:
> >
> > EquivalentClasses(
> >     :NotStartingPointOfHasChild
> >     ObjectComplementOf(
> >         :ObjectSomeValuesFrom(:hasChild :Person)
> >      )
> > )
>
> Nope. At least, not by itself. You could still have children that are not
> persons. (Assuming the right additional axioms are in play, that might
> suffice).
>
> > And the class of individuals defined by universal quantification over
> hasChild as follows:
>
> There are potentially many such classes.
>
> > EquivalentClasses(
> >     :UniversalQualificationOverHasChild
> >     ObjectAllValuesFrom(:hasChild QualoverHasChild)
> > )
>
> Bit garbled there. I think my example is clearer.
>
> > So because NotStartingPointOfHasChild has no individuals who are members
> of :UniversalQualificationOverHasChild,
>
> Er...if things came out as in my example, it SHOULD have members who are
> UniversalQualificationOverHasChild. That's the point.
>
> > or to put it another way, all none of them are related to
> UniversalQualificationOverHasChild by hasChild,
>
> This is off the rails. We're not talking about the successors.
>
> > they all meet the restriction and are therefore members.
> >
> > If the above is true, does the solution of including an
> ObjectSomeValuesFrom(:hasChild :HappyPerson) restriction in the example
> class expression prevent entailment of a paradox, or have I just been
> spending too long looking at OWL semantics?
>
> Nothing at all to do with paradox! The main reason for this somewhat
> curious condition is to ensure certain closure conditions for negation.
> I.e., that negated existentials always have a corresponding universal.
>
> If you define (P only C) as not(P some not C) (in the standard way, it's
> clear that you can fit the second expression either by having ALL your Ps be
> Cs or by having no Ps at all.
>
> Hope this helps.
>
> Cheers,
> Bijan.