Subcountability
In constructive mathematics, a collection is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as
where are the counting numbers ( with disregard for arithmetic) and where denotes that the intersection of and gives a total relation that is surjective. In other words, all elements of a subcountable collection are functionally in the image of an indexing set of counting numbers and thus the set can be understood as being dominated by the countable set .
Discussion
Example
An important case is where denotes some subclass of a bigger class of functions as studied in computability theory.
Consider the subclass of total functions and note that being total is not a decidable property, i.e. there cannot be a constructive bijection between the total functions and the natural numbers. However, via enumeration of the codes of all possible partial functions (which also includes non-terminating functions), subsets of those, such as the total functions, are seen to be a subcountable sets. Note that by Rice's theorem on index sets, most domains are not recursive. Indeed, no effective map between all counting numbers and the infinite (non-finite) indexing set is asserted here, merely the subset relation . Being dominated by a constructively non-countable set of numbers , the name subcountable thus conveys that the uncountable set is no bigger than .
The demonstration that is subcountable also implies that it is classically (non-constructively) formally countable, but this does not reflect any effective countability. In other words, the fact that an algorithm listing all total functions in sequence cannot be coded up is not captured by classical axioms regarding set and function existence. We see that, depending on the axioms, subcountability may be more likely to be provable than countability.
Relation to Excluded Middle
In constructive logics and set theories, which tie the existence of a function between infinite (non-finite) sets to questions of effectivity and decidability, the subcountability property splits from countability and is thus not a redundant notion. The indexing set of natural numbers may be posited to exist, e.g. as a subset via set theoretical axioms like Separation axiom, so that
- .
But this set may then still fail to be detachable, in the sense that
cannot be proven without assuming it as an axiom. One may fail to effectively count if one fails to map the counting numbers into the indexing set , for this reason.
In classical mathematics
Asserting all laws of classical logic, the disjunctive property of discussed above indeed does hold for all sets. Then, for nonempty , the properties numerable ( injects into ), countable ( has as its range), subcountable (a subset of surjects into ) and also not -productive (a countability property essentially defined in terms of subsets of , formalized below) are all equivalent and express that a set is finite or countably infinite.
Non-classical assertions
Not asserting the law of excluded middle
- for all proposition ,
it can then also 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 out of the full set , as in , may be disproven. But subcountability of an uncountable set by a set that is not effectively detachable from may be permitted.
Set theories
Into function spaces
As an example, the theory CZF has Bounded Separation, Infinity, is agnostic towards the existence of power sets, but it includes the axiom that asserts that any function space is set, given are also sets. In this theory, it is moreover consistent to assert that every set is subcountable.
Asserting the permitted subcountability of all sets, is subcountable in particular. For a function on an infinite subset of the counting numbers, , consider the set comprehended as[1]
with the diagonalizing predicate defined as
which we can also phrase without the negations as
- .
This set is classically a function in and can there be used to argue that cannot be a surjection. However, constructively, unless the propositions in its definition are decidable so that the set actually defined a functional assignment, we cannot draw this the conclusion about the surjectivity of .
For any non-zero number , the functions in cannot be extended to all of for the same reason. Note that when given a , one cannot necessarily decide whether , i.e. whether the value of a potential function extension on is already determined by . In other words, there are then partial functions that cannot be extended to full functions .
Nevertheless, even in this case, the existence of a full surjection , with domain , is indeed contradictory, since membership of is decidable.
The subcountibility axiom is incompatible with any new axiom making countable, including LEM.
Into power classes
Assuming is a set, the set violating a possible surjection , given by
where
- ,
in Cantors theorem about power sets exists via Separation and indeed immediately leads to a contradiction.[2] This demonstrates that can actually not be a set and is thus a proper class.
The two discussed situations are different in that a function makes accessible the data for all its subdomains (subsets of the superset). Naturally, in CZF, the total functions are not in bijection with the subsets of , a more involved concept. In fact, even the power set of a singleton, e.g. , is shown to be a proper class in this context (there are provably not just the two truth values and ).
The notion of size
Motivated by the above, the infinite set may be considered "smaller" than the class . Subcountability shall not be confused with the standard mathematical definition of cardinality relations as defined by Cantor, with smaller cardinality being defined in terms of injections out of and equality of cardinalities being defined in terms of bijections. Moreover, note that constructively, an ordering "" like that of cardinalities can be undecidable. As seen in the example of the function space considered in computability theory, not every infinite subset of necessarily is in constructive bijection with , thus making room for a more refined distinction between uncountabile sets in constructive contexts. The function space (and also ) in a moderately rich set theory is always found to be neither finite nor in bijection with , by Cantor's diagonal argument. This is what it means to be uncountable. 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.
Models
The above analysis affects formal properties of codings of . Models for this non-classical extension of CZF theory have been constructed.[3] 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.
More examples:
- There are models of IZF in which all sets with apartness relations are subcountable.[4]
- In CZF, as discussed, it is indeed consistent to assert the Subcountability Axiom that all sets are (internally) subcountable. The resulting theory is in contradiction to the Axiom of power set and with the law of excluded middle.
- More stronger yet, some models of Kripke-Platek set theory validate that all sets are even countable.
Subcountable implies not -productive
Any countable set is subcountable and any subcountable set is not -productive: A set is said to be -productive if, whenever any of its subsets is the range of some partial function , there always remains at least one element that lies outside that range. This may be expressed as
A set being -productive speaks for how hard it is to generate its elements: They cannot be generated using a single function. As such, -productive sets escape subcountability. Diagonal arguments often involve this notion, be it explicitly or implicitly.
See also
References
- John L. Bell "Russel's Paradox and Diagonalization in a Constructive Context"
- Daniel Méhkeri "A simple computational interpretation of set theory"
- Rathjen, M. "Choice principles in constructive and classical set theories", Proceedings of the Logic Colloquium, 2002
- McCarty, J. "Subcountability under realizability", Notre Dame Journal of Formal Logic, Vol 27 no 2 April 1986