2DM3 2018 — Mid-November Theorem Reference

Only parts of this will be available as “Midterm 2 Theorem List”!

Equality

Axiom (1.2) “Reflexivity of =”: x = x
Axiom (1.3) “Symmetry of =”: (x = y) = (y = x)

Inequality

Axiom “Definition of ≠”: x ≠ y ≡ ¬ (x = y)
Theorem “Definition of ≠”: x ≠ y ≡ (x = y ≡ false)
Theorem “Irreflexivity of ≠”: ¬ (x ≠ x)
Theorem “Irreflexivity of ≠”: x ≠ x ≡ false
Theorem “Symmetry of ≠”: x ≠ y ≡ y ≠ x

Basic Propositional Logic

Equivalence

Axiom “Definition of ≡”: (p ≡ q) = (p = q)
Axiom (3.1) “Associativity of ≡”: ((p ≡ q) ≡ r) ≡ (p ≡ (q ≡ r))
Axiom (3.2) “Symmetry of ≡”: (p ≡ q) ≡ (q ≡ p)
Axiom (3.3) “Identity of ≡”: true ≡ (q ≡ q)
Theorem (3.4): true
Theorem (3.5) “Reflexivity of ≡”: p ≡ p

Negation and Inequivalence

Axiom (3.8) “Definition of `false`”: false ≡ ¬ true
Axiom (3.9) “Commutativity of ¬ with ≡” “Distributivity of ¬ over ≡”: ¬ (p ≡ q) ≡ (¬ p ≡ q)
Axiom (3.10) “Definition of ≢”: (p ≢ q) ≡ ¬ (p ≡ q)
Theorem (3.11) “¬ connection”: ¬ p ≡ (q ≡ (p ≡ ¬ q))
Theorem (3.12) “Double negation”: ¬ (¬ p) ≡ p
Theorem (3.13) “Negation of `false`”: ¬ false ≡ true
Theorem (3.14): (p ≢ q) ≡ (¬ p ≡ q)
Theorem (3.15): ¬ p ≡ (p ≡ false)
Theorem “Identity of ≢”: (p ≢ false) ≡ p
Theorem (3.16) “Symmetry of ≢”: (p ≢ q) ≡ (q ≢ p)
Theorem (3.17) “Associativity of ≢”: ((p ≢ q) ≢ r) ≡ (p ≢ (q ≢ r))
Theorem (3.18) “Mutual associativity of ≡ with ≢”: ((p ≢ q) ≡ r) ≡ (p ≢ (q ≡ r))
Theorem (3.19) “Mutual interchangeability of ≡ with ≢”: (p ≢ (q ≡ r)) ≡ (p ≡ (q ≢ r))

Disjunction

Axiom (3.24) “Symmetry of ∨”: p ∨ q ≡ q ∨ p
Axiom (3.25) “Associativity of ∨”: (p ∨ q) ∨ r ≡ p ∨ (q ∨ r)
Axiom (3.26) “Idempotency of ∨”: p ∨ p ≡ p
Axiom (3.27) “Distributivity of ∨ over ≡”: p ∨ (q ≡ r) ≡ (p ∨ q ≡ p ∨ r)
Axiom (3.28) “Excluded middle” “LEM”: p ∨ ¬ p
Theorem (3.29) “Zero of ∨”: p ∨ true ≡ true
Theorem (3.30) “Identity of ∨”: p ∨ false ≡ p
Theorem (3.31) “Distributivity of ∨ over ∨”: p ∨ (q ∨ r) ≡ (p ∨ q) ∨ (p ∨ r)
Theorem (3.32): p ∨ q ≡ (p ∨ ¬ q ≡ p)

Conjunction

Axiom (3.35) “Golden rule”: p ∧ q ≡ (p ≡ (q ≡ p ∨ q))
Theorem (3.36) “Symmetry of ∧”: p ∧ q ≡ q ∧ p
Theorem (3.37) “Associativity of ∧”: (p ∧ q) ∧ r ≡ p ∧ (q ∧ r)
Theorem (3.38) “Idempotency of ∧”: p ∧ p ≡ p
Theorem (3.39) “Identity of ∧”: p ∧ true ≡ p
Theorem (3.40) “Zero of ∧”: p ∧ false ≡ false
Theorem (3.41) “Distributivity of ∧ over ∧”: p ∧ (q ∧ r) ≡ (p ∧ q) ∧ (p ∧ r)
Theorem (3.42) “Contradiction”: p ∧ ¬ p ≡ false
Theorem (3.43) (3.43a) “Absorption”: p ∧ (p ∨ q) ≡ p
Theorem (3.43) (3.43b) “Absorption”: p ∨ (p ∧ q) ≡ p
Theorem (3.44) (3.44a) “Absorption”: p ∧ (¬ p ∨ q) ≡ p ∧ q
Theorem (3.44) (3.44b) “Absorption”: p ∨ (¬ p ∧ q) ≡ p ∨ q
Theorem (3.44) (3.44c) “Absorption”: ¬ p ∧ (p ∨ q) ≡ ¬ p ∧ q
Theorem (3.44) (3.44d) “Absorption”: ¬ p ∨ (p ∧ q) ≡ ¬ p ∨ q
Theorem (3.45) “Distributivity of ∨ over ∧”: p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
Theorem (3.46) “Distributivity of ∧ over ∨”: p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
Theorem (3.47) (3.47a) “De Morgan”: ¬ (p ∧ q) ≡ ¬ p ∨ ¬ q
Theorem (3.47) (3.47b) “De Morgan”: ¬ (p ∨ q) ≡ ¬ p ∧ ¬ q
Theorem (3.48): p ∧ q ≡ (p ∧ ¬ q ≡ ¬ p)
Theorem (3.49) “Semi-distributivity of ∧ over ≡”: p ∧ (q ≡ r) ≡ (p ∧ q ≡ (p ∧ r ≡ p))
Theorem (3.50) “Strong Modus Ponens”: p ∧ (q ≡ p) ≡ p ∧ q
Theorem (3.51) “Replacement”: (p ≡ q) ∧ (r ≡ p) ≡ (p ≡ q) ∧ (r ≡ q)
Theorem (3.52) “Alternative definition of ≡”: p ≡ (q ≡ (p ∧ q) ∨ (¬ p ∧ ¬ q))
Theorem (3.53) “Exclusive or” “Alternative definition of ≢”: (p ≢ q) ≡ (¬ p ∧ q) ∨ (p ∧ ¬ q)
Theorem (3.55): (p ∧ q) ∧ r ≡ (p ≡ (q ≡ (r ≡ (p ∨ q ≡ (q ∨ r ≡ (r ∨ p ≡ p ∨ (q ∨ r)))))))
Theorem: toBe ∨ ¬ toBe ≡ true

Implication

