Prooftoys logic theorem list
This page shows a set of basic theorems of the logic as rendered by the Prooftoys/Mathtoys system. A primary value of this page is for anyone interested in seeing proofs of these theorems. To view a proof to any desired level of detail, click on one of the bits of text displayed in blue like hyperlinks.
Furthermore, all tautologies are also theorems of the logic.
[1]x = y ≡ y = x symmetry of equality
[2]x = y and y = z ⇒ x = z transitivity of equality
[3](x ↦ p x) = p eta conversion
[4] ∀{x. T} fact
[5] ∃{x. T} fact
[6] ¬( ∀{x. F}) fact
[7] ∀p ⇒ p x fact
[8]p x ⇒ ∃p fact
[9] ∀{x. p x ⇒ q x} ⇒ ( ∀p ⇒ ∀q) fact
[10] ∀{x. p x ⇒ q x} and ∀p ⇒ ∀q fact
[11] ∀{x. p x ⇒ q x} ⇒ ( ∃p ⇒ ∃q) fact
[12] ∀{x. p x ⇒ q x} and ∃p ⇒ ∃q fact
[13] ∀{x. ∀{y. p x y}} ≡ ∀{y. ∀{x. p x y}} fact
[14] ∃{x. ∃{y. p x y}} ≡ ∃{y. ∃{x. p x y}} fact
[15] ∀{x. a or q x} ≡ a or ∀q fact
[16] ∃{x. a and q x} ≡ a and ∃q fact
[17] ∀{x. a ⇒ q x} ≡ a ⇒ ∀q fact
[18] ∀{x. a} ≡ a fact
[19] ∃{x. a} ≡ a fact
[20] ∀{x. p x and q x} ≡ ∀p and ∀q fact
[21] ∃{x. p x or q x} ≡ ∃p or ∃q fact
[22] ∀p or ∀q ⇒ ∀{x. p x or q x} fact
[23] ∃{x. p x and q x} ⇒ ∃p and ∃q fact
[24] ∀{x. p x ⇒ q} ≡ ∃p ⇒ q fact
[25] ∃p ≡ ¬( ∀{x. ¬(p x)}) fact
[26] ¬( ∃p) ≡ ∀{x. ¬(p x)} fact
[27] ∃{x. ¬(p x)} ≡ ¬( ∀p) fact
[28] ∃!p ≡ ∃{x. p = {y. y = x}} fact
[29] ∃!p ≡ ∃{x. ∀{y. p y ≡ y = x}} fact
[30] ∃!p
≡ ∃{x. p x and ∀{y. p y ⇒ y = x}} fact
≡ ∃{x. p x and ∀{y. p y ⇒ y = x}}
[31] ∃!p ⇒ (p x ≡ x = the1 p) fact
[32]p x and ∀{x1. p x1 ⇒ x1 = x}
⇒ ∃!p fact
⇒ ∃!p
[33]f x = the1 (Q x) and ∃!(Q x)
⇒ (Q x y ≡ f x = y) fact
⇒ (Q x y ≡ f x = y)