W3C home > Mailing lists > Public > www-rdf-rules@w3.org > December 2002

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>
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 spam
Received 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