- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 3 Apr 2001 12:39:41 -0700
- To: Dan Connolly <connolly@w3.org>
- Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, kenb@ccs.neu.edu, www-rdf-logic@w3.org
>pat hayes wrote: > > > > >Ken may have pointed out a problem with the KIF axiomatization for > > >DAML+OIL. > > > > Yes. The issue of finite models is a delicate one for KIF itself, in > > fact. If KIF is taken to be a strict first-order language then there > > is no way to guarantee, on semantic grounds, that all lists are > > finite. > >Would you please elaborate on that? Chris Menzel and I are writing this up now. Draft available in a few days. >Are you just saying that the earlier KIF specs goofed, >or are you saying that there's no way, in first order logic, >to specify the set of finite lists? The latter. There is no way to specify finiteness in first-order logic. To be precise: there is first-order sentence which has the property that it is true only of finite objects in every first-order interpretation. That is a famous theorem about first-order logic. (In fact it follows from the completeness theorem.) KIF (3.0) comes very close to goofing, but doest quite step over the edge. It says that every interpretation must contain all finite lists (sequences), but it doesnt say that lists are *restricted* to being only the finite ones. People often assume that they must all be finite, and write recursive axioms which only work when they are finite, and of course they never actually get into any trouble, since all the lists anyone actually builds are finite; but the axioms don't in fact say what people often think they are saying. (To see the kind of thing that could go wrong, imagine building a circular list which would set the recursions going for ever, and think of it as a finite encoding of an infinite list. That infinite list satisfies all the first-order list axioms, so it is in some interpretation somewhere; so if the axiomatisations were adequate they should be able to handle them. But the axioms are written with one class of models in mind, even though they don't in fact capture that class. That is what might be called an ontological bug.) >It sounds very much like a claim you made earlier >that induction (over, say, natural numbers) isn't >first order. Yes, they are closely related. There is no way to write a complete arithmetic in first order logic either. You can write useful arithmetics in first order logic, but they all have 'nonstandard' models which cannot be ruled out by any first-order axiomatization, and some of those 'nonstandard' interpretations have things like omega-plus-one in them, ie transfinite ordinals which can violate induction. If we could state induction as intended, we could rule those out. But they can't be ruled out in first order (theorem). Ergo, induction isn't first-order. The same goes for first-order set theories, by the way. (I owe you a reply to an earlier message which I havnt had time to finish yet and will send soon, which goes into this in more detail.) >I've been researching that claim for a while, and >I found some pretty persuasive evidence to the >contrary; it was pointed out to me that > > (a) natural induction is a theorem in set theory > (b) set theory has been axiomatized, finitely, > in first order logic >so > (c) natural induction has been axiomatized, > finitely, in first order logic. The problem is that the sets that are in the first-order universes of the first-order set theories aren't all the sets there are, so when those thoeries say 'for all sets S....;', they are in fact only quantifying over some sets (the ones they are able to describe). In other words, there are 'nonstandard' models of first-order set theory as well. Note, this doesnt mean these theories are wrong, exactly, just kind of under-powered. They still pose an hell of a challenge for theorem-provers, though: >I haven't found the whole argument written up in >detail, but as to the interesting bit, (b): >[[[ >Computer Assisted Proofs in Set Theory > >Belinfante's interest in computer assisted theorem proving has mainly >concentrated on obtaining proofs of theorems in set theory using the >first-order logic resolution-style theorem prover Otter, a powerful >automated reasoning program developed by William McCune at >Argonne National Laboratories. > >Robert Boyer's idea of using Kurt Gödel's finite axiomatization of set >theory is the basis for all Otter proofs of theorems in set theory. Art >Quaife in his remarkable PhD thesis showed how to reduce the >plethora of Skolem functions that had plagued earlier work, and listed >several hundred theorems in set theory that he proved. > >Belinfante explored the use of Otter for more advanced topics in set >theory, including theorems about certain standard functions in set >theory, cross products, ordinal number theory, equipollence, the >theory of finite sets, partial ordering, transitive closure, and so on. >]]] Yes, this is very good work (though see the smartly critical review at http://www.maths.utas.edu.au/People/dfs/QuaifeReview.html). But it is proving theorems in set theory, not doing higher-order reasoning. In fact OTTER is really a very basic (but wonderfully fast) first-order resolution engine, and wouldnt be able to handle KIF as it stands (eg it couldnt deal with sequence quantifiers). It grinds through some amazingly large search spaces to prove some very simple things, if you check it out. Pat Hayes --------------------------------------------------------------------- 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 Tuesday, 3 April 2001 15:38:12 UTC