- From: Richard Fikes <fikes@KSL.Stanford.EDU>
- Date: Thu, 13 Sep 2001 11:16:08 -0700
- To: Pat Hayes <phayes@ai.uwf.edu>
- CC: waldinger@AI.SRI.COM, "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>

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