Axiom (3.57) “Definition of ⇒” “Definition of Implication”: p ⇒ q ≡ (p ∨ q ≡ q)
Axiom (3.58) “Definition of ⇐” “Consequence”: p ⇐ q ≡ q ⇒ p
Theorem (3.59) “Definition of ⇒” “Definition of Implication”: p ⇒ q ≡ ¬ p ∨ q
Theorem (3.60) “Definition of ⇒” “Definition of Implication”: p ⇒ q ≡ (p ∧ q ≡ p)
Theorem (3.61) “Contrapositive”: p ⇒ q ≡ ¬ q ⇒ ¬ p
Theorem (3.62): p ⇒ (q ≡ r) ≡ (p ∧ q ≡ p ∧ r)
Theorem (3.63) “Distributivity of ⇒ over ≡”: p ⇒ (q ≡ r) ≡ (p ⇒ q ≡ p ⇒ r)
Theorem (3.64) “Self-distributivity of ⇒”: p ⇒ (q ⇒ r) ≡ (p ⇒ q) ⇒ (p ⇒ r)
Theorem (3.65) “Shunting”: p ∧ q ⇒ r ≡ p ⇒ (q ⇒ r)
Theorem (3.66): p ∧ (p ⇒ q) ≡ p ∧ q
Theorem (3.67): p ∧ (q ⇒ p) ≡ p
Theorem (3.68): p ∨ (p ⇒ q) ≡ true
Theorem (3.69): p ∨ (q ⇒ p) ≡ q ⇒ p
Theorem (3.70): p ∨ q ⇒ p ∧ q ≡ (p ≡ q)
Theorem (3.71) “Reflexivity of ⇒”: p ⇒ p
Theorem (3.72) “Right-zero of ⇒”: p ⇒ true
Theorem (3.73) “Left-identity of ⇒”: true ⇒ p ≡ p
Theorem “Definition of ¬” (3.74): p ⇒ false ≡ ¬ p
Theorem (3.75) “ex falso quodlibet”: false ⇒ p
Theorem (3.76) (3.76a) “Weakening” “Strengthening”: p ⇒ p ∨ q
Theorem (3.76) (3.76a) “Weakening” “Strengthening”: p ⇒ p ∨ q
Theorem (3.76) (3.76b) “Weakening” “Strengthening”: p ∧ q ⇒ p
Theorem (3.76) (3.76c) “Weakening” “Strengthening”: p ∧ q ⇒ p ∨ q
Theorem (3.76) (3.76d) “Weakening” “Strengthening”: p ∨ (q ∧ r) ⇒ p ∨ q
Theorem (3.76) (3.76e) “Weakening” “Strengthening”: p ∧ q ⇒ p ∧ (q ∨ r)
Theorem “Reflexivity of ⇒”: (p ≡ q) ⇒ (p ⇒ q)
Theorem (3.77) “Modus ponens”: p ∧ (p ⇒ q) ⇒ q
Theorem (3.78) “Case analysis”: (p ⇒ r) ∧ (q ⇒ r) ≡ p ∨ q ⇒ r
Theorem (3.79) “Case analysis”: (p ⇒ r) ∧ (¬ p ⇒ r) ≡ r
Theorem (3.80) “Mutual implication”: (p ⇒ q) ∧ (q ⇒ p) ≡ (p ≡ q)
Theorem (3.81) “Antisymmetry of ⇒”: (p ⇒ q) ∧ (q ⇒ p) ⇒ (p ≡ q)
Theorem (3.82) (3.82a) “Transitivity of ⇒”: (p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)
Theorem (3.82) (3.82b) “Transitivity of ⇒”: (p ≡ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)
Theorem (3.82) (3.82c) “Transitivity of ⇒”: (p ⇒ q) ∧ (q ≡ r) ⇒ (p ⇒ r)
Theorem “Implication strengthening”: p ⇒ q ≡ p ⇒ p ∧ q

Leibniz as Axiom and Substitution/Replacement Laws

Axiom (3.83) “Leibniz”: e = f ⇒ E[z ≔ e] = E[z ≔ f]
Theorem (3.84) (3.84a) “Substitution” “Replacement”: e = f ∧ E[z ≔ e] ≡ e = f ∧ E[z ≔ f]
Theorem (3.84) (3.84b) “Substitution” “Replacement”: e = f ⇒ E[z ≔ e] ≡ e = f ⇒ E[z ≔ f]
Theorem (3.84) (3.84c) “Substitution” “Replacement”: q ∧ e = f ⇒ E[z ≔ e] ≡ q ∧ e = f ⇒ E[z ≔ f]
Theorem “Transitivity of =”: e = f ∧ f = g ⇒ e = g
Theorem (3.85) (3.85a) “Replace by `true`”: p ⇒ E[z ≔ p] ≡ p ⇒ E[z ≔ true]
Theorem (3.85) (3.85b) “Replace by `true`”: q ∧ p ⇒ E[z ≔ p] ≡ q ∧ p ⇒ E[z ≔ true]
Theorem (3.85c) “Replace by `false`”: ¬ p ⇒ E[z ≔ p] ≡ ¬ p ⇒ E[z ≔ false]
Theorem (3.85e) “Replace by `true`”: p ⇒ E[z ≔ p] = E[z ≔ true]
Theorem (3.86) (3.86a) “Replace by `false`”: E[z ≔ p] ⇒ p ≡ E[z ≔ false] ⇒ p
Theorem (3.86) (3.86b) “Replace by `false`”: E[z ≔ p] ⇒ p ∨ q ≡ E[z ≔ false] ⇒ p ∨ q
Theorem (3.87) “Replace by `true`”: p ∧ E[z ≔ p] ≡ p ∧ E[z ≔ true]
Theorem (3.88) “Replace by `false`”: p ∨ E[z ≔ p] ≡ p ∨ E[z ≔ false]
Theorem (3.89) “Shannon”: E[z ≔ p] ≡ (p ∧ E[z ≔ true]) ∨ (¬ p ∧ E[z ≔ false])

Monotonicity with Respect to Implication

Theorem “Left-monotonicity of ∨” “Monotonicity of ∨”: (p ⇒ q) ⇒ (p ∨ r ⇒ q ∨ r)
Theorem “Left-monotonicity of ∨” “Monotonicity of ∨”: (p ⇒ q) ⇒ (p ∨ r ⇒ q ∨ r)
Theorem (4.2) “Left-monotonicity of ∨” “Monotonicity of ∨”: (p ⇒ q) ⇒ (p ∨ r ⇒ q ∨ r)
Theorem “Monotonicity of ∨”: (p ⇒ q) ⇒ ((r ⇒ s) ⇒ (p ∨ r ⇒ q ∨ s))
Theorem (4.3) “Left-monotonicity of ∧” “Monotonicity of ∧”: (p ⇒ q) ⇒ (p ∧ r ⇒ q ∧ r)
Theorem “Monotonicity of ∧”: (p ⇒ p') ⇒ ((q ⇒ q') ⇒ (p ∧ q ⇒ p' ∧ q'))
Theorem “Monotonicity of ∧”: (p ⇒ p') ⇒ ((q ⇒ q') ⇒ (p ∧ q ⇒ p' ∧ q'))
Theorem “Antitonicity of ¬”: (p ⇒ q) ⇒ (¬ q ⇒ ¬ p)
Theorem “Monotonicity of ⇒” “Right-monotonicity of ⇒”: (p ⇒ q) ⇒ ((r ⇒ p) ⇒ (r ⇒ q))
Theorem “Antitonicity of ⇒” “Left-antitonicity of ⇒”: (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))

Equational Theory of Integers

Axiom (15.1) (15.1a) “Associativity of +”: (a + b) + c = a + (b + c)
Axiom (15.1) (15.1b) “Associativity of ·”: (a · b) · c = a · (b · c)
Axiom (15.2) (15.2a) “Symmetry of +”: a + b = b + a
Axiom (15.2) (15.2b) “Symmetry of ·”: a · b = b · a
Axiom (15.3) “Additive identity” “Identity of +”: 0 + a = a
Axiom (15.4) “Multiplicative identity” “Identity of ·”: 1 · a = a
Axiom (15.5) “Distributivity” “Distributivity of · over +”: a · (b + c) = a · b + a · c
Axiom (15.9) “Zero of ·”: a · 0 = 0
Axiom (15.13) “Unary minus”: a + - a = 0
Axiom (15.14) “Subtraction”: a - b = a + - b
Theorem (15.17) “Self-inverse of unary minus”: - (- a) = a
Theorem (15.18) “Fixpoint of unary minus”: - 0 = 0
Theorem (15.20): - a = - 1 · a
Theorem (15.19) “Distributivity of unary minus over +”: - (a + b) = - a + - b
Theorem (15.21): - a · b = a · - b
Theorem (15.22): a · - b = - (a · b)
Theorem (15.23): - a · - b = a · b
Theorem (15.24) “Right-identity of -”: a - 0 = a
Theorem (15.25): (a - b) + (c - d) = (a + c) - (b + d)
Theorem (15.25a) “Mutual associativity of + and -”: a + (b - c) = (a + b) - c
Theorem (15.25b) “Subtraction of addition”: a - (b + c) = (a - b) - c
Theorem (15.25c): (a - b) + (b - c) = a - c
Theorem (15.26): (a - b) - (c - d) = (a + d) - (b + c)
Theorem (15.27): (a - b) · (c - d) = (a · c + b · d) - (a · d + b · c)
Theorem (15.29) “Distributivity of · over -”: (a - b) · c = a · c - b · c

