Day 6: There exists
Read ∃, and see why the order of ∀ and ∃ matters.
∃ means there exists:
theorem some_big : ∃ n : Nat, n > 100 := ⟨101, ⊢ 101 > 100 All goals completed! 🐙⟩
There is a natural number n with n > 100.
To prove it, you give one example (here 101, called the witness) and show it works. The angle brackets ⟨101, …⟩ package the witness with the proof about it.
Order matters. Compare:
theorem always_bigger : ∀ n : Nat, ∃ m : Nat, m > n := fun n => ⟨n + 1, n:Nat⊢ n + 1 > n All goals completed! 🐙⟩
For every n there is some m bigger than it. (True: m can depend on n, take n + 1.)
Swap the order and you get: “there is one m bigger than every n”, ∃ m : Nat, ∀ n : Nat, m > n. That is false, since m would have to be bigger than itself. Same symbols, opposite truth.
Two patterns to remember:
-
“Every P is Q” is
∀ x, P x → Q x(with →). -
“Some P is Q” is
∃ x, P x ∧ Q x(with ∧).
Mixing them up gives statements that look right but say something silly. ∃ n : Nat, n > 100 → n = 7 is true, for a silly reason: take n = 0. Then 0 > 100 is false, and “if false then anything” is true.
theorem silly : ∃ n : Nat, n > 100 → n = 7 := ⟨0, ⊢ 0 > 100 → 0 = 7 All goals completed! 🐙⟩