# Proving Cantor Theorem in Clojure Using LaTTe *[LaTTe](https://github.com/latte-central/LaTTe) is a Lisp proof assistant based on the [calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions). It is written in Clojure by [Frédéric Peschanski](https://www.lip6.fr/actualite/personnes-fiche.php?ident=P201) and exposes a powerful DSL for expressing fundamental 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. This not hard to prove on paper, indeed [just three lines](https://en.wikipedia.org/wiki/Cantor%27s_theorem#Proof), but it's pretty funny to see how LaTTe verifies the logical steps to obtain the very same proof.* This article reuses the dependencies built in [LaTTe environment](https://nextjournal.com/zampino/latte-environment). clojure id=7c17851a-2ebe-4842-a0eb-da7fa29ebedf (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]]))  LaTTe develops a [theory of sets over a type T](https://github.com/latte-central/latte-sets) as type-valued "predicates" over T denoted by (set T) and defined as: clojure id=f2c6d2a0-f4ce-4664-8912-7a3a3a86224b (clojure.repl/source set)  A **Cantor inequality** in this setting states that given a fixed type $T$ there is strictly less inhabitants of T than sets over T: $$\lvert T\rvert < \lvert (\mathsf{set}\,\,T)\rvert$$ To prove the above inequality we will exhibit an injective function from T into (set T) but we will show that there cannot be a bijection between the two. clojure id=2512b1e6-6f90-44a5-ae4a-b0edd5e9d54f (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 T into the corresponding singleton sets: clojure id=a1bb8830-590c-488b-8de1-fb59a7bea88d (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))))  clojure id=da0e6b14-29e0-46fe-ac1c-f2e3525f30d6 (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 (equal x x) :by (e/eq-refl x)) (have (elem x X) :by ) (have (set-equal X Y) :by p) (have (sets/seteq X Y) :by ((sets/set-equal-implies-seteq T X Y) )) (have (sets/subset X Y) :by (prop/and-elim-left )) (have (elem x Y) :by ( x )) (have (Y x) :by ) (have (equal y x) :by ) (have (equal x y) :by (e/eq-sym ))) (qed ))  The above results shows a first inequality $\mid T\mid \leq \mid (\mathsf{set}\,\,T)\mid$ but this inequality is indeed a strict one. **Theorem (Cantor for typed Sets)**: *Given a type* T *there exists no surjective function of* T *onto* (set T). clojure id=4e475b7d-dbaf-4213-ab07-70636109e189 (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 clojure id=e1590c9a-8557-4bcb-9500-161e001568c3 (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*.* clojure id=876ed7d0-9c3c-4429-8fda-da0477481777 (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

(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 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 absurd :by ((prop/absurd-intro (Diag t)) e <9>))) "(or (AntiDiag t) (Diag t)) is always true..." (have (==> (AntiDiag t) (AntiDiagPreimage t) absurd) :by ) (have (==> (Diag t) (AntiDiagPreimage t) absurd) :by ) (have (==> (AntiDiagPreimage t) absurd) :by (prop/or-elim (classic/excluded-middle-ax (AntiDiag t)) (==> (AntiDiagPreimage t) absurd) ))) (have (forall [t T] (==> (AntiDiagPreimage t) absurd)) :by ) (have ⚡️ absurd :by ((ex-elim AntiDiagPreimage absurd)

))) (qed ⚡️)) 

This notebook was exported from https://nextjournal.com/a/KaSsVzuqUkXj6eoiLm1Pu?change-id=CnaRgcbekxYHni5L5fBBx9 edn nextjournal-metadata {:article {:settings nil, :nodes {"2512b1e6-6f90-44a5-ae4a-b0edd5e9d54f" {:compute-ref #uuid "be65a668-b6a3-4ef7-b992-bdd361062f1b", :exec-duration 187, :id "2512b1e6-6f90-44a5-ae4a-b0edd5e9d54f", :kind "code", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "4e475b7d-dbaf-4213-ab07-70636109e189" {:compute-ref #uuid "468b2074-8148-44e3-98e3-96b87e75cf58", :exec-duration 324, :id "4e475b7d-dbaf-4213-ab07-70636109e189", :kind "code", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "7c17851a-2ebe-4842-a0eb-da7fa29ebedf" {:compute-ref #uuid "807d44b6-17ef-417c-8e1e-4246ddcc60b3", :exec-duration 5724, :id "7c17851a-2ebe-4842-a0eb-da7fa29ebedf", :kind "code", :name "ns-requires", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "876ed7d0-9c3c-4429-8fda-da0477481777" {:compute-ref #uuid "92004de0-501f-47c6-bfc1-0a0cacf0a5b3", :exec-duration 903, :id "876ed7d0-9c3c-4429-8fda-da0477481777", :kind "code", :name "Cantor proof", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "8ad7e97b-91d5-4649-be5b-9a471e396dad" {:environment [:environment {:article/nextjournal.id #uuid "0297fe65-de88-4b31-97b1-ed0d10efb902", :change/nextjournal.id #uuid "5c2f7798-ba91-4c91-bd16-e7a7d5810856", :node/id "80403b0a-1226-48ff-9bcc-624ed02e3635"}], :id "8ad7e97b-91d5-4649-be5b-9a471e396dad", :kind "runtime", :language "clojure", :name "LaTTe Cantor", :type :nextjournal}, "a1bb8830-590c-488b-8de1-fb59a7bea88d" {:compute-ref #uuid "d91bac91-7a96-4e16-8a9a-73f9ea2e76f7", :exec-duration 197, :id "a1bb8830-590c-488b-8de1-fb59a7bea88d", :kind "code", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "da0e6b14-29e0-46fe-ac1c-f2e3525f30d6" {:compute-ref #uuid "b206f5e3-52d2-44dc-b0fc-ca01642e9cd7", :exec-duration 619, :id "da0e6b14-29e0-46fe-ac1c-f2e3525f30d6", :kind "code", :name "proof-injective", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "e1590c9a-8557-4bcb-9500-161e001568c3" {:compute-ref #uuid "592636e0-4e13-4f19-a2dc-48a8af27eb12", :exec-duration 79, :id "e1590c9a-8557-4bcb-9500-161e001568c3", :kind "code", :output-log-lines {}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}, "f2c6d2a0-f4ce-4664-8912-7a3a3a86224b" {:compute-ref #uuid "0b1c421d-5014-419c-a046-285655d5433b", :exec-duration 519, :id "f2c6d2a0-f4ce-4664-8912-7a3a3a86224b", :kind "code", :name "set definition", :output-log-lines {:stdout 5}, :refs (), :runtime [:runtime "8ad7e97b-91d5-4649-be5b-9a471e396dad"]}}, :nextjournal/id #uuid "0297ffed-8be9-4785-bd59-005090713fe0", :article/change {:nextjournal/id #uuid "5f71981a-1f82-46a2-bb2e-ce24c5f94016"}}}