- From: Pat Hayes <phayes@ai.uwf.edu>
- Date: Thu, 13 Sep 2001 16:23:10 -0500
- To: Richard Fikes <fikes@KSL.Stanford.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? Well, yes and no. Yes, you can simply stipulate that Integer is true of finite integers as a semantic assumption, outside of the axioms themselves, and work on that basis; and everything else is then in FOL, and you only draw FOL-valid conclusions from that. The problem being, of course, that this stipulation will have consequences that are invisible to a formal FOL reasoner working with the axioms. What you can't do is write a collection of first-order axioms which guarantee that Integer is true only of finite integers. (If you could, then you could axiomatize arithmetic, and Goedel's ghost would never give you any peace.) So you can't both claim that you are working in a purely first-order axiomatic framework, and also claim (or legitimately assume) that (Integer ?x) really says that ?x is finite. > That is, is it >within FOL to have a relation "Finite-Integer"? To have, in a sense, but not to have a complete axiomatization of. (Shouldn't be too surprising; after all, we often write predicates like (Is-Human ?x) without thinking that this is guaranteed to really mean 'is human' in *all* models, right? Someone once said that the integers are the work of God and all the rest is the work of Man, and I think this is what he meant; contrary to what pre-Goedelian optimists thought, the integers are more like a piece of the real world than most mathematical categories; they are too complicated to be fully captured in any set of axioms we can write down. A group is anything that satisfies the axioms of group theory, a set anything that satisfies the axioms of set theory, etc.. But the integers we just have to take on faith.) > 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". Yep, I thought you did. That's what Genesereth had in mind when he defined List in KIF as well. :-) Which, to repeat, is fine, as long as you don't claim to have axiomatized (exactly) what you have in mind. Pat PS. BTW, heres why you get stuck, in a nutshell. Suppose you could axiomatize Integer somehow so that it was true of exactly the finite integers, and consider the infinite disjunction (or (= ?x 0) (= ?x 1)(= ?x 2).......) This also is true just of the finite integers, considered as a predicate on ?x, so the following: (iff (Integer ?x) (or (= ?x 0) (= ?x 1)(= ?x 2).......)) must be true in all models. But you are never going to be able to write this in any version of FOL. One way round is fine: (implies (or (= ?x 0) (= ?x 1)(= ?x 2).......) (Integer ?x)) turns into an infinite conjunction: (and (implies (= ?x 0)(Integer ?x)) (implies (= ?x 1)(Integer ?x)) (implies (= ?x 2)(Integer ?x)) .......) which is really just an infinite collection of regular FOL axioms (implies (= ?x 0)(Integer ?x)) (implies (= ?x 1)(Integer ?x)) (implies (= ?x 2)(Integer ?x)) ..... which is fine, and could be captured by a schema defined in terms of numerals: (implies (= ?x [n])(Integer ?x)) which one could do pretty directly in KIF. But its the other way round that is impossible, since that is (implies (Integer ?x)(or (= ?x 0) (= ?x 1)(= ?x 2).......)) which just can't be said in any first-order way. (If you try to use a schema-like trick you get a skolemization problem since (exists ([n])... is inside (forall (?x)...), and how are you going to axiomatize the resulting function from finite integers to numerals?) But you would need to be able to say this, or something equivalent to it, in order to have a complete theory of finiteness. As things stand, you can say only a finite subset of it, which always leaves some wiggle room to allow one of the unmentioned numerals to denote some transfinite ordinal and still satisfy your axioms. (Note, this isn't a *proof* that arithmetic can't be described in FOL, but it helped me see what is going on.) -- --------------------------------------------------------------------- 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 17:23:35 UTC