- From: Chris Menzel <cmenzel@tamu.edu>
- Date: Tue, 7 Aug 2007 21:21:48 -0500
- To: "[ontolog-forum] " <ontolog-forum@ontolog.cim3.net>
- Cc: SemWeb <semantic-web@w3.org>
On Tue, Aug 07, 2007 at 04:44:06PM -0400, Jon Awbrey wrote: > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o > > Chris Menzel has supplied our discussion with a very helpful set of > definitions for many of the words that we've been bandying about, and > I think that it would serve our aims to extract these handy files from > their embeddings in that many-layered cake currently on the table. > These are of course not the only ways of defining these terms, but the > conceptions marked in them are very widely used, if not predominantly, > and so it will be handy to have them in one place for future > reference. I thank Jon for his surgery on my post. I take very mild exception only to his introduction of several sets of quotation marks into the discussion of first order logic. Thus, I'd prefer to return that paragraph to its original state: What makes a logic *first-order* is a fairly technical matter, but it consists essentially in the possession of two semantic properties, compactness and the downward Löwenheim-Skolem property. These properties are critically connected to the fact that FOL is *complete*, that is, that it is possible to *axiomatize* logical consequence, i.e., the fundamental logical relation that holds between a set S of sentences and a given sentence A when any interpretation that makes all the members of S true also makes A true. It is (among other things) completeness that makes FOL so important to automated reasoning, as it means that, whenever A is a logical consequence of S in a first-order logic, there is actually a *proof* of A from some (finite) subset of S. (Alas, finding that proof is another kettle of fish entirely, which is why we have more constrained, less expressive logics like description logics and their ilk.) Jon had put double quotes around 'S' and 'A' above. However, in the discussion, they are serving as metavariables, ranging over sets and formulas, respectively. Hence, as I was using them, they should not be quoted. A minor point, admittedly, but picky, I mean "picky", is my middle name. :-) -chris ps: Re compactness and the downward L-S property, for those who might be interested: Say that a set S of sentences of a logic is *satisfiable* if there is *model* of S, that is, an interpretation of the language of the logic in which all the members of S are true, and that S is *unsatisfiable* if it is not satisfiable. Compactness says, roughly, that unsatisfiability is in a certain sense a finite property; more exactly, compactness says that if a set S of sentences is unsatisfiable, then some finite subset of S is as well. From the compactness of FOL follows the very interesting fact that FOL is incapable of expressing the concept of finitude. The downward L-S property says, roughly, that it is not possible to force all of the models of any set of sentences to be larger than the set N of natural numbers; more exactly, a logic has the downward L-S property if, whenever, a set of sentences has an infinite model of any size, it also has a model the size of N. This property gives rise to what is usually called Skolem's Paradox. It is a theorem of, say, Zermelo-Fraenkel set theory that there are more sets than there are natural numbers. Nonetheless, because FOL has the downward L-S property, there is a model M of ZF set theory in which there are, in fact, only as many sets as there are natural numbers. But since M is a model of ZF, the theorem "There are more sets than there are natural numbers" is true in M -- despite the fact that there are only as many sets in M as there are natural numbers! (The "paradox" here is actually quite easy to explain, but it seems pretty mysterious when first encountered.) The characterization of first-order logic in terms of compactness and the downward L-S property is known as Lindström's Theorem.
Received on Wednesday, 8 August 2007 02:26:28 UTC