(1) P, Q |- (P&Q)vR
1 (1) P A
2 (2) Q A
1,2 (3) P&Q 1,2&I
1,2 (4) (P&Q)vR 3vI
(2) P |- PvR
1 (1) P A
1 (2) PvR 1vI
(3) (P&Q)&R |- Q
1 (1) (P&Q)&R A
1 (2) P&Q 1&E
1 (3) Q 2&E
(4) PvQ, ~P |- Q
1 (1) PvQ
A
2 (2) ~P A
1,2 (3)
Q 1,2vE
(5) PvQ ⊢ ~P→Q
1 (1) PvQ A
2 (2) ~P
A
1,2 (3)
Q 1,2vE
1 (4) ~P->Q 3->I(2)
(6) P→(QvR), P ⊢ QvR
1 (1) P->(QvR) A
2 (2) P
A
1,2 (3)
QvR 1,2->E
(7) P ⊢ Q→(P&Q)
1 (1) P A
2 (2) Q A
1,2 (3)
P&Q 1,2&I
1 (4) Q->(P&Q) 3->I(2)
(8) P, P→Q ⊢ QvR
1 (1) P A
2 (2) P->Q A
1,2 (3) Q 1,2->E
1,2 (4) QvR 3vI
(9) P, P→Q, Q→R ⊢ R
1 (1) P A
2 (2) P->Q A
3 (3)
Q->R A
1,2 (4) Q 1,2->E
1,2,3 (5) R 3,4->E
(10) Pv(Q&R), ~(Q&R) |- P
1 (1) Pv(Q&R) A
2 (2) ~(Q&R) A
1,2 (3)
P 1,2vE
(11) P&Q |- Q&P
1 (1) P&Q A
1 (2) Q 1&E
1 (3) P 1&E
1 (4) Q&P 2,3&I
(12) P→(Q&R), P ⊢ P&Q
1 (1)
P->(Q&R) A
2 (2) P
A
1,2 (3) Q&R 1,2->E
1,2 (4) Q 3&E
1,2 (5) P&Q 2,4&I
(13) P→Q, Q→R ⊢ P→R
1 (1)
P->Q A
2 (2)
Q->R A
3 (3)
P A
1,3 (4)
Q 1,3->E
1,2,3 (5)
R 2,4->E
1,2 (6)
P->R 5->I(3)
(14) P |- (PvQ)&(PvR)
1 (1) P A
1 (2) PvQ 1vI
1 (3) PvR 1vI
1 (4) (PvQ)&(PvR) 2,3&I
(15) P ⊢ (~PvQ)→Q
1 (1) P A
2 (2) ~PvQ A
1,2 (3) Q 1,2vE
1 (4) (~PvQ)->Q 3->I(2)
(16) P→R ⊢ P→(RvS)
1 (1) P->R A
2 (2) P A
1,2 (3) R 1,2->E
1,2 (4) RvS 3vI
1 (5) P->(RvS) 4->I(2)
Nenhum comentário:
Postar um comentário