Subcountability

Last updated

In constructive mathematics, a collection is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as

Contents

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 .

Discussion

Nomenclature

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 being characterized. The language here is common in constructive set theory texts, but the name subcountable has otherwise also been given to properties in terms of injections out of the set being characterized.

The set in the definition can also be abstracted away, and in terms of the more general notion may be called a subquotient of .

Example

Important cases are where the set in question is some subclass of a bigger class of functions as studied in computability theory.

There cannot be a computable surjection from onto the set of total computable functions , as demonstrated via the function from the diagonal construction, which could never be in such a surjections image. However, via the codes of all possible partial computable functions, which also allows non-terminating programs, such subsets of functions, such as the total functions, are seen to be subcountable sets: The total functions are the range of some strict subset of the natural numbers. Being dominated by an uncomputable set of natural numbers, the name subcountable thus conveys that the set is no bigger than . But in the strictest constructive semantics, when is provenly uncomputable, it is at the same time also not countable, and the same holds for . Note that no effective map between all counting numbers and the unbounded and non-finite indexing set is asserted in the definition of subcountability - merely the subset relation . Being total is famously not a decidable property of function. By Rice's theorem on index sets, most domains of indices are, in fact, not computable sets.

The demonstration that is subcountable at the same time 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 logics 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. In the appropriate context with Markov's principle, the converse is equivalent to the law of excluded middle, i.e. that for all proposition holds . In particular, constructively this converse direction does not generally hold.

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 or countably infinite.

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.

A constructive proof is also classically valid. If a set is proven uncountable constructively, then in a classical context is it provably not subcountable. As this applies to , 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 if, whenever any of its subsets is the range of some partial function on , there always exists an element that remains in the complement of that range. [1]

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, a set being -productive speaks for how hard it is to generate all the elements of it: They cannot be generated from the naturals using a single function. The -productivity property constitutes 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 subsets and one may require the set of all obstructing 's to be the image of a total recursive so called production function.

denotes the space that exactly hold all the partial functions on that have, as their range, only subsets of . In set theory, functions are modeled as collection of pairs. Whenever is a set, the set of sets of pairs may be used to characterize the space of partial functions on . The 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 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 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 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 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 about power sets, define [2]

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. Also 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.

Following the above prove makes it clear that we cannot map onto just either. Bounded separation indeed implies that no set whatsoever maps onto .

Relatedly, for any function , a similar analysis using the subset of its range shows that cannot be an injection. The situation is more complicated for function spaces. [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. [4] 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 [5]

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. [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.

The notion of size

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 and equality of cardinalities being defined in terms of bijections. Constructively, the preorder "" on the class of sets fails to be decidable and anti-symmetric. 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.

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 uncountable sets in constructive contexts. Motivated by the above sections, the infinite set may be considered "smaller" than the class .

A subcountable set has alternatively also been called subcountably indexed. 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 all these notions are subquotients.

See also

Related Research Articles

In mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

In mathematics, a topological space is called separable if it contains a countable, dense subset; that is, there exists a sequence of elements of the space such that every nonempty open subset of the space contains at least one element of the sequence.

In mathematical analysis and in probability theory, a σ-algebra on a set X is a nonempty collection Σ of subsets of X closed under complement, countable unions, and countable intersections. The ordered pair is called a measurable space.

<span class="mw-page-title-main">Probability space</span> Mathematical concept

In probability theory, a probability space or a probability triple is a mathematical construct that provides a formal model of a random process or "experiment". For example, one can define a probability space which models the throwing of a die.

<span class="mw-page-title-main">Cantor's diagonal argument</span> Proof in set theory

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 mathematical proof that there are infinite sets which cannot be put into one-to-one correspondence with the infinite set of natural numbers. Such sets are now known as uncountable sets, and the size of infinite sets is now treated by the theory of cardinal numbers which Cantor began.

In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite sets in ZF.

In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. Intuitively, forcing can be thought of as a technique to expand the set theoretical universe to a larger universe by introducing a new "generic" object .

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.

In set theory, -induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

A Dynkin system, named after Eugene Dynkin, is a collection of subsets of another universal set satisfying a set of axioms weaker than those of 𝜎-algebra. Dynkin systems are sometimes referred to as 𝜆-systems or d-system. These set families have applications in measure theory and probability.

In mathematics, a π-system on a set is a collection of certain subsets of such that

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In mathematics, a cardinal function is a function that returns cardinal numbers.

<span class="mw-page-title-main">Cartesian product</span> Mathematical set formed from two given sets

In mathematics, specifically set theory, the Cartesian product of two sets A and B, denoted A × B, is the set of all ordered pairs (a, b) where a is in A and b is in B. In terms of set-builder notation, that is

In mathematics, especially measure theory, a set function is a function whose domain is a family of subsets of some given set and that (usually) takes its values in the extended real number line which consists of the real numbers and

In mathematics, a polyadic space is a topological space that is the image under a continuous function of a topological power of an Alexandroff one-point compactification of a discrete space.

<span class="mw-page-title-main">Selection principle</span> Rule in mathematics

In mathematics, a selection principle is a rule asserting the possibility of obtaining mathematically significant objects by selecting elements from given sequences of sets. The theory of selection principles studies these principles and their relations to other mathematical properties. Selection principles mainly describe covering properties, measure- and category-theoretic properties, and local properties in topological spaces, especially function spaces. Often, the characterization of a mathematical property using a selection principle is a nontrivial task leading to new insights on the characterized property.

<span class="mw-page-title-main">Ultrafilter on a set</span> Maximal proper filter

In the mathematical field of set theory, an ultrafilter on a set is a maximal filter on the set In other words, it is a collection of subsets of that satisfies the definition of a filter on and that is maximal with respect to inclusion, in the sense that there does not exist a strictly larger collection of subsets of that is also a filter. Equivalently, an ultrafilter on the set can also be characterized as a filter on with the property that for every subset of either or its complement belongs to the ultrafilter.

References

  1. Gert Smolka, Skolems paradox and constructivism, Lecture Notes, Saarland University, Jan. 2015
  2. Méhkeri, Daniel (2010), A simple computational interpretation of set theory, arXiv: 1005.4380
  3. Bauer, A. "An injection from N^N to N", 2011
  4. Gitman, Victoria (2011), What is the theory ZFC without power set, arXiv: 1110.2430
  5. Bell, John L. (2004), "Russell's paradox and diagonalization in a constructive context" (PDF), in Link, Godehard (ed.), One hundred years of Russell's paradox, De Gruyter Series in Logic and its Applications, vol. 6, de Gruyter, Berlin, pp. 221–225, MR   2104745
  6. Rathjen, Michael (2006), "Choice principles in constructive and classical set theories" (PDF), in Chatzidakis, Zoé; Koepke, Peter; Pohlers, Wolfram (eds.), Logic Colloquium '02: Joint proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic and the Biannual Meeting of the German Association for Mathematical Logic and the Foundations of Exact Sciences (the Colloquium Logicum) held in Münster, August 3–11, 2002, Lecture Notes in Logic, vol. 27, La Jolla, CA: Association for Symbolic Logic, pp. 299–326, MR   2258712
  7. McCarty, Charles (1986), "Subcountability under realizability", Notre Dame Journal of Formal Logic, 27 (2): 210–220, doi: 10.1305/ndjfl/1093636613 , MR   0842149