# RE: Is n3 a rules language or a logic language?

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>

```
>  > 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 spam
```
Received on Wednesday, 11 December 2002 14:22:03 UTC

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:13 UTC