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: Mon, 9 Dec 2002 12:16:31 -0600
Message-Id: <p05111b1eba1a84251763@[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

(Sorry this response is so delayed, I only just discovered this 
thread in my mailbox. But the issue is so important, and the 
conclusions apparently arrived at so wrong, that it is worth opening 
this wound up to lance the pus a little. -Pat)

>  > I think the concept of a difference between a  rule and a
>  statement is a trap.
>Like the difference (argued to bits
>>  on the list from time to time!) between entailment and
>>  implication.  The fact is that you can take
>>  one logic in which something occurs as an axiom, expressed
>>  as an entailment, and convert the same data into another
>>  logic in which there is a general axiom for an implication
>>  operator, and then the same information originally in an
>>  axiom is expressed as a a ground fact using implication. 
>
>Yes, this correspondence is generally provided by the
>"deduction theorem" which is either provable in a logic
>or it is used as the definition for introducing an
>implication connective.

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. (That in fact sounds like something to do 
with reification, if I follow it.) Second, some logical proof systems 
satisfy the deduction theorem, but by no means all of them. So SOME 
proof systems allow a certain to-and-fro between implication and 
entailment, but by no means all of them. 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). 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.

>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*.

Pat Hayes
-- 
---------------------------------------------------------------------
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 Monday, 9 December 2002 13:17:00 GMT

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