Positivity of Integers

Axiom (15.7) “Cancellation of ·”: c ≠ 0 ⇒ (c · a = c · b ≡ a = b)
Axiom (15.8) “Cancellation of +”: a + b = a + c ≡ b = c
Theorem “Non-zero multiplication”: a ≠ 0 ⇒ (b ≠ 0 ⇒ a · b ≠ 0)

Positivity

Axiom (15.30) “Positivity under +”: pos a ∧ pos b ⇒ pos (a + b)
Axiom (15.31) “Positivity under ·”: pos a ∧ pos b ⇒ pos (a · b)
Axiom (15.32) “Non-positivity of 0”: ¬ pos 0
Axiom (15.33) “Positivity under unary minus”: b ≠ 0 ⇒ (pos b ≡ ¬ pos (- b))
Theorem (15.30a) “Positivity under +”: pos a ⇒ (pos b ⇒ pos (a + b))
Theorem (15.31a) “Positivity under ·”: pos a ⇒ (pos b ⇒ pos (a · b))
Theorem (15.33a) “Positivity under unary minus”: b ≠ 0 ⇒ (pos b ≢ pos (- b))
Theorem (15.33b) “Positivity under unary minus”: b ≠ 0 ⇒ (pos (- b) ≡ ¬ pos b)
Theorem (15.33c) “Positivity under unary minus”: (pos (- b) ≡ pos b) ⇒ b = 0
Theorem “Positive implies non-zero”: pos a ⇒ a ≠ 0
Theorem (15.34) “Positivity of squares”: b ≠ 0 ⇒ pos (b · b)
Theorem (15.34) “Positivity of squares”: b ≠ 0 ⇒ pos (b · b)
Theorem (15.34) “Positivity of squares”: b ≠ 0 ⇒ pos (b · b)
Corollary “Positivity of 1”: pos 1
Theorem “Positivity”: pos a ≡ a ≠ 0 ∧ ¬ pos (- a)
Theorem (15.35) “Positivity under positive ·”: pos a ⇒ (pos b ≡ pos (a · b))
Theorem (15.35) “Positivity under ·”: pos a ⇒ (pos b ≡ pos (a · b))
Theorem (15.35) “Positivity under ·”: pos a ⇒ (pos b ≡ pos (a · b))

Order on Integers

Theorem “Cancellation of unary minus”: - a = - b ≡ a = b

Orders and Strict-Orders

Axiom (15.36) “Less” “Definition of <”: a ”: a > b ≡ pos (a - b)
Axiom (15.38) “At most” “Definition of ≤”: a ≤ b ≡ a b ∨ a = b
Theorem “Irreflexivity of <”: ¬ (a < a)
Theorem “Irreflexivity of <”: a = b ⇒ ¬ (a < b)
Theorem “Irreflexivity of <”: a b ≡ b < a
Theorem “Converse of ≤”: a ≥ b ≡ b ≤ a
Theorem “Irreflexivity of >”: ¬ (a > a)
Theorem “Irreflexivity of >”: a = b ⇒ ¬ (a > b)
Theorem “Irreflexivity of >”: a > b ⇒ ¬ (a = b)
Theorem “Irreflexivity of >”: ¬ (a > b ∧ a = b)
Theorem (15.40) “Positive elements”: pos b ≡ 0 < b
Theorem (15.41) (15.41a) “Transitivity” “Transitivity of <”: a < b ∧ b < c ⇒ a < c
Theorem (15.41) (15.41b) “Transitivity” “Transitivity of ≤ with <”: a ≤ b ∧ b < c ⇒ a < c
Theorem (15.41) (15.41c) “Transitivity” “Transitivity of < with ≤”: a < b ∧ b ≤ c ⇒ a < c
Theorem (15.41) (15.41d) “Transitivity” “Transitivity of ≤”: a ≤ b ∧ b ≤ c ⇒ a ≤ c
Theorem “Transitivity of ≤”: a ≤ b ⇒ (b ≤ c ⇒ a ≤ c)
Theorem “Transitivity” “Transitivity of >”: a > b ∧ b > c ⇒ a > c
Theorem (15.42) “<-Isotonicity of +”: a < b ≡ a + d < b + d
Theorem “<-Monotonicity of +”: a < b ⇒ a + d < b + d
Theorem “<-Monotonicity of +”: a < b ⇒ (c < d ⇒ a + c < b + d)
Theorem “<-Monotonicity of +”: a < b ∧ c < d ⇒ a + c < b + d
Theorem “≤-Isotonicity of +”: a ≤ b ≡ a + d ≤ b + d
Theorem “≤-Monotonicity of +”: a ≤ b ⇒ a + d ≤ b + d
Theorem “≤-Isotonicity of -”: a ≤ b ≡ a - d ≤ b - d
Theorem “Monotonicity of -” “≤-Monotonicity of -”: a ≤ b ⇒ a - d ≤ b - d
Theorem “<-Anti-isotonicity of unary minus”: a < b ≡ - b < - a
Theorem “<-Antitonicity of unary minus”: a < b ⇒ - b < - a
Theorem “Anti-isotonicity of unary minus” “≤-Anti-isotonicity of unary minus”: a ≤ b ≡ - b ≤ - a
Theorem “Antitonicity of unary minus” “≤-Antitonicity of unary minus”: a ≤ b ⇒ - b ≤ - a
Theorem “Anti-isotonicity of -” “≤-Anti-isotonicity of -”: c ≤ b ≡ a - b ≤ a - c
Theorem “Antitonicity of -” “≤-Antitonicity of -”: c ≤ b ⇒ a - b ≤ a - c
Theorem (15.42) “Monotonicity of ·”: 0 < d ⇒ (a < b ≡ a · d < b · d)
Theorem (15.42) “Monotonicity of ·” “<-Monotonicity of ·”: 0 < d ⇒ (a < b ≡ a · d b)
Theorem (15.44B) “Trichotomy — B”: ¬ (a b))
Theorem (15.44) “Trichotomy”: (a b)) ∧ ¬ (a b))
Theorem “Complement of <”: a ”: a > b ≢ a ≤ b
Theorem “Trichotomy” “Trichotomy — ∨”: a b)
Theorem (15.45) “Antisymmetry of ≤”: a ≤ b ∧ b ≤ a ≡ a = b
Theorem (15.46) “Reflexivity of ≤”: a ≤ a

Integrality

Axiom “Least positive”: pos a ≡ 1 ≤ a
Theorem “Least greater element”: a b ≡ a ≥ b + 1
Theorem “Less than successor”: a b ≡ a ≥ b
Theorem “Split-off top”: m ≤ n ⇒ (m ≤ i < n + 1 ≡ m ≤ i < n ∨ i = n)
Theorem “Split-off bottom”: m ≤ n ⇒ (m ≤ i < n + 1 ≡ m + 1 ≤ i < n + 1 ∨ i = m)
Theorem “Example for use of Contrapositive”: x + y ≥ 2 ⇒ x ≥ 1 ∨ y ≥ 1

Inductive Theory of the Natural Numbers

Addition

Axiom “Definition of +” “Left-identity of +” “Definition of + for 0”: 0 + n = n
Axiom “Definition of +” “Addition of successor” “Definition of + for `S`”: S m + n = S (m + n)
Theorem “Right-identity of +”: m + 0 = m
Theorem “Adding the successor”: m + S n = S (m + n)
Theorem “Symmetry of +”: m + n = n + m
Theorem “Associativity of +”: (a + b) + c = a + (b + c)
Theorem “Identity of +”: 0 + a = a
Theorem “Definition of 1”: 1 = S 0
Theorem “Successor”: S n = n + 1

Multiplication

