Cardinality Restriction Axioms too Weak

I know there has been a lot of discussion about restrictions, but I
think this is a different wrinkle.  This has to do with several
varieties of cardinality restrictions.  It appears as if these axioms 
are not strong enough to prove simple consequences that anyone would 
expect to be true.  These problems were found in attempting to use 
Kestrel's Specware System, and the embedded SRI theorem prover SNARK, 
to verify some of these consequences.

For example, in the DAML Language Walkthrough 
  http://www.daml.org/2001/03/daml+oil-walkthru.html
the class Person is defined in part as a class of objects having 
precisely one father:

  <rdfs:subClassOf>
    <daml:Restriction daml:cardinality="1">
      <daml:onProperty rdf:resource="#hasFather"/>
    </daml:Restriction>
  </rdfs:subClassOf>

One would expect that it would follow from this that each person has
precisely one father.  In fact, from the axioms in the Axiomatic
Semantics document,
  http://www.daml.org/2001/03/axiomatic-semantics-071601.html 
it does follow that each person has at least one father, but not, it
seems, that a person cannot have two fathers.

The above restriction can be expressed in axioms (in Specware notation)
as

 axiom person-in-fatherclass is
  PropertyValue(subClassOf, Person, FatherClass)

[Every Person is in the FatherClass, where FatherClass is the anonymous
restriction, of objects with precisely one father.]


 axiom onproperty-of-fatherclass-is-hasfather is
  PropertyValue(onProperty, FatherClass, hasFather)

[The onProperty of FatherClass is hasFather.]


 axiom cardinality-of-fatherclass-is-one is
  PropertyValue(cardinality, FatherClass, 1)

[The cardinality of FatherClass is 1.]

Note that the names attached to axioms are only for our
convenience--they have no logical significance.


 From this and the axioms for restrictions we would expect to be able to
prove the following conjecture:

 conjecture people-have-at-most-one-father is
  fa(i : Element, p1 : Element, p2 : Element)
   Type(c, Person) &
   PropertyValue(hasFather, i, p1) &
   PropertyValue(hasFather, i, p2) =>
   p1 = p2

In other words, if a person i has two fathers p1 and p2, then p1 and p2
must be the same. 

By properties of lists, to show that p1 and p2 are the same, it suffices
to show that they are both items on a list of length 1. One way to do
this is to appeal to the definition of cardinality,

 axiom definition-of-cardinality is
  fa(r : Element, p : Element, n : Nat)
   ((PropertyValue(onProperty, r, p) &
     PropertyValue(cardinality, r, n)) =>
    (fa(i : Element)
     (Type(i, r) <=>
      (fa(l : Element)
       ((NoRepeatsList(l) &
         (fa(v : Element)
           (Item(l, v) <=>
            PropertyValue(p, i, v)))) =>
       (length(l) = n))))))

[I am using the predicate symbol Item].  According to this axiom, taking
n to be 1 and p to be hasFather, it suffices to show the existence of a
non-repeating list l whose items are precisely the fathers of i, and
then to show that this list has length 1.

However, and here is the problem, all lists are finite, and it could be
that i has infinitely many fathers.  In that case, there is no list l
whose elements are precisely the fathers of i.  But if there are no such
lists, it follows vacuously that all such lists are of length 1.  Hence
the restriction does not rule out the case that i has infinitely many
fathers.  In other words, as defined by the axiom, FatherClass contains
elements which have either one father or infinitely many fathers.

In practice, we can't use the cardinality axiom to show that there is a
list l of length 1 having the desired property, since there might not be
such a list.

If it is the intention that the entire class of elements is finite, this
is not expressed in the axioms.

A similar problem may be expected to apply to other axioms for
cardinality restrictions in DAML, such as maxCardinality, cardinalityQ, 
and maxCardinalityQ, which also use a non-repeating list which is
supposed to contain all elements having a certain property.  It is
possible that the axioms for minCardinality and minCardinaltyQ escape
the problem, because the non-repeating list there is supposed to contain
only a subset of the elements in question.
 
Another problem is that the definition of NoRepeatsList(l) does not
explicitly state that l must be a list.

%% A NoRepeatsList is a list for which no item occurs more than once.
(<=> (NoRepeatsList ?l)                          [NoRepeatsList axiom 1]
     (or (= ?l nil)
         (exists (?x) (= ?l (listof ?x)))
         (and (not (item (rest ?l) (first ?l)))
              (NoRepeatsList (rest ?l)))))


There could be models in which a nonlist j, whose first is not a
member of its rest and whose rest is equal to j itself, was a
NoRepeatsList---this would not violate the axioms. Perhaps j = bottom
is such an element.  The problem could be fixed by putting in a
condition that l be a list, on the right hand side of the equivalence:


(<=> (NoRepeatsList ?l)               [revised NoRepeatsList axiom 1]
     (or (= ?l nil)
         (exists (?x) (= ?l (listof ?x)))
         (and (Type(?l, List))
              (not (item (rest ?l) (first ?l)))
              (NoRepeatsList (rest ?l)))))



This being said, it may be a relief that the unrevised axioms do imply
that every person has at least one father.  Here is the conjecture:


 conjecture people-have-at-least-one-father is
  fa(c : Element)
   Type(c, Person) =>
   (ex(p : Element) HasFather(c, p))

Here is a proof by SNARK, with my annotations:

