Rules of Propositional Logic
The negation operator used in these rules may be optionally interpreted as an opposition operator that negates affirmative sentences and unnegates negative sentences. This option gives negation rules a wider range of application.
MP
p ⊃ q ,
p
/∴ q
MT
p ⊃ q ,
~q
/∴ ~p
Hyp Syll
p ⊃ q ,
q ⊃ r
/∴ p ⊃ r
Simp
p & q
/∴ p ,
/∴ q
Conj
p ,
q
/∴ p & q
/∴ q & p
Disj Syll
p V q ,
~p
/∴ q
Disj Syll
p V q ,
~q
/∴ p
Disj Add
p
/∴ p V q
/∴ q V p
Dilem
p V q ,
p ⊃ r ,
q ⊃ s
/∴ r V s
Dilem
p V q ,
p ⊃ r ,
q ⊃ r
/∴ r
RAA
p ⊃ q ,
p ⊃ ~q
/∴ ~p
Dbl Thens
p ⊃ (q & r)
/∴ p ⊃ q ,
/∴ p ⊃ r
Dbl Thens
p ⊃ q ,
p ⊃ r
/∴ p ⊃ (q & r)
Bicond
p ≡ q
/∴ p ⊃ q ,
/∴ q ⊃ p
Bicond
p ⊃ q ,
q ⊃ p
/∴ p ≡ q
DN
~~p
= p
DeM
~(p & q)
= ~p V ~q
DeM
~(p V q)
= ~p & ~q
Contrap
~q ⊃ ~p
= p ⊃ q
Cond
p ⊃ q
= ~p V q
Bicond
p ≡ q
= (p ⊃ q) & (q ⊃ p)
Double Ifs
(p & q) ⊃ r
= p ⊃ (q ⊃ r)
Dbl Thens
p ⊃ (q & r)
= (p ⊃ q) & (p ⊃ r)
Dupl
p & p
= p
Dupl
p V p
= p
Comm
p & q
= q & p
Comm
p V q
= q V p
Assoc
p & (q & r)
= (p & q) & r
Assoc
p V (q V r)
= (p V q) V r
Dist
p & (q V r)
= (p & q) V (p & r)
Dist
p V (q & r)
= (p V q) & (p V r)
Tautology
p V ~p , ~(p & ~p) , p ⊃ p , (p & q) ⊃ p , (p & q) ⊃ q , p ⊃ (p V q) , p ⊃ (q V p)