Revised Axioms for Cardinality Restrictions

 
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.