Background Link to heading
This fun second order logic problem is given as an extra credit problem in RPI’s intro to logic class that I TA for. It is sometimes given as a required problem in the intermediate logic class. In these classes, students must use the HyperSlate graphical interactive theorem prover. Here, I take a look at a proof in Lean4 as well.
The Problem Link to heading
Given that:
For any property $X$ of an object $a$, all objects that are not $a$ do not have the property $X$. $$ \forall X: X(a) \rightarrow (\forall y: y \neq a \rightarrow \lnot X(y)) $$
$a$ has a property $Q$. $$ Q(a) $$
Prove that there exists a property $Z$ such that there do not exist any distinct objects that share that property. $$ \exists Z: \lnot \exists x, y: x \neq y \land Z(x) \land Z(y) $$
An Informal proof Link to heading
$Q$ is the property we are looking for. By hypothesis 2 we have $a$ has property $Q$. By hypothesis 1 then, we have that all objects that are not $a$ do not have $Q$, thus there do not exist any distinct objects that share the property $Q$ (as only $a$ has property $Q$). $\square$
A Formal Proof Link to heading
Take $Q$ as the property and prove by contradiction, hence we assume $\exists x, y: x \neq y \land Q(x) \land Q(y)$ and try to derive $\bot$. For existential elimination we take $w_1$ and $w_2$ as our witnesses for $x$ and $y$ and will use $w_1 \neq w_2 \land Q(w_1) \land Q(w_2)$ along with our hypotheses to prove the contradiction. By the law of excluded middle we have that either $ a = w_2 $ or $ a \neq w_2 $. In the $ a = w_2 $ case, we can use $ a = w_2 $ with hypothesis 1 to obtain $w_1 \neq w_2 \rightarrow \lnot Q(w_1)$, a contradiction follows trivially form this with $w_1 \neq w_2 \land Q(w_1) \land Q(w_2)$. In the $ a \neq w_2 $ case, we use hypothesis 1 to obtain $w_2 \neq a → \lnot Q(w_2)$, use modes ponens to obtain $\lnot Q(w_2)$ and see that this trivially contradicts with $w_1 \neq w_2 \land Q(w_1) \land Q(w_2)$. $\square$
Lean4 Proof Link to heading
We use the above formal proof as the basis for a Lean4 proof of this.
import Mathlib.Tactic.Basic
example (a : α) (Q : α -> Prop)
(H1 : ∀(X : α -> Prop), (X a) -> (∀ (y : α ), y ≠ a -> ¬X y))
(H2 : Q a) : ∃ (Z : α -> Prop), ¬ ∃(x y : α), x ≠ y ∧ Z x ∧ Z y := by
have T1 := H1 Q H2
exists Q
intro ⟨w1, w2, T2⟩
by_cases C : (a = w2)
. case pos =>
have T3 := T1 w1
rw [C] at T3
apply Not.elim (T3 T2.left) T2.right.left
. case neg =>
have T3 := T1 w2
simp [C, Ne.symm] at T3
apply Not.elim T3 T2.right.right