Axiom “Definition of ·” “Left-zero of ·”: 0 · n = 0
Axiom “Definition of ·”: S m · n = n + m · n
Theorem “Left-identity of ·”: 1 · n = n
Theorem “Right-zero of ·”: m · 0 = 0
Theorem “Multiplying the successor”: m · S n = m · n + m
Theorem “Symmetry of ·”: m · n = n · m
Theorem “Zero of ·”: m · 0 = 0
Theorem “Identity of ·”: 1 · m = m
Theorem “Distributivity of · over +”: k · (m + n) = k · m + k · n
Theorem “Associativity of ·”: (k · m) · n = k · (m · n)
Axiom “Subtraction from zero”: 0 - n = 0
Axiom “Subtraction of zero from successor”: S m - 0 = S m
Axiom “Subtraction of successor from successor”: S m - S n = m - n
Theorem “Right-identity of subtraction”: m - 0 = m
Theorem “Self-cancellation of subtraction”: m - m = 0
Theorem “Subtraction after addition”: (m + n) - n = m
Theorem “Subtraction from multiplication with successor”: m · S n - m = m · n
Theorem “Subtraction of sum”: k - (m + n) = (k - m) - n
Theorem “Distributivity of · over subtraction”: k · (m - n) = k · m - k · n
Theorem “Monus exchange”: m + (n - m) = n + (m - n)

Order in the Inductive Theory of the Natural Numbers

Axiom “Cancellation of `S`”: S m = S n ≡ m = n
Axiom “Zero is not suc”: 0 = S n ≡ false
Theorem “Cancellation of +”: k + m = k + n ≡ m = n
Axiom “Predecessor of zero”: pred 0 = 0
Axiom “Predecessor of successor”: pred (S n) = n
Axiom “Zero is least element”: 0 ≤ a
Axiom “Isotonicity of successor”: S a ≤ S b ≡ a ≤ b
Axiom “Successor is not at most zero”: S a ≤ 0 ≡ false
Theorem “Zero is unique least element”: a ≤ 0 ≡ a = 0
Theorem “Reflexivity of ≤”: a ≤ a
Theorem “Antisymmetry of ≤”: a ≤ b ⇒ (b ≤ a ⇒ a = b)
Theorem “Transitivity of ≤”: a ≤ b ⇒ (b ≤ c ⇒ a ≤ c)
Theorem “Isotonicity of +”: a + b ≤ a + c ≡ b ≤ c
Theorem “Monotonicity of +”: a ≤ b ⇒ (c ≤ d ⇒ a + c ≤ b + d)
Theorem “Monotonicity of predecessor”: a ≤ b ⇒ pred a ≤ pred b
Theorem “Monotonicity of -”: a ≤ b ⇒ a - c ≤ b - c
Theorem “Monotonicity of -”: a ≤ b ⇒ a - c ≤ b - c
Theorem “Monotonicity of -”: a ≤ b ⇒ a - c ≤ b - c
Theorem “Monotonicity of ·”: b ≤ c ⇒ a · b ≤ a · c
Theorem “Successor is non-decreasing”: a ≤ S a
Theorem “Subtraction is non-increasing”: a - b ≤ a
Theorem “Antitonicity of -”: b ≤ c ⇒ a - c ≤ a - b
Axiom “Zero is less than successor”: 0 < S a
Axiom “Isotonicity of successor”: S a < S b ≡ a < b
Axiom “Nothing is less than zero”: a < 0 ≡ false
Theorem “Irreflexivity of <”: a < a ≡ false
Theorem “Zero is <-least element”: 0 < a ∨ 0 = a
Theorem “Less than successor”: a < S b ≡ a < b ∨ a = b
Theorem “Less than successor”: a < S a
Theorem “Only zero is less than one”: a < 1 ≡ a = 0
Theorem “Transitivity of <”: a < b ⇒ (b < c ⇒ a < c)
Theorem “Irreflexivity of <”: a < b ⇒ ¬ (a = b)
Theorem “Definition of ≤ in terms of `S` and <”: a ≤ b ≡ a < S b
Theorem “Definition of ≤ in terms of <”: a ≤ b ≡ a < b ∨ a = b
Theorem “Empty Range”: a < b < a ⇒ false
Theorem “Empty Range”: a b ≡ b < a
Axiom “Converse of ≤”: a ≥ b ≡ b ≤ a
Theorem “Asymmetry of <”: a ”: ¬ (a > b) ≡ a ≤ b
Theorem “Complement of <”: ¬ (a < b) ≡ a ≥ b

Sum Quantification

Axioms Corresponding to the Leibniz Rules for Quantification

Axiom “Leibniz for ∑ range”: (∀ x • R₁ ≡ R₂ ) ⇒ (∑ x ❙ R₁ • E ) = (∑ x ❙ R₂ • E )
Axiom “Leibniz for ∑ body”: (∀ x • R ⇒ E₁ = E₂ ) ⇒ (∑ x ❙ R • E₁ ) = (∑ x ❙ R • E₂ )

Empty Range Axiom

Axiom (8.13) “Empty range for ∑”: (∑ x ❙ false • E ) = 0

One-Point Rule Axiom

Axiom (8.14) “One-point rule for ∑”: (∑ x ❙ x = D • E ) = E[x ≔ D]
— CalcCheck: Proviso: ¬occurs(`x`, `D`)

Distributivity Axiom

Axiom (8.15) “Distributivity of ∑ over +”: (∑ x ❙ R • E₁ + E₂ ) = (∑ x ❙ R • E₁ ) + (∑ x ❙ R • E₂ )

Range Split Axiom

Axiom (8.17) “Range split”: (∑ x ❙ Q ∨ R • E ) + (∑ x ❙ Q ∧ R • E ) = (∑ x ❙ Q • E ) + (∑ x ❙ R • E )
Theorem (8.16) “Disjoint range split for ∑”: (∀ x • Q ∧ R ≡ false ) ⇒ (∑ x ❙ Q ∨ R • E ) = (∑ x ❙ Q • E ) + (∑ x ❙ R • E )

Multiple Quantification Axioms

Axiom (8.20) “Nesting for ∑”: (∑ x ❙ Q • (∑ y ❙ R • E ) ) = (∑ x, y ❙ Q ∧ R • E )
— CalcCheck: Proviso: ¬occurs(`y`, `Q`)
Theorem “Replacement in ∑”: (∑ x ❙ R ∧ e = f • E[y ≔ e] ) = (∑ x ❙ R ∧ e = f • E[y ≔ f] )
Axiom (8.20a) “Dummy list permutation for ∑”: (∑ x, y ❙ R • E ) = (∑ y, x ❙ R • E )
Theorem (8.19) “Interchange of dummies”: (∑ x ❙ Q • (∑ y ❙ R • P ) ) = (∑ y ❙ R • (∑ x ❙ Q • P ) )
— CalcCheck: Proviso: ¬occurs(`x`, `R`), ¬occurs(`y`, `Q`)

Dummy Alteration Laws

Axiom (8.21) “Dummy renaming for ∑” “α-conversion”: (∑ x ❙ R • E ) = (∑ y ❙ R[x ≔ y] • E[x ≔ y] )
— CalcCheck: Proviso: ¬occurs(`y`, `E, R`)

Specific Material for Sum Quantification

Axiom “Distributivity of · over ∑”: a · (∑ x ❙ R • E ) = (∑ x ❙ R • a · E )
— CalcCheck: Proviso: ¬occurs(`x`, `a`)
Theorem “Zero ∑ body”: (∑ x ❙ R • 0 ) = 0

Manipulating Ranges over ℕ

Theorem “Definition of ≤ in terms of <”: a ≤ b ≡ a < b ∨ a = b
Theorem “Definition of ≤ in terms of `S` and <”: a ≤ b ≡ a < S b
Theorem “Split range at top”: m ≤ n ⇒ (m ≤ i < S n ≡ m ≤ i < n ∨ i = n)
Theorem “Split off term” “Split off term at top”: (∑ i : ℕ ❙ i < S n • E ) = (∑ i : ℕ ❙ i < n • E ) + E[i ≔ n]
— CalcCheck: Proviso: ¬occurs(`i`, `n`)
Theorem “Split off term” “Split off term at top”: m ≤ n ⇒ (∑ i ❙ m ≤ i < S n • E ) = (∑ i ❙ m ≤ i < n • E ) + E[i ≔ n]
— CalcCheck: Proviso: ¬occurs(`i`, `m, n`)
Theorem “Split off term at top using ≤”: (∑ i ❙ i ≤ S n • E ) = (∑ i ❙ i ≤ n • E ) + E[i ≔ S n]
— CalcCheck: Proviso: ¬occurs(`i`, `n`)

