# 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. This not hard to prove on paper, indeed **just three lines**, 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.

`(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 `(set T)`

and defined as:

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

:

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.

`(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:

`(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 $\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)`

.

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