THEOREMS FROM GRIES AND SCHNEIDER’S LADM

J. STANLEY WARFORD

Abstract. This is a collection of the axioms and theorems in Gries and Schneider’s book
A Logical Approach to Discrete Math (LADM), Springer-Verlag, 1993. The numbering is
consistent with that text. Additional theorems not included or numbered in LADM are indi-
cated by a three-part number. This document serves as a reference for homework exercises
and taking exams.

Table of Precedences
(a) [x := e] (textual substitution) (highest precedence)
(b) . (function application)
(c) unary prefix operators: + − ¬ # ∼ P
(d) ∗∗
(e) · / ÷ mod gcd
(f) + − ∪ ∩ × ◦ •
(g) ↓ ↑
(h) #
(i) ◁ ▷ ^
(j) = < > ∈ ⊂ ⊆ ⊃ ⊇ | (conjunctional)
(k) ∨ ∧
(l) ⇒ ⇐
(m) ≡ (lowest precedence)

All nonassociative binary infix operators associate from left to right except ∗∗, ◁, and
⇒, which associate from right to left.

Definition of /: The operators on lines (j), (l), and (m) may have a slash / through them
to denote negation—e.g. x /∈ T is an abbreviation for ¬(x ∈ T ).

Some Basic Types
Name Symbol Type (set of values)
integer Z integers: …,−3,−2,−1,0,1,2,3,…
nat N natural numbers: 0,1,2,…
positive Z+ positive integers: 1,2,3,…
negative Z− negative integers: −1,−2,−3,…
rational Q rational numbers: i/ j for i, j integers, j ̸= 0
reals R real numbers
positive reals R+ positive real numbers
bool B booleans: true, f alse

Date: January 8, 2020.
1

2 J. STANLEY WARFORD

Theorems of the Propositional Calculus
Equivalence and true.
(3.1) Axiom, Associativity of ≡ : ((p ≡ q) ≡ r) ≡ (p ≡ (q ≡ r))
(3.2) Axiom, Symmetry of ≡ : p ≡ q ≡ q ≡ p
(3.3) Axiom, Identity of ≡ : true ≡ q ≡ q
(3.4) true
(3.5) Reflexivity of ≡ : p ≡ p

Negation, inequivalence, and f alse.
(3.8) Definition of f alse : f alse ≡ ¬true
(3.9) Axiom, Distributivity of ¬ over ≡ : ¬(p ≡ q) ≡ ¬p ≡ q
(3.10) Definition of ̸≡ : (p ̸≡ q) ≡ ¬(p ≡ q)
(3.11) ¬p ≡ q ≡ p ≡ ¬q
(3.12) Double negation: ¬¬p ≡ p
(3.13) Negation of f alse: ¬ f alse ≡ true
(3.14) (p ̸≡ q) ≡ ¬p ≡ q
(3.15) ¬p ≡ p ≡ f alse
(3.16) Symmetry of ̸≡ : (p ̸≡ q) ≡ (q ̸≡ p)
(3.17) Associativity of ̸≡ : ((p ̸≡ q) ̸≡ r) ≡ (p ̸≡ (q ̸≡ r))
(3.18) Mutual associativity: ((p ̸≡ q) ≡ r) ≡ (p ̸≡ (q ≡ r))
(3.19) Mutual interchangeability: p ̸≡ q ≡ r ≡ p ≡ q ̸≡

r

(3.19.1) p ̸≡ p ̸≡ q ≡ q

Disjunction.
(3.24) Axiom, Symmetry of ∨ : p ∨ q ≡ q ∨ p
(3.25) Axiom, Associativity of ∨ : (p ∨ q)∨ r ≡ p ∨(q ∨ r)
(3.26) Axiom, Idempotency of ∨ : p ∨ p ≡ p
(3.27) Axiom, Distributivity of ∨ over ≡ : p ∨(q ≡ r) ≡ p ∨ q ≡ p ∨ r
(3.28) Axiom, Excluded middle: p ∨¬p
(3.29) Zero of ∨ : p ∨ true ≡ true
(3.30) Identity of ∨ : p ∨ f alse ≡ p
(3.31) Distributivity of ∨ over ∨ : p ∨(q ∨ r) ≡ (p ∨ q)∨(p ∨ r)
(3.32) p ∨ q ≡ p ∨¬q ≡ p

Conjunction.
(3.35) Axiom, Golden rule: p ∧ q ≡ p ≡ q ≡ p ∨ q
(3.36) Symmetry of ∧ : p ∧ q ≡ q ∧ p
(3.37) Associativity of ∧ : (p ∧ q)∧ r ≡ p ∧(q ∧ r)
(3.38) Idempotency of ∧ : p ∧ p ≡ p
(3.39) Identity of ∧ : p ∧ true ≡ p
(3.40) Zero of ∧ : p ∧ f alse ≡ f alse

THEOREMS FROM LADM 3

(3.41) Distributivity of ∧ over ∧ : p ∧(q ∧ r) ≡ (p ∧ q)∧(p ∧ r)
(3.42) Contradiction: p ∧¬p ≡ f alse
(3.43) Absorption:

(a) p ∧(p ∨ q) ≡ p
(b) p ∨(p ∧ q) ≡ p

(3.44) Absorption:
(a) p ∧(¬p ∨ q) ≡ p ∧ q
(b) p ∨(¬p ∧ q) ≡ p ∨ q

(3.45) Distributivity of ∨ over ∧ : p ∨(q ∧ r) ≡ (p ∨ q)∧(p ∨ r)
(3.46) Distributivity of ∧ over ∨ : p ∧(q ∨ r) ≡ (p ∧ q)∨(p ∧ r)
(3.46.1) Consensus: (p ∧ q)∨(¬p ∧ r)∨(q ∧ r) ≡ (p ∧ q)∨(¬p ∧ r)
(3.47) De Morgan:

(a) ¬(p ∧ q) ≡ ¬p ∨¬q
(b) ¬(p ∨ q) ≡ ¬p ∧¬q

(3.48) p ∧ q ≡ p ∧¬q ≡ ¬p
(3.49) p ∧(q ≡ r) ≡ p ∧ q ≡ p ∧ r ≡ p
(3.50) p ∧(q ≡ p) ≡ p ∧ q
(3.51) Replacement: (p ≡ q)∧(r ≡ p) ≡ (p ≡ q)∧(r ≡ q)
(3.52) Equivalence: p ≡ q ≡ (p ∧ q)∨(¬p ∧¬q)
(3.53) Exclusive or: p ̸≡ q ≡ (¬p ∧ q)∨(p ∧¬q)
(3.55) (p ∧ q)∧ r ≡ p ≡ q ≡ r ≡ p ∨ q ≡ q ∨ r ≡ r ∨ p ≡ p ∨ q ∨ r

Implication.
(3.57) Definition of Implication: p ⇒ q ≡ p ∨ q ≡ q
(3.58) Axiom, Consequence: p ⇐ q ≡ q ⇒ p
(3.59) Implication: p ⇒ q ≡ ¬p ∨ q
(3.60) Implication: p ⇒ q ≡ p ∧ q ≡ p
(3.61) Contrapositive: p ⇒ q ≡ ¬q ⇒ ¬p
(3.62) p ⇒ (q ≡ r) ≡ p ∧ q ≡ p ∧ r
(3.63) Distributivity of ⇒ over ≡ : p ⇒ (q ≡ r) ≡ (p ⇒ q) ≡ (p ⇒ r)
(3.63.1) Distributivity of ⇒ over ∧ : p ⇒ q ∧ r ≡ (p ⇒ q)∧(p ⇒ r)
(3.63.2) Distributivity of ⇒ over ∨ : p ⇒ q ∨ r ≡ (p ⇒ q)∨(p ⇒ r)
(3.64) p ⇒ (q ⇒ r) ≡ (p ⇒ q) ⇒ (p ⇒ r)
(3.65) Shunting: p ∧ q ⇒ r ≡ p ⇒ (q ⇒ r)
(3.66) p ∧(p ⇒ q) ≡ p ∧ q
(3.67) p ∧(q ⇒ p) ≡ p
(3.68) p ∨(p ⇒ q) ≡ true
(3.69) p ∨(q ⇒ p) ≡ q ⇒ p
(3.70) p ∨ q ⇒ p ∧ q ≡ p ≡ q
(3.71) Reflexivity of ⇒ : p ⇒ p
(3.72) Right zero of ⇒ : p ⇒ true ≡ true
(3.73) Left identity of ⇒ : true ⇒ p ≡ p

