S64: ~P->P -||- P
Left to right:
| 1 | (1) | ~P->P | A |
| 2 | (2) | ~P | A |
| 1,2 | (3) | P | 1,2 ->E |
| 1 | (4) | P | 2.3 RAA (2) |
Right to left:
| 1 | (1) | P | A |
| 1 | (2) | ~P->P | 1 FA (or TC) |
S65: P<->Q -||- ~((P->Q)->~(Q->P))
Left to right:
| 1 | (1) | P<->Q | A |
| 1 | (2) | P->Q | 1 <->E |
| 1 | (3) | Q->P | 1 <->E |
| 1 | (4) | (P->Q)&(Q->P) | 2,3 &I |
| 1 | (5) | ~((P->Q)->~(Q->P)) | 4 Neg-> |
Right to left:
| 1 | (1) | ~((P->Q)->~(Q->P)) | A |
| 1 | (2) | (P->Q)&(Q->P) | 4 Neg-> |
| 1 | (3) | P->Q | 1 <->E |
| 1 | (4) | Q->P | 1 <->E |
| 1 | (5) | P<->Q | 2,3 <->I |
S68: P<->Q -||- ~(P&Q)->~(PvQ)
Left to right:
| 1 | (1) | P<->Q | A |
| 2 | (2) | PvQ | A |
| 2 | (3) | ~P->Q | 2 v-> |
| 1 | (4) | P->Q | 1 <->E |
| 1,2 | (5) | Q | 3,4 SD |
| 2 | (6) | ~Q->P | 2 v-> |
| 1 | (7) | Q->P | 1 <->E |
| 1,2 | (8) | P | 6,7 SD |
| 1,2 | (9) | P&Q | 5,8 &I |
| 1 | (10) | (PvQ)->(P&Q) | 9 ->I (2) |
| 1 | (11) | ~(P&Q)->~(PvQ) | 10 Trans |
Right to left:
| 1 | (1) | ~(P&Q)->~(PvQ) | A |
| 2 | (2) | ~(P<->Q) | A |
| 2 | (3) | ~P<->Q | 2 Neg<-> |
| 1 | (4) | (PvQ)->(P&Q) | 1 Trans |
| 2 | (5) | ~P->Q | 3 <->E |
| 2 | (6) | PvQ | 5 v-> |
| 1,2 | (7) | P&Q | 4,6 ->E |
| 2 | (8) | Q->~P | 3 <->E |
| 1,2 | (9) | Q | 7 &E |
| 1,2 | (10) | ~P | 8,9 ->E |
| 1,2 | (11) | P | 7 &E |
| 1 | (12) | P<->Q | 10,11 RAA (2) |
S69: P<->Q -||- ~(~(P&Q)&~(~P&~Q))
Left to right:
| 1 | (1) | P<->Q | A |
| 2 | (2) | ~(P&Q) | A |
| 2 | (3) | ~Pv~Q | 2 DM |
| 2 | (4) | P->~Q | 3 v-> |
| 1 | (5) | P->Q | 1 <->E |
| 1,2 | (6) | ~P | 4,5 IA |
| 1,2 | (7) | ~Q | 1,6 BT |
| 1,2 | (8) | ~P&~Q | 6,7 &I |
| 1 | (9) | ~(P&Q)->~(~P&~Q) | 8 ->I (2) |
| 1 | (10) | ~(P&Q)v~(~P&~Q) | 9 v-> |
| 1 | (11) | ~(~(P&Q)&~(~P&~Q)) | 10 DM |
Right to left:
| 1 | (1) | ~(~(P&Q)&~(~P&~Q)) | A |
| 1 | (2) | ~(P&Q)->(~P&~Q) | 1 Neg-> |
| 3 | (3) | ~P | A |
| 3 | (4) | ~Pv~Q | 3 vI |
| 3 | (5) | ~(P&Q) | 4 DM |
| 1,3 | (6) | ~P&~Q | 2,5 ->E |
| 1,3 | (7) | ~Q | 6 &E |
| 1 | (8) | ~P->~Q | 7 ->I (3) |
| 9 | (9) | P | A |
| 9 | (10) | PvQ | 9 vI |
| 9 | (11) | ~(~P&~Q) | 10 DM |
| 1,9 | (12) | P&Q | 2,11 MTT |
| 1,9 | (13) | Q | 12 &E |
| 1 | (14) | P->Q | 13 ->I (9) |
| 1 | (15) | Q->P | 8 Trans |
| 1 | (16) | P<->Q | 14,15 <->I |
S70: PvQ->R&~P, QvR, ~R |- C
| 1 | (1) | PvQ->R&~P | A |
| 2 | (2) | QvR | A |
| 3 | (3) | ~R | A |
| 2,3 | (4) | Q | 2,3 vE |
| 2,3 | (5) | PvQ | 4 vI |
| 1,2,3 | (6) | R&~P | 1,5 ->E |
| 1,2,3 | (7) | R | 6 &E |
| 3 | (8) | R->C | 3 FA |
| 1,2,3 | (9) | C | 7,8 ->E |
S71: ~P<->Q, P->R, ~R |- ~Q<->R
| 1 | (1) | ~P<->Q | A |
| 2 | (2) | P->R | A |
| 3 | (3) | ~R | A |
| 2,3 | (4) | ~P | 2,3 MT |
| 1,2,3 | (5) | Q | 1,4 BP [S35] |
| 6 | (6) | Q<->R | A |
| 1,2,3,6 | (7) | R | 5,6 BP [S35] |
| 1,2,3 | (8) | ~(Q<->R) | 3,7 RAA (6) |
| 1,2,3 | (9) | ~Q<->R | 8 Neg<-> (S42) |
S72: ~((P<->~Q)<->R), S->P&(Q&T), Rv(P&S) |- S&K->R&Q
| 1 | (1) | ~((P<->~Q)<->R) | A |
| 2 | (2) | S->P&(Q&T) | A |
| 3 | (3) | Rv(P&S) | A |
| 4 | (4) | S&K | A |
| 4 | (5) | S | 4 &E |
| 2,4 | (6) | P&(Q&T) | 2,5 ->E |
| 2,4 | (7) | Q&T | 6 &E |
| 2,4 | (8) | Q | 7 &E |
| 1 | (9) | (P<->~Q)<->~R | 1 Neg<-> |
| 10 | (10) | ~R | A |
| 1,10 | (11) | P<->~Q | 9,10 BP |
| 1,2,4,10 | (12) | ~P | 8,11 BT |
| 2,4 | (13) | P | 6 &E |
| 1,2,4 | (14) | R | 12,13 RAA (10) |
| 1,2,4 | (15) | R&Q | 13,14 &I |
| 1,2 | (16) | S&K->R&Q | 15 ->I (4) |
Note: Premise 3 is not used in this proof.
S74: P&(~Q&~R), P->(~S->T), ~S->(T<->RvQ) |- S
| 1 | (1) | P&(~Q&~R) | A |
| 2 | (2) | P->(~S->T) | A |
| 3 | (3) | ~S->(T<->RvQ) | A |
| 4 | (4) | ~S | A |
| 3,4 | (5) | T<->RvQ | 3,4 ->E |
| 1 | (6) | ~Q&~R | 1 &E |
| 1 | (7) | ~R&~Q | 6 &Comm |
| 1 | (8) | ~(RvQ) | 7 DM |
| 1,3,4 | (9) | ~T | 5,8 BT |
| 1 | (10) | P | 1 &E |
| 1,2 | (11) | ~S->T | 2,10 ->E |
| 1,2,4 | (12) | T | 4,11 ->E |
| 1,2,3 | (13) | S | 9,12 RAA (4) |
S75: P&~Q->~R, (~S->~P)<->~R |- R<->Q&(P&~S)
| 1 | (1) | P&~Q->~R | A |
| 2 | (2) | (~S->~P)<->~R | A |
| 3 | (3) | R | A |
| 1,3 | (4) | ~(P&~Q) | 1,3 MTT |
| 2,3 | (5) | ~(~S->~P) | 2,3 BT |
| 2,3 | (6) | ~S&P | 5 Neg-> |
| 1,3 | (7) | ~PvQ | 4 DM |
| 2,3 | (8) | P | 6 &E |
| 1,2,3 | (9) | Q | 7,8 vE |
| 2,3 | (10) | P&~S | 6 & Comm |
| 1,2,3 | (11) | Q&(P&~S) | 9,10 &I |
| 1,2 | (12) | R->Q&(P&~S) | 11 ->I (3) |
| 13 | (13) | Q&(P&~S) | A |
| 13 | (14) | P&~S | 13 &E |
| 13 | (15) | ~S&P | 14 & Comm |
| 13 | (16) | ~(~S->~P) | 15 Neg-> |
| 2,13 | (17) | R | 2,16 BT |
| 2 | (18) | Q&(P&~S)->R | 17 ->I (13) |
| 1,2 | (19) | R<->Q&(P&~S) | 12,18 <->I |
S77: P->QvR, (~Q&S)v(T->~P), ~(~R->~P) |- ~T&Q
| 1 | (1) | P->QvR | A |
| 2 | (2) | (~Q&S)v(T->~P) | A |
| 3 | (3) | ~(~R->~P) | A |
| 3 | (4) | ~R&P | 3 Neg-> |
| 3 | (5) | ~R | 4 &E |
| 3 | (6) | P | 4 &E |
| 1,3 | (7) | QvR | 1,6 ->E |
| 1,3 | (8) | Q | 5,7 vE |
| 1,3 | (9) | Qv~S | 8 vI |
| 1,3 | (10) | ~(~Q&S) | 9 DM |
| 1,2,3 | (11) | T->~P | 2,10 vE |
| 1,2,3 | (12) | ~T | 6,11 MTT |
| 1,2,3 | (13) | ~T&Q | 8,12 &I |
S86: ~(P&~Q)v~(~R&~S), ~S&~Q, T->(~S->~R&P) |- ~T
| 1 | (1) | ~(P&~Q)v~(~R&~S) | A |
| 2 | (2) | ~S&~Q | A |
| 3 | (3) | T->(~S->~R&P) | A |
| 4 | (4) | T | A |
| 3,4 | (5) | ~S->~R&P | 3,4 ->E |
| 2 | (6) | ~S | 2 &E |
| 2,3,4 | (7) | ~R&P | 5,6 ->E |
| 2,3,4 | (8) | ~R | 7 &E |
| 2,3,4 | (9) | ~R&~S | 6,8 &I |
| 1,2,3,4 | (10) | ~(P&~Q) | 1,9 vE |
| 1,2,3,4 | (11) | ~PvQ | 10 DM |
| 2 | (12) | ~Q | 2 &E |
| 1,2,3,4 | (13) | ~P | 11,12 vE |
| 2,3,4 | (14) | P | 7 &E |
| 1,2,3 | (15) | ~T | 13,14 RAA (4) |