Talk:Disjunction elimination

From Wikipedia, the free encyclopedia

This article is within the scope of WikiProject Mathematics.
Mathematics grading:	Stub Class	Importance unassessed.	Field unassessed.

It's been a while, but I seem to remember being taught that there was a second type of disjunction elimination:

 A ∨ B
 ¬A   
 ∴ B

It's obviously logically valid. Does it have a different name? I can't find it listed on propositional calculus. Evercat 00:07 18 Jun 2003 (UTC)

While I'm at it, does this look like a valid derivation of the above? It's been a while since I've done a derivation...

1       1  P v Q            A
2       2  -P               A
3       3  P                A (for v-E)
4       4  -Q               A (for RAA)
2,3     5  P & -P           &-I 2,3
2,3,4   6  (P & -P) & -Q    &-I 4,5
2,3,4   7  P & -P           &-E 6
2,3     8  --Q              RAA 7,4
2,3     9  Q                DNE 8
10     10  Q                A (for v-E)
1,2    11  Q                v-E 1,3,9,10,10

I worked this out myself. :-)

Still, looking at my notes I can't actually find this as a 2nd type of or-elimination, so I'll just leave this lying in the talk page for now... Evercat 16:56 21 Jun 2003 (UTC)