- Idempotence
-
[ P ∧ P ≡ P ]
[ P ∨ P ≡ P ]
- Commutativity
-
[ P ∧ Q ≡ Q ∧ P ]
[ P ∨ Q ≡ Q ∨ P ]
[ (P ≡ Q) ≡ (Q ≡ P) ]
- Associativity
-
[ (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R) ]
[ (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R) ]
[ ((P ≡ Q) ≡ R) ≡ (P ≡ (Q ≡ R)) ]
- Distributivity
-
[ (P ∧ (Q ∨ R) ≡ (P ∧ R) ∨ (Q ∧ R) ]
[ (P ∨ (Q ∧ R) ≡ (P ∨ R) ∧ (Q ∨ R) ]
[ P ∨ (Q ≡ R) ≡ (P ∨ Q ≡ P ∨ R) ]
- Absorption
-
[ P ∧ (P ∨ R) ≡ P ]
[ P ∨ (P ∧ R) ≡ P ]
- False-true
-
[ P ∧ true ≡ P ]
[ P ∧ false ≡ false ]
[ P ∨ true ≡ true ]
[ P ∨ false ≡ P ]
- De Morgan
-
[ ¬(P ∧ Q) ≡ ¬P ∨ ¬Q ]
[ ¬(P ∨ Q) ≡ ¬P ∧ ¬Q ]
- Negation
-
[ ¬¬P ≡ P ]
[ ¬(P ≡ Q) ≡ (¬P ≡ Q) ]
[ P ∨ ¬P ≡ true ]
[ P ∧ ¬P ≡ false ]
- Implication
-
[ P ⇒ Q ≡ ¬P ∨ Q ]
[ P ⇒ Q ≡ (P ∧ Q ≡ P) ]
[ P ⇒ Q ≡ (P ∨ Q ≡ Q) ]
[ P ⇒ P ∨ Q ]
[ P ∧ Q ⇒ P ]
[ false ⇒ P ]
[ P ⇒ true ]
[ true ⇒ P ≡ P ]
[ P ⇒ false ≡ ¬P ]
- Equivalence
-
[ P ≡ P ]
[ P ≡ P ≡ true ]
[ ¬P ≡ P ≡ 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 : Q ∧ P.i) ]
[ Q ∨ (∃i : R.i : P.i) ≡ (∃i : R.i : Q ∨ P.i) ] for R non-empty
[ (∃i : R : P) ∨ (∃i : R : Q) ≡ (∃i : R : P ∨ Q) ]
[ (∃i : R : P) ∨ (∃i : S : P) ≡ (∃i : R ∨ S : P) ]
[ (∃i : R.i : P.i) ∧ (∃i : S.i : Q.i) ≡ (∃i,j : R.i ∧ S.j : P.i ∧ Q.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 : Q ∨ P.i) ]
[ Q ∧ (∀i : R.i : P.i) ≡ (∀i : R.i : Q ∧ P.i) ] for R non-empty
[ (∀i : R : P) ∧ (∀i : R : Q) ≡ (∀i : R : P ∧ Q) ]
[ (∀i : R : P) ∧ (∀i : S : P) ≡ (∀i : R ∧ S : P) ]
[ (∀i : R.i : P.i) ∨ (∀i : S.i : Q.i) ≡ (∀i,j : R.i ∧ S.j : P.i ∨ Q.j) ]
- Universal and existential quantifications are coupled by De Morgan's law:
-
[ ¬(∃i : R : P) ≡ (∀i : R : ¬P) ]