Definitions and analytic truth

sowa@watson.ibm.com
Message-id: <9201061639.AA27422@cs.umn.edu>
Reply-To: cg@cs.umn.edu
Date: Mon, 6 Jan 92 11:39:15 EST
From: sowa@watson.ibm.com
To: jmc@cs.stanford.edu, schubert@cs.rochester.edu, macgreg@isi.edu,
        fikes@hpp.stanford.edu, interlingua@isi.edu, krss@isi.edu,
        cg@cs.umn.edu
Subject: Definitions and analytic truth

I would strongly endorse John McCarthy's point:

> All this is rather complicated, so I'm still not sure whether the
> word "definition" is being used in the sense of mathematical logic
> as a sentence that introduces a constant symbol in a conservative
> way.  If not, then you should choose another word instead of
> "definition", because definitions in the sense of mathematical
> logic will surely be required.

There are several distinct notions that should be clearly separated:

 1. The act of introducing a new symbol and specifying its syntactic
    properties, such as the number of arguments in a relation.

 2. The mechanism of lambda abstraction for taking an expression and
    parametrizing one or more of its variables.

 3. "Conservative" definitions that say that symbol X is synonymous
    with some other expression in the language, which may be a lambda
    expression or possibly some other kind of expression.

 4. Metalanguage to specify that proposition p is to be considered
    to have a privileged status, such as an axiom or law.

 5. Metalanguage to specify that proposition p is to have a lower
    status, such as a default or an assumption for hypothetical
    reasoning.

 6. Contexts for grouping propositions into "microtheories" or
    packages for an "object-oriented" style of definition.

Each of these notions could be used separately or in various
combinations.  "Normal" function definition combines #1, #2, and #3.
A primitive is a symbol introduced by #1 and associated with some
axioms by #4.  If each of these notions were available separately,
you could mix and match them to define any convenient functions
you prefer, such as defun, defprimrelation, etc.

Once you introduce metalanguage for saying that one proposition is
a law and another is a default, you need to introduce some semantics
for determining what to do when a conflict (i.e. contradiction) arises
among the laws, facts, and defaults.

My personal preference is to stick with a purely first-order logic
and to treat both modal and nonmonotonic reasoning as belief revision
processes for picking and choosing the "ideal" premises.  There could
be three (or more if you like) levels of "epistemic entrenchment":

 1. Axioms or laws

 2. Facts

 3. Defaults

The question of which propositions are laws, facts, or defaults might
vary from one context to another.  But within any context, you would
try to select a maximally consistent set, giving priority to the laws
over the facts and to the facts over the defaults.  Various systems
of nonmonotonic reasoning may be considered different bookkeeping
mechanisms for doing the picking and choosing.

John Sowa