2LC3 Axioms and Theorems

"Identity of +":

0 + a = a

"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

"Subtraction after addition":

(m + n) - n = m

"Subtraction from multiplication with successor":

m · suc n - m = m · n

"Subtraction of sum":

k - (m + n) = (k - m) - n

"Distributivity of · over subtraction":

k · (m - n) = k · m - k · n

Axiom (3.83) "Leibniz":

e = f ⇒ E[z ≔ e] = E[z ≔ f]

(3.84a) "Replacement":

e = f ∧ E[z ≔ e] ≡ e = f ∧ E[z ≔ f]

(3.84b) "Replacement":

e = f ⇒ E[z ≔ e] ≡ e = f ⇒ E[z ≔ f]

"Zero is not successor":

0 = suc n ≡ false

"Cancellation of `suc`":

suc m = suc n ≡ m = n

"Cancellation of +":

k + m = k + n ≡ m = n

"Zero sum":

0 = a + b ≡ 0 = a ∧ 0 = b