Prev: Wittgenstein. An analysis of syntax.
Next: A new definition of Cardinality.
From: Jan Burse on 21 Nov 2009 21:52
Dear All

Just looking at the SEP natural deduction entry (*).
I find the following existential elimination rule
(slightly adapted, switching D and G):

G |- Ex A D, A |- B
------------------------- (E E) (x not in D, B)
D, G |- B

Looks quite complicated to me. Why? I can instantiate
it as follows:

------------ (Id)
Ex A |- Ex A D, A |- B
------------------------- (E E) (x not in D, B)
D, ExA |- B

Which boils down to the following new rule:

D, A |- B
------------ (E E') (x not in D, B)
D, ExA |- B

Which can in turn be used to derive the original rule
again, as follows:

D, A |- B
----------- (E E') (x not in D, B)
D, ExA |- B
------------ (-> Intro)
G |- ExA D |- ExA -> B
----------------------------- (MP)
D, G |- B

So there would be no loss in using (E E') instead
of the rule (E E).

Anybody an idea why the complicated rule (E E) is
given and not the more simple (E E') rule?

Best Regards

P.S.: Same question can be posed for (v E).

(*)
http://plato.stanford.edu/entries/logic-classical/
From: Jan Burse on 21 Nov 2009 22:11
Jan Burse schrieb:
> Anybody an idea why the complicated rule (E E) is
> given and not the more simple (E E') rule?
>
> Best Regards
>
> P.S.: Same question can be posed for (v E).
>
> (*)
> http://plato.stanford.edu/entries/logic-classical/

Ok, the new rule is not anymore an elimination rule,
rather a left rule which complements the right rule.

Another aim than Gentzen's...

Bye
 | 
Pages: 1
Prev: Wittgenstein. An analysis of syntax.
Next: A new definition of Cardinality.