[Fwd: Re: Revised Axioms for Cardinality Restrictions]

The revised axiom Richard Fikes proposed for the cardinality restriction
succeeded in allowing proofs of a number of expected properties of the
construct.  

While I had proposed introducing a comprehension axiom, which says that
a list (or set) exists that contains all elements that satisfy certain
properties, the new axiom avoids any such requirement.  The axiom is
formulated in terms of NoRepeatLists --- I think it might be slightly
simpler if formulated in terms of sets, but that would require
introducing axioms for sets as well as lists.

The revised theory, like the original one, is agnostic about whether
some lists are infinite or all lists are finite.  

The revised theory also avoids versions of Russell's paradox that
threatened formulations that contained a comprehension axiom.  The new
theory has defeated earnest attempts (5 CPU hours) to find
contradictions. 

The validation of the revised theory was carried out using
theory-manipulation facilities of Specware --- proofs were done by the
theorem prover SNARK, which is embedded in Specware.

The revised axiom says that if restriction r has onProperty p and
cardinality component n, then an element i is in r iff some
NoRepeatsList that contains precisely the values of p on i has length
n.  In Specware notation, this is


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

The earlier axiom said that i is in the restriction r iff
*every* NoRepeatsList that contains precisely the values of p on i has
length n:

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

The chief difference between these is that the earlier axiom says that
every list having the right elements has length n.  The new axiom says
that there exists a list of the right elements with length n. The
earlier axiom left open the possibility that no list exists that has the
right elements.  Since the new axiom implies that there exists a list
with the right elements, there is
no need to prove it.

The validation was carried out on a particular example: we define a
restriction OneFatherClass that is intended to consist of all elements
with precisely one father:

 axiom onproperty-of-onefatherclass-is-hasfather is
  PropertyValue(onProperty,OneFatherClass, hasFather)

 axiom cardinality-of-onefatherclass-is-one is
  PropertyValue(cardinality, OneFatherClass, _1)

The class Person of all people is asserted to be a subclass of this
restriction class:

 axiom restriction-subclass-of-class-Ax55 is
 PropertyValue(subClassOf, Restriction, Class)

This example was obtained from the DAML Walkthru document,
 http://www.daml.org/2001/03/daml+oil-walkthru.html .

We expect to be able to prove the following claims:

If an element has precisely one father, then it is in the
OneFatherClass; i.e.,

 conjecture one-father-in-onefatherclass is
  fa(c : Element, p1 : Element)
   (fa(p : Element)(PropertyValue(hasFather, c, p) <=> p = p1)) =>
    Type(c, OneFatherClass)


Every person has at least one father; i.e.,

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

No person has two distinct fathers; i.e.,

 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

The original axiom did not imply this last property;
with the new axiom Specware/SNARK can prove all of them.

Copies of the theory slice, which contains all the axioms and lemmas
necessary to prove the desired properties, are available on request.

Received on Tuesday, 25 September 2001 20:36:01 UTC