Idempotence
[ PPP ]
[ PPP ]
Commutativity
[ PQQP ]
[ PQQP ]
[ (PQ) ≡ (QP) ]
Associativity
[ (PQ) ∧ RP ∧ (QR) ]
[ (PQ) ∨ RP ∨ (QR) ]
[ ((PQ) ≡ R) ≡ (P ≡ (QR)) ]
Distributivity
[ (P ∧ (QR) ≡ (PR) ∨ (QR) ]
[ (P ∨ (QR) ≡ (PR) ∧ (QR) ]
[ P ∨ (QR) ≡ (PQPR) ]
Absorption
[ P ∧ (PR) ≡ P ]
[ P ∨ (PR) ≡ P ]
False-true
[ P ∧ true ≡ P ]
[ P ∧ false ≡ false ]
[ P ∨ true ≡ true ]
[ P ∨ false ≡ P ]
De Morgan
[ ¬(PQ) ≡ ¬P ∨ ¬Q ]
[ ¬(PQ) ≡ ¬P ∧ ¬Q ]
Negation
[ ¬¬PP ]
[ ¬(PQ) ≡ (¬PQ) ]
[ P ∨ ¬P ≡ true ]
[ P ∧ ¬P ≡ false ]
Implication
[ PQ ≡ ¬PQ ]
[ PQ ≡ (PQP) ]
[ PQ ≡ (PQQ) ]
[ PPQ ]
[ PQP ]
[ false ⇒ P ]
[ P ⇒ true ]
[ true ⇒ PP ]
[ P ⇒ false ≡ ¬P ]
Equivalence
[ PP ]
[ PP ≡ true ]
[ ¬PP ≡ false ]
Existential quantification:
[ (∃i : false : P) ≡ false ]
[ (∃i : i = x : P) (≡ P(i := x) ]
[ (∃i : R ∧ S : P) ≡ (∃i : R : S ∧ P) ]
[ Q ∧ (∃i : R.i : P.i) ≡ (∃i : R.i : QP.i) ]
[ Q ∨ (∃i : R.i : P.i) ≡ (∃i : R.i : QP.i) ] for R non-empty
[ (∃i : R : P) ∨ (∃i : R : Q) ≡ (∃i : R : PQ) ]
[ (∃i : R : P) ∨ (∃i : S : P) ≡ (∃i : R ∨ S : P) ]
[ (∃i : R.i : P.i) ∧ (∃i : S.i : Q.i) ≡ (∃i,j : R.iS.j : P.iQ.j) ]
Universal quantification:
[ (∀i : false : P) ≡ true ]
[ (∀i : i = x : P) ≡ P(i := x)]
[ (∀i : R ∧ S : P) ≡ (∀i : R : S ⇒ P) ]
[ Q ∨ (∀i : R.i : P.i) ≡ (∀i : R.i : QP.i) ]
[ Q ∧ (∀i : R.i : P.i) ≡ (∀i : R.i : QP.i) ] for R non-empty
[ (∀i : R : P) ∧ (∀i : R : Q) ≡ (∀i : R : PQ) ]
[ (∀i : R : P) ∧ (∀i : S : P) ≡ (∀i : R ∧ S : P) ]
[ (∀i : R.i : P.i) ∨ (∀i : S.i : Q.i) ≡ (∀i,j : R.iS.j : P.iQ.j) ]
Universal and existential quantifications are coupled by De Morgan's law:
[ ¬(∃i : R : P) ≡ (∀i : R : ¬P) ]