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 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]]))
4.9s
ns-requiresLaTTe Cantor (Clojure)

LaTTe develops a theory of sets over a type T as type-valued "predicates" over T denoted by(setT)(\mathsf{set}\,\,T)and defined as:

(clojure.repl/source set)
0.5s
set definitionLaTTe Cantor (Clojure)

A Cantor inequality in this setting states that given a fixed type TTthere is strictly less inhabitants of TT than sets over TT:

To prove the above inequality we will exhibit an injective function from TT into (setT)(\mathsf{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))
0.2s
LaTTe Cantor (Clojure)
true

A candidate for an injective function is the map which brings elements of TT 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))))
0.3s
LaTTe Cantor (Clojure)
Vector(3) [:declared, :theorem, set-injection-injective]
(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>))
0.5s
proof-injectiveLaTTe Cantor (Clojure)
Vector(2) [:qed, set-injection-injective]

The above results shows a first inequality T(setT)\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 TT there exists no surjective function of TT onto (setT)(\mathsf{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)))
0.3s
LaTTe Cantor (Clojure)
Vector(3) [:declared, :theorem, cantor-theorem]

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

(type-check?
 [T :type][m (section T)]
 (ad T m)
 (set T))
0.1s
LaTTe Cantor (Clojure)
true

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 ⚡️))
0.8s
Cantor proofLaTTe Cantor (Clojure)
Vector(2) [:qed, cantor-theorem]
Runtimes (1)