is subcountable if there exists a partial surjection from the natural numbers onto it.
are functionally in the image of an indexing set of counting numbers
Note that nomenclature of countability and finiteness properties vary substantially - in part because many of them coincide when assuming excluded middle.
To reiterate, the discussion here concerns the property defined in terms of surjections onto the set
Important cases are those where the set in question is some subclass of a bigger class of functions as studied in computability theory.
For context, recall that being total is famously not a decidable property of functions.
At the same time, for some particular restrictive constructive semantics of function spaces, in cases when
In the appropriate context with Markov's principle, the converse is equivalent to the law of excluded middle, i.e. that for all proposition
Asserting all laws of classical logic, the disjunctive property of
) are all equivalent and express that a set is finite or countably infinite.
Without the law of excluded middle, it can be consistent to assert the subcountability of sets that classically (i.e. non-constructively) exceed the cardinality of the natural numbers.
Note that in a constructive setting, a countability claim about the function space
If a set is proven uncountable constructively, then in a classical context is it provably not subcountable.
, the classical framework with its large function space is incompatible with the constructive Church's thesis, an axiom of Russian constructivism.
As this also implies uncountability, diagonal arguments often involve this notion, explicitly since the late seventies.
's to be the image of a total recursive so called production function.
one finds Read constructively, this associates any partial function
As reference theory we look at the constructive set theory CZF, which has Replacement, Bounded Separation, strong Infinity, is agnostic towards the existence of power sets, but includes the axiom that asserts that any function space
The compatibility of various further axioms is discussed in this section by means of possible surjections on an infinite set of counting numbers
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
As membership in a generally defined set is not necessarily decidable, the (total) functions
into a set, via Replacement in CZF, and so this function existence is unconditionally impossible.
[3] 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.
Models for the non-classical extension of CZF theory by subcountability postulates have been constructed.
[6] Such non-constructive axioms can be seen as choice principles which, however, do not tend to increase the proof-theoretical strengths of the theories much.
) in a moderately rich set theory is always found to be neither finite nor in bijection with
But the argument that the cardinality of that set would thus in some sense exceed that of the natural numbers relies on a restriction to just the classical size conception and its induced ordering of sets by cardinality.
As seen in the example of the function space considered in computability theory, not every infinite subset of
, thus making room for a more refined distinction between uncountable sets in constructive contexts.