Return to Answer

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• It's not clear that the Dedekind reals are even definable in CZF. (though it seems it is possible - see the comment by David roberts).

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• It's not clear that the Dedekind reals are even definable in CZF. (though it seems it is possible - see the comment by David Roberts below).

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• I don't think you can even form the set of Dedekind Reals in CZF. (or rather, I'm fairly certain you can't — but I'm not even sure what it would mean to prove this claim). So the result about CZF can't even be applied to the Dedekind real number.

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• It's not clear that the Dedekind reals are even definable in CZF. (though it seems it is possible - see the comment by David roberts).

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• I don't think you can even form the set of Dedekind Reals in CZF. (or rather, I'm fairly certain you can't — but I'm not even sure what it would mean to prove this claim). So the result about CZF can't even be applied to the Dedekind real number.

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on your classical definition of "countable" and of "the reals", it was already known that "you need LEM to show that the reals are countable". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.

A first big difference between Brauer & Hansen's result and the one you are talking about is that CZF is a predicative theory (it doesn't have power set/power object) so consistency with CZF doesn't say anything about what is possible in a topos. The internal logic of toposes has more to do with IZF, or rather something like IZF with bounded replacement. For example:

• I don't think you can even form the set of Dedekind Reals in CZF. (or rather, I'm fairly certain you can't — but I'm not even sure what it would mean to prove this claim). So the result about CZF can't even be applied to the Dedekind real number.

• The usual Cantor diagonal argument shows that it is not consistent (say in IZF or in a topos) that $\mathcal{P}(\mathbb{N})$ is subcountable (as in "is a subquotient of $\mathbb{N}$"). But $\mathcal{P}(\mathbb{N})$ doesn't exist in CZF so it's fine, but it shows that it is inconsistent with IZF that every object is subcountable.

Edit: However, as pointed out by Andrej in the comments 1 2 — that's not where the new contribution of their result lies: Independently of the result cited in the OP. It was already known that the Dedekind reals can be sub-countable in a topos (and that it is consistent with IZF) — this holds in the effective topos. So depending on which classically equivalent definition of "countable" and of "the reals" you are using, it was already known that "You cannot prove he reals are uncountable in IZF(that is ZFC without AC and LEM)". The new contribution lies in the difference between "countable" which means being a quotient of the natural numbers and "subcountable" which means "being a quotient of a subobjects of the natural numbers" or equivalently, "being a subset of a countable set". Without LEM there is a big difference between these two notions! In intuitionistic mathematics, a subset can be much more complicated that the set itself. For example, a subset of a finite set doesn't have to be finite.