4 J. STANLEY WARFORD

(3.74) p ⇒ f alse ≡ ¬p
(3.74.1) ¬p ⇒ f alse ≡ p
(3.74.2) p ⇒ ¬p ≡ ¬p
(3.75) f alse ⇒ p ≡ true
(3.76) Weakening/strengthening:

(a) p ⇒ p ∨ q (Weakening the consequent)
(b) p ∧ q ⇒ p (Strengthening the antecedent)
(c) p ∧ q ⇒ p ∨ q (Weakening/strengthening)
(d) p ∨(q ∧ r) ⇒ p ∨ q
(e) p ∧ q ⇒ p ∧(q ∨ r)

(3.76.1) p ∧ q ⇒ p ∨ r (Weakening/strengthening)
(3.76.2) (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))
(3.77) Modus ponens: p ∧(p ⇒ q) ⇒ q
(3.77.1) Modus tollens: (p ⇒ q)∧¬q ⇒ ¬p
(3.78) (p ⇒ r)∧(q ⇒ r) ≡ p ∨ q ⇒ r
(3.78.1) (p ⇒ r)∨(q ⇒ r) ≡ p ∧ q ⇒ r
(3.79) (p ⇒ r)∧(¬p ⇒ r) ≡ r
(3.80) Mutual implication: (p ⇒ q)∧(q ⇒ p) ≡ (p ≡ q)
(3.81) Antisymmetry: (p ⇒ q)∧(q ⇒ p) ⇒ (p ≡ q)
(3.82) Transitivity:

(a) (p ⇒ q)∧(q ⇒ r) ⇒ (p ⇒ r)
(b) (p ≡ q)∧(q ⇒ r) ⇒ (p ⇒ r)
(c) (p ⇒ q)∧(q ≡ r) ⇒ (p ⇒ r)

(3.82.1) Transitivity of ≡ : (p ≡ q)∧(q ≡ r) ⇒ (p ≡ r)
(3.82.2) (p ≡ q) ⇒ (p ⇒ q)
Leibniz as an axiom.
This section uses the following notation: E zX means E[z := X].
(3.83) Axiom, Leibniz: e = f ⇒ E ze = E zf
(3.84) Substitution:

(a) (e = f )∧ E ze ≡ (e = f )∧ E zf
(b) (e = f ) ⇒ E ze ≡ (e = f ) ⇒ E zf
(c) q ∧(e = f ) ⇒ E ze ≡ q ∧(e = f ) ⇒ E zf

(3.85) Replace by true:
(a) p ⇒ E zp ≡ p ⇒ E ztrue
(b) q ∧ p ⇒ E zp ≡ q ∧ p ⇒ E ztrue

(3.86) Replace by f alse:
(a) E zp ⇒ p ≡ E zf alse ⇒ p
(b) E zp ⇒ p ∨ q ≡ E zf alse ⇒ p ∨ q

(3.87) Replace by true: p ∧ E zp ≡ p ∧ E ztrue
(3.88) Replace by f alse: p ∨ E zp ≡ p ∨ E zf alse
(3.89) Shannon: E zp ≡ (p ∧ E ztrue)∨(¬p ∧ E zf alse)
(3.89.1) E ztrue ∧ E zf alse ⇒ E

z
p

THEOREMS FROM LADM 5

Additional theorems concerning implication.
(4.1) p ⇒ (q ⇒ p)
(4.2) Monotonicity of ∨ : (p ⇒ q) ⇒ (p ∨ r ⇒ q ∨ r)
(4.3) Monotonicity of ∧ : (p ⇒ q) ⇒ (p ∧ r ⇒ q ∧ r)

Proof technique metatheorems.
(4.4) Deduction (assume conjuncts of antecedent):

To prove P1 ∧ P2 ⇒ Q, assume P1 and P2, and prove Q.
You cannot use textual substitution in P1 or P2.

(4.5) Case analysis: If E ztrue and E zf alse are theorems, then so is E
z
P.

(4.6) Case analysis: (p ∨ q ∨ r)∧(p ⇒ s)∧(q ⇒ s)∧(r ⇒ s) ⇒ s
(4.7) Mutual implication: To prove P ≡ Q, prove P ⇒ Q and Q ⇒ P.
(4.7.1) Truth implication: To prove P, prove true ⇒ P.
(4.9) Proof by contradiction: To prove P, prove ¬P ⇒ f alse.
(4.9.1) Proof by contradiction: To prove P, prove ¬P ≡ f alse.
(4.12) Proof by contrapositive: To prove P ⇒ Q, prove ¬Q ⇒ ¬P.

General Laws of Quantification
For symmetric and associative binary operator ⋆ with identity u.
(8.13) Axiom, Empty range: (⋆x f alse : P) = u
(8.14) Axiom, One-point rule: Provided ¬occurs(‘x’,‘E’),

(⋆x x = E : P) = P[x := E]
(8.15) Axiom, Distributivity: Provided P,Q : B or R is finite,

(⋆x R : P)⋆(⋆x R : Q) = (⋆x R : P ⋆ Q)
(8.16) Axiom, Range split: Provided R ∧ S ≡ f alse and P : B or R and S are finite,

(⋆x R ∨ S : P) = (⋆x R : P)⋆(⋆x S : P)
(8.17) Axiom, Range split: Provided P : B or R and S are finite,

(⋆x R ∨ S : P)⋆(⋆x R ∧ S : P) = (⋆x R : P)⋆(⋆x S : P)
(8.18) Axiom, Range split for idempotent ⋆ : Provided P : B or R and S are finite,

(⋆x R ∨ S : P) = (⋆x R : P)⋆(⋆x S : P)
(8.19) Axiom, Interchange of dummies: Provided ⋆ is idempotent or R and Q are finite,

¬occurs(‘y’,‘R’), ¬occurs(‘x’,‘Q’),
(⋆x R : (⋆y Q : P)) = (⋆y Q : (⋆x R : P))

(8.20) Axiom, nesting: Provided ¬occurs(‘y’,‘R’),
(⋆x,y R ∧ Q : P) = (⋆x R : (⋆y Q : P))

(8.21) Axiom, Dummy renaming: Provided ¬occurs(‘y’,‘R,P’),
(⋆x R : P) = (⋆y R[x := y] : P[x := y])

(8.22) Change of dummy: Provided ¬occurs(‘y’,‘R,P’), and f has an inverse,
(⋆x R : P) = (⋆y R[x := f .y] : P[x := f .y])

6 J. STANLEY WARFORD

(8.23) Split off term: For n: N,
(a) (⋆i 0 ≤ i < n + 1 : P) = (⋆i 0 ≤ i < n : P)⋆ P[i := n] (b) (⋆i 0 ≤ i < n + 1 : P) = P[i := 0]⋆(⋆i 0 < i < n + 1 : P)

