Re: Revised Axioms for Cardinality Restrictions

> >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.

Can't we require the second argument of relation NoRepeatsList to be a
finite (non-negative) integer and still remain in FOL?  That is, is it
within FOL to have a relation "Finite-Integer"?  That is what I had in
mind regarding both the second argument of NoRepeatsList and the
relation in the existence axiom that I called "Integer".

Richard

Received on Thursday, 13 September 2001 14:16:16 UTC