More Examples of Hilbert-style proofs

I give you here a couple of Hilbert-style proofs for “visual practice”. Of course, the best practice is when you prove things yourselves, not just reading other people’s proofs. By the way, I use “□” to mark the end of a proof.

A.1 “Distributivity” (This is 8.15 in the GS text).

⊢ (∀x)(A ⇒ B) ∧ (∀x)(A ⇒ C) ≡ (∀x)(A ⇒ B ∧ C)  (1)

In GS’s notation—recall the translation: (∀x|A : B) stands for (∀x)(A ⇒ B)— this is

⊢ (∀x|A : B) ∧ (∀x|A : C) ≡ (∀x|A : B ∧ C)

Taking A (range) to be the formula true we have the special case mentioned in our “Toolbox”, namely,

⊢ (∀x)B ∧ (∀x)C ≡ (∀x)(B ∧ C)  (2)

Let us prove (1). We split ≡ in two directions and use the DThm in each.

(⇒ direction)

1. (∀x)(A ⇒ B) ∧ (∀x)(A ⇒ C)  ⟨assume⟩
2. (∀x)(A ⇒ B)  ⟨1. and taut. implication⟩
3. (∀x)(A ⇒ C)  ⟨1. and taut. implication⟩
4. A ⇒ B  ⟨2. and specialization⟩
5. A ⇒ C  ⟨3. and specialization⟩
6. A ⇒ B ∧ C  ⟨4., 5. and taut. implication⟩
7. (∀x)(A ⇒ B ∧ C)  ⟨6. and generalization; OK: no free x in 1.⟩

By the Deduction Theorem, we are done.

(⇐) With amended “annotation”, the above proof can be reversed (7.–1.) □

A.2 (8.16)–(8.18) in GS boil down to just (8.18) if “∗” is “∀”. GS call (8.18) “Range split ”. This is

⊢ (∀x)(A ∨ B ⇒ C) ≡ (∀x)(A ⇒ C) ∧ (∀x)(B ⇒ C)

To prove the above we again split ≡ and use the DThm for each direction. Again we show only one direction as the other is entirely similar.

(⇒)

1. (∀x)(A ∨ B ⇒ C)  ⟨assume⟩
2. A ∨ B ⇒ C  ⟨1. and specialization⟩
3. A ⇒ C  ⟨2. and taut. implication⟩
4. B ⇒ C  ⟨2. and taut. implication⟩
5. (∀x)(A ⇒ C)  ⟨3. and generalization; OK: no free x in 1.⟩
6. (∀x)(B ⇒ C)  ⟨4. and generalization; OK: no free x in 1.⟩
7. (∀x)(A ⇒ C) ∧ (∀x)(B ⇒ C)  ⟨5., 6. and taut. implication⟩

By the Deduction Theorem, we are done. (⇐) Reverse the above proof. □

A.3 The following is a famous result of Bertrand Russell’s:

Let P be any predicate of arity 2^{∗} (this could be anything: E.g., =, <, >, ≤, ∈) Russell proved that the following is an absolute theorem (provable without any nonlogical assumptions—in particular, no axioms about P are needed)

¬(∃y)(∀x)(P (x, y) ≡ ¬P (x, x))  (3)

Now (3) is tautologically equivalent^{†} to

(∃y)(∀x)(P (x, y) ≡ ¬P (x, x)) ≡ false  (4)

and since ⊢ false ⇒ A (Why?), to show (4) I only need to show

(∃y)(∀x)(P (x, y) ≡ ¬P (x, x)) ⇒ false  (5)

I prove (5) using the DThm:

1. (∃y)(∀x)(P (x, y) ≡ ¬P (x, x))  ⟨assume⟩
2. (∀x)(P (x, z) ≡ ¬P (x, x))  ⟨by 1, add new assumption with z new⟩
3. P (z, z) ≡ ¬P (z, z)  ⟨2. and Axiom 2 (using z for “t”)⟩
4. false  ⟨3. and taut. implication⟩

To sum up “in slow motion”, the proof 1–4 establishes

1., 2. ⊢ false

∗Recall that “arity” is a word that mathematicians made up. It denotes the number of arguments that are syntactically appropriate for a function or predicate. It came from words such as “binary”, “ternary” (three argument slots), “n-ary”.

†“A is tautologically equivalent to B” means ⊧_{taut} A ≡ B.

Lecture notes in MATH2090—Fall 2003\begin{matrix}c \\ ◯ \end{matrix} George Tourlakis

But z is in neither in 1. nor in false, thus, by the Auxiliary Variable Metatheorem, we have also 1. ⊢ false. The DThm immediately gives (5). □

Why is (3) famous? Well, if you choose P to be specifically the “is a member of” predicate of set theory, “∈”, then we have—in particular—proved that

(∃y)(∀x)(x ∈ y ≡ ¬x ∈ x)  (6)

is a contradiction; or as we say refutable^{‡}.

But (6), in plain English, says “There is a set (y) whose members (x) are precisely those objects that are not members of themselves”. Russell’s result of the refutability of (6) means that no such set exists. (More on this when we do set theory).

‡The negation is provable.

Lecture notes in MATH2090—Fall 2003\begin{matrix}c \\ ◯ \end{matrix} George Tourlakis