Application Exercises

Theorem “Odd-number sum”: (∑ i : ℕ ❙ i < n • S i + i ) = n · n
— CalcCheck: Proviso: ¬occurs(`i`, `n`)
Theorem “Sum the numbers”: 2 · (∑ i ❙ i ≤ n • i ) = n · S n
— CalcCheck: Proviso: ¬occurs(`i`, `n`)

Universal Quantification

General Quantification Material, Instantiated for Universal Quantification

Axiom “Leibniz for ∀ range”: (∀ x • R₁ ≡ R₂ ) ⇒ ((∀ x ❙ R₁ • P ) ≡ (∀ x ❙ R₂ • P ))
Axiom “Leibniz for ∀ body”: (∀ x • R ⇒ (P₁ ≡ P₂) ) ⇒ ((∀ x ❙ R • P₁ ) ≡ (∀ x ❙ R • P₂ ))

Substitution Axiom

Axiom (8.11) “Substitution” “Substitution into ∀”: (∀ x ❙ R • P )[y ≔ F] ≡ (∀ x ❙ R[y ≔ F] • P[y ≔ F] )
— CalcCheck: Proviso: ¬occurs(`x`, `F`)

Empty Range Axiom

Axiom (8.13) “Empty range for ∀”: (∀ x ❙ false • P ) ≡ true

One-Point Rule Axiom

Axiom (8.14) “One-point rule for ∀”: (∀ x ❙ x = E • P ) ≡ P[x ≔ E]
— CalcCheck: Proviso: ¬occurs(`x`, `E`)

Distributivity Axiom

Axiom (8.15) “Distributivity of ∀ over ∧”: (∀ x ❙ R • P ) ∧ (∀ x ❙ R • Q ) ≡ (∀ x ❙ R • P ∧ Q )

Range Split Axiom

Axiom (8.17) “Range split for ∀”: (∀ x ❙ R ∨ S • P ) ∧ (∀ x ❙ R ∧ S • P ) ≡ (∀ x ❙ R • P ) ∧ (∀ x ❙ S • P )

Multiple Quantification Axioms

Axiom (8.20) “Nesting for ∀”: (∀ x, y ❙ R ∧ S • P ) ≡ (∀ x ❙ R • (∀ y ❙ S • P ) )
— CalcCheck: Proviso: ¬occurs(`y`, `R`)
Theorem (8.20a) “Nesting for ∀”: (∀ x, y ❙ S • P ) ≡ (∀ x • (∀ y ❙ S • P ) )
Theorem “Replacement in ∀”: (∀ y ❙ R ∧ e = f • P[x ≔ e] ) ≡ (∀ y ❙ R ∧ e = f • P[x ≔ f] )
Axiom (8.20a) “Dummy list permutation for ∀”: (∀ x, y ❙ R • P ) ≡ (∀ y, x ❙ R • P )
Theorem (8.19) “Interchange of dummies for ∀”: (∀ x ❙ R • (∀ y ❙ S • P ) ) ≡ (∀ y ❙ S • (∀ x ❙ R • P ) )
— CalcCheck: Proviso: ¬occurs(`x`, `S`), ¬occurs(`y`, `R`)

Material Specific to Universal Quantification

Axiom (9.2) “Trading” “Trading for ∀”: (∀ x ❙ R • P ) ≡ (∀ x • R ⇒ P )
Theorem (9.3) (9.3a) “Trading” “Trading for ∀”: (∀ x ❙ R • P ) ≡ (∀ x • ¬ R ∨ P )
Theorem (9.3) (9.3b) “Trading” “Trading for ∀”: (∀ x ❙ R • P ) ≡ (∀ x • R ∧ P ≡ R )
Theorem (9.3) (9.3b) “Trading” “Trading for ∀”: (∀ x ❙ R • P ) ≡ (∀ x • R ∧ P ≡ R )
Theorem (9.3) (9.3c) “Trading” “Trading for ∀”: (∀ x ❙ R • P ) ≡ (∀ x • R ∨ P ≡ P )
Theorem (9.4) (9.4a) “Trading” “Trading for ∀”: (∀ x ❙ Q ∧ R • P ) ≡ (∀ x ❙ Q • R ⇒ P )
Theorem (9.4) (9.4b) “Trading” “Trading for ∀”: (∀ x ❙ Q ∧ R • P ) ≡ (∀ x ❙ Q • ¬ R ∨ P )
Theorem (9.4) (9.4c) “Trading” “Trading for ∀”: (∀ x ❙ Q ∧ R • P ) ≡ (∀ x ❙ Q • R ∧ P ≡ R )
Theorem (9.4) (9.4d) “Trading” “Trading for ∀”: (∀ x ❙ Q ∧ R • P ) ≡ (∀ x ❙ Q • R ∨ P ≡ P )
Theorem “Leibniz for ∀ body”: (∀ x ❙ R • P₁ ≡ P₂ ) ⇒ ((∀ x ❙ R • P₁ ) ≡ (∀ x ❙ R • P₂ ))
Theorem (8.18) “Range split for ∀”: (∀ x ❙ R ∨ S • P ) ≡ (∀ x ❙ R • P ) ∧ (∀ x ❙ S • P )
Axiom (9.5) “Distributivity of ∨ over ∀”: P ∨ (∀ x ❙ R • Q ) ≡ (∀ x ❙ R • P ∨ Q )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.6): P ∨ (∀ x • ¬ R ) ≡ (∀ x ❙ R • P )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem “Distributivity of ⇒ over ∀”: P ⇒ (∀ x ❙ R • Q ) ≡ (∀ x ❙ R • P ⇒ Q )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.7) “Distributivity of ∧ over ∀”: ¬ (∀ x • ¬ R ) ⇒ (P ∧ (∀ x ❙ R • Q ) ≡ (∀ x ❙ R • P ∧ Q ))
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.8) “True ∀ body”: (∀ x ❙ R • true )
Theorem “Introducing fresh ∀”: P ⇒ (∀ x ❙ R • P )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.9) “Sub-distributivity of ∀ over ≡”: (∀ x ❙ R • P ≡ Q ) ⇒ ((∀ x ❙ R • P ) ≡ (∀ x ❙ R • Q ))
Theorem (9.10) “Range weakening for ∀” “Range strengthening for ∀”: (∀ x ❙ Q ∨ R • P ) ⇒ (∀ x ❙ Q • P )
Theorem (9.11) “Body weakening for ∀” “Body strengthening for ∀”: (∀ x ❙ R • P ∧ Q ) ⇒ (∀ x ❙ R • P )
Theorem (9.12) “Monotonicity of ∀” “Body monotonicity of ∀”: (∀ x ❙ R • Q ⇒ P ) ⇒ ((∀ x ❙ R • Q ) ⇒ (∀ x ❙ R • P ))
Theorem (9.12a) “Range antitonicity of ∀”: (∀ x • Q ⇒ R ) ⇒ ((∀ x ❙ R • P ) ⇒ (∀ x ❙ Q • P ))
Theorem (9.12a) “Range antitonicity of ∀”: (∀ x ❙ ¬ P • Q ⇒ R ) ⇒ ((∀ x ❙ R • P ) ⇒ (∀ x ❙ Q • P ))
Theorem “Leibniz for ∀ body”: (∀ x • P₁ ≡ P₂ ) ⇒ ((∀ x ❙ R • P₁ ) ≡ (∀ x ❙ R • P₂ ))

Instantiation

