# Re: Revised Axioms for Cardinality Restrictions

From: Pat Hayes <phayes@ai.uwf.edu>
Date: Thu, 13 Sep 2001 12:19:20 -0500
Message-Id: <p05101001b7c68674fe7c@[205.160.76.190]>
To: Richard Fikes <fikes@KSL.Stanford.EDU>

```>  > 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
>
>>  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.
>
>As discussed earlier, the cardinality axioms that use NoRepeatsList do
>not require or assume that lists can be infinite in length.  So, that is
>not an issue.

No, it is an issue. The axioms cannot *prevent* lists being infinite
in length; but if lists are infinite, then the axioms don't do their
intended job. So the axioms do not fully capture the intended
meanings.

>I agree with your observation that the cardinality axioms are flawed in
>that there is nothing in the axioms that entails the existence of a
>NoRepeatsList containing any given finite set of values of a given
>property for a given object.  However, I think there is a much simpler
>fix than introducing a set theory.  That is, I think we can modify the
>axioms so that the existence of a NoRepeatsList containing any given
>finite number of objects is assured.  Attached below is a
>straightforward way of doing that.
>
>
>Richard
>
>--------------------------
>Add a second argument to relation NoRepeatsList that is the length of
>the list.  Then, the axiom defining NoRepeatsList becomes the following:
>
>(<=> (NoRepeatsList ?l ?n)
>      (or (and (= ?n 0) (= ?l nil))
>          (and (= ?n 1) (exists (?x) (= ?l (listof ?x))))
>          (and (not (item (rest ?l) (first ?l)))
>               (NoRepeatsList (rest ?l) (- ?n 1))))) 	[NoRepeatsList
>axiom 1]
>
>Add an axiom stating that NoRepeatsLists exist for any finite collection
>of objects as follows:
>
>(=> (and (Integer ?n)
>          (>= ?n 0)
>          (NoRepeatsList ?l1 ?n)
>          (not (item ?l1 ?x)))
>     (exists (?l2) (and (NoRepeatsList ?l2 (+ ?n 1)) (item ?l2 ?x))))

This seems to assume that (Integer ?n) is true of only finite
objects, though, which begs the question. There is no way to
axiomatize this in FOL which guarantees that all things satisfying
this (or any other) predicate are finite in all models. For example,
suppose that there are infinite lists, say with lengths w+1, w+2,
etc., where w is the first transfinite ordinal, and also that w is an
integer, ie (Integer ?n) is true when '?n' denotes w, w+1, etc.. Then
both your axioms are satisfied, and any first-order version of the
induction axiom for arithmetic can be be satisfied also. (This
follows from the compactness theorem for FOL.) The only way to rule
out models like this is to go beyond first-order logic, eg by using
infinitary logic, as KIF does (implicitly) in the parts that you have
decided, wisely, not to use in your axioms.

Or, you could just say that your axioms aren't actually in FOL at
all, but are in KIF, which is a subset of Lw1w. Then they would have
content that wouldn't be fully captured by a first-order reasoner
like SNARK, so you could just soar above the fray. We are doing
semantics here, after all :-)

Pat

--
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes
```
Received on Thursday, 13 September 2001 13:19:25 UTC

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