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

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

From: Wagner, G.R. <G.R.Wagner@tm.tue.nl>
Date: Tue, 10 Dec 2002 20:27:21 +0100
Message-ID: <AA2E843B3FC96349BF60350202650BE925737E@tmex1.tm.tue.nl>
To: "'pat hayes'" <phayes@ai.uwf.edu>
Cc: "'Tim Berners-Lee'" <timbl@w3.org>, Sandro Hawke <sandro@w3.org>, www-rdf-rules@w3.org

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

Right (I overlooked the GROUND), but it provides a correspondence
between what Tim said, "an axiom, expressed as an entailment" and an 

   A |- B  iff  |- A->B

> Second, some logical proof systems 
> satisfy the deduction theorem, but by no means all of them. 

If they don't, they don't have a genuine implication (but only
a faked one). 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!

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

I can't follow you here: since it is a theorem relating an
entailment relation with an implication connective, how 
would it depend on proof stratgies (like forward versus backward 

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

I think noone has claimed that.

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

That's exactly what constitutes entailment in intuistionistic logic 
(notice that, i general, entailment may be both a model-theoretic
and a proof-theoretic notion).

Received on Tuesday, 10 December 2002 14:28:42 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:46:14 UTC