David SchmuddeProving 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 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 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 ⚡️))