Theorem (9.13) “Instantiation”: (∀ x • P ) ⇒ P[x ≔ E]
Theorem (9.13a) “Instantiation”: (∀ x • P ) ⇒ P[x ≔ x]
Theorem (9.13b) “Instantiation”: (∀ x ❙ R • P ) ⇒ (R ⇒ P)[x ≔ E]
Theorem “Fresh ∀”: P ≡ (∀ x • P )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)

Disjoint Range Split

Theorem (8.16) “Disjoint range split for ∀”: (∀ x • R ∧ S ≡ false ) ⇒ ((∀ x ❙ R ∨ S • P ) ≡ (∀ x ❙ R • P ) ∧ (∀ x ❙ S • P ))
Theorem (8.16) “Disjoint range split for ∀”: (∀ x • R ∧ S ≡ false ) ⇒ ((∀ x ❙ R ∨ S • P ) ≡ (∀ x ❙ R • P ) ∧ (∀ x ❙ S • P ))

Change of Dummy

Theorem (8.22) “Change of dummy”: (∀ f • (∀ g • (∀ x • (∀ y • x = f y ≡ y = g x ) ) ⇒ ((∀ x ❙ R • P ) ≡ (∀ y ❙ R[x ≔ f y] • P[x ≔ f y] )) ) )
— CalcCheck: Proviso: ¬occurs(`y`, `P, R`)
Theorem “Change of dummy — variant”: (∀ x • (∀ y • x = f y ⇒ y = g x ) ) ⇒ ((∀ x ❙ R ∧ x = f (g x) • P ) ≡ (∀ y ❙ R[x ≔ f y] • P[x ≔ f y] ))
— CalcCheck: Proviso: ¬occurs(`x, y`, `f`), ¬occurs(`y`, `P, R, g`)
Lemma “Range replacement in nested ∀”: (∀ x ❙ R • (∀ y • Q₁ ≡ Q₂ ) ) ⇒ ((∀ x ❙ R • (∀ y ❙ Q₁ • P ) ) ≡ (∀ x ❙ R • (∀ y ❙ Q₂ • P ) ))
Theorem (8.22a) “Change of restricted dummy”: (∀ f • (∀ g • (∀ x ❙ R • (∀ y • x = f y ≡ y = g x ) ) ⇒ ((∀ x ❙ R • P ) ≡ (∀ y ❙ R[x ≔ f y] • P[x ≔ f y] )) ) )
— CalcCheck: Proviso: ¬occurs(`y`, `P, R`)

Existential Quantification

General Quantification Material, Instantiated for Existential Quantification

Axiom “Leibniz for ∃ range”: (∀ x • R₁ ≡ R₂ ) ⇒ ((∃ x ❙ R₁ • P ) ≡ (∃ x ❙ R₂ • P ))
Axiom “Leibniz for ∃ body”: (∀ x • R ⇒ (P₁ ≡ P₂) ) ⇒ ((∃ x ❙ R • P₁ ) ≡ (∃ x ❙ R • P₂ ))
Theorem “Leibniz for ∃ body”: (∀ x ❙ R • P₁ ≡ P₂ ) ⇒ ((∃ x ❙ R • P₁ ) ≡ (∃ x ❙ R • P₂ ))
Theorem “Leibniz for ∃ body”: (∀ x • P₁ ≡ P₂ ) ⇒ ((∃ x ❙ R • P₁ ) ≡ (∃ x ❙ R • P₂ ))
Axiom (8.13) “Empty range for ∃”: (∃ x ❙ false • P ) ≡ false
Axiom (8.14) “One-point rule for ∃”: (∃ x ❙ x = E • P ) ≡ P[x ≔ E]
— CalcCheck: Proviso: ¬occurs(`x`, `E`)
Axiom (8.15) “Distributivity of ∃ over ∨”: (∃ x ❙ R • P ) ∨ (∃ x ❙ R • Q ) ≡ (∃ x ❙ R • P ∨ Q )
Axiom (8.17) “Range split”: (∃ x ❙ R ∨ S • P ) ∨ (∃ x ❙ R ∧ S • P ) ≡ (∃ x ❙ R • P ) ∨ (∃ x ❙ S • P )

Multiple Quantification Axioms

Axiom (8.20) “Nesting for ∃”: (∃ x, y ❙ R ∧ S • P ) ≡ (∃ x ❙ R • (∃ y ❙ S • P ) )
— CalcCheck: Proviso: ¬occurs(`y`, `R`)
Theorem (8.20a) “Nesting for ∃”: (∃ x, y ❙ S • P ) ≡ (∃ x • (∃ y ❙ S • P ) )
Theorem “Replacement in ∃”: (∃ y ❙ R ∧ e = f • P[x ≔ e] ) ≡ (∃ y ❙ R ∧ e = f • P[x ≔ f] )
Axiom (8.20a) “Dummy list permutation for ∃”: (∃ x, y ❙ R • P ) ≡ (∃ y, x ❙ R • P )
Theorem (8.19) “Interchange of dummies”: (∃ x ❙ R • (∃ y ❙ S • P ) ) ≡ (∃ y ❙ S • (∃ x ❙ R • P ) )
— CalcCheck: Proviso: ¬occurs(`x`, `S`), ¬occurs(`y`, `R`)

Dummy Alteration Laws

Axiom (8.21) “Dummy renaming for ∃” “α-conversion”: (∃ x ❙ R • P ) ≡ (∃ y ❙ R[x ≔ y] • P[x ≔ y] )
— CalcCheck: Proviso: ¬occurs(`y`, `P, R`)

Material Specific to Existential Quantification

Axiom (9.17) “Generalised De Morgan” “Definition of ∃”: (∃ x ❙ R • P ) ≡ ¬ (∀ x ❙ R • ¬ P )
Theorem (9.18) (9.18a) “Generalised De Morgan”: ¬ (∃ x ❙ R • ¬ P ) ≡ (∀ x ❙ R • P )
Theorem (9.18) (9.18b) “Generalised De Morgan”: ¬ (∃ x ❙ R • P ) ≡ (∀ x ❙ R • ¬ P )
Theorem (9.18) (9.18c) “Generalised De Morgan”: (∃ x ❙ R • ¬ P ) ≡ ¬ (∀ x ❙ R • P )
Theorem (9.19) “Trading” “Trading for ∃”: (∃ x ❙ R • P ) ≡ (∃ x • R ∧ P )
Theorem (9.20) “Trading” “Trading for ∃”: (∃ x ❙ Q ∧ R • P ) ≡ (∃ x ❙ Q • R ∧ P )
Theorem (9.20) “Trading” “Trading for ∃”: (∃ x ❙ Q ∧ R • P ) ≡ (∃ x ❙ Q • R ∧ P )
Theorem (8.18) “Range split for ∃”: (∃ x ❙ R ∨ S • P ) ≡ (∃ x ❙ R • P ) ∨ (∃ x ❙ S • P )
Theorem (8.16) “Disjoint range split for ∃”: (∀ x • R ∧ S ≡ false ) ⇒ ((∃ x ❙ R ∨ S • P ) ≡ (∃ x ❙ R • P ) ∨ (∃ x ❙ S • P ))
Theorem (9.21) “Distributivity of ∧ over ∃”: P ∧ (∃ x ❙ R • Q ) ≡ (∃ x ❙ R • P ∧ Q )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.22): P ∧ (∃ x • R ) ≡ (∃ x ❙ R • P )
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem “Distributivity of ∧ over ∀”: (∃ x • R ) ⇒ (P ∧ (∀ x ❙ R • Q ) ≡ (∀ x ❙ R • P ∧ Q ))
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.23) “Distributivity of ∨ over ∃”: (∃ x • R ) ⇒ (P ∨ (∃ x ❙ R • Q ) ≡ (∃ x ❙ R • P ∨ Q ))
— CalcCheck: Proviso: ¬occurs(`x`, `P`)
Theorem (9.24) “False ∃ body”: (∃ x ❙ R • false ) ≡ false
Theorem (9.25) “Range weakening for ∃” “Range strengthening for ∃”: (∃ x ❙ R • P ) ⇒ (∃ x ❙ Q ∨ R • P )
Theorem “Range weakening for ∃” “Range strengthening for ∃”: (∃ x ❙ Q ∧ R • P ) ⇒ (∃ x ❙ R • P )
Theorem (9.26) “Body weakening for ∃” “Body strengthening for ∃”: (∃ x ❙ R • P ) ⇒ (∃ x ❙ R • P ∨ Q )
Theorem (9.26a) “Body weakening for ∃” “Body strengthening for ∃”: (∃ x ❙ R • P ∧ Q ) ⇒ (∃ x ❙ R • P )
Theorem (9.27) “Monotonicity of ∃” “Body monotonicity of ∃”: (∀ x ❙ R • Q ⇒ P ) ⇒ ((∃ x ❙ R • Q ) ⇒ (∃ x ❙ R • P ))
Theorem (9.27a) “Range monotonicity of ∃”: (∀ x • Q ⇒ R ) ⇒ ((∃ x ❙ Q • P ) ⇒ (∃ x ❙ R • P ))
Theorem (9.27a) “Range monotonicity of ∃”: (∀ x ❙ P • Q ⇒ R ) ⇒ ((∃ x ❙ Q • P ) ⇒ (∃ x ❙ R • P ))

