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

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

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

-Gerd