From: Drew McDermott <drew.mcdermott@yale.edu>

Date: Thu, 4 Dec 2003 11:55:01 -0500 (EST)

Message-Id: <200312041655.hB4Gt1u11552@pantheon-po04.its.yale.edu>

To: www-rdf-rules@w3.org

Date: Thu, 4 Dec 2003 11:55:01 -0500 (EST)

Message-Id: <200312041655.hB4Gt1u11552@pantheon-po04.its.yale.edu>

To: www-rdf-rules@w3.org

[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 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:53:11 GMT
*