<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](https://ncatlab.org/nlab/show/Lawvere%27s+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](https://www.degruyter.com/view/j/tmj.2017.10.issue-3/tmj-2017-0107/tmj-2017-0107.xml), 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**: @username_0 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`.  

---

