<p>Short answer: yes! You don't need that much machinery to get the proof to go through.</p>

<p>One subtlety: it seems on the face of it that there is a use of the excluded middle: one builds a set $D$ and a number $d$, and shows that either $d\in D$ or $d\not\in D$ which leads to a contradiction. But there is a lemma, <em>true</em> in intuitionistic logic, that states:</p>

<p>$$ \mbox{ for all statements } P, (P\iff \neg P) \Rightarrow \bot$$</p>

<p>This suffices, along with the usual proof. Note that in general "surjection" may have some subtle nuance in constructive/intuitionistic logic (without choice) so you have to make due with "right invertible" instead.</p>

<p>A very standard proof in Coq (which for some reason I couldn't find online) might go as follows:</p>

<pre><code>Inductive right_invertible {A B:Type}(f : A-&gt;B):Prop :=
| inverse: forall g, (forall b:B, f (g b) = b) -&gt; right_invertible f.


Lemma case_to_false :  forall P : Prop, (P &lt;-&gt; ~P) -&gt; False.
Proof.
  intros P H; apply H.
    - apply &lt;- H.
      intro p.
      apply H; exact p.
    - apply &lt;- H; intro p; apply H; exact p.
Qed.


Theorem cantor :  forall f : nat -&gt; (nat -&gt; Prop), ~right_invertible f.
Proof.
  intros f inv.
  destruct inv.
  pose (diag := fun n =&gt; ~ (f n n)).
  apply case_to_false with (diag (g diag)).
  split.
  - intro I; unfold diag in I.
    rewrite H in I. auto.
  - intro nI.
    unfold diag. rewrite H. auto.
Qed.
</code></pre>

<p>Of course, the "right" framework in which to think about these maters, which can be seen as the minimal requirements for this proof to go through, is <a href="https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem" rel="noreferrer">Lawvere's fixed point theorem</a> which states the the theorem holds in every Cartesian Closed Category (so in particular, in any reasonable type theory).</p>

<p>Andrej Bauer writes beautifully about this theorem in the paper <a href="https://www.degruyter.com/view/j/tmj.2017.10.issue-3/tmj-2017-0107/tmj-2017-0107.xml" rel="noreferrer">On fixed-point theorems in synthetic computability</a>, and I suspect might have some interesting things to add to this answer.</p>

CC BY-SA 3.0
2018-02-09T04:20:58.727Z
If I understand correctly, in your definition of `cantor`, `nat` plays the role of "any set A" and `nat -> Prop` plays the role of "the set of all subsets of A". What would be the implications of replacing `nat -> Prop` with `nat -> bool`? I guess using `Prop` is more appropriate in constructive logic, but classical logic and set theory often assume excluded middle, so we should be able to replace `Prop` with `bool` and still be able to prove the theorem, right?
Paula Vega
CC BY-SA 3.0
2018-02-09T12:09:46.843Z
Yes, replacing Prop with bool works fine using the negation map. Lawvere's fixed point theorem shows you can do it with any type A that has a map A -> A with no fixed points, so a type with 3 elements or type of all natural numbers also work
Max New
CC BY-SA 3.0
2018-02-09T13:20:47.627Z
@PaulaVega Max pretty much says it all, but I recommend playing around with the example, e.g. using `bool` instead of `Prop` and `nat` and `diag := fun b => negb (f b b)`, or just replacing `Prop` with `nat` and using `diag := fun n => (f b b) + 1`.
cody
CC BY-SA 3.0
2018-02-09T01:42:22.100Z
2018-02-09T01:42:22.100Z
cody
<p>Cantor's theorem states that </p>

<blockquote>
  <p>For any set A, the set of all subsets of A has a strictly greater cardinality than A itself.</p>
</blockquote>

<p>Is it possible to encode something like this using only types / propositions without referring to ZFC sets? Code or pseudocode for encoding this proposition in a dependently typed language would be appreciated.</p>

<type-theory><set-theory>
Cantor's theorem in type theory
Paula Vega
# Cantor's theorem in type theory

(Asked by: username_0 on 2018-02-08)

Cantor's theorem states that

> For any set A, the set of all subsets of A has a strictly greater cardinality than A itself.

Is it possible to encode something like this using only types / propositions without referring to ZFC sets? Code or pseudocode for encoding this proposition in a dependently typed language would be appreciated.

**Tags:** type-theory, set-theory


---

## 1 answers

### Answer by username_1 on 2018-02-09. Score: 9 | Accepted answer

Short answer: yes! You don't need that much machinery to get the proof to go through.
One subtlety: it seems on the face of it that there is a use of the excluded middle: one builds a set $D$ and a number $d$, and shows that either $d\in D$ or $d\not\in D$ which leads to a contradiction. But there is a lemma, true in intuitionistic logic, that states:
$$ \mbox{ for all statements } P, (P\iff \neg P) \Rightarrow \bot$$
This suffices, along with the usual proof. Note that in general "surjection" may have some subtle nuance in constructive/intuitionistic logic (without choice) so you have to make due with "right invertible" instead.
A very standard proof in Coq (which for some reason I couldn't find online) might go as follows:
Inductive right_invertible {A B:Type}(f : A->B):Prop :=
| inverse: forall g, (forall b:B, f (g b) = b) -> right_invertible f.


Lemma case_to_false :  forall P : Prop, (P <-> ~P) -> False.
Proof.
  intros P H; apply H.
    - apply <- H.
      intro p.
      apply H; exact p.
    - apply <- H; intro p; apply H; exact p.
Qed.


Theorem cantor :  forall f : nat -> (nat -> Prop), ~right_invertible f.
Proof.
  intros f inv.
  destruct inv.
  pose (diag := fun n => ~ (f n n)).
  apply case_to_false with (diag (g diag)).
  split.
  - intro I; unfold diag in I.
    rewrite H in I. auto.
  - intro nI.
    unfold diag. rewrite H. auto.
Qed.

Of course, the "right" framework in which to think about these maters, which can be seen as the minimal requirements for this proof to go through, is Lawvere's fixed point theorem which states the the theorem holds in every Cartesian Closed Category (so in particular, in any reasonable type theory).
Andrej Bauer writes beautifully about this theorem in the paper On fixed-point theorems in synthetic computability, and I suspect might have some interesting things to add to this answer.

> **Comments:**
> **username_0**: If I understand correctly, in your definition of `cantor`, `nat` plays the role of "any set A" and `nat -> Prop` plays the role of "the set of all subsets of A". What would be the implications of replacing `nat -> Prop` with `nat -> bool`? I guess using `Prop` is more appropriate in constructive logic, but classical logic and set theory often assume excluded middle, so we should be able to replace `Prop` with `bool` and still be able to prove the theorem, right?  
> **username_2**: Yes, replacing Prop with bool works fine using the negation map. Lawvere's fixed point theorem shows you can do it with any type A that has a map A -> A with no fixed points, so a type with 3 elements or type of all natural numbers also work  
> **username_1**: @PaulaVega Max pretty much says it all, but I recommend playing around with the example, e.g. using `bool` instead of `Prop` and `nat` and `diag := fun b => negb (f b b)`, or just replacing `Prop` with `nat` and using `diag := fun n => (f b b) + 1`.  

---

