Double Negation
Permits introduction and elimination of pairs of tildes
p : : ~~p
Double Negation
p : : ~~p
Permits introduction and elimination of redundant disjuncts and conjuncts
p : : p v p
p : : p * p
Duplication
p : : p v p
p : : p *p
Permits inverting of conjuncts, disjuncts
p v q : : q v p
p * q : : q * p
Commutation
p v q : : q v p
p * q : : q * p
Permits regrouping of iterated disjuntions or conjuncts
p v (q v r) : : (p v q) v r
p * (q * r) : : (p * q) * r
Association
p v (q v r) : : (p v q) v r
p * (q * r) : : (p * q) * r
Permits inverting of conditionals, with appropriate negation changes
p [horseshoe] q : : ~q [horseshoe] ~p
Contraposition
p [horseshoe] q : : ~q [horseshoe] ~p
Permits distribution of negation across disjunctions and conjunctions used extensively
~(p v q) : : ~p * ~q
~(p * q) : : ~p v ~ q
De Morgan's
~(p v q) : : ~p * ~q
~(p * q) : : ~p v ~q
Permits introduction and elimination of triple bar
p [tb] q : : (p [hs] q) * (q [hs] p)
Biconditional Exchange
p [tb] q : : (p [hs] q) * (q [hs] p)
Permits exchange of conditional and disjuntion
p [hs] q : : ~p v q
Conditional Exchange
p [hs] q : : ~p v q
Permits changing of major operator from* tov and vice versa
p * (q v r) : : (p * q) v (p * r)
p v (q * r) : : (p v q) * (p v r)
Distribution
p * (q v r) : : (p * q) v (p * r)
