2LC3 Axioms and Theorems

"Identity of +":

0 + a = a

Cancellation of ·

c ≠ 0 ⇒ (c · a = c · b ≡ a = b)

Cancellation of +

a + b = a + c ≡ b = c

Subtraction of addition

a - (b + c) = (a - b) - c

Mutual associativity of + and -

a + (b - c) = (a + b) - c

Commutativity of unary minus with ·

a · (- b) = - (a · b)

Negation as multiplication

- a = (- 1) · a

Symmetry of ·

a · b = b · a

Symmetry of +

a + b = b + a

15.21

(- a) · b = a · (- b)

Associativity of ·

(a · b) · c = a · (b · c)

Associativity of +

(a + b) + c = a + (b + c)

"Identity of ·":

1 · a = a

"Distributivity of · over +":

a · (b + c) = a · b + a · c

"Zero of ·":

a · 0 = 0

"Unary minus":

a + - a = 0

"Subtraction":

a - b = a + - b

"Self-inverse of unary minus":

- (- a) = a

"Fixpoint of unary minus":

- 0 = 0

"Distributivity of unary minus over +":

- (a + b) = - a + - b

Theorem (15.20):

- a = - 1 · a

"Right-identity of -":

a - 0 = a

"ex falso quodlibet":

false ⇒ p ≡ true

"Contrapositive":

p ⇒ q ≡ ¬ q ⇒ ¬ p

"Shunting":

p ⇒ (q ⇒ r) ≡ p ∧ q ⇒ r

"Reflexivity of ⇒":

p ⇒ p

"`true` is greatest element":

p ⇒ true

"Definition of ≡":

(p ≡ q) = (p = q)

"Identity of ≡":

true ≡ (q ≡ q)

"Reflexivity of ≡":

p ≡ p

"Definition of `false`":

false ≡ ¬ true

"Commutativity of ¬ with ≡":

¬ (p ≡ q) ≡ (¬ p ≡ q)

"¬ connection":

(¬ p ≡ q) ≡ (p ≡ ¬ q)

"Double negation":

¬ (¬ p) ≡ p

"Negation of `false`":

¬ false ≡ true

"Definition of ≢":

(p ≢ q) ≡ ¬ (p ≡ q)

"Definition of ¬ from ≡":

¬ p ≡ (p ≡ false)

"Mutual associativity of ≡ with ≢":

((p ≢ q) ≡ r) ≡ (p ≢ (q ≡ r))

"Idempotency of ∨":

p ∨ p ≡ p

"Distributivity of ∨ over ≡":

p ∨ (q ≡ r) ≡ (p ∨ q ≡ p ∨ r)

"Excluded Middle" "LEM":

p ∨ ¬ p

"Zero of ∨":

p ∨ true ≡ true

"Identity of ∨":

p ∨ false ≡ p

"Distributivity of ∨ over ∨":

p ∨ (q ∨ r) ≡ (p ∨ q) ∨ (p ∨ r)

"Golden rule":

p ∧ q ≡ (p ≡ (q ≡ p ∨ q))

"Idempotency of ∧":

p ∧ p ≡ p

"Identity of ∧":

p ∧ true ≡ p

"Zero of ∧":

p ∧ false ≡ false

"Distributivity of ∧ over ∧":

p ∧ (q ∧ r) ≡ (p ∧ q) ∧ (p ∧ r)

"Contradiction":

p ∧ ¬ p ≡ false

(3.43a) "Absorption":

p ∧ (p ∨ q) ≡ p

(3.43b) "Absorption":

p ∨ (p ∧ q) ≡ p

(3.44a) "Absorption":

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

(3.44b) "Absorption":

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

(3.44c) "Absorption":

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

(3.44d) "Absorption":

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

"Distributivity of ∨ over ∧":

p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

"Distributivity of ∧ over ∨":

p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)

(3.47a) "De Morgan":

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

(3.47b) "De Morgan":

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

Theorem (3.48):

p ∧ q ≡ (p ∧ ¬ q ≡ ¬ p)

"Semi-distributivity of ∧ over ≡":

p ∧ (q ≡ r) ≡ (p ∧ q ≡ (p ∧ r ≡ p))

Theorem (3.50) "Strong modus monens for ≡":

p ∧ (q ≡ p) ≡ p ∧ q

"Replacement":

(p ≡ q) ∧ (r ≡ p) ≡ (p ≡ q) ∧ (r ≡ q)

"Definition of ⇒ via ∨":

p ⇒ q ≡ (p ∨ q ≡ q)

"Definition of ⇐" "Consequence":

p ⇐ q ≡ q ⇒ p

"Material implication":

p ⇒ q ≡ ¬ p ∨ q

"Definition of ⇒ via ∧":

p ⇒ q ≡ (p ∧ q ≡ p)

"¬-connection for ⇒":

p ⇒ ¬ q ≡ q ⇒ ¬ p

"¬-connection for ⇒":

¬ p ⇒ q ≡ ¬ q ⇒ p

Theorem (3.62):

p ⇒ (q ≡ r) ≡ (p ∧ q ≡ p ∧ r)

"Distributivity of ⇒ over ≡":

p ⇒ (q ≡ r) ≡ (p ⇒ q ≡ p ⇒ r)

"Self-distributivity of ⇒":

p ⇒ (q ⇒ r) ≡ (p ⇒ q) ⇒ (p ⇒ r)

Theorem (3.66) "Strong modus ponens": p ∧ (p ⇒ q) ≡ p ∧ q

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)

"Right-zero of ⇒":

p ⇒ true

"Left-identity of ⇒":

true ⇒ p ≡ p

"Definition of ¬ from ⇒" (3.74):

p ⇒ false ≡ ¬ p

"Weakening" "Strengthening":

p ⇒ p ∨ q

"Weakening" "Strengthening":

p ∧ q ⇒ p

"Weakening" "Strengthening":

p ∧ q ⇒ p ∨ q

"Weakening" "Strengthening":

p ∨ (q ∧ r) ⇒ p ∨ q

"Weakening" "Strengthening":

p ∧ q ⇒ p ∧ (q ∨ r)

"Modus ponens":

p ∧ (p ⇒ q) ⇒ q

"Mutual implication":

(p ⇒ q) ∧ (q ⇒ p) ≡ (p ≡ q)

"Antisymmetry of ⇒":

(p ⇒ q) ∧ (q ⇒ p) ⇒ (p ≡ q)

"Definition of · for 0":

0 · n = 0

"Definition of · for `suc`":

suc m · n = n + m · n

"Left-identity of ·":

1 · n = n

"Right-zero of ·":

m · 0 = 0

"Multiplying the successor":

m · suc n = m + m · n

"Distributivity of · over +":

(k + m) · n = k · n + m · n

"Subtraction from zero":

0 - n = 0

"Subtraction of zero from successor":

suc m - 0 = suc m

"Subtraction of successor from successor":

suc m - suc n = m - n

"Right-identity of subtraction":

m - 0 = m

"Self-cancellation of subtraction":

m - m = 0