From: pat hayes <phayes@ai.uwf.edu>

Date: Mon, 9 Dec 2002 12:16:31 -0600

Message-Id: <p05111b1eba1a84251763@[10.0.100.86]>

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

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

Date: Mon, 9 Dec 2002 12:16:31 -0600

Message-Id: <p05111b1eba1a84251763@[10.0.100.86]>

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

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

(Sorry this response is so delayed, I only just discovered this thread in my mailbox. But the issue is so important, and the conclusions apparently arrived at so wrong, that it is worth opening this wound up to lance the pus a little. -Pat) > > I think the concept of a difference between a rule and a > statement is a trap. >Like the difference (argued to bits >> on the list from time to time!) between entailment and >> implication. The fact is that you can take >> one logic in which something occurs as an axiom, expressed >> as an entailment, and convert the same data into another >> logic in which there is a general axiom for an implication >> operator, and then the same information originally in an >> axiom is expressed as a a ground fact using implication. > >Yes, this correspondence is generally provided by the >"deduction theorem" which is either provable in a logic >or it is used as the definition for introducing an >implication connective. 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. (That in fact sounds like something to do with reification, if I follow it.) Second, some logical proof systems satisfy the deduction theorem, but by no means all of them. So SOME proof systems allow a certain to-and-fro between implication and entailment, but by no means all of them. 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). 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. >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*. Pat Hayes -- --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32501 (850)291 0667 cell phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes s.pam@ai.uwf.edu for spamReceived on Monday, 9 December 2002 13:17:00 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 20:49:37 UTC
*