Theorems of the Predicate Calculus
Universal quantification.
Notation: (⋆x : P) means (⋆x true : P).
(9.2) Axiom, Trading: (∀x R : P) ≡ (∀x : R ⇒ P)
(9.3) Trading:

(a) (∀x R : P) ≡ (∀x : ¬R ∨ P)
(b) (∀x R : P) ≡ (∀x : R ∧ P ≡ R)
(c) (∀x R : P) ≡ (∀x : R ∨ P ≡ P)

(9.4) Trading:
(a) (∀x Q ∧ R : P) ≡ (∀x Q : R ⇒ P)
(b) (∀x Q ∧ R : P) ≡ (∀x Q : ¬R ∨ P)
(c) (∀x Q ∧ R : P) ≡ (∀x Q : R ∧ P ≡ R)
(d) (∀x Q ∧ R : P) ≡ (∀x Q : R ∨ P ≡ P)

(9.4.1) Universal double trading: (∀x R : P) ≡ (∀x ¬P : ¬R)
(9.5) Axiom, Distributivity of ∨ over ∀ : Provided ¬occurs(‘x’,‘P’),

P ∨(∀x R : Q) ≡ (∀x R : P ∨ Q)
(9.6) Provided ¬occurs(‘x’,‘P’), (∀x R : P) ≡ P ∨(∀x : ¬R)
(9.7) Distributivity of ∧ over ∀ : Provided ¬occurs(‘x’,‘P’),

¬(∀x : ¬R) ⇒ ((∀x R : P ∧ Q) ≡ P ∧(∀x R : Q))
(9.8) (∀x R : true) ≡ true
(9.9) (∀x R : P ≡ Q) ⇒ ((∀x R : P) ≡ (∀x R : Q))
(9.10) Range weakening/strengthening: (∀x Q ∨ R : P) ⇒ (∀x Q : P)
(9.11) Body weakening/strengthening: (∀x R : P ∧ Q) ⇒ (∀x R : P)
(9.12) Monotonicity of ∀ : (∀x R : Q ⇒ P) ⇒ ((∀x R : Q) ⇒ (∀x R : P))
(9.13) Instantiation: (∀x : P) ⇒ P[x := E]
(9.16) Metatheorem: P is a theorem iff (∀x : P) is a theorem.

Existential quantification.
(9.17) Axiom, Generalized De Morgan: (∃x R : P) ≡ ¬(∀x R : ¬P)
(9.18) Generalized De Morgan:

(a) ¬(∃x R : ¬P) ≡ (∀x R : P)
(b) ¬(∃x R : P) ≡ (∀x R : ¬P)
(c) (∃x R : ¬P) ≡ ¬(∀x R : P)

(9.19) Trading: (∃x R : P) ≡ (∃x : R ∧ P)
(9.20) Trading: (∃x Q ∧ R : P) ≡ (∃x Q : R ∧ P)
(9.20.1) Existential double trading: (∃x R : P) ≡ (∃x P : R)

THEOREMS FROM LADM 7

(9.20.2) (∃x : R) ⇒ ((∀x R : P) ⇒ (∃x R : P))
(9.21) Distributivity of ∧ over ∃ : Provided ¬occurs(‘x’,‘P’),

P ∧(∃x R : Q) ≡ (∃x R : P ∧ Q)
(9.22) Provided ¬occurs(‘x’,‘P’), (∃x R : P) ≡ P ∧(∃x : R)
(9.23) Distributivity of ∨ over ∃ : Provided ¬occurs(‘x’,‘P’),

(∃x : R) ⇒ ((∃x R : P ∨ Q) ≡ P ∨(∃x R : Q))
(9.24) (∃x R : f alse) ≡ f alse
(9.25) Range weakening/strengthening: (∃x R : P) ⇒ (∃x Q ∨ R : P)
(9.26) Body weakening/strengthening: (∃x R : P) ⇒ (∃x R : P ∨ Q)
(9.26.1) Body weakening/strengthening: (∃x R : P ∧ Q) ⇒ (∃x R : P)
(9.27) Monotonicity of ∃ : (∀x R : Q ⇒ P) ⇒ ((∃x R : Q) ⇒ (∃x R : P))
(9.28) ∃-Introduction: P[x := E] ⇒ (∃x : P)
(9.29) Interchange of quantification: Provided ¬occurs(‘y’,‘R’) and ¬occurs(‘x’,‘Q’),

(∃x R : (∀y Q : P)) ⇒ (∀y Q : (∃x R : P))
(9.30) Provided ¬occurs(‘x̂’,‘Q’),

(∃x R : P) ⇒ Q is a theorem iff (R ∧ P)[x := x̂] ⇒ Q is a theorem.

A Theory of Sets
(11.2) {e0,…,en−1} = {x x = e0 ∨···∨ x = en−1 : x}
(11.3) Axiom, Set membership: Provided ¬occurs(‘x’,‘F’),

F ∈ {x R : E} ≡ (∃x R : F = E)
(11.4) Axiom, Extensionality: S = T ≡ (∀x : x ∈ S ≡ x ∈ T )
(11.4.1) Axiom, Empty set: /0 = {x f alse : E}
(11.4.2) e ∈ /0 ≡ f alse
(11.4.3) Axiom, Universe: U = {x : x}, U: set(t) = {x: t : x}
(11.4.4) e ∈ U ≡ true, for e: t and U: set(t)
(11.5) S = {x x ∈ S : x}
(11.5.1) Axiom, Abbreviation: For x a single variable, {x R} = {x R : x}
(11.6) Provided ¬occurs(‘y’,‘R’) and ¬occurs(‘y’,‘E’),

{x R : E} = {y (∃x R : y = E)}
(11.7) x ∈ {x R} ≡ R

R is the characteristic predicate of the set.
(11.7.1) y ∈ {x R} ≡ R[x := y] for any expression y
(11.9) {x Q} = {x R} ≡ (∀x : Q ≡ R)
(11.10) {x Q} = {x R} is valid iff Q ≡ R is valid.
(11.11) Methods for proving set equality S = T :

(a) Use Leibniz directly.
(b) Use axiom Extensionality (11.4) and prove the (9.8) Lemma

v ∈ S ≡ v ∈ T for an arbitrary value v.
(c) Prove Q ≡ R and conclude {x Q} = {x R}.

8 J. STANLEY WARFORD

Operations on sets.
(11.12) Axiom, Size: #S = (Σx x ∈ S : 1)
(11.13) Axiom, Subset: S ⊆ T ≡ (∀x x ∈ S : x ∈ T )
(11.14) Axiom, Proper subset: S ⊂ T ≡ S ⊆ T ∧ S ̸= T
(11.15) Axiom, Superset: T ⊇ S ≡ S ⊆ T
(11.16) Axiom, Proper superset: T ⊃ S ≡ S ⊂ T
(11.17) Axiom, Complement: v ∈∼ S ≡ v ∈ U ∧ v /∈ S
(11.18) v ∈∼ S ≡ v /∈ S, for v in U
(11.19) ∼∼ S = S
(11.20) Axiom, Union: v ∈ S ∪ T ≡ v ∈ S ∨ v ∈ T
(11.21) Axiom, Intersection: v ∈ S ∩ T ≡ v ∈ S ∧ v ∈ T
(11.22) Axiom, Difference: v ∈ S − T ≡ v ∈ S ∧ v /∈ T
(11.23) Axiom, Power set: v ∈ PS ≡ v ⊆ S
(11.24) Definition. Let Es be a set expression constructed from set variables, /0, U, ∼, ∪, and ∩.

Then Ep is the expression constructed from Es by replacing:
/0 with f alse, U with true, ∪ with ∨, ∩ with ∧, ∼ with ¬.
The construction is reversible: Es can be constructed from Ep.

