Re: 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
>
>>  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.
>
>Comments welcome.
>
>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