(Refutation

The first two axioms are from the definition of FatherClass:
 (Row cardinality-of-fatherclass-is-one.7
      (PropertyValue cardinality FatherClass 1)
      assertion)
 (Row onproperty-of-fatherclass-is-hasfather.8
      (PropertyValue onProperty FatherClass
       hasFather)
      assertion)

This is part of the definition of Person, that it is a subclass of
FatherClass:
 (Row person-in-fatherclass.9
      (SubClassOf Person FatherClass)
      assertion)

Here are some basic axioms for lists and numbers:
 (Row nil-is-no-repeats-list.224
      (NoRepeatsList nil)
      assertion)
 (Row nothing-is-in-nil-Ax140.252
      (not (Item nil ?Element))
      assertion)
 (Row nil-is-a-list-Ax139.253
      (Type nil List)
      assertion)
 (Row zero-not-posnat.263
      (not (= 0 ?Pos-Nat))
      assertion)


In SNARK notation, ?Pos-Nat is a variable of sort Pos-Nat---it ranges
over positive integers.  Variables in assertions have tacit universal
quantification.  Thus, the axiom zero-not-posnat says that zero is not
equal to any positive integer.  

The theorem prover works by negating the theorem and finding a
contradiction.  Hence it assumes that some element is a Person but does
not have a father.  SK56 is taken to be one such element.
 (Row 218
      (not (HasFather #Element-SK56 ?Element))
      ~conclusion)
 (Row 219
      (Type #Element-SK56 Person)
      ~conclusion)


Here is another property of lists, that a list has length 0 if it is
nil.  Note that axioms are in clausal form;  implications P&Q => R are
translated into (or (not P) (not Q) R):

 (Row length-nil.231-247
      (or (not (Type ?Element List))
          (= (length ?Element) 0)
          (not (= ?Element nil)))
      assertion)

This is from the definition of SubClass:
 (Row definition-of-subclassof-Ax32.185-283
      (or (not (SubClassOf ?Element ?Element1))
          (not (Type ?Element2 ?Element))
          (Type ?Element2 ?Element1))
      assertion)

This is a key axiom, from the definition of cardinality of
restrictions;  ?Element stands for the restriction, ?Element1 stands
for its onProperty:

 (Row definition-of-cardinality.70-417
      (or (not (PropertyValue onProperty ?Element
         ?Element1))
      (not (PropertyValue cardinality ?Element ?Nat))
      (not (Type ?Element2 ?Element))
      (not (No-repeats-list ?Element3))
      (PropertyValue item ?Element3
        (#Element-SK9 ?Element3 ?Element1 ?Element2))
      (PropertyValue ?Element1 ?Element2
        (#Element-SK9 ?Element3 ?Element1 ?Element2))
      (= (length ?Element3) ?Nat))
         assertion)
This says that the nonrepeating list of elements that satisfies the
onProperty has length 1.

This axiom lets us translate between formulas in terms of the constant
hasFather and equivalent formulas in terms of the predicate symbol
HasFather:
  (Row hasfather-predicate-definition.11-458
      (or (HasFather ?Element ?Element1)
            (not (PropertyValue hasFather ?Element
         ?Element1)))
      assertion)

Finally the proof begins; we translate the predicate symbol HasFather
into the constant hasFather:
 (Row 470
      (not (PropertyValue hasFather #Element-SK56
     ?Element))
      (negative-hyperresolve 
        hasfather-predicate-definition.11-458 218))

Since Person is a subclass of FatherClass, SK-56 must be in FatherClass:

 (Row 472
      (Type #Element-SK56 FatherClass)
      (hyperresolve definition-of-subclassof-Ax32.185-283
person-in-fatherclass.9 219))

Since we have supposed that SK56 has no father, the list of its fathers
must be nil; but by the cardinality restriction, this means that nil
must have length 1:
 (Row 565
      (= (length nil) 1)
      (rewrite 
       (hyperresolve definition-of-cardinality-Ax113.70-417 472
        onproperty-of-fatherclass-is-hasfather.8
        cardinality-of-fatherclass-is-one.7 
        nil-is-no-repeats-list.224)
       nothing-is-in-nil-Ax140.252 470))

But this contradicts the fact that the length of nil is 0.
 (Row 1226
      false
      (rewrite (paramodulate length-nil.231-247 565)
        nil-is-a-list-Ax139.253
        zero-not-posnat.263 
        code-for-=))
 )


To those who are interested in such things, here are some statistics
from the SNARK proof search:

;
; Run time in seconds excluding printing time:
;      2.9  41%   Resolution
;      0.1   2%   Paramodulation
;      0.1   1%   Factoring
;      1.5  22%   Forward subsumption
;      0.4   6%   Backward subsumption
;      0.5   8%   Forward simplification
;      0.0   1%   Backward simplification
;      0.0   0%   Equality ordering
;      0.2   3%   Sortal reasoning
;      1.2  17%   Other
;      7.0        Total

The problem with the axiom doesn't affect this proof, since even if a
person has infinitely many fathers, he or she still has at least one. 

My idea for fixing this problem involves introducing into the theory
explicit sets, which may be finite or infinite.  Cardinality
restrictions would then be expressed in terms of sets rather than
nonrepeating lists.   But I am interested in hearing reactions before
going ahead with this.  E.g., is this all wrong?  

---Richard W.

Received on Friday, 3 August 2001 18:34:09 UTC