(11.25) Metatheorem. For any set expressions Es and Fs:
(a) Es = Fs is valid iff Ep ≡ Fp is valid,
(b) Es ⊆ Fs is valid iff Ep ⇒ Fp is valid,
(c) Es = U is valid iff Ep is valid.

Basic properties of ∪.
(11.26) Symmetry of ∪ : S ∪ T = T ∪ S
(11.27) Associativity of ∪ : (S ∪ T )∪U = S ∪(T ∪U)
(11.28) Idempotency of ∪ : S ∪ S = S
(11.29) Zero of ∪ : S ∪ U = U
(11.30) Identity of ∪ : S ∪ /0 = S
(11.31) Weakening: S ⊆ S ∪ T
(11.32) Excluded middle: S∪ ∼ S = U

Basic properties of ∩.
(11.33) Symmetry of ∩ : S ∩ T = T ∩ S
(11.34) Associativity of ∩ : (S ∩ T )∩U = S ∩(T ∩U)
(11.35) Idempotency of ∩ : S ∩ S = S
(11.36) Zero of ∩ : S ∩ /0 = /0
(11.37) Identity of ∩ : S ∩ U = S
(11.38) Strengthening: S ∩ T ⊆ S
(11.39) Contradiction: S ∩ ∼ S = /0

THEOREMS FROM LADM 9

Basic properties of combinations of ∪ and ∩.
(11.40) Distributivity of ∪ over ∩ : S ∪(T ∩U) = (S ∪ T )∩(S ∪U)
(11.41) Distributivity of ∩ over ∪ : S ∩(T ∪U) = (S ∩ T )∪(S ∩U)
(11.42) De Morgan:

(a) ∼ (S ∪ T ) = ∼ S ∩ ∼ T
(b) ∼ (S ∩ T ) = ∼ S ∪ ∼ T

Additional properties of ∪ and ∩.
(11.43) S ⊆ T ∧U ⊆ V ⇒ (S ∪U) ⊆ (T ∪V )
(11.44) S ⊆ T ∧U ⊆ V ⇒ (S ∩U) ⊆ (T ∩V )
(11.45) S ⊆ T ≡ S ∪ T = T
(11.46) S ⊆ T ≡ S ∩ T = S
(11.47) S ∪ T = U ≡ (∀x x ∈ U : x /∈ S ⇒ x ∈ T )
(11.48) S ∩ T = /0 ≡ (∀x : x ∈ S ⇒ x /∈ T )

Properties of set difference.
(11.49) S − T = S ∩ ∼ T
(11.50) S − T ⊆ S
(11.51) S − /0 = S
(11.52) S ∩(T − S) = /0
(11.53) S ∪(T − S) = S ∪ T
(11.54) S −(T ∪U) = (S − T )∩(S −U)
(11.55) S −(T ∩U) = (S − T )∪(S −U)

Implication versus subset.
(11.56) (∀x : P ⇒ Q) ≡ {x P} ⊆ {x Q}

Properties of subset.
(11.57) Antisymmetry: S ⊆ T ∧ T ⊆ S ≡ S = T
(11.58) Reflexivity: S ⊆ S
(11.59) Transitivity: S ⊆ T ∧ T ⊆ U ⇒ S ⊆ U
(11.60) /0 ⊆ S
(11.61) S ⊂ T ≡ S ⊆ T ∧¬(T ⊆ S)
(11.62) S ⊂ T ≡ S ⊆ T ∧(∃x x ∈ T : x /∈ S)
(11.63) S ⊆ T ≡ S ⊂ T ∨ S = T
(11.64) S ̸⊂ S
(11.65) S ⊂ T ⇒ S ⊆ T
(11.66) S ⊂ T ⇒ T ⊈ S
(11.67) S ⊆ T ⇒ T ̸⊂ S
(11.68) S ⊆ T ∧¬(U ⊆ T ) ⇒ ¬(U ⊆ S)

10 J. STANLEY WARFORD

(11.69) (∃x x ∈ S : x /∈ T ) ⇒ S ̸= T
(11.70) Transitivity:

(a) S ⊆ T ∧ T ⊂ U ⇒ S ⊂ U
(b) S ⊂ T ∧ T ⊆ U ⇒ S ⊂ U
(c) S ⊂ T ∧ T ⊂ U ⇒ S ⊂ U

Theorems concerning power set P.
(11.71) P /0 = {/0}
(11.72) S ∈ PS
(11.73) #(PS) = 2#S (for finite set S)

Union and intersection of families of sets.
(11.74.1) Definition: v ∈ (∪x R : E) ≡ (∃x R : v ∈ E)
(11.75.1) Definition: v ∈ (∩x R : E) ≡ (∀x R : v ∈ E)
(11.76) Axiom, Partition: Set S partitions T if

(i) the sets in S are pairwise disjoint and
(ii) the union of the sets in S is T , that is, if
(∀u,v u ∈ S ∧ v ∈ S ∧ u ̸= v : u ∩ v = /0)∧(∪u u ∈ S : u) = T

