# Proving Cantor 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 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 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]]))

LaTTe develops a theory of sets over a type T as type-valued "predicates" over T denoted by

(clojure.repl/source set)

A **Cantor inequality** in this setting states that given a fixed type

To prove the above inequality we will exhibit an injective function from

(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

(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 inequality

**Theorem (Cantor for typed Sets)**:** ***Given a type**there exists no surjective function of *

(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 ⚡️))