Introduction and Interchange for ∃

Theorem (9.28) “∃-Introduction”: P[x ≔ E] ⇒ (∃ x • P )
Theorem (9.29a) “Interchange of quantifications”: (∃ x • (∀ y • P ) ) ⇒ (∀ y • (∃ x • P ) )
Theorem (9.29a) “Interchange of quantifications”: (∃ x • (∀ y • P ) ) ⇒ (∀ y • (∃ x • P ) )
Theorem (9.30a) “Witness”: (∃ x ❙ R • P ) ⇒ Q ≡ (∀ x • R ∧ P ⇒ Q )
— CalcCheck: Proviso: ¬occurs(`x`, `Q`)
Theorem (9.30b) “Witness”: (∃ x • P ) ⇒ Q ≡ (∀ x • P ⇒ Q )
— CalcCheck: Proviso: ¬occurs(`x`, `Q`)

Set theory close to LADM

Membership Properties

Axiom (11.3) “Set membership”: F ∈ { x ❙ R • E } ≡ (∃ x ❙ R • F = E )
— CalcCheck: Proviso: ¬occurs(`x`, `F`)
Theorem “Set Abbreviation”: { x ❙ P } = { x ❙ P • x }
Theorem (11.7) (11.7s) “Simple Membership”: e ∈ { x ❙ P } ≡ P[x ≔ e]
Theorem (11.7) (11.7x) “Simple Membership”: x ∈ { x ❙ P } ≡ P
Theorem (11.7) (11.7∀) “Simple Membership”: (∀ x • x ∈ { x ❙ P } ≡ P )
Lemma “Membership in two-element set enumeration”: x ∈ {x, y}
Lemma “Membership in set enumeration”: x ∈ { u ❙ u = x ∨ R }
— CalcCheck: Proviso: ¬occurs(`u`, `x`)

Extensionality

Axiom (11.4) “Set extensionality” “Set equality” “Extensionality”: S = T ≡ (∀ e • e ∈ S ≡ e ∈ T )
— CalcCheck: Proviso: ¬occurs(`e`, `S, T`)
Theorem (11.6) “Mathematical formulation of set comprehension”: { x ❙ P • E } = { y ❙ (∃ x ❙ P • y = E ) }
— CalcCheck: Proviso: ¬occurs(`y`, `E, P`)
Theorem (11.9) “Simple set comprehension equality”: { x ❙ Q } = { x ❙ R } ≡ (∀ x • Q ≡ R )

Inclusion

Axiom (11.13) “Subset” “Definition of ⊆” “Set inclusion”: S ⊆ T ≡ (∀ e ❙ e ∈ S • e ∈ T )
— CalcCheck: Proviso: ¬occurs(`e`, `S, T`)
Theorem “Subset” “Definition of ⊆” “Set inclusion”: S ⊆ T ≡ (∀ e • e ∈ S ⇒ e ∈ T )
— CalcCheck: Proviso: ¬occurs(`e`, `S, T`)
Theorem “Subset membership” “Casting”: X ⊆ Y ⇒ (x ∈ X ⇒ x ∈ Y)
Theorem (11.58) “Reflexivity of ⊆”: X ⊆ X
Theorem (11.59) “Transitivity of ⊆”: X ⊆ Y ⇒ (Y ⊆ Z ⇒ X ⊆ Z)
Theorem (11.59) “Flipped transitivity of ⊆”: Y ⊆ Z ⇒ (X ⊆ Y ⇒ X ⊆ Z)
Theorem (11.57) “Antisymmetry of ⊆”: X ⊆ Y ⇒ (Y ⊆ X ⇒ X = Y)
Theorem “Empty set”: {} = { x ❙ false }
Theorem “Empty set”: x ∈ {} ≡ false
Theorem “Empty set is least” “Bottom set”: {} ⊆ X
Axiom “Universal set”: 𝐔 = { x ❙ true }
Theorem “Universal set”: x ∈ 𝐔
Theorem “Universal set is greatest” “Top set”: X ⊆ 𝐔
Theorem (11.56) “Simple set comprehension inclusion”: { x ❙ P } ⊆ { x ❙ Q } ≡ (∀ x • P ⇒ Q )

Singleton Sets

Lemma “Singleton set membership”: x ∈ {y} ≡ x = y
Lemma “Singleton set inclusion”: {x} ⊆ S ≡ x ∈ S

Complement

Axiom “Complement”: e ∈ ~ S ≡ ¬ (e ∈ S)
Theorem (11.19) “Self-inverse of complement”: ~ (~ S) = S
Theorem “Lower ~ connection for ⊆”: ~ X ⊆ Y ≡ ~ Y ⊆ X
Theorem “Upper ~ connection for ⊆”: X ⊆ ~ Y ≡ Y ⊆ ~ X

Union and Intersection

Axiom “Union”: e ∈ S ∪ T ≡ e ∈ S ∨ e ∈ T
Axiom “Intersection”: e ∈ S ∩ T ≡ e ∈ S ∧ e ∈ T

Basic Properties of Union

Theorem (11.26) “Symmetry of ∪”: S ∪ T = T ∪ S
Theorem (11.27) “Associativity of ∪”: S ∪ (T ∪ W) = (S ∪ T) ∪ W
Theorem (11.28) “Idempotency of ∪”: S ∪ S = S
Theorem (11.30) “Zero of ∪”: S ∪ 𝐔 = 𝐔
Theorem (11.30) “Identity of ∪”: S ∪ {} = S
Theorem (11.31) “Weakening of ∪”: S ⊆ S ∪ T
Theorem (11.32) “LEM of ∪”: S ∪ ~ S = 𝐔

Basic Properties of Intersection

Theorem (11.33) “Symmetry of ∩”: S ∩ T = T ∩ S
Theorem (11.34) “Associativity of ∩”: S ∩ (T ∩ W) = (S ∩ T) ∩ W
Theorem (11.35) “Idempotency of ∩”: S ∩ S = S
Theorem (11.36) “Zero of ∩”: S ∩ {} = {}
Theorem (11.37) “Identity of ∩”: S ∩ 𝐔 = S
Theorem (11.38) “Weakening of ∩”: S ∩ T ⊆ S
Theorem (11.39) “Contradiction of ∩”: S ∩ ~ S = {}

Interactions between Union and Intersection

Theorem “Golden rule for ∩ and ∪” “Golden Rule”: S ∩ T = S ≡ T = S ∪ T
Theorem “Set inclusion via ∩”: S ⊆ T ≡ S ∩ T = S
Theorem “Set inclusion via ∪”: S ⊆ T ≡ S ∪ T = T

Monotonicity with Respect to Inclusion

Theorem “Monotonicity of ∩”: S ⊆ T ⇒ S ∩ U ⊆ T ∩ U
Theorem “Monotonicity of ∩”: S ⊆ T ⇒ S ∩ U ⊆ T ∩ U
Theorem “Monotonicity of ∩”: S ⊆ T ⇒ (U ⊆ V ⇒ S ∩ U ⊆ T ∩ V)