Bags.
(11.80) Axiom, Size: #{| x R : E |} = (Σx R : 1)
(11.81) Axiom, Number of occurrences: v#{| x R : E |} = (Σx R ∧ v = E : 1)
(11.82) Axiom, Bag equality: B = C ≡ (∀v : v#B = v#C)
(11.83) Axiom, Subbag: B ⊆ C ≡ (∀v : v#B ≤ v#C)
(11.84) Axiom, Proper subbag: B ⊂ C ≡ B ⊆ C ∧ B ̸= C
(11.85) Axiom, Union: B ∪C = {| v,i 0 ≤ i < v#B + v#C : v |} (11.86) Axiom, Intersection: B ∩C = {| v,i 0 ≤ i < v#B ↓ v#C : v |} (11.87) Axiom, Difference: B −C = {| v,i 0 ≤ i < v#B − v#C : v |}

Mathematical Induction
(12.3) Axiom, Mathematical Induction over N:

(∀n: N : (∀i 0 ≤ i < n : P.i) ⇒ P.n) ⇒ (∀n: N : P.n) (12.4) Mathematical Induction over N:

(∀n: N : (∀i 0 ≤ i < n : P.i) ⇒ P.n) ≡ (∀n: N : P.n) (12.5) Mathematical Induction over N:

P.0 ∧(∀n: N : (∀i 0 ≤ i ≤ n : P.i) ⇒ P(n + 1)) ≡ (∀n: N : P.n)
(12.11) Definition, b to the power n:

b0 = 1
bn+1 = b · bn for n ≥ 0

THEOREMS FROM LADM 11

(12.12) b to the power n:
b0 = 1
bn = b · bn−1 for n ≥ 1

(12.13) Definition, factorial:
0! = 1
n! = n ·(n − 1)! for n > 0

(12.14) Definition, Fibonacci:
F0 = 0, F1 = 1
Fn = Fn−1 + Fn−2 for n > 1

(12.14.1) Definition, Golden Ratio: ϕ = (1 +
√

5)/2 ≈ 1.618 ϕ̂ = (1 −
√

5)/2 ≈ −0.618
(12.15) ϕ 2 = ϕ + 1 and ϕ̂ 2 = ϕ̂ + 1
(12.16) Fn ≤ ϕ n−1 for n ≥ 1
(12.16.1) ϕ n−2 ≤ Fn for n ≥ 1
(12.17) Fn+m = Fm · Fn+1 + Fm−1 · Fn for n ≥ 0 and m ≥ 1

Inductively defined binary trees.
(12.30) Definition, Binary Tree:

/0 is a binary tree, called the empty tree.
(d,l,r) is a binary tree, for d: Z and l, r binary trees.

(12.31) Definition, Number of Nodes:
# /0 = 0
#(d,l,r) = 1 + #l + #r

(12.32) Definition, Height:
height./0 = 0
height.(d,l,r) = 1 + max(height.l,height.r)

(12.32.1) Definition, Leaf: A leaf is a node with no children (i.e. two empty subtrees).
(12.32.2) Definition, Internal node: An internal node is a node that is not a leaf.
(12.32.3) Definition, Complete: A binary tree is complete if every node has either

0 or 2 children.
(12.33) The maximum number of nodes in a tree with height n is 2n − 1 for n ≥ 0.
(12.34) The minimum number of nodes in a tree with height n is n for n ≥ 0.
(12.35) (a) The maximum number of leaves in a tree with height n is 2n−1 for n > 0.

(b) The maximum number of internal nodes in a tree with height n is 2n−1 − 1 for n > 0.
(12.36) (a) The minimum number of leaves in a tree with height n is 1 for n > 0.

(b) The minimum number of internal nodes in a tree with height n is n − 1 for n > 0.
(12.37) Every nonempy complete tree has an odd number of nodes.

A Theory of Programs
(p.1) Axiom, Excluded miracle: wp.S. false ≡ false
(p.2) Axiom, Conjunctivity: wp.S.(X ∧Y ) ≡ wp.S.X ∧ wp.S.Y

12 J. STANLEY WARFORD

(p.3) Monotonicity: (X ⇒ Y ) ⇒ (wp.S.X ⇒ wp.S.Y )
(p.4) Definition, Hoare triple: {Q} S {R} ≡ Q ⇒ wp.S.R
(p.4.1) {wp.S.R} S {R}
(p.5) Postcondition rule: {Q} S {A}∧(A ⇒ R) ⇒ {Q} S {R}
(p.6) Definition, Program equivalence: S = T ≡ (For all R,wp.S.R ≡ wp.T.R)
(p.7) (Q ⇒ A)∧{A} S {R} ⇒ {Q} S {R}
(p.8) {Q0} S {R0} ∧{Q1} S {R1} ⇒ {Q0 ∧ Q1} S {R0 ∧ R1}
(p.9) {Q0} S {R0} ∧{Q1} S {R1} ⇒ {Q0 ∨ Q1} S {R0 ∨ R1}
(p.10) Definition, skip: wp.skip.R ≡ R
(p.11) {Q} skip {R} ≡ Q ⇒ R
(p.12) Definition, abort: wp.abort.R ≡ false
(p.13) {Q} abort {R} ≡ Q ≡ false
(p.14) Definition, Composition: wp.(S; T ).R ≡ wp.S.(wp.T.R)
(p.15) {Q} S {H} ∧ {H} T {R} ⇒ {Q} S; T {R}
(p.16) Identity of composition:

(a) S ; skip = S (b) skip ; S = S
(p.17) Zero of composition:

(a) S ; abort = abort (b) abort ; S = abort
(p.18) Definition, Assignment: wp.(x := E).R ≡ R[x := E]
(p.19) Proof method for assignment: (p.19) is (10.2)

To show that x := E is an implementation of {Q}x :=?{R},
prove Q ⇒ R[x := E].

(p.20) (x := x) = skip
(p.21) IF G : (p.21) is (10.6)

if B1 → S1
[] B2 → S2
[] B3 → S3
fi

(p.22) Definition, IF G: wp.IF G.R ≡ (B1 ∨ B2 ∨ B3) ∧
B1 ⇒ wp.S1.R ∧ B2 ⇒ wp.S2.R ∧ B3 ⇒ wp.S3.R

(p.23) Empty guard: if fi = abort
(p.24) Proof method for IF G: (p.24) is (10.7)

To prove {Q}IF G{R}, it suffices to prove
(a) Q ⇒ B1 ∨ B2 ∨ B3,
(b) {Q ∧ B1} S1 {R},
(c) {Q ∧ B2} S2 {R}, and
(d) {Q ∧ B3} S3 {R}.

(p.25) ¬(B1 ∨ B2 ∨ B3) ⇒ IF G = abort
(p.26) One-guard rule: {Q} if B → S fi {R} ⇒ {Q} S {R}
(p.27) Distributivity of program over alternation:

if B1 → S1; T [] B2 → S2; T fi = if B1 → S1 [] B2 → S2 fi ; T

THEOREMS FROM LADM 13

(p.28) DO : do B → S od
(p.29) Fundamental Invariance Theorem. (p.29) is (12.43)

Suppose
• {P ∧ B} S {P} holds—i.e. execution of S begun in a state

in which P and B are true terminates with P true—and
• {P} do B → S od {true}—i.e. execution of the loop begun

in a state in which P is true terminates.
Then {P} do B → S od {P ∧¬B} holds.

(p.30) Proof method for DO: (p.30) is (12.45)
To prove {Q} initialization; {P} do B → S od {R},
it suffices to prove
(a) P is true before execution of the loop: {Q} initialization; {P},
(b) P is a loop invariant: {P ∧ B} S {P},
(c) Execution of the loop terminates, and
(d) R holds upon termination: P ∧¬B ⇒ R.

(p.31) False guard: do f alse → S od = skip

Relations and Functions
(14.2) Axiom, Pair equality: ⟨b,c⟩ = ⟨b′,c′⟩ ≡ b = b′ ∧ c = c′
(14.2.1) Ordered pair one-point rule: Provided ¬occurs(‘x,y’,‘E,F’),

(⋆x,y ⟨x,y⟩ = ⟨E,F⟩ : P) = P[x,y := E,F]
(14.3) Axiom, Cross product: S × T = {b,c b ∈ S ∧ c ∈ T : ⟨b,c⟩}
(14.3.1) Axiom, Ordered pair extensionality:

U = V ≡ (∀x,y : ⟨x,y⟩ ∈ U ≡ ⟨x,y⟩ ∈ V )

Theorems for cross product.
(14.4) Membership: ⟨x,y⟩ ∈ S × T ≡ x ∈ S ∧ y ∈ T
(14.5) ⟨x,y⟩ ∈ S × T ≡ ⟨y,x⟩ ∈ T × S
(14.6) S = /0 ⇒ S × T = T × S = /0
(14.7) S × T = T × S ≡ S = /0 ∨ T = /0 ∨ S = T
(14.8) Distributivity of × over ∪ :

(a) S ×(T ∪U) = (S × T )∪(S ×U)
(b) (S ∪ T )×U = (S ×U)∪(T ×U)

(14.9) Distributivity of × over ∩ :
(a) S ×(T ∩U) = (S × T )∩(S ×U)
(b) (S ∩ T )×U = (S ×U)∩(T ×U)

(14.10) Distributivity of × over − :
S ×(T −U) = (S × T )−(S ×U)

(14.11) Monotonicity: T ⊆ U ⇒ S × T ⊆ S ×U
(14.12) S ⊆ U ∧ T ⊆ V ⇒ S × T ⊆ U ×V

14 J. STANLEY WARFORD

(14.13) S × T ⊆ S ×U ∧ S ̸= /0 ⇒ T ⊆ U
(14.14) (S ∩ T )×(U ∩V ) = (S ×U)∩(T ×V )
(14.15) For finite S and T , #(S × T ) = #S · #T

Relations.
(14.15.1) Definition, Binary relation:

A binary relation over B ×C is a subset of B ×C.
(14.15.2) Definition, Identity: The identity relation iB on B is iB = {x: B : ⟨x,x⟩}
(14.15.3) Identity lemma: ⟨x,y⟩ ∈ iB ≡ x = y
(14.15.4) Notation: ⟨b,c⟩ ∈ ρ and b ρ c are interchangeable notations.
(14.15.5) Conjunctive meaning: b ρ c σ d ≡ b ρ c ∧ c σ d
The domain Dom.ρ and range Ran.ρ of a relation ρ on B ×C are defined by
(14.16) Definition, Domain: Dom.ρ = {b: B (∃c : b ρ c)}
(14.17) Definition, Range: Ran.ρ = {c: C (∃b : b ρ c)}
The inverse ρ−1 of a relation ρ on B ×C is the relation defined by
(14.18) Definition, Inverse: ⟨b,c⟩ ∈ ρ−1 ≡ ⟨c,b⟩ ∈ ρ, for all b: B, c: C
(14.19) Let ρ and σ be relations.

(a) Dom(ρ−1) = Ran.ρ
(b) Ran(ρ−1) = Dom.ρ
(c) If ρ is a relation on B ×C, then ρ−1 is a relation on C × B
(d) (ρ−1)−1 = ρ
(e) ρ ⊆ σ ≡ ρ−1 ⊆ σ −1

Let ρ be a relation on B ×C and σ be a relation on C × D. The product
of ρ and σ, denoted by ρ ◦ σ, is the relation defined by
(14.20) Definition, Product: ⟨b,d⟩ ∈ ρ ◦ σ ≡ (∃c c ∈ C : ⟨b,c⟩ ∈ ρ ∧⟨c,d⟩ ∈ σ)
or, using the alternative notation by
(14.21) Definition, Product: b (ρ ◦ σ) d ≡ (∃c : b ρ c σ d)

Theorems for relation product.
(14.22) Associativity of ◦ : ρ ◦(σ ◦ θ ) = (ρ ◦ σ)◦ θ
(14.23) Distributivity of ◦ over ∪ :

(a) ρ ◦(σ ∪ θ ) = (ρ ◦ σ)∪(ρ ◦ θ )
(b) (σ ∪ θ )◦ ρ = (σ ◦ ρ)∪(θ ◦ ρ)

(14.24) Distributivity of ◦ over ∩ :
(a) ρ ◦(σ ∩ θ ) ⊆ (ρ ◦ σ)∩(ρ ◦ θ )
(b) (σ ∩ θ )◦ ρ ⊆ (σ ◦ ρ)∩(θ ◦ ρ)

THEOREMS FROM LADM 15

Theorems for powers of a relation.
(14.25) Definition:

ρ 0 = iB
ρ n+1 = ρ n ◦ ρ for n ≥ 0

(14.26) ρ m ◦ ρ n = ρ m+n for m ≥ 0,n ≥ 0
(14.27) (ρ m)n = ρ m·n for m ≥ 0,n ≥ 0
(14.28) For ρ a relation on finite set B of n elements,

(∃i, j 0 ≤ i < j ≤ 2n 2

: ρ i = ρ j)
(14.29) Let ρ be a relation on a finite set B. Suppose ρ i = ρ j and 0 ≤ i < j. Then

(a) ρ i+k = ρ j+k for k ≥ 0
(b) ρ i = ρ i+p·( j−i) for p ≥ 0

Table 14.1 Classes of relations ρ over set B
Name Property Alternative

(a) reflexive (∀b : b ρ b) iB ⊆ ρ
(b) irreflexive (∀b : ¬(b ρ b)) iB ∩ ρ = /0
(c) symmetric (∀b,c : b ρ c ≡ c ρ b) ρ−1 = ρ
(d) antisymmetric (∀b,c : b ρ c ∧ c ρ b ⇒ b = c) ρ ∩ ρ−1 ⊆ iB
(e) asymmetric (∀b,c : b ρ c ⇒ ¬(c ρ b)) ρ ∩ ρ−1 = /0
(f) transitive (∀b,c,d : b ρ c ∧ c ρ d ⇒ b ρ d) ρ = (∪i i > 0 : ρ i)

(14.30.1) Definition: Let ρ be a relation on a set. The reflexive closure of ρ is the
relation r(ρ) that satisfies:
(a) r(ρ) is reflexive;
(b) ρ ⊆ r(ρ);
(c) If any relation σ is reflexive and ρ ⊆ σ, then r(ρ) ⊆ σ.

(14.30.2) Definition: Let ρ be a relation on a set. The symmetric closure of ρ is the
relation s(ρ) that satisfies:
(a) s(ρ) is symmetric;
(b) ρ ⊆ s(ρ);
(c) If any relation σ is symmetric and ρ ⊆ σ, then s(ρ) ⊆ σ.

(14.30.3) Definition: Let ρ be a relation on a set. The transitive closure of ρ is the
relation ρ+ that satisfies:
(a) ρ+ is transitive;
(b) ρ ⊆ ρ+;
(c) If any relation σ is transitive and ρ ⊆ σ, then ρ+ ⊆ σ.

(14.30.4) Definition: Let ρ be a relation on a set. The reflexive transitive closure of ρ
is the relation ρ∗ that is both the reflexive and the transitive closure of ρ.

16 J. STANLEY WARFORD

(14.31) (a) A reflexive relation is its own reflexive closure.
(b) A symmetric relation is its own symmetric closure.
(c) A transitive relation is its own transitive closure.

(14.32) Let ρ be a relation on a set B. Then,
(a) r(ρ) = ρ ∪ iB
(b) s(ρ) = ρ ∪ ρ−1
(c) ρ+ = (∪i 0 < i : ρ i) (d) ρ∗ = ρ+ ∪ iB

Equivalence relations.
(14.33) Definition: A relation is an equivalence relation iff it is reflexive, symmetric,

and transitive
(14.34) Definition: Let ρ be an equivalence relation on B. Then [b]ρ, the equivalence

class of b, is the subset of elements of B that are equivalent (under ρ) to b:
x ∈ [b]ρ ≡ x ρ b

(14.35) Let ρ be an equivalence relation on B, and let b, c be members of B. The
following three predicates are equivalent:
(a) b ρ c
(b) [b]∩[c] ̸= /0
(c) [b] = [c]
That is, (b ρ c) = ([b]∩[c] ̸= /0) = ([b] = [c])

(14.35.1) Let ρ be an equivalence relation on B. The equivalence classes partition B.
(14.36) Let P be the set of sets of a partition of B. The following relation ρ on B is an

equivalence relation:
b ρ c ≡ (∃p p ∈ P : b ∈ p ∧ c ∈ p)

Functions.
(14.37) (a) Definition: A binary relation f on B ×C is determinate iff

(∀b,c,c′ b f c ∧ b f c′ : c = c′)
(b) Definition: A binary relation is a function iff it is determinate.

(14.37.1) Notation: f .b = c and b f c are interchangeable notations.
(14.38) Definition: A function f on B ×C is total if B = Dom. f .

Otherwise it is partial.
We write f : B → C for the type of f if f is total and f : B ; C if f is partial.

(14.38.1) Total: A function f on B ×C is total if, for an arbitrary element b: B,
(∃c: C : f .b = c)

(14.39) Definition, Composition: For functions f and g, f • g = g ◦ f .
(14.40) Let g : B → C and f : C → D be total functions.

Then the composition f • g of f and g is the total function defined by
( f • g).b = f (g.b)

THEOREMS FROM LADM 17

ρ a relation on B ×C
f a function, f : B → C

Determinate (14.37) Total (14.38)

B C B C

Determinate: f is a function Total

B C B C

Not determinate: ρ is not a function Not total (partial)

Onto (14.41a) One-to-one (14.41b)

B C B C

Onto One-to-one

B C B C

Not onto Not one-to-one

Inverses of total functions.
(14.41) Definitions:

(a) Total function f : B → C is onto or surjective if Ran. f = C.
(b) Total function f is one-to-one or injective if

(∀b,b′: B,c: C : b f c ∧ b′ f c ≡ b = b′).
(c) Total function f is bijective if it is one-to-one and onto.

(14.42) Let f be a total function, and let f −1 be its relational inverse.
(a) Then f −1 is a function, i.e. is determinate, iff f is one-to-one.
(b) And, f −1 is total iff f is onto.

(14.43) Definitions: Let f : B → C.
(a) A left inverse of f is a function g : C → B such that g • f = iB.
(b) A right inverse of f is a function g : C → B such that f • g = iC.
(c) Function g is an inverse of f if it is both a left inverse and a right inverse.

(14.44) Function f : B → C is onto iff f has a right inverse.
(14.45) Let f : B → C be total. Then f is one-to-one iff f has a left inverse.

18 J. STANLEY WARFORD

(14.46) Let f : B → C be total. The following statements are equivalent.
(a) f is one-to-one and onto.
(b) There is a function g : C → B that is both a left and a right inverse of f .
(c) f has a left inverse and f has a right inverse.

Order relations.
(14.47) Definition: A binary relation ρ on a set B is called a partial order on b if it is

reflexive, antisymmetric, and transitive. In this case, pair ⟨B,ρ⟩ is called a partially
ordered set or poset.

We use the symbol ⪯ for an arbitrary partial order, sometimes writing c ⪰ b instead of b ⪯ c.
(14.47.1) Definition, Incomparable: incomp(b,c) ≡ ¬(b ⪯ c)∧¬(c ⪯ b)
(14.48) Definition: Relation ≺ is a quasi order or strict partial order if ≺ is transitive

and irreflexive
(14.48.1) Definition, Reflexive reduction: Given ⪯, its reflexive reduction ≺ is computed

by eliminating all pairs ⟨b,b⟩ from ⪯.
(14.48.2) Let ≺ be the reflexive reduction of ⪯. Then,

¬(b ⪯ c) ≡ c ≺ b ∨ incomp(b,c)
(14.49) (a) If ρ is a partial order over a set B, then ρ − iB is a quasi order.

(b) If ρ is a quasi order over a set B, then ρ ∪ iB is a partial order.

Total orders and topological sort.
(14.50) Definition: A partial order ⪯ over B is called a total or linear order if

(∀b,c : b ⪯ c ∨ b ⪰ c), i.e. iff ⪯ ∪ ⪯−1= B × B.
In this case, the pair ⟨B,⪯⟩ is called a linearly ordered set or a chain.

(14.51) Definitions: Let S be a nonempty subset of poset ⟨U,⪯⟩.
(a) Element b of S is a minimal element of S if no element of S is smaller than b,

i.e. if b ∈ S ∧(∀c c ≺ b : c /∈ S).
(b) Element b of S is the least element of S if b ∈ S ∧(∀c c ∈ S : b ⪯ c).
(c) Element b is a lower bound of S if (∀c c ∈ S : b ⪯ c).

(A lower bound of S need not be in S.)
(d) Element b is the greatest lower bound of S, written glb.S if b is a lower bound

and if every lower bound c satisfies c ⪯ b.
(14.52) Every finite nonempty subset S of poset ⟨U,⪯⟩ has a minimal element.
(14.53) Let B be a nonempty subset of poset ⟨U,⪯⟩.

(a) A least element of B is also a minimal element of B (but not necessarily
vice versa).

(b) A least element of B is also a greatest lower bound of B (but not necessarily
vice versa).

THEOREMS FROM LADM 19

(c) A lower bound of B that belongs to B is also a least element of B.

((14.54) Definitions: Let S be a nonempty subset of poset ⟨U,⪯⟩.
(a) Element b of S is a maximal element of S if no element of S is larger than b,

i.e. if b ∈ S ∧(∀c b ≺ c : c /∈ S).
(b) Element b of S is the greatest element of S if b ∈ S ∧(∀c c ∈ S : c ⪯ b).
(c) Element b is an upper bound of S if (∀c c ∈ S : c ⪯ b).

(An upper bound of S need not be in S.)
(d) Element b is the least upper bound of S, written lub.S, if b is an upper bound

and if every upper bound c satisfies b ⪯ c.

Relational databases.
(14.56.1) Definition, select: For Relation R and predicate F, which may contain names

of fields of R, σ(R,F) = {t t ∈ R ∧ F}
(14.56.2) Definition, project: For A1,…,Am a subset of the names of the fields of

relation R, π(R,A1,…,Am) = {t t ∈ R : ⟨t.A1,t.A2,…,t.Am⟩}
(14.56.3) Definition, natural join: For Relations R1 and R2, R1 ▷◁ R2 has all the attributes

that R1 and R2 have, but if an attribute appears in both, then it appears only once in
the result; further, only those tuples that agree on this common attribute are included.

Growth of Functions
(g.1) Definition of asymptotic upper bound: For a given function g.n, O(g.n),

pronounced “big-oh of g of n”, is the set of functions
{ f .n (∃c,n0 c > 0 ∧ n0 > 0 : (∀n n ≥ n0 : 0 ≤ f .n ≤ c · g.n) )}

(g.2) O-notation: f .n = O(g.n) means function f .n is in the set O(g.n).
(g.3) Definition of asymptotic lower bound: For a given function g.n, Ω (g.n),

pronounced “big-omega of g of n”, is the set of functions
{ f .n (∃c,n0 c > 0 ∧ n0 > 0 : (∀n n ≥ n0 : 0 ≤ c · g.n ≤ f .n) )}

(g.4) Ω-notation: f .n = Ω (g.n) means function f .n is in the set Ω (g.n).
(g.5) Definition of asymptotic tight bound: For a given function g.n, Θ (g.n),

pronounced “big-theta of g of n”, is the set of functions
{ f .n (∃c1,c2,n0 c1 > 0 ∧ c2 > 0 ∧ n0 > 0 :

(∀n n ≥ n0 : 0 ≤ c1 · g.n ≤ f .n ≤ c2 · g.n) )}
(g.6) Θ-notation: f .n = Θ (g.n) means function f .n is in the set Θ (g.n).
(g.7) f .n = Θ (g.n) if and only if f .n = O(g.n) and f .n = Ω (g.n)

20 J. STANLEY WARFORD

Comparison of functions.
(g.8) Reflexivity:

(a) f .n = O( f .n)
(b) f .n = Ω ( f .n)
(c) f .n = Θ ( f .n)

(g.9) Symmetry: f .n = Θ (g.n) ≡ g.n = Θ ( f .n)
(g.10) Transpose symmetry: f .n = O(g.n) ≡ g.n = Ω ( f .n)
(g.11) Transitivity:

(a) f .n = O(g.n) ∧ g.n = O(h.n) ⇒ f .n = O(h.n)
(b) f .n = Ω (g.n) ∧ g.n = Ω (h.n) ⇒ f .n = Ω (h.n)
(c) f .n = Θ (g.n) ∧ g.n = Θ (h.n) ⇒ f .n = Θ (h.n)

(g.12) Define an asymptotically positive polynomial p.n of degree d to be
p.n = (Σi 0 ≤ i ≤ d : aini) where the constants a0,a1,…,ad are the
coefficients of the polynomial and ad > 0. Then p.n = Θ (nd).

(g.13) (a) O(1) ⊂ O(lg n) ⊂ O(n) ⊂ O(n lg n) ⊂ O(n2) ⊂ O(n3) ⊂ O(2n)
(b) Ω (1) ⊃ Ω (lg n) ⊃ Ω (n) ⊃ Ω (n lg n) ⊃ Ω (n2) ⊃ Ω (n3) ⊃ Ω (2n)

A Theory of Integers
Minimum and maximum.
(15.53) Definition of ↓ : (∀z : z ≤ x ↓ y ≡ z ≤ x ∧ z ≤ y)

Definition of ↑ : (∀z : z ≥ x ↑ y ≡ z ≥ x ∧ z ≥ y)
(15.54) Symmetry:

(a) x ↓ y = y ↓ x (b) x ↑ y = y ↑ x
(15.55) Associativity:

(a) (x ↓ y) ↓ z = x ↓ (y ↓ z) (b) (x ↑ y) ↑ z = x ↑ (y ↑ z)

Restrictions. Although ↓ and ↑ are symmetric and associative, they do not have identities
over the integers. Therefore, axiom (8.13) empty range does not apply to ↓ or ↑. Also,
when using range-split axioms, no range should be false.

(15.56) Idempotency:
(a) x ↓ x = x (b) x ↑ x = x

Divisibility.
(15.77) Definition of | : c | b ≡ (∃d : c · d = b)
(15.78) c | c
(15.79) c | 0
(15.80) 1 | b
(15.80.1) −b | c ≡ b | c
(15.80.2) −1 | b

THEOREMS FROM LADM 21

(15.81) c | 1 ⇒ c = 1 ∨ c = −1
(15.81.1) c | 1 ≡ c = 1 ∨ c = −1
(15.82) d | c ∧ c | b ⇒ d | b
(15.83) b | c ∧ c | b ≡ b = c ∨ b = −c
(15.84) b | c ⇒ b | c · d
(15.85) b | c ⇒ b · d | c · d
(15.86) 1 < b ∧ b | c ⇒ ¬(b | (c + 1)) (15.87) Theorem: Given integers b, c with c > 0, there exist (unique) integers q and r

such that b = q · c + r, where 0 ≤ r < c. (15.89) Corollary: For given b, c, the values q and r of Theorem (15.87) are unique.

Greatest common divisor.
(15.90) Definition of ÷ and mod for operands b and c, c ̸= 0 :

b ÷ c = q, b mod c = r where b = q · c + r and 0 ≤ r < c (15.91) b = c ·(b ÷ c)+ b mod c for c ̸= 0 (15.92) Definition of gcd:

b gcd c = (↑ d d | b ∧ d | c : d) for b, c not both 0
0 gcd 0 = 0

(15.94) Definition of lcm :
b lcm c = (↓ k: Z+ b | k ∧ c | k : k) for b ̸= 0 and c ̸= 0
b lcm c = 0 for b = 0 or c = 0

Properties of gcd.
(15.96) Symmetry: b gcd c = c gcd b
(15.97) Associativity: (b gcd c) gcd d = b gcd (c gcd d)
(15.98) Idempotency: (b gcd b) = abs.b
(15.99) Zero: 1 gcd b = 1
(15.100) Identity: 0 gcd b = abs.b
(15.101) b gcd c = (abs.b) gcd (abs.c)
(15.102) b gcd c = b gcd (b + c) = b gcd (b − c)
(15.103) b = a · c + d ⇒ b gcd c = c gcd d
(15.104) Distributivity: d ·(b gcd c) = (d · b) gcd (d · c) for 0 ≤ d
(15.105) Definition of relatively prime ⊥ : b ⊥ c ≡ b gcd c = 1
(15.107) Inductive definition of gcd:

b gcd 0 = b
b gcd c = c gcd (b mod c)

(15.108) (∃x,y : x · b + y · c = b gcd c) for all b,c: N
(15.111) k | b ∧ k | c ≡ k | (b gcd c)

22 J. STANLEY WARFORD

Combinatorial Analysis
(16.1) Rule of sum: The size of the union of n (finite) pairwise disjoint sets is the

sum of their sizes.
(16.2) Rule of product: The size of the cross product of n sets is the product of

their sizes.
(16.3) Rule of difference: The size of a set with a subset of it removed is the size of

the set minus the size of the subset.
(16.4) Definition: P(n,r) = n!/(n − r)!
(16.5) The number of r-permutations of a set of size n equals P(n,r).
(16.6) The number of r-permutations with repetition of a set of size n is nr.
(16.7) The number of permutations of a bag of size n with k distinct elements occurring

n1,n2,…,nk times is
n!

n1! · n2! ····· nk!
.

(16.9) Definition: The binomial coefficient
(n

r

)
, which is read as “n choose r”, is

defined by
(

n
r

)
=

n!
r! ·(n − r)!

for 0 ≤ r ≤ n.

(16.10) The number of r-combinations of n elements is
(n

r

)
.

(16.11) The number
(n

r

)
of r-combinations of a set of size n equals the number of

permutations of a bag that contains r copies of one object and n − r copies of
another.

A Theory of Graphs
(19.1) Definition: Let V be a finite, nonempty set and E a binary relation on V .

Then G = ⟨V,E⟩ is called a directed graph, or digraph. An element of V is
called a vertex; an element of E is called an edge.

(19.1.1) Definitions:
(a) In an undirected graph ⟨V,E⟩, E is a set of unordered pairs.
(b) In a multigraph ⟨V,E⟩, E is a bag of undirected edges.
(c) The indegree of a vertex of a digraph is the number of edges for which it is

an end vertex.
(d) The outdegree of a vertex of a digraph is the number of edges for which it is

a start vertex.
(e) The degree of a vertex is the sum of its indegree and outdegree.
(f) An edge ⟨b,b⟩ for some vertex b is a self-loop.
(g) A digraph with no self-loops is called loop-free.

(19.3) The sum of the degrees of the vertices of a digraph or multigraph equals 2 · #E.
(19.4) In a digraph or multigraph, the number of vertices of odd degree is even.

THEOREMS FROM LADM 23

(19.4.1) Definition: A path has the following properties.
(a) A path starts with a vertex, ends with a vertex, and alternates between

vertices and edges.
(b) Each directed edge in a path is preceded by its start vertex and followed by

its end vertex. An undirected edge is preceded by one of its vertices and
followed by the other.

(c) No edge appears more than once.
(19.4.2) Definitions:

(a) A simple path is a path in which no vertex appears more than once, except
that the first and last vertices may be the same.

(b) A cycle is a path with at least one edge, and with the first and last vertices
the same.

(c) An undirected multigraph is connected if there is a path between any two
vertices.

(d) A digraph is connected if making its edges undirected results in a connected
multigraph.

(19.6) If a graph has a path from vertex b to vertex c, then it has a simple path from b to c.
(19.6.1) Definitions:

(a) An Euler path of a multigraph is a path that contains each edge of the graph
exactly once.

(b) An Euler circuit is an Euler path whose first and last vertices are the same.
(19.8) An undirected connected multigraph has an Euler circuit iff every vertex has even

degree.
(19.8.1) Definitions:

(a) A complete graph with n vertices, denoted by Kn, is an undirected, loop-
free graph in which there is an edge between every pair of distinct vertices.

(b) A bipartite graph is an undirected graph in which the set of vertices are
partitioned into two sets X and Y such that each edge is incident on one
vertex in X and one vertex in Y .

(19.10) A path of a bipartite graph is of even length iff its ends are in the same partition
element.

(19.11) A connected graph is bipartite iff every cycle has even length.
(19.11.1) Definition: A complete bipartite graph Km,n is a bipartite graph in which

one partition element X has m vertices, the other partition element Y has n
vertices, and there is an edge between each vertex of X and each vertex of Y .

(19.11.2) Definitions:
(a) A Hamilton path of a graph or digraph is a path that contains each vertex

exactly once, except that the end vertices of the path may be the same.
(b) A Hamilton circuit is a Hamilton path that is a cycle.

24 J. STANLEY WARFORD

Natural Science Division, Pepperdine University, Malibu, CA 90263
Email address: Stan.Warford@pepperdine.edu
URL: https://www.cslab.pepperdine.edu/warford/