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

Date: Tue, 10 Dec 2002 14:55:01 -0600

Message-Id: <p05111b4aba1c02876fc3@[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: Tue, 10 Dec 2002 14:55:01 -0600

Message-Id: <p05111b4aba1c02876fc3@[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

> > 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). No. It is to do with the ways that different systems treat provability. Simple logical proof systems have rules to infer sentences from other sentences; they will typically satisfy the deduction theorem. A proof in such a system is simply a list of sentences each derived from some previous ones in the list. But other logics have more structured notions of proof, including for example sequent calculi or various kind of natural-deduction proof; in these cases the deduction theorem does not apply directly. For example, the typical rule of CI in a natural-deduction system can be phrased as a permission to infer (A->B) from a proof of B from A, discharging the assumption A and closing the (sub) proof. This is close to the deduction theorem, but it is not the deduction theorem as stated. Other proof systems can be goal-oriented, and in these cases the deduction theorem would be incorrect. >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! That is a very misleading way to phrase it, in my view. If this were correct then the deduction theorem would be trivial, but in fact in many classical systems it is quite hard to prove. > >> 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, It is not. It relates a *provability* relation with an implication connective. The deduction theorem is a metatheorem of proof theory. >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. But it would follow from the simple identification. > >> >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). We are speaking different languages. Entailment is a purely model-theoretic notion; provability is a purely proof-theoretical one. Pat -- --------------------------------------------------------------------- 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 Tuesday, 10 December 2002 15:55:18 GMT

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