W3C home > Mailing lists > Public > semantic-web@w3.org > August 2007

Re: [ontolog-forum] Definition Set 1

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>
Message-ID: <20070808022148.GO7150@tamu.edu>

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 GMT

This archive was generated by hypermail 2.3.1 : Tuesday, 26 March 2013 21:45:17 GMT