Re: plain rules, please [was: Semantic Web Rule Language (SWRL) 0.5 released]

   [Graham Klyne]
   My question about the distinction between "deduction" and other forms of 
   inference was posed to help me better understand the points you have been 
   making about the utility of non-deductive inferences.

    From your response, I think that "deduction" is the process of finding a 
   proof in some theory.  Thus, "deductions" (deduced results) are precisely 
   those that are proven to be true in some (accepted) proof theory.  

Instead of "proof theory," it would be better to say "logical theory,"
that is, a set of axioms and inference rules.  Generally speaking,
the inference rules remain constant across a broad range of logical
theories, so that the term "logical theory" usually applies to a set of
axioms, with some inference machinery being postulated up front.  In the
case of first-order logical theories, there are many candidates for
the basic machinery, and they all do the same thing, so one often
doesn't bother mentioning the inference rules or logical axioms (i.e.,
domain-independent axioms of pure logic, such as p->(q->p)).

   (And, 
   maybe, for a proof theory to be acceptable, it must be sound with respect 
   to some accepted model theory.)

I would rather say, "It must be sound with respect to its agreed-upon
formal semantics," but for some reason the phrase "model theory of X"
has come to mean "formal semantics of X."

   On this basis, I understand the further points you are making to be that 
   there may be useful results (inferences) that cannot be proven.  Which, I 
   guess, takes us into issues of how dependable one needs results to be in 
   order for them to be useful.

   Am I following your key points?

Yes.

   (This leaves me wondering if it is not generally possible to turn any 
   non-deduction into a deduction by strengthening the accompanying proof 
   theory.  Picking an example from another thread here:  based on a given 
   knowledge of airports, I might usefully infer, via NAF, that the closest to 
   my current location is LHR, because I don't know of a closer one (and 
   there's a general presumption that I know about airports close to my 
   current location).  This is not a provable deduction, but maybe it is made 
   so by adding to the proof theory concerned an axiom to the effect that a 
   given list of airports is complete.)

The problem is that there is a trivial way to turn an inference of P
into a deduction: add P as an axiom.  So you have to be careful in
what you allow as an axiom.

Perhaps a better strategy is to stay away from particular statements
that we want to be theorems, and just look for logical theories with
lots of useful conclusions that are very rarely wrong.  The question
then is how many domains there are in which such theories exist.
Putting it this way makes it a matter of degree instead of a
theological schism; fans and nonfans of deduction must be prepared to
win some and lose some.

                                             -- Drew

-- 
                                             -- Drew McDermott
                                                Yale University CS Dept.

Received on Thursday, 4 December 2003 11:55:02 UTC