- From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>
- Date: Wed, 11 Dec 2002 12:35:14 +0100
- To: "'pat hayes'" <phayes@ai.uwf.edu>
- 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. > >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. -Gerd
Received on Wednesday, 11 December 2002 07:00:51 UTC