5
$\begingroup$

In these slides of a talk Giovanni Curi shows that the generalized uniformity principle follows from Troesltra’s uniformity principle and from the subcountability of all sets, which are both claimed to be consistent with CZF. Subcountability’s consistency with CZF is not surprising in light of counterintuitive results like that subsets of finite sets aren’t necessarily finite, but it seems to have a different flavor.

What are the intuitions or motivations for subcountability?

What references prove that subcountability is consistent with CZF?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

An intuition for ESC (every set is subcountable, i.e., a subquotient of the natural numbers) in a predicative framework is that everything is built up from below starting with natural numbers, so we may assume that every set can be represented as a set of codes (natural numbers) quotiented out by an equivalence relation (denoting equality of whatever the codes represent).

For the consistency of CZF + ESC (indeed, CZF + REA + ESC), see Michael Rathjen's Choice principles in constructive and classical set theories, Thm. 8.3.

Improve this answer
$\endgroup$
2
  • $\begingroup$ How are real numbers, for example, represented as codes? I guess it’s necessary to specify the Dedekind reals since in CZF they form a set. $\endgroup$
    – ToucanIan
    Commented Dec 15, 2021 at 17:09
  • 2
    $\begingroup$ You picked about the most complicated case possible, because we need subset collection (or strong collection + fullness). In any case, looking at Rathjen's proof, you obtain the description by combining Aczel's sets-as-trees interpretation of CZF into a version of Martin-Löf type theory with one inductive type of trees, together with a recursive realizability interpretation. (The Cauchy reals also form a set and would be easier to represent directly via codes for recursive functions.) $\endgroup$
    – Ulrik Buchholtz
    Commented Dec 15, 2021 at 18:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .