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

> 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 
implication:

   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 
inference)?

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

-Gerd

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