From: Richard Waldinger <waldinge@kestrel.edu>

Date: Wed, 12 Sep 2001 18:25:27 -0700

Message-ID: <3BA00B07.76251B20@kestrel.edu>

To: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>

Date: Wed, 12 Sep 2001 18:25:27 -0700

Message-ID: <3BA00B07.76251B20@kestrel.edu>

To: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>

In an earlier message I mentioned a weakness in the axioms for some of the DAML cardinality restrictions, in http://www.daml.org/2001/03/axiomatic-semantics-071601.html , that made it impossible to prove some expected properties, including some claimed in the DAML Walkthru document http://www.daml.org/2001/03/daml+oil-walkthru.html . In this message, I introduce axioms that suffice to establish the desired properties. The Problem: Cardinality restrictions, a central component of DAML+OIL, are intended to make it possible to define objects by restricting the number of certain entities they possess; for instance, a bicycle has two wheels. More precisely, a cardinality restriction r is intended to be the class of all elements i such that there are exactly n elements v such that p(i,v), where p is the "onProperty" of the restriction and n is its "cardinality component". Thus a cardinality restriction is a definition of form r = {i : Element | card{v : Element | p(i,v) = n}} Here Element is a general sort of elements and card is the cardinality of a set. For instance, in the Walkthru, a restriction, which we will call OneFatherClass, is defined to have onProperty hasFather and cardinality component 1. In DAML, this is written <rdfs:subClassOf> <daml:Restriction daml:cardinality="1"> <daml:onProperty rdf:resource="#hasFather"/> </daml:Restriction> </rdfs:subClassOf> . The intention here is that OneFatherClass (an anonymous class in DAML) is the class of all elements i that have exactly one father. In other words, OneFatherClass = {i : Element | card{v : Element | HasFather(i,v)} = 1} . One would expect, then, that if i is an element of OneFatherClass, then i does have precisely one father. The document asserts that Person, the class of all people, is a subclass of OneFatherClass, from which we might reasonably be expected to conclude that each person has precisely one father. Although it is intuitively evident that this is so, repeated efforts to reproduce the intuitive proof from the DAML axioms with an automated theorem prover failed. The Original Cardinality Restriction Axiom: The axiom in the current axiomatic semantics document that defines cardinality restrictions is, in KIF notation, (=> (and (PropertyValue onProperty ?r ?p) [cardinality axiom 3] (PropertyValue cardinality ?r ?n)) (forall (?i) (<=> (Type ?i ?r) (forall (?vl) (=> (and (NoRepeatsList ?vl) (forall (?v) (<=> (PropertyValue item ?vl ?v) (PropertyValue ?p ?i ?v)))) (= (length ?vl) ?n)))))) In other words, if r is a cardinality restriction with onProperty p and cardinality component n, then an element i is of type r if and only if, for any nonrepeating list v1 that contains precisely the elements v such that p(i, v), the length of v1 is n. The axiom makes use of the DAML convention that PropertyValue(p, i, v) means p(i, v). The problem is that there is nothing in the axioms that implies the existence of such a list v1. In particular, the axioms are agnostic about whether lists are finite or infinite. A possible model of the DAML axioms is one in which all lists are finite. Suppose, then, such a model includes a planet in which some creature i0 has an infinite number of fathers. In that case, there is no list v1 of all the elements v that are fathers of i0. Hence, vacuously, the length of any such list is 1 (and anything else). Hence, by the axiom, i0 is in the OneFatherClass. But, contrary to our expectations, i0 does not have precisely one father---it has infinitely many fathers. To show that a set of axioms does not imply a conclusion, it suffices to find a single model under which all the axioms are true but the conclusion is false. Under the exobiological model we have described, all the axioms are true, but some element of OneFatherClass does not have a unique father. Consequently, it is impossible from the axioms to conclude that elements of OneFatherClass have precisely one father. And merely knowing that Person is a subclass of OneFatherClass is not enough to allow us to conclude the people have precisely one father. Similar weaknesses infect the axioms for other DAML cardinality restrictions, such as maxCardinality and cardinalityQ. Lists versus Sets: The axiom that is missing is a "comprehension" axiom, which says that a list exists consisting of precisely those elements that satisfy certain conditions. Introducing a comprehension axiom forces us to admit the existence of infinite lists. It is possible introduce a comprehension axiom for lists, but conventional lists are finite. Also lists are ordered and allow multiple copies of the same element--features that are unnecessary for axiomatizing the cardinality restriction. All these considerations suggest using sets instead of lists in the axiomatization. Infinite sets are commonly accepted, and the order and multiplicity of elements in a set are irrelevant. The axiomatization presented below includes a simple subclass of set theory that is just strong enough for the purpose. All the reasoning required has been carried out using Kestrel's Specware system, which includes the automatic theorem provers SNARK (from SRI) and Gandalf (from Goteborg). Proofs are fast (seconds, not minutes). Although I have not proved that the theory is consistent, neither SNARK nor Gandalf was able to find a contradiction in a reasonable amount of time. The axioms have been formulated to avoid Russell's paradox, and an earnest effort to obtain the paradox from the axioms failed. The Revised Axioms: In the axioms for sets, Element is the class of elements. Set is the class of sets. empty is the empty set. Insert(x, s) is the result of inserting an element x into a set s. Choice(s) is some element of a nonempty set s. (Choice is a true function but the axioms do not always allow us to determine its value.) Others(s) is the set of elements of a nonempty set s other than Choice(s). Member(x, s) holds if x is an element of the set s. The basic axioms for sets used in proving the desired properties are, in Specware Notation: axiom empty-is-a-set is Type(empty, Set) axiom decomposition-of-set is fa(s : Element) Type(s, Set) => s = empty or (Type(Others(s), Set) & ~(Member(Choice(s), Others(s))) & s = Insert(Choice(s), Others(s))) axiom not-member-empty is fa(x : Element) ~(Member(x, empty)) axiom member-insertion is fa(x : Element, y: Element, s : Element) Type(s, Set) => (Member(x, Insert(y, s)) => (x = y or Member(x, s))) axiom member-insertion-self is fa(x : Element, s : Element) Type(s, Set) => Member(x, Insert(x, s)) We assume a theory of nonnegative integers of sort NatInf, that includes infinite integers. Nat is the subsort of NatInf that is intended to include only the finite integers. (Although finiteness cannot be expressed in first-order logic, but we can state the properties we need.) We can then introduce a cardinality function card, from sets into NatInf, by the following axioms: axiom card-zero is fa(s : Element) Type(s, Set) => (card(s) = 0 => s = empty) axiom card-empty is card(empty) = 0 axiom card-insertion is fa(s : Element, x : Element) (Type(s, Set) & ~(Member(x, s))) => card(Insert(x, s)) = 1 + card(s) Our early efforts in this direction led to a version of Russell's paradox, because of the existence of a DAML class Thing, which had the property that each element is a Thing. To avoid paradox, we introduce a subclass SmallClass, where Thing is not asserted to be a SmallClass. Most ordinary classes are SmallClasses. axiom smallclass-is-class is Type(SmallClass, Class) axiom smallclasses-are-classes is PropertyValue(subClassOf, SmallClass, Class) We now introduce the comprehension axiom. If p is a two-place predicate symbol, the range of p is c, c is a SmallClass, and i is an element, the axiom defines a set setofall(p, i,c) to stand for the set of all elements v of type c that satisfy the condition p(i, v) or, more precisely, PropertyValue(p, i, v). We require that the range of p be a SmallClass. For example, if c is a SmallClass, p is the hasFather predicate, the range of hasFather is c, and i is an Element, then setofall(p, i, c) is the set of all elements v of type c such that i has v as a father. Here is the axiom that defines setofall(p, i, c): axiom definition-of-setofall is fa(p : Element, i: Element, c: Element) Type(c, SmallClass) & PropertyValue(range, p, c) => (Type(setofall(p, i, c), Set) & (fa(v : Element) Member(v, setofall(p, i, c)) <=> Type(v, c) & PropertyValue(p, i, v))) Note that, because the axiom defines setofall(p, i, c), it implicitly asserts that such a set exists. If Element is an infinite class, setofall(p,i,c) can be forced to be infinite (e.g., take c to be any SmallClass and p to be a predicate with range c and infinite domain that is always true) We can now use setofall to formulate a revised axiom for the cardinality restriction: axiom definition-of-cardinality-revised is fa(r : Element, p : Element, n : NatInf, c : Element) ((PropertyValue(onProperty, r, p) & PropertyValue(cardinality, r, n) & PropertyValue(range, p, c) & Type(c, SmallClass)) => (fa(i : Element) (Type(i, r) <=> card(setofall(p, i, c)) = n))) In other words, roughly speaking, if a restriction r has onProperty p and cardinality component n, then if i is an element satisfying restriction r, the cardinality of the set of all v such that p(i, v) is n. For example, suppose a restriction OneFatherClass is defined to have onProperty hasFather and cardinality 1. The range of hasFather is asserted to be a SmallClass, say Fathers. Then, if i is an element of type OneFatherClass, the cardinality of all elements v that are fathers of i is 1. From this axiom, and the assertion that Person is a subclass of OneFatherClass, we can prove: People have at least one father: conjecture people-have-at-least-one-father is fa(c : Element) Type(c, Person) => (ex(p : Element) PropertyValue(hasFather, c, p)) People have at most one father: conjecture people-have-at-most-one-father is fa(c : Element, p1 : Element, p2 : Element) Type(c, Person) & PropertyValue(hasFather, c, p1) & PropertyValue(hasFather, c, p2) => p1 = p2 Although the first of these conjectures can be proven from the original axioms, the second, it seems, cannot. I have given all the axioms for sets needed to axiomatize the cardinality restrictions and prove the expected properties. Copies of the full theory slice, or the proofs, are available on request.Received on Wednesday, 12 September 2001 21:26:32 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:36 UTC
*