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

No. It is to do with the ways that different systems treat 
provability. Simple logical proof systems have rules to infer 
sentences from other sentences; they will typically satisfy the 
deduction theorem. A proof in such a system is simply a list of 
sentences each derived from some previous ones in the list. But other 
logics have more structured notions of proof, including for example 
sequent calculi or various kind of natural-deduction proof; in these 
cases the deduction theorem does not apply directly. For example, the 
typical rule of CI in a natural-deduction system can be phrased as a 
permission to infer (A->B) from a proof of B from A, discharging the 
assumption A and closing the (sub) proof. This is close to the 
deduction theorem, but it is not the deduction theorem as stated.
Other proof systems can be goal-oriented, and in these cases the 
deduction theorem would be incorrect.

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

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

It is not. It relates a *provability* relation with an implication 
connective. The deduction theorem is a metatheorem of proof theory.

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

But it would follow from the simple identification.

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

We are speaking different languages. Entailment is a purely 
model-theoretic notion; provability is a purely proof-theoretical one.

Pat



-- 
---------------------------------------------------------------------
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 Tuesday, 10 December 2002 15:55:18 UTC