Proving Cantor's Theorem in Clojure Using LaTTe

LaTTe is a Lisp proof assistant based on the calculus of constructions. It is written in Clojure by Frédéric Peschanski and exposes a powerful DSL for expressing the basic terms of mathematical reasoning: definitions, axioms, theorems, and proofs. In this short article we're showing how LaTTe can prove — ad absurdum of course — the well known Cantor inequality using the diagonal method. In words, given a type T, there have to be strictly more sets (predicates) over T than inhabitants of T itself. This not hard to prove on paper, indeed just three lines, but it's awesome to see how LaTTe verifies the natural logical steps to obtain the very same proof.

This article reuses the dependencies built in LaTTe environment.

(ns latte-cantor (:refer-clojure :exclude [and or not set complement]) (:require [latte.core :refer [defthm defaxiom definition example lambda try-proof proof assume have pose qed type-of type-check?]] [latte-prelude.quant :refer [ex exists ex-elim] :as q] [latte-prelude.classic :as classic] [latte-prelude.prop :refer [and or not absurd] :as prop] [latte-prelude.equal :refer [equal] :as e] [latte-sets.core :refer [set elem set-equal set-equal-prop] :as sets] [latte-sets.algebra :refer [complement]]))
(clojure.repl/source set)

A Cantor inequality in this setting states that given a fixed type TTTthere is strictly less inhabitants of TTTthan sets overTTT:

T<(setT)\lvert T\rvert < \lvert (\mathsf{set}\,\,T)\rvertT<(setT)

To prove the above inequality we will exhibit an injective function from TTTinto(setT)(\mathsf{set}\,\,T)(setT)but we will show that there cannot be a bijection between the two.

(definition singleton "A singleton set consisting of the element x of T" [[T :type][x T]] (lambda [t T] (equal x t))) (type-check? [T :type][x T] (singleton T x) (set T))

A candidate for an injective function is the map which brings elements of TTTinto the corresponding singleton sets:

(definition set-injection "Given a type T we inject T into (set T)" [[T :type]] (lambda [t T] (singleton T t))) (assert (type-check? [T :type] (set-injection T) (==> T (set T)))) (defthm set-injection-injective "set injection is injective" [[T :type]] (forall [x y T] (==> (set-equal ((set-injection T) x) ((set-injection T) y)) (equal x y))))
(proof 'set-injection-injective (assume [x T y T p (set-equal ((set-injection T) x) ((set-injection T) y))] (pose X := (singleton T x)) (pose Y := (singleton T y)) (have <e> (equal x x) :by (e/eq-refl x)) (have <f> (elem x X) :by <e>) (have <g> (set-equal X Y) :by p) (have <h> (sets/seteq X Y) :by ((sets/set-equal-implies-seteq T X Y) <g>)) (have <i> (sets/subset X Y) :by (prop/and-elim-left <h>)) (have <j> (elem x Y) :by (<i> x <f>)) (have <k> (Y x) :by <j>) (have <l> (equal y x) :by <k>) (have <m> (equal x y) :by (e/eq-sym <l>))) (qed <m>))

The above results shows a first inequalityT(setT)\mid T\mid \leq \mid (\mathsf{set}\,\,T)\midT(setT)but this inequality is indeed a strict one.

Theorem (Cantor for typed Sets): Given a typeTTTthere exists no surjective function of TTTonto(setT)(\mathsf{set}\,T)(setT).

(definition section "A section of T is a map from T to sets over T" [[T :type]] (==> T (set T))) (definition section-surjective "a set-based definition for surjectivity" [[T :type][m (section T)]] (forall [s (set T)] (exists [x T] (set-equal (m x) s)))) (definition ad "Given a type T and a section m of T, the antidiagonal of m is the set of inhabitants of T which avoid the diagonal of m" [[T :type][m (section T)]] (lambda [x T] (not (elem x (m x))))) (defthm cantor-theorem "Given a type T, there is no surjective section of T." [[T :type][m (section T)]] (not (section-surjective T m)))

Let's first check that anti-diagonals have the correct type

(type-check? [T :type][m (section T)] (ad T m) (set T))

We're proving Cantor's theorem with the usual argument: since belonging to the anti-diagonal of a section m leads to a contradiction, there is no element of type T which can reach the anti-diagonal via m.

(proof 'cantor-theorem "Take the antidiagonal of T via m" (pose AntiDiag := (ad T m)) "an abstraction to claim the preimage of the anti-diagonal via m" (pose AntiDiagPreimage := (lambda [x T] (set-equal (m x) AntiDiag))) "we just call Diag the complement of the anti diagonal set" (pose Diag := (complement AntiDiag)) (assume [Hs (section-surjective T m)] "Apply surjectivity of m to the anti-diagonal of m" (have <p> (ex AntiDiagPreimage) :by (Hs AntiDiag)) "Fix an arbitrary t in T, then (AntiDiagPreimage t) leads to absurdity" (assume [t T] (pose N := (lambda [s (set T)] (not (elem t s)))) (assume [e (AntiDiag t) p (AntiDiagPreimage t)] (have <1> (not (elem t (m t))) :by e) (have <2> (not (AntiDiag t)) :by ((set-equal-prop T (m t) AntiDiag N) p <1>)) (have <abs-l> absurd :by ((prop/absurd-intro (AntiDiag t)) e <2>))) (assume [e (Diag t) p (AntiDiagPreimage t)] (have <3> (not (elem t AntiDiag)) :by e) (have <4> (set-equal AntiDiag (m t)) :by ((sets/set-equal-sym (m t) AntiDiag) p)) (have <5> (not (elem t (m t))) :by ((set-equal-prop T AntiDiag (m t) N) <4> <3>)) (have <6> (AntiDiag t) :by <5>) (have <7> (elem t AntiDiag) :by <6>) (have <8> (not (not (elem t AntiDiag))) :by ((prop/impl-not-not (elem t AntiDiag)) <7>)) (have <9> (not (Diag t)) :by <8>) (have <abs-r> absurd :by ((prop/absurd-intro (Diag t)) e <9>))) "(or (AntiDiag t) (Diag t)) is always true..." (have <left> (==> (AntiDiag t) (AntiDiagPreimage t) absurd) :by <abs-l>) (have <right> (==> (Diag t) (AntiDiagPreimage t) absurd) :by <abs-r>) (have <a> (==> (AntiDiagPreimage t) absurd) :by (prop/or-elim (classic/excluded-middle-ax (AntiDiag t)) (==> (AntiDiagPreimage t) absurd) <left> <right>))) (have <b> (forall [t T] (==> (AntiDiagPreimage t) absurd)) :by <a>) (have ⚡️ absurd :by ((ex-elim AntiDiagPreimage absurd) <p> <b>))) (qed ⚡️))