In
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
, a collection
is subcountable if there exists a
partial
Partial may refer to:
Mathematics
* Partial derivative, derivative with respect to one of several variables of a function, with the other variables held constant
** ∂, a symbol that can denote a partial derivative, sometimes pronounced "partial ...
surjection
In mathematics, a surjective function (also known as surjection, or onto function) is a function that every element can be mapped from element so that . In other words, every element of the function's codomain is the image of one element of i ...
from the
natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
onto it.
This may be expressed as
where
denotes that
is a surjective function from a
onto
. The surjection is a member of
and here the subclass
of
is required to be a set.
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
.
Note that nomenclature of countability and finiteness properties vary substantially, historically. The discussion here concerns the property defined in terms of surjections onto the set in question.
Discussion
Example
An important case is where
denotes some subclass of a bigger class of functions as studied in
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
.
Consider the
total computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
s 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
code
In communications and information processing, code is a system of rules to convert information—such as a letter, word, sound, image, or gesture—into another form, sometimes shortened or secret, for communication through a communication ...
s of all possible partial computable functions (which also allows non-terminating programs), subsets of those, such as the total functions, are seen to be subcountable sets. Note that by
Rice's theorem
In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, does the program terminate for all inputs), unlike a synta ...
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 of a theory, subcountability may be more likely to be provable than countability.
Relation to excluded middle
In
constructive logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
s and
set theories tie the existence of a function between infinite (non-finite) sets to questions of
decidability and possibly of
effectivity. There, 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 the
separation axiom schema. Then by definition of
,
But this set may then still fail to be detachable, in the sense that
may not be provable without assuming it as an axiom.
One may fail to effectively count the subcountable set
if one fails to map the counting numbers
into the indexing set
, for this reason.
Being countable implies being subcountable. But the converse does not generally hold without asserting the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
, i.e. that for all proposition
holds
.
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 (which here shall mean that
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
) are all equivalent and express that a set is
finite
Finite is the opposite of infinite. It may refer to:
* Finite number (disambiguation)
* Finite set, a set whose cardinality (number of elements) is some natural number
* Finite verb, a verb form that has a subject, usually being inflected or marke ...
or
countably infinite
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
.
Non-classical assertions
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
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.
As
is uncountable and classically in turn provably not subcountable, the classical framework with its large function space is incompatible with the
constructive Church's thesis, an axiom of Russian constructivism.
Subcountable and ω-productive are mutually exclusive
A set
shall be called
-
productive
Productivity is the efficiency of production of goods or services expressed by some measure. Measurements of productivity are often expressed as a ratio of an aggregate output to a single input or an aggregate input used in a production proces ...
if, whenever any of its subsets
is the
range of some
partial function
In mathematics, a partial function from a set to a set is a function from a subset of (possibly itself) to . The subset , that is, the domain of viewed as a function, is called the domain of definition of . If equals , that is, if is de ...
on
, there always exists an element
that remains in the complement of that range.
If there exists any surjection onto some
, then its corresponding compliment as described would equal the empty set
, and so a subcountable set is never
-productive.
As defined above, the property of being
-productive associates the range
of any partial function to a particular value
not in the functions range. In this way, being
-productive speaks for how hard it is to generate all the elements of
: They cannot be generated using a single function. The
-productivity property produces an obstruction to subcountability. As this also implies uncountability,
diagonal arguments often involve this notion, explicitly since the late seventies.
One may establish the impossibility of computable enumerability of
by considering only the
computably enumerable
In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:
*There is an algorithm such that the ...
subsets
and one may require the set of all obstructing
's to be the image of a total recursive so called production function.
In set theory, where partial functions are modeled as collection of pairs, the space
given as
exactly holds all partial functions on
that have, as their range, only subsets
of
.
For an
-productive set
one finds
:
Read constructively, this associates any partial function
with an element
not in that functions range.
This property emphasizes the incompatibility of an
-productive set
with any surjective (possibly partial) function. Below this is applied in the study of subcountability assumptions.
Set theories
Cantorian arguments on subsets of the naturals
As reference theory we look at the
constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a co ...
CZF, which has
Replacement,
Bounded Separation, strong
Infinity
Infinity is that which is boundless, endless, or larger than any natural number. It is often denoted by the infinity symbol .
Since the time of the ancient Greeks, the philosophical nature of infinity was the subject of many discussions amo ...
, is agnostic towards the existence of
power set
In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
s, but 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.
The compatibility of various further axioms is discussed in this section by means of possible surjections on an infinite set of counting numbers
. Here
shall denote a model of the standard natural numbers.
Recall that for functions
, by definition of total functionality, there exists a unique return value for all values
in the domain,
:
and for a subcountable set, the surjection is still total on a subset of
. 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
). When as
characteristic function In mathematics, the term "characteristic function" can refer to any of several distinct concepts:
* The indicator function of a subset, that is the function
::\mathbf_A\colon X \to \,
:which for a given subset ''A'' of ''X'', has value 1 at points ...
s 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
are not automatically in bijection with all the subsets of
. 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
of all subsets of
, is shown to be a proper class.
Onto power classes
Below, the fact is used that the special case
of the
negation introduction law implies that
is contradictory.
For simplicitly of the argument, assume
is a set. Then consider a subset
and a function
. Further, as in
Cantor's theorem
In mathematical set theory, Cantor's theorem is a fundamental result which states that, for any set A, the set of all subsets of A, the power set of A, has a strictly greater cardinality than A itself.
For finite sets, Cantor's theorem can be ...
about power sets, define
where,
This is a subclass of
defined in dependency of
and it can also be written
It exists as subset via Separation. Now assuming there exists a number
with
implies the contradiction
So as a set, one finds
is
-productive in that we can define an obstructing
for any given surjection. Note that the existence of a surjection
would automatically make
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
being a set, as implied e.g. by the power set axiom.
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
.
Onto function spaces
By definition of function spaces, the set
holds those subsets of the set
which are provably total and functional.
Asserting the permitted subcountability of all sets turns, in particular,
into a subcountable set.
So here we consider a surjective function
and the subset of
separated as
with the diagonalizing predicate defined as
which we can also phrase without the negations as
This set is classically provably a function in
, designed to take the value
for particular inputs
. And it can classically be used to prove that the existence of
as a surjection is actually contradictory. However, constructively, unless the proposition
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
is permitted, and indeed models of the theory exist. Nevertheless, also in the case of CZF, the existence of a full surjection
, with domain
, is indeed contradictory. The decidable membership of
makes the set also not countable, i.e. uncountable.
Beyond these observations, also note that for any non-zero number
, the functions
in
involving the surjection
cannot be extended to all of
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
.
Note that when given a
, one cannot necessarily decide whether
, and so one cannot even decide whether the value of a potential function extension on
is already determined for the previously characterized surjection
.
The subcountibility axiom, asserting all sets are subcountable, is incompatible with any new axiom making
countable, including LEM.
Models
The above analysis affects formal properties of codings of
. Models for the non-classical extension of CZF theory by subcountability postulates have been constructed.
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.
* There are models of IZF in which all sets with
apartness relation In constructive mathematics, an apartness relation is a constructive form of inequality, and is often taken to be more basic than equality. It is often written as \# (⧣ in unicode) to distinguish from the negation of equality (the ''denial inequ ...
s are subcountable.
* CZF has a model in, for example, the
Martin-Löf type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative Foundations of mathematics, foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a ...
. In this
constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a co ...
with classically uncountable function spaces, it is indeed consistent to assert the Subcountability Axiom, saying that every set is subcountable. As discussed, the resulting theory is in contradiction to the
axiom of power set
In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory.
In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:
:\forall x \, \exists y \, \forall z \, \in y \iff \forall w \ ...
and with the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
.
* More stronger yet, some models of
Kripke–Platek set theory
The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek.
The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it.
Axioms
In its fo ...
, a theory without the function space postulate, even validate that all sets are countable.
The notion of size
As seen in the example of the function space considered in
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
, not every infinite subset of
necessarily is in constructive bijection with
, thus making room for a more refined distinction between uncountable 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
In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...
. This is what it means to be uncountable. But the argument that the
cardinality
In mathematics, the cardinality of a set is a measure of the number of elements of the set. For example, the set A = \ contains 3 elements, and therefore A has a cardinality of 3. Beginning in the late 19th century, this concept was generalized ...
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. Motivated by the above sections, the infinite set
may be considered "smaller" than the class
. Subcountability as judgement of small size shall not be conflated 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.
Related properties
Similar to subcountability, the analogous notion exists in which "
" 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
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
these notions are
subquotients.
See also
*
Cantor's diagonal argument
In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...
*
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do ...
*
Constructive set theory
Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a co ...
*
Schröder–Bernstein theorem In set theory, the Schröder–Bernstein theorem states that, if there exist injective functions and between the sets and , then there exists a bijective function .
In terms of the cardinality of the two sets, this classically implies that if ...
*
Subquotient
*
Total order
In mathematics, a total or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation \leq on some set X, which satisfies the following for all a, b and c in X:
# a \leq a ( reflexive) ...
References
Constructivism (mathematics)