AXIOMS AND THEOREMS

Name Rule
Double Negation ¬¬p ≡ p
Definition of f alse f alse ≡ ¬true
Negation of f alse ¬f alse ≡ true

Table 1: Equivalences for False / True and Double Negation

Name Op Rule Op Rule

Conmutativity ∨ p∨q ≡q∨p ∧ p∧q ≡q∧p
Asociativity ∨ (p ∨ q) ∨ r ≡ p ∨ (q ∨ r) ∧ (p ∧ q) ∧ r ≡ p ∧ (q ∧ r)
Identity ∨ p ∨ f alse ≡ p ∧ p ∧ true ≡ p
Dominance ∨ p ∨ true ≡ true ∧ p ∧ f alse ≡ f alse
Idempotence ∨ p∨p≡p ∧ p∧p≡p
Distributivity ∨/∧ p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r) ∧/∨ p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
de Morgan ¬∨ ¬(p ∨ q) ≡ ¬p ∧ ¬q ¬∧ ¬(p ∧ q) ≡ ¬p ∨ ¬q
Absorption ∨/∧ p ∨ (p ∧ q) ≡ p ∧/∨ p ∧ (p ∨ q) ≡ p
Absorption-¬ ∨/∧ ¬p ∨ (p ∧ q) ≡ ¬p ∨ q ∧/∨ ¬p ∧ (p ∨ q) ≡ ¬p ∧ q
Negation ∨ p ∨ ¬p ≡ true ∧ p ∧ ¬p ≡ f alse

Table 2: Equivalences of ∨ y of ∧

Negation of ∨ is called Excluded Middle. Negation of ∧ is called Contradiction.

Rule Name
p → q ≡ ¬p ∨ q Definition of →
p → q ≡ ¬q → ¬p Contrapositive
true → p ≡ p Left Identity of →
p → f alse ≡ ¬p Right Negation of →
f alse → p ≡ true Left False of →
p → true ≡ true Right Zero of →
p → p ≡ true Reflexivity →
p ∨ q ≡ ¬p → q Definition of ∨ with →
p ∧ q ≡ ¬(p → ¬q) Definition of ∧ with →
¬(p → q) ≡ p ∧ ¬q Negation of →
(p → q) ∧ (p → r) ≡ (p → (q ∧ r)) Left Distributivity → /∧
(p → q) ∨ (p → r) ≡ (p → (q ∨ r)) Left Distributivity → /∨
(p → r) ∧ (q → r) ≡ (p ∨ q) → r Right Distributivity → /∧
(p → r) ∨ (q → r) ≡ (p ∧ q) → r Right Distributivity → /∧
p → (q → r) ≡ (p ∧ q) → r Left Associativity of →

Table 3: → Equivalences
Rule Name
p ↔ q ≡ (p → q) ∧ (q → p) Definition1 of ≡
p ⊕ q ≡ ¬(p ↔ q) Definition1 ⊕
p ↔ q ≡ (p ∧ q) ∨ (¬q ∧ ¬p) Definition2 of ≡
(p ↔ q) ≡ (q ↔ p) Commutativity of ↔
((p ↔ q) ↔ r) ≡ (p ↔ (q ↔ r)) Associativity of ↔
p ↔ p ≡ true Identity
p ↔ ¬p ≡ f alse Definition2 of false
¬(p ↔ q) ≡ ¬p ↔ q Negation1 ↔
¬(p ↔ q) ≡ p ↔ ¬q Negation2 ↔
p ⊕ q ≡ (p ∧ ¬q) ∨ (¬p ∧ q) Definition2 ⊕
p ⊕ q ≡ (p ∨ q) ∧ ¬(p ∧ q) Definition3 ⊕
(p ⊕ q) ≡ (q ⊕ p) Commutativity of ⊕
((p ⊕ q) ⊕ r) ≡ (p ⊕ (q ⊕ r)) Associativity of ⊕
r ∨ (p ↔ q) ≡ (r ∨ p) ↔ (r ∨ q) Distrib ∨/ ↔
r ∧ (p ↔ q) ≡ (r ∧ p) ↔ (r ∧ q) ↔ r Distrib ∧/ ↔

