Rule | do Application | Explanation |
---|---|---|
Wedge Introduction | do X 3 vI L | X is the disjunct to be introduced, 3 is the line number to which Wedge Introduction needs to be applied and L denotes - introduce the argument X on left side. Similarly you can specify "do X 3 vI R" to introduce the argument on the Right side. |
Wedge Elimination | do 2, 4 vE | 2,4 are the line numbers to which Wedge Elimination needs to be applied. |
Ampersand Introduction | do 5,6 &I R | 5,6 are the line numbers to which Ampersand Introduction needs to be applied. L means place sentence at first listed line on left side of the junction; R means place it on the right. |
Ampersand Elimination | do 7 &E | 7 is the line numbers to which Ampersand Elimination needs to be applied. |
Arrow Introduction | do 4->I(2) | 2,4 are the line numbers to which Arrow Introduction needs to be applied. |
Arrow Elimination | do 7,10 ->E | 7,10 are the line numbers to which Arrow Elimination needs to be applied. |
Biconditional Introduction | do 3,5 <->I L | 3,5 are the line numbers to which Biconditional Introduction needs to be applied, L or R to swap the arguments on either side of the biconditional.You can use "do 3,5 <->I R" to swap the arguments |
Biconditional Elimination | do 4 <->E R | 4 is the line number to which Biconditional Elimination needs to be applied, R - conditional statement with right side one as antencedent and left one as consequent. Similarly you can use "do 4 <->E L" to form conditional statement with left side one as antecedent and right side one as consequent. |
e.g. proofs :
PvQ->R, P, @xFx, Fa&R->S |- S |
P->Q, Q->R |- P->R |
1 (1) PvQ->R A 2 (2) P A do Q 2vI R do 1,3 ->E 5 (5) @xFx A 5 (6) Fa 5 @E do 4,6 &I R 8 (8) Fa&R->S A do 7,8 ->E |
1 (1) P->Q A 2 (2) Q->R A 3 (3) P A do 1,3 ->E do 2,4 ->E do 5->I(3) |