Subcountability

In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq{\mathbb N}).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twoheadrightarrow X denotes that f is a surjective function from I onto X . The surjection is a member of {\mathbb N}\rightharpoonup X and here the subclass I of {\mathbb N} is required to be a set. In other words, all elements of a subcountable collection X are functionally in the image of an indexing set of counting numbers I\subseteq{\mathbb N} and thus the set X can be understood as being dominated by the countable set {\mathbb N} .

In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq{\mathbb N}).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twoheadrightarrow X denotes that f is a surjective function from I onto X . The surjection is a member of {\mathbb N}\rightharpoonup X and here the subclass I of {\mathbb N} is required to be a set. In other words, all elements of a subcountable collection X are functionally in the image of an indexing set of counting numbers I\subseteq{\mathbb N} and thus the set X can be understood as being dominated by the countable set {\mathbb N} . \forall (i\in I). (i\in{\mathbb N}). But this set may then still fail to be detachable, in the sense that \forall (n\in {\mathbb N}). \big((n\in I) \lor \neg(n\in I)\big) may not be provable without assuming it as an axiom. One may fail to effectively count the subcountable set X if one fails to map the counting numbers {\mathbb N} into the indexing set I , for this reason. Being countable implies being subcountable. In the appropriate context with Markov's principle, the converse is equivalent to the law of excluded middle, i.e. that for all proposition \phi holds \phi\lor \neg \phi . In particular, constructively this converse direction does not generally hold. \exists!(y\in Y). g(x)=y, and for a subcountable set, the surjection is still total on a subset of {\mathbb N} . Constructively, fewer such existential claims will be provable than classically. The situations discussed below—onto power classes versus onto function spaces—are different from one another: Opposed to general subclass defining predicates and their truth values (not necessarily provably just true and false), a function (which in programming terms is terminating) does makes accessible information about data for all its subdomains (subsets of the X ). When as characteristic functions for their subsets, functions, through their return values, decide subset membership. As membership in a generally defined set is not necessarily decidable, the (total) functions X\to\{0,1\} are not automatically in bijection with all the subsets of X . So constructively, subsets are a more elaborate concept than characteristic functions. In fact, in the context of some non-classical axioms on top of CZF, even the power class of a singleton, e.g. the class {\mathcal P}\{0\} of all subsets of \{0\} , is shown to be a proper class. ====Onto power classes==== Below, the fact is used that the special case (P\to \neg P)\to\neg P of the negation introduction law implies that P\leftrightarrow \neg P is contradictory. For simplicitly of the argument, assume {\mathcal P}{\mathbb N} is a set. Then consider a subset I\subseteq{\mathbb N} and a function w\colon I\to{\mathcal P}{\mathbb N} . Further, as in Cantor's theorem about power sets, define d=\{k \in {\mathbb N}\mid k\in I \land D(k)\} where, D(k)=\neg (k\in w(k)). This is a subclass of {\mathbb N} defined in dependency of w and it can also be written d=\{k \in I\mid \neg (k\in w(k))\}. It exists as subset via Separation. Now assuming there exists a number n\in I with w(n)=d implies the contradiction n\in d\,\leftrightarrow\,\neg(n\in d). So as a set, one finds {\mathcal P}{\mathbb N} is \omega -productive in that we can define an obstructing d for any given surjection. Also note that the existence of a surjection f\colon I\twoheadrightarrow{\mathcal P}{\mathbb N} would automatically make {\mathcal P}{\mathbb N} into a set, via Replacement in CZF, and so this function existence is unconditionally impossible. We conclude that the subcountability axiom, asserting all sets are subcountable, is incompatible with {\mathcal P}{\mathbb N} being a set, as implied e.g. by the power set axiom. Following the above prove makes it clear that we cannot map I onto just {\mathcal P}I either. Bounded separation indeed implies that no set X whatsoever maps onto {\mathcal P}X . Relatedly, for any function h\colon{\mathcal P}Y\to Y , a similar analysis using the subset of its range \{y\in Y\mid \exists(S\in{\mathcal P}Y). y=h(S)\land y\notin S\} shows that h cannot be an injection. The situation is more complicated for function spaces. In classical ZFC without Powerset or any of its equivalents, it is also consistent that all subclasses of the reals which are sets are subcountable. In that context, this translates to the statement that all sets of real numbers are countable. Of course, that theory does not have the function space set {\mathbb N}^{\mathbb N} . ====Onto function spaces==== By definition of function spaces, the set {\mathbb N}^{\mathbb N} holds those subsets of the set {\mathbb N}\times{\mathbb N} which are provably total and functional. Asserting the permitted subcountability of all sets turns, in particular, {\mathbb N}^{\mathbb N} into a subcountable set. So here we consider a surjective function f\colon I\twoheadrightarrow{\mathbb N}^{\mathbb N} and the subset of {\mathbb N}\times{\mathbb N} separated as \Big\{\langle n, y\rangle \in {\mathbb N}\times{\mathbb N} \mid \big(n\in I\land D(n, y)\big) \lor \big(\neg(n\in I)\land y=1\big)\Big\} with the diagonalizing predicate defined as D(n, y) = \big(\neg(f(n)(n)\ge 1)\land y=1\big) \lor \big(\neg(f(n)(n)=0)\land y=0\big) which we can also phrase without the negations as D(n, y) = \big(f(n)(n)=0\land y=1\big) \lor \big(f(n)(n)\ge 1\land y=0\big). This set is classically provably a function in {\mathbb N}^{\mathbb N} , designed to take the value y=0 for particular inputs n . And it can classically be used to prove that the existence of f as a surjection is actually contradictory. However, constructively, unless the proposition n\in I in its definition is decidable so that the set actually defined a functional assignment, we cannot prove this set to be a member of the function space. And so we just cannot draw the classical conclusion. In this fashion, subcountability of {\mathbb N}^{\mathbb N} is permitted, and indeed models of the theory exist. Nevertheless, also in the case of CZF, the existence of a full surjection {\mathbb N}\twoheadrightarrow{\mathbb N}^{\mathbb N} , with domain {\mathbb N} , is indeed contradictory. The decidable membership of I={\mathbb N} makes the set also not countable, i.e. uncountable. Beyond these observations, also note that for any non-zero number a , the functions i\mapsto f(i)(i)+a in I\to{\mathbb N} involving the surjection f cannot be extended to all of {\mathbb N} by a similar contradiction argument. This can be expressed as saying that there are then partial functions that cannot be extended to full functions in {\mathbb N}\to{\mathbb N} . Note that when given a n\in{\mathbb N} , one cannot necessarily decide whether n\in I , and so one cannot even decide whether the value of a potential function extension on n is already determined for the previously characterized surjection f . The subcountibility axiom, asserting all sets are subcountable, is incompatible with any new axiom making I countable, including LEM. ==Related properties== A subcountable set has alternatively also been called subcountably indexed. The analogous notion exists in which " \exists(I\subseteq{\mathbb N}) " in the definition is replaced by the existence of a set that is a subset of some finite set. This property is variously called subfinitely indexed. In category theory all these notions are subquotients. ==See also== Cantor's diagonal argument Computable function Constructive set theory Schröder–Bernstein theorem Subquotient Total order

Text derived from https://en.wikipedia.org/w/index.php?oldid=1353262140 under CC BY-SA 4.0; modifications have been made.