Table 4: Equivalence Laws for ↔

Rule Name Rule Name

p p↔q
↔ Simplification1
p→q Modus ponens p→q
q p↔q
↔ Simplification2
¬q q→p
p→q Modus tollens p↔q
↔ Simplification3
¬p ¬p → ¬q
p→q p↔q
q→r ↔ Simplification4
Transitivity ¬q → ¬p
p→r p
p∨q p↔q ↔ Deduction1
¬q Disjunctive Syllogism q
p q
p p↔q ↔ Deduction2
Addition
p∨q p
p∧q ¬p
Simplification
p p↔q ↔ Deduction3
p ¬q
q Conjunction ¬q
p∧q p↔q ↔ Deduction3
p∨q ¬p
¬p ∨ r Resolution
q∨r Table 6: Rules of Inference 2

Table 5: Rules of Inference 1

Rule Name
∀x(Q(x) ∧ P (x)) ≡ ∀xP (x) ∧ ∀xQ(x) Distributivity ∀
∃x(P (x) ∨ Q(x)) ≡ (∃xP (x)) ∨ (∃xQ(x)) Distributivity ∃
x doesn’t appear in P: ∀x(Q(x) ∨ P ) ≡ (∀xQ(x)) ∨ P Distributivity ∨/∀
x doesn’t appear in P: ∃x(Q(x) ∧ P ) ≡ (∃xQ(x)) ∧ P Distributivity ∧/∃
¬∃xP (x) ≡ ∀x¬P (x) Generalized de Morgan
¬∀xP (x) ≡ ∃x¬P (x) Generalized de Morgan2
¬∀x(P (x) → Q(x)) ≡ ∃x(P (x) ∧ ¬Q(x)) Generalized de Morgan3
¬∃x(P (x) ∧ Q(x)) ≡ ∀x(P (x) → ¬Q(x)) Generalized de Morgan4
∀x(Q → ∀y(P → R)) ≡ ∀x∀y((Q ∧ P ) → R) Nesting; y does not appear in Q

Table 7: Equivalence Laws for Predicates

Name Rule Condition

∀xP (x)
Universal Instantiation Any c
∴ P (c)
P (c)
Universal Generalization c is an arbitrary element,
∴ ∀xP (x)
(usually obtained from a universal instantiation)
∃xP (x)
Existential Instantiation ĉ is a particular element for which P is true
∴ P (ĉ)
P (c)
Existential Generalization c is a value that makes P true
∴ ∃P (x)
∀x(P (x) → Q(x))
Universal Modus Ponens P (c) Any c
∴ Q(c)
∀x(P (x) → Q(x))
Universal Modus Tollens ¬Q(c) Any c
∴ ¬P (c)
∀x(R(x) → P (x))
Universal Instantiation2 Any c
∴ R(c) → P (c)
R(c) → P (c)
Universal Generalization2 c is an arbitrary element,
∴ ∀x(R(x) → P (x))
(usually obtained from a universal instantiation)
∃x(R(x) ∧ P (x))
Existential Instantiation2 ĉ a particular element that makes P and Q true
∴ R(ĉ) ∧ P (ĉ)
R(c) ∧ P (c)
Existential Generalization2 c any element that makes R and C true
∴ ∃x(R(x) ∧ P (x))
∀x(P (x) → Q(x))
Transitivity ∀x(Q(x) → R(x))
∴ ∀x(P (x) → R(x))
∀x(P (x) ∨ Q(x))
Universal Disjunctive Syllogism ¬Q(c) Any c
∴ P (c)
∀x∀yP (x, y)
Instantiation
∴ P (a, b)

Table 8: Inference Rules for Predicates