# 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 UTC

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