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

Date: Wed, 11 Dec 2002 13:21:57 -0600

Message-Id: <p05111b06ba1d3b4d5498@[10.0.100.86]>

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

Cc: www-rdf-rules@w3.org

Date: Wed, 11 Dec 2002 13:21:57 -0600

Message-Id: <p05111b06ba1d3b4d5498@[10.0.100.86]>

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

Cc: www-rdf-rules@w3.org

> > Other proof systems can be goal-oriented, and in these cases the >> deduction theorem would be incorrect. > >No matter how proofs are established, the proof system defines >a provability relation (which normally corresponds to the >entailment relation), and the deduction theorem refers to this >*relation*, and not to the procedure. OK, with that understanding I agree, but then one has to remember that for some systems that relation may have a very tenuous or subtle connection with the actual operation of the 'rules' of the proof system itself. In the case of resolution, for example, one has to pay attention to the source of the literals in a resolvent, and interpret the ones from the axioms differently from those derived from the goal, when describing the provability relation in your sense. > > >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. > >In a constructive approach to logic, the (idea of the) deduction >theorem is the basis for introducing implication. In a more classical >(axiomatic) approach it has to be proved. In natural deduction systems (many of which are constructive) the ideas are indeed closely connected, but in those cases the simple deduction theorem is in fact *incorrect* since one needs to discharge the assumption when introducing the implication. In fact, I think I have never seen a logical system in which the simple deduction theorem is correct, in which it was easy or trivial to prove. 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 Wednesday, 11 December 2002 14:22:03 GMT

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