From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>

Date: Tue, 10 Dec 2002 20:27:21 +0100

Message-ID: <AA2E843B3FC96349BF60350202650BE925737E@tmex1.tm.tue.nl>

To: "'pat hayes'" <phayes@ai.uwf.edu>

Cc: "'Tim Berners-Lee'" <timbl@w3.org>, Sandro Hawke <sandro@w3.org>, www-rdf-rules@w3.org

Date: Tue, 10 Dec 2002 20:27:21 +0100

Message-ID: <AA2E843B3FC96349BF60350202650BE925737E@tmex1.tm.tue.nl>

To: "'pat hayes'" <phayes@ai.uwf.edu>

Cc: "'Tim Berners-Lee'" <timbl@w3.org>, Sandro Hawke <sandro@w3.org>, www-rdf-rules@w3.org

> That is highly misleading. First, the deduction theorem doesn't > provide what Tim said, a correspondence between an axiom and a GROUND > fact using implication. Right (I overlooked the GROUND), but it provides a correspondence between what Tim said, "an axiom, expressed as an entailment" and an implication: A |- B iff |- A->B > Second, some logical proof systems > satisfy the deduction theorem, but by no means all of them. If they don't, they don't have a genuine implication (but only a faked one). In fact, this relationship between genuine implication and entailment shows that implication is the most sophisticated connective: it captures/reflects entailment in the object language! > The deduction theorem only > applies to forward inference natural-deduction style systems, in > general. Machine-oriented inference systems like resolution do not > satisfy it, for example (in spades). I can't follow you here: since it is a theorem relating an entailment relation with an implication connective, how would it depend on proof stratgies (like forward versus backward inference)? > And to simply *confuse* > implication with entailment is just a common beginners mistake, and > is not sanctioned, even by the deduction theorem. Proofs are not > sentences, for example, in any system. I think noone has claimed that. > >Notice that in a constructive > >logic approach (e.g., in intuitionistic logic) implication > >is defined on the basis of entailment and not as "material > >implication" by means of disjunction and negation. > > Again, that is a highly oversimplified and misleading statement. > First, being a statement as opposed to a rule is one thing; being > material implication is something else. Intuitionist implication is > not material implication, but it is a connective in a language, not a > rule of inference; it can be negated, for example. And it is not > "defined on the basis of entailment", but rather in terms of a > certain kind of proof or proof method: that is the heart of > intuitionism as a philosophy of mathematics, in fact: a rejection of > semantic notions like entailment in favor of the notion of > constructive *proof*. That's exactly what constitutes entailment in intuistionistic logic (notice that, i general, entailment may be both a model-theoretic and a proof-theoretic notion). -GerdReceived on Tuesday, 10 December 2002 14:28:42 UTC

*
This archive was generated by hypermail 2.4.0
: Friday, 17 January 2020 22:46:14 UTC
*