Reputation: 6338
I am half way reading the OWL2 primer and is having problem understanding the universal quantification
The example given is
EquivalentClasses(
:HappyPerson
ObjectAllValuesFrom( :hasChild :HappyPerson )
)
It says somebody is a happy person exactly if all their children are happy persons. But what if John Doe has no children can he be an instance of HappyPerson? What about his parent?
I also find this part very confusing, it says:
Hence, by our above statement, every childless person would be qualified as happy.
but wouldn't it violate the ObjectAllValuesFrom() constructor?
Upvotes: 4
Views: 1090
Reputation: 69
I am facing the same kind of issue while reading the "OWL 2 Web Ontology Language Primer (Second Edition - 2012)" and I am not convinced that the answer by Sharky clarifies the issue.
At page 15, when introducing the universal quantifier ∀, the book states: "Another property restriction, called universal quantification is used to describe a class of individuals for which all related individuals must be instances of a given class. We can use the following statement to indicate that somebody is a happy person exactly if all their children are happy persons." [I omit the OWL statements in the different sintaxes, they can be found in the book.] I think that a more formal and may be less ambiguos representation of what the author states is
(1) HappyPerson = {x | ∀y (x HasChild y → y ∈ HappyPerson)}
I hope every reader understands this notation, because I find the notation used in the answer less clear (or may be I am just not accustomed to it).
The book proceeds: "... There is one particular misconception concerning the universal role restriction. As an example, consider the above happiness axiom. The intuitive reading suggests that in order to be happy, a person must have at least one happy child [my note: actually the definition states that every children should be happy, not just at least one, in order for his/her parents to be happy. This appears to be a lapsus of the author]. Yet, this is not the case: any individual that is not a “starting point” of the property hasChild is a class member of any class defined by universal quantification over hasChild. Hence, by our above statement, every childless person would be qualified as happy . ..." That is, the author states that (assume '~' for logical NOT), given
(2) ChildessPerson = { x | ~∃y( x HasChild y)}
then (1) and the meaning of ∀ imply
(3) ChildessPerson ⊂ HappyPerson
This does not seem true to me. If it were true then every child, as far as s/he is a childless person, is happy and so only some parents can be unhappy persons.
Consider this model:
Persons = {a,b,c}, HasChild = {(a,b)}, HappyPerson={a,b}
and c is unhappy (independently from the close world or open world assumption). It is a possible model, which falsifies the thesis of the author.
Upvotes: -1
Reputation:
I think the primer actually does quite a good job at explaining this, particularly the following:
Natural language indicators for the usage of universal quantification are words like “only,” “exclusively,” or “nothing but.”
To simplify this a bit further, consider the expression you've given:
HappyPerson ≡ ∀ hasChild . HappyPerson
This says that a HappyPerson
is someone who only has children who are also HappyPerson
(are also happy). Logically, this actually says nothing about the existence of instances of happy children. It simply serves as a universal constraint on any children that may exist (note that this includes any instances of HappyPerson
that don't have any children).
Compare this to the existential quantifier, exists (∃):
HappyPerson ≡ ∃ hasChild . HappyPerson
This says that a HappyPerson
is someone who has at least one child that is also a HappyPerson
. In constrast to (∀), this expression actually implies the existence of a happy child for every instance of a HappyPerson
.
The answer, albeit initially unintuitive, lies in the interpretation/semantics of the ObjectAllValuesFrom
OWL construct in first-order logic (actually, Description Logic). Fundamentally, the ObjectAllValuesFrom
construct relates to the logical universal quantifier (∀), and the ObjectSomeValuesFrom
construct relates to the logical existential quantifier (∃).
Upvotes: 7