Inclusion and Proper Subset

Theorem “Reflexivity of ⊆”: S = T ⇒ S ⊆ T
Axiom (11.14) “Proper subset” “Definition of ⊂”: S ⊂ T ≡ S ⊆ T ∧ S ≠ T
Theorem (11.61): S ⊂ T ≡ S ⊆ T ∧ ¬ (T ⊆ S)
Theorem (11.61): S ⊂ T ≡ S ⊆ T ∧ ¬ (T ⊆ S)
Theorem (11.63) “Inclusion in terms of ⊂”: S ⊆ T ≡ S ⊂ T ∨ S = T
Theorem (11.70) “Transitivity of ⊆ with ⊂”: X ⊆ Y ⇒ (Y ⊂ Z ⇒ X ⊂ Z)
Theorem (11.70) “Transitivity of ⊆ with ⊂”: X ⊆ Y ⇒ (Y ⊂ Z ⇒ X ⊂ Z)

Set Difference

Axiom (11.22) “Set difference”: v ∈ S - T ≡ v ∈ S ∧ ¬ (v ∈ T)
Theorem (11.52): S ∩ (T - S) = {}
Theorem (11.54): S - (T ∪ U) = (S - T) ∩ (S - U)

Relative Pseudo-complement

Axiom “Characterisation of ➩”: S ⊆ A ➩ B ≡ S ∩ A ⊆ B
Theorem “Membership in ➩”: x ∈ A ➩ B ≡ x ∈ A ⇒ x ∈ B
Theorem “Definition of ➩”: A ➩ B = ~ A ∪ B
Theorem “Pseudocomplement of union”: (A ∪ B) ➩ C = (A ➩ C) ∩ (B ➩ C)
Theorem “Monotonicity of ➩”: B ⊆ C ⇒ A ➩ B ⊆ A ➩ C

Cartesian Products of Sets

Axiom (14.2) “Pair equality”: ⟨b, c⟩ = ⟨b', c'⟩ ≡ b = b' ∧ c = c'
Axiom “Definition of `fst`”: fst ⟨x, y⟩ = x
Axiom “Definition of `snd`”: snd ⟨x, y⟩ = y
Axiom “Membership in ×”: p ∈ S × T ≡ fst p ∈ S ∧ snd p ∈ T
Theorem (14.4) “Membership in ×”: ⟨x, y⟩ ∈ S × T ≡ x ∈ S ∧ y ∈ T
Theorem (14.5) “Membership in swapped ×”: ⟨x, y⟩ ∈ S × T ≡ ⟨y, x⟩ ∈ T × S
Theorem (14.6) “Empty factor in ×”: S = {} ⇒ S × T = {}

Relations via Set Theory

Relationship

Axiom “Definition of ↔”: A ↔ B = ℙ (A × B)
Axiom “Infix relationship” “Definition of `_⦗_⦘_`”: a ⦗ R ⦘ b ≡ ⟨a, b⟩ ∈ R
Axiom “Relation extensionality”: R = S ≡ (∀ x • (∀ y • x ⦗ R ⦘ y ≡ x ⦗ S ⦘ y ) )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R, S`)
Axiom “Relation inclusion”: R ⊆ S ≡ (∀ x • (∀ y • x ⦗ R ⦘ y ⇒ x ⦗ S ⦘ y ) )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R, S`)
Theorem “Relation inclusion”: R ⊆ S ≡ (∀ x, y ❙ x ⦗ R ⦘ y • x ⦗ S ⦘ y )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R, S`)
Axiom “Relationship via ⌜_⌝”: a ⦗ ⌜ f ⌝ ⦘ b ≡ (f a) b

Set Operations used as Relation Operations

Theorem “Relation union”: a ⦗ R ∪ S ⦘ b ≡ a ⦗ R ⦘ b ∨ a ⦗ S ⦘ b
Theorem “Relation intersection”: a ⦗ R ∩ S ⦘ b ≡ a ⦗ R ⦘ b ∧ a ⦗ S ⦘ b
Theorem “Relation difference”: a ⦗ R - S ⦘ b ≡ a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ b)
Theorem “Relation pseudocomplement”: a ⦗ R ➩ S ⦘ b ≡ a ⦗ R ⦘ b ⇒ a ⦗ S ⦘ b
Theorem “Relation complement”: a ⦗ ~ R ⦘ b ≡ ¬ (a ⦗ R ⦘ b)
Theorem “Empty relation”: a ⦗ {} ⦘ b ≡ false
Axiom “Universal relation”: (∀ A : Type • (∀ B : Type • a ⦗ A × B ⦘ b ) )
Lemma “Singleton relation”: a₁ ⦗ {⟨a₂, b₂⟩} ⦘ b₁ ≡ a₁ = a₂ ∧ b₁ = b₂
Lemma “Singleton relation inclusion”: {⟨a, b⟩} ⊆ R ≡ a ⦗ R ⦘ b

Relation-specific Operations

Relation Converse

Axiom “Relation converse” “Relationship via ˘”: y ⦗ R ˘ ⦘ x ≡ x ⦗ R ⦘ y

Relation Composition

Axiom “Relation composition”: a ⦗ R ⨾ S ⦘ c ≡ (∃ b • a ⦗ R ⦘ b ∧ b ⦗ S ⦘ c )
— CalcCheck: Proviso: ¬occurs(`b`, `R, S, a, c`)

Identity Relations

Axiom “Identity relation” “Relationship via `Id`”: x ⦗ Id ⦘ y ≡ x = y

Relations via Set Theory: Properties

Axiom “Definition of reflexivity”: is-reflexive R ≡ (∀ x • x ⦗ R ⦘ x )
— CalcCheck: Proviso: ¬occurs(`x`, `R`)
Theorem “`Id` is reflexive”: is-reflexive Id
Theorem “Reflexivity”: is-reflexive R ≡ Id ⊆ R
Theorem “Composition of reflexive relations”: is-reflexive R ⇒ (is-reflexive S ⇒ is-reflexive (R ⨾ S))
Theorem “Converse of reflexive relations”: is-reflexive R ⇒ is-reflexive (R ˘)

Transitivity

Axiom “Definition of transitivity”: is-transitive R ≡ (∀ x • (∀ y • (∀ z • x ⦗ R ⦘ y ⦗ R ⦘ z ⇒ x ⦗ R ⦘ z ) ) )
— CalcCheck: Proviso: ¬occurs(`x, y, z`, `R`)
Theorem “Converse of transitive relations”: is-transitive R ⇒ is-transitive (R ˘)
Theorem “Transitivity”: is-transitive R ≡ R ⨾ R ⊆ R

Symmetry

Axiom “Definition of symmetry”: is-symmetric R ≡ (∀ x • (∀ y • x ⦗ R ⦘ y ⇒ y ⦗ R ⦘ x ) )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R`)
Theorem “Symmetry”: is-symmetric R ≡ R ˘ ⊆ R

Antisymmetry

Axiom “Definition of antisymmetry”: is-antisymmetric R ≡ (∀ x • (∀ y • x ⦗ R ⦘ y ⦗ R ⦘ x ⇒ x = y ) )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R`)
Theorem “Antisymmetry”: is-antisymmetric R ≡ R ∩ R ˘ ⊆ Id

Asymmetry

Axiom “Definition of asymmetry”: is-asymmetric R ≡ (∀ x • (∀ y • x ⦗ R ⦘ y ⇒ ¬ (y ⦗ R ⦘ x) ) )
— CalcCheck: Proviso: ¬occurs(`x, y`, `R`)
Theorem “Asymmetry”: is-asymmetric R ≡ R ∩ R ˘ ⊆ {}

Irreflexivity

Axiom “Definition of irreflexivity”: is-irreflexive R ≡ (∀ x • ¬ (x ⦗ R ⦘ x) )
— CalcCheck: Proviso: ¬occurs(`x`, `R`)
Theorem “Irreflexivity”: is-irreflexive R ≡ R ∩ Id ⊆ {}