Definition Set 1

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.

'''Logic'''

| There are a number of ways of approaching the issues,
| but for purposes here a *logic* can be thought of as
| a (typically rather large and inclusive) family of
| formal languages together with a semantic theory
| for those languages.

'''Semantic Theory'''

| A *semantic theory* for a class of languages is simply
| a systematic method of assigning semantic values to
| the members of the various syntactic categories of
| those languages.

'''Interpretation'''

| An application of a semantic theory to a particular language yields
| an *interpretation* of the language, i.e., an assignment of appropriate
| semantic values to the basic lexical items of the language.  Appropriate
| semantic values are then assigned by the theory to complex syntactic
| constructions of the language -- notably, truth and falsity to sentences --
| recursively in terms of the semantic values of their component parts.

'''First Order Logic'''

| 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.)
|
| '''Source.'''  Chris Menzel,  "Current Semantic Web Layer Cake"
| http://ontolog.cim3.net/forum/ontolog-forum/2007-08/msg00182.html

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
¢iare: http://www.centiare.com/Directory:Jon_Awbrey
getwiki: http://www.getwiki.net/-UserTalk:Jon_Awbrey
zhongwen wp: http://zh.wikipedia.org/wiki/User:Jon_Awbrey
http://www.altheim.com/ceryle/wiki/Wiki.jsp?page=JonAwbrey
wp review: http://wikipediareview.com/index.php?showuser=398
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Received on Tuesday, 7 August 2007 20:44:33 UTC