Constructive set theory on arvau

Wikipedia / Constructive set theory

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order" 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 addition to rejecting the principle of excluded middle), constructive set theories often require some logical quantifiers in their axioms to be set bounded. The latter is motivated by results tied to impredicativity.

Introduction

Constructive outlook

In constructive mathematical theories, one is commonly unable to prove the existence of relations that cannot be realized. Nonetheless, such theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

involving unbounded collections constitute a (mathematical, and so always meaning total) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Adopting the standard definition of set equality via extensionality, the full Axiom of Choice for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity existence claim, as shown below. The latter has a classically equivalent inductive substitute. So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which non-logical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.

Metalogic

With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets. Also the real line may be taken to be indecomposable in this sense. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers. This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.

In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numbers, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.

that uniquely so that

The role analogous to that of realized numbers in arithmetic is played here by defined sets proven to exist by (or according to) the theory. Questions concerning the axiomatic set theory's strength and its relation to term construction are subtle. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.

Some theories with a classical reading of existence can in fact also be constrained so as to exhibit the strong existence property. In Zermelo–Fraenkel set theory with sets all taken to be ordinal-definable, no sets without such definability exist. The property is also enforced via the constructible universe plus the full axiom of choice existence postulate: Recall that this collection of axioms proves the well-ordering theorem with respect to those relations). This is despite the fact that definability of such an ordering is known to be independent formally proves the existence for which the property could be validated can possibly be defined.

Anti-classical principles

is closed under that rule.

, as an axiom schema is a number variable in language of the theory. For example, Church's rule is an admissible rule and, furthermore, the corresponding Church's thesis principle, also known as Peano arithmetic.

The focus in this subsection shall be on set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function space, as it will be introduced further below. A translation of Church's rule into the language of the theory itself may here read

Kleene's T predicate is the index of a computable function halting, but which still make principles inconsistent that claim the existence of functions which provenly have no recursive realization. Some forms of a Church's thesis as principle are even consistent with the classical, weak so called second-order arithmetic, a subsystem of the two-sorted.

The collection of computable functions is classically subcountable that total functions (in the set theory sense) do exist that cannot be captured by a Turing machine) as an axiom in a constructive theory, the "smallness" (in classical terms) of this collection, in some set theoretical realizations, is then already captured by the theory itself. A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.

correspond to decision problems. Motivated by provenly computably undecidable problems. As another example, such a situation is enforced in Brouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle strictly rules out that this could be proven decidable for all the sequences.

So in a constructive context with a so-called non-classical logic as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also non-constructive in the computable sense or as gauged by meta-logical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study non-classical theories, say rings modeling smooth infinitesimal analysis.

History and overview

") begun with John Myhill. is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics.

, leading up to Peter Aczel's well studied , is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical general topology, as detailed below., but less conservative or predicative, the classical Kripke–Platek set theory without a form of Powerset and where even the Axiom of Collection is bounded.

Models, interpretations and realizations

Many theories studied in constructive set theory are mere restrictions of {\mathsf{ZF}}).

Comparing arithmetics with theories in the language of set theory on the one end, classical Peano arithmetic is bi-interpretable minus Infinity and without infinite sets, plus the existence of all transitive closures. (The latter is also implied after promoting Regularity to the Set Induction schema: Heyting arithmetic is bi-interpretable with a weak constructive set theory, - that all sets in its theory are in bijection with a (finite) von Neumann natural. This context further validates Extensionality, Pairing, Union, Binary Intersection (which is related to the Axiom schema of predicative separation also proves that the hereditarily finite sets plus full Separation is not stronger than classical second-order arithmetic.

As far as constructive realizations go there is a relevant realizability has been interpreted in a Martin-Löf type theories. In this way, theorems provable in this and weaker set theories are candidates for a computer realization.

Presheaf models for constructive set theories have also been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott in the 1980s. within the effective topos, independence of premise in the formulation for all predicates.

ECST

. Later, it is highlighted which non-classical axioms are, in turn, consistent.

In set theory, the Elementary Constructive Set Theory is a constructive subtheory of Zermelo–Fraenkel set theory. Using only bounded Separation, the theory is conservatively designed so that it can also be considered predicative.

allows for the native operations of set union as well as set intersection. Unlike Kripke-Platek set theory, it adopts the axiom of replacement but not epsilon induction, but has no classically uncountable ones. The theory also still fails to model operations of Heyting arithmetic. The section's text concludes by detailing the relation of further set theoretical principles to primitive recursion, which enables these operations.

Over intuitionistic logic plus the powerset axiom, when further adding the strictly classical combination of full separation and the axiom of regularity.

Notation

In an axiomatic set theory, sets are the entities exhibiting properties. But there is then a more intricate relation between the set concept and logic. For example, the property of being a natural number smaller than 100 may be reformulated as being a member of the set of numbers with that property. The set theory axioms govern set existence and thus govern which predicates can be materialized as entity in itself, in this sense. Specification is also directly governed by the axioms, as discussed below. For a practical consideration, consider for example the property of being a sequence of coin flip outcomes that overall show more heads than tails. This property may be used to separate out a corresponding subset of any set of finite sequences of coin flips. Relatedly, the measure theoretic formalization of a probabilistic event is explicitly based around sets and provides many more examples.

This section introduces the object language and auxiliary notions used to formalize this materialization.

Language

The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality" of sets and that symbol may, by abuse of notation, be used for classes. A set in which the equality predicate is decidable is also called discrete". However, in a context with apartness relations, for example when dealing with sequences, the latter symbol is also sometimes used for something different.

Variables

denotes a proposition or predicate variable in axiom schemas is used for particular such predicates. The word "predicate" is sometimes used interchangeably with "formulas" as well, even in the unary case.

". Unique existence.

Classes

As is also common, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class.

. The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemas, as seen in the discussion of axioms below. Express the subclass, has been used in set theoretical investigation as well, but will not be further highlighted here.

If there provenly exists, then one calls it inhabited is then provenly not the empty set, introduced below. While classically equivalent, constructively non-empty is a weaker notion with two negations and ought to be called not uninhabited. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics.

Two ways to express that classes are disjoint.

is called detachable holds. It is also called decidable if the superclass is clear from the context - often this is the set of natural numbers.

Extensional equivalence

. This is not to be conflated with the concept of equinumerosity also used below.

postulate that the class holds actually forms a set as a set.

", and so on.

itself.

On the use of intuitionistic logic

The logic of the set theories discussed here is constructive, i.e. that the disjunction. This is also often called the law (resp. the statement using the quantifier above) without demonstrating the truth of either side of the disjunction(s). This is often the case in classical logic. In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable.

The law of noncontradiction is a special case of the propositional form of modus ponens, one valid De Morgan's law already in the more conservative minimal logic. In words, intuitionistic logic) from the assumed axioms.

The intuitionistic logic underlying the set theories discussed here, unlike minimal logic, still permits double negation elimination for which excluded middle holds. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.

In an inhabited domain and using explosion would logically lead to a contradiction without the aid of a specific counter-example, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.

Equality

" of two sets. By the logical properties of equality, the converse direction of the postulated implication holds automatically.. And (unless the whole disjunction follows from axioms) in the Brouwer–Heyting–Kolmogorov interpretation may be not decidable must a priori be distinguished.

for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the right hand side is judged equal to the one on the left hand side.

, in any formula.

" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.

Alternative approaches

While often adopted, this axiom has been criticized in constructive thought, as it effectively collapses differently defined properties, or at least the sets viewed as the extension of these properties, a Fregian notion.

" in terms of functions, see e.g. type equivalence. The related concept of function extensionality is often not adopted in type theory.

Other frameworks for constructive mathematics might instead demand a particular rule for equality or apartness" of those subsets. Relatedly, a loose notion of complementation of two subsets is algebraically well behaved.

Merging sets

, and so on.

Two other basic existence postulates given some other sets are as follows. Firstly,, which hold at least those two sets.

the standard ordered pair denotes another bounded formula in the formal language of the theory.

And then, using existential quantification and a conjunction,. The minimal such set is the union.

is an existential statement, like here in the union axiom, there is also another formulation using a universal quantifier.

. This goes to show that partitioning is also a more involved notion, constructively.

Set existence

The property that is false for any set corresponds to the empty. That the empty class is a set readily follows from other existence axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the.

have no urelements, as characterized by the extensionality axiom above.

Successor sets

" and logical symbols, including quantifiers. Accompanied by a metamathematical analysis that the capabilities of the new theories are equivalent in an effective manner, formal extensions may also be considered.

, define the successor set is always inhabited.

BCST

The following makes use of axiom schemas).

Separation

consists of several axioms also part of standard set theory, except the so-called "full" Separation axiom is weakened. Beyond the four axioms above, it postulates Predicative Separation as well as the Replacement schema. obtained by the intersection. Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction.

, the Predicative Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a formula schema.

, the lowest level in the set theoretical Lévy hierarchy. General predicates in set theory are never syntactically restricted in such a way and so, in praxis, generic subclasses of sets are still part of the mathematical language. As the scope of subclasses that are provably sets is sensitive to what sets already exist, this scope is expanded when further set existence postulates are added.

is decided either way through establishing how.

is a subset, which may be called the truth value.

No universal set

When using the informal class terminology, any set is also considered a class. At the same time, there do arise so called proper on sets, a theory which has full Separation, proper classes are generally thought of as those that are "too big" to be a set. More technically, they are subclasses of the cumulative hierarchy that extend beyond any ordinal bound.)

is empty, i.e. when the right side is the universal class. Being negative results, it reads as in the classical theory.

-related to one another.

does not involve unbounded quantification and is thus allowed in Separation. Russel's construction. In particular, no universal set can exist in this theory.

In a theory further adopting the axiom of regularity is the empty set.

in the formula above gives

without Regularity it is consistent for there to be a proper class of singletons which each contain exactly themselves.

As an aside, in a theory with stratification like Intuitionistic New Foundations may be disallowed in Separation. In turn, the above proof of negation of the existence of a universal set cannot be performed, in that theory.

Predicativity

-Separation or Bounded Separation, as in Separation for set-bounded quantifiers in the arithmetical hierarchy classification of a formula may be expressed up to equivalence in the theory.)

The schema is also the way in which Mac Lane weakens a system close to Zermelo set theory, for mathematical foundations related to topos theory. It is also used in the study of absoluteness, and there part of the formulation of Kripke-Platek set theory.

The restriction in the axiom is also gatekeeping impredicative definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without Axiom of power set to be a set, in case that it is defined, for example, as in

, would play a role in its own characterization.

While predicative Separation leads to fewer given class definitions being sets, it may be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to the weaker logic. Due to the potential undecidability, which however spoils the existence property as well as the standard type theoretical interpretations, and in this way spoils a bottom-up view of constructive sets. As an aside, as subtyping is not a necessary feature of constructive type theory, constructive set theory can be said to quite differ from that framework.

Replacement

Next consider theIt is granting existence, as sets, of the range of function-like predicates, obtained via their domains. In the above formulation, the predicate is not restricted akin to the Separation schema, but this axiom already involves an existential quantifier in the antecedent. Of course, weaker schemas could be considered as well.

can also be demonstrated using Separation.

With the Replacement schema, the theory outlined thus far proves that the equivalence classes or indexed sums are sets. In particular, the Cartesian product is decidable.

Replacement is relevant for function comprehension and can be seen as a form of comprehension more generally. Only when, Replacement is mostly important to prove the existence of sets of high rank.

, but instead merely to gain back some provability strength. Such stronger axioms exist that do not spoil the strong existence properties of a theory, as discussed further below.

(all discussed in detail below), then the image. In other approaches to the set concept, the notion of subsets is defined in terms of "operations", in this fashion.

Hereditarily finite sets

Pendants of the elements of the class of hereditarily finite sets can be implemented in any common programming language. The axioms discussed above abstract from common operations on the set data type: Pairing and Union are related to nesting and flattening, or taken together concatenation. Replacement is related to comprehension and Separation is then related to the often simpler filtering. Replacement together with Set Induction constructively and that theory is also studied without Infinity.

A sort of blend between pairing and union, an axiom more readily related to the successor is the Axiom of adjunction. Such principles are relevant for the standard modeling of individual Neumann ordinals, some form of induction is. For comparison, consider the very weak classical theory called General set theory that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation.

The discussion now proceeds with axioms granting existence of objects which, in different but related form, are also found in dependent type theories, namely products and the collection of natural numbers as a completed set. Infinite sets are particularly handy to reason about operations applied to sequences defined on unbounded index domains, say the formal differentiation of a generating function or the addition of two Cauchy sequences.

ECST via Strong Infinity

. The aim of the axiom of infinity is to eventually obtain unique smallest inductive set.

In the context of common set theory axioms, one statement of infinitude is to state that a class is inhabited and also includes a chain of membership (or alternatively a chain of supersets). That is,

the inductive property,

, but we only use this notion for the following auxiliary definition.)

to be the desired set, the language here forms the basis for the following axiom, granting natural number induction for predicates that constitute a set.

as well as the postulate to denote the now unique smallest inductive set, an unbounded von Neumann ordinal that contains one element more.

Symbols called zero and successor are in the signature of the theory of Peano follow directly from the characterization of the natural naturals by our von Neumann model. Since the successor of such a set contains itself, one also finds that no successor equals zero. So two of the Peano axioms can be proven to be an injective operation.

holds for all subsets of the set of naturals. And the axiom now proves such sets do exist. Such quantification is also possible in second-order arithmetic.

". The theory proves the order as well as the equality relation on this set to be decidable. Not only is no number, it is exactly the empty set which has no least member. The contrapositive of this proves the double-negated least number existence to be well-ordered.

Weaker formulations of infinity

predecessor existence property in the sense of the von Neumann model:

, no two different sets have this property. Also note that there are also longer formulations" in favor unbounded quantifiers.

Number bounds

bounded if the following existence statement holds

-statements in arithmetic, but with the Axiom of Infinity, the two quantifiers are set-bound.

, the logically positive unboundedness statement

Moderate induction in ECST

" is mere notation for its predecessor (i.e. not involving subtraction function).

as a theorem may not be possible. The set theory can thus be strengthened by more set existence axioms, to be used with predicative bounded-statements.

. The so-called axiom of full mathematical induction are sets. Mathematical induction is also superseded by the (full) Set induction axiom.

Warning note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The first-order induction schema of natural number arithmetic theory claims induction for all predicates definable in the language of first-order arithmetic, one interprets these arithmetical formulas. In that context, the bounded quantification, in a form explicitly expressed for subsets of the naturals. That class of subsets can be taken to correspond to a richer collection of formulas than the first-order arithmetic definable ones. In the program of reverse mathematics with very low complexity comprehension studied in that framework have a language that does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Theorems therein can be a relevant reference point for weak set theories with a set of naturals, predicative separation and only some further restricted form of induction. Constructive reverse mathematics exists as a field but is less developed than its classical counterpart.. Typical set theories like the one discussed here are also first-order, but those theories are not arithmetics and so formulas may also quantify over the subsets of the naturals. When discussing the strength of axioms concerning numbers, it is also important to keep in mind that the arithmetical and the set theoretical framework do not share a common signature. Likewise, care must always be taken with insights about totality of functions. In computability theory, the μ operator enables all partial general recursive functions-total, such as the Ackermann function. The definition of the operator involves predicates over the naturals and so the theoretical analysis of functions and their totality depends on the formal framework and proof calculus at hand.

Functions

General note on programs and functions

express a property such that a mathematical framework validates what amounts to the statement

(a unique. Expressed through the rewriting, this function object may be understood as witnessing the proposition. Consider for example the notions of proof in through realizability theory or function terms in a type theory with a notion of quantifiers. The latter captures proof of logical proposition through programs via the Curry–Howard correspondence.

Depending on the context, the word "function" may be used in association with a particular model of computation, and this is a priori narrower than what is discussed in the present set theory context. One notion of program is formalized by partial recursive "functions" in computability theory. But beware that here the word "function" is used in a way that also comprises partial functions, and not just "total functions". The scare quotes are used for clarity here, as in a set theory context there is technically no need to speak of total functions, because this requirement is part of the definition of a set theoretical function and partial function spaces can be modeled via unions. At the same time, when combined with a formal arithmetic, partial function programs provides one particularly sharp notion of totality for functions. By Kleene's normal form theorem. Kreisel is added., this totality constitutes an undecidable. As a third warning, note that this notion is really about programs and several indices will in fact constitute the same function, in the extensional sense.

A theory in first-order logic, such as the axiomatic set theories discussed here, comes with a joint notion of total and functional (the number three), may metalogically, classical Robinson arithmetic exactly fulfills this. Its existence claims are intended to only concern natural numbers and instead of using the full mathematical induction represents) prove the graph to be total functional.

Which predicates are provably functional for various inputs, or even total functional on their domain, generally depends on the adopted axioms of a theory and proof calculus. For example, for the diagonal halting problem (a decision problem implies that it is. Proof theoretical function hierarchies. Which sets proven to exist do constitute a total function, in the sense introduced next, also always depends on the axioms and the proof calculus. Finally, note that the soundness of halting claims is a metalogical property beyond consistency, i.e. a theory may be consistent and from it one may prove that some program will eventually halt, despite this never actually occurring when said program is run. More formally, assuming consistency of a theory does not imply it is also arithmetically \Sigma_1-sound.

Total functional relations

In set theory language here, speak of a function and provenly

. In the case that this holds one may use function application are among the classes discussed in the next section.

. This is worth mentioning since also more broader concepts of "assignment routines" or "operations" exist in the mathematical literature, which may not in general respect this. Variants of the functional predicate definition using apartness relations on setoids. This is mostly a matter of bookkeeping, but affects how other predicates are defined, and affects questions of size. This choice is also just enforced by some mathematical frameworks. Similar considerations apply to any treatment of partial functions and their domains.

are sets, then the above function predicate only involves bounded quantifiers. Common notions such as injectivity and surjectivity can be expressed in a bounded fashion as well, and thus so is bijectivity. Both of these tie in to notions of size. Importantly, injection existence between any two sets provides a preorder. A power class does not inject into its underlying set and the latter does not map onto the former. Surjectivity is formally a more complex definition. Note that injectivity shall be defined positively, not by its contrapositive, which is common practice in classical mathematics. The version without negations is sometimes called weakly injective. The existence of value collisions is a strong notion of non-injectivity. And regarding surjectivity, similar considerations exist for outlier-production in the codomain.

. Now if the domain is a set, the function comprehension principle, also called axiom of unique choice. Also compare with the Replacement axiom that adding a function symbol for a provenly total class function is a conservative extension, despite this formally changing the scope of bounded Separation. In summary, in the set theory context the focus is on capturing particular total relations that are functional. To delineate the notion of function in the theories of the previous subsection (a 2-ary logical predicate defined to express a functions graph, together with a proposition that it is total and functional) from the "material" set theoretical notion here, one may explicitly call the latter graph of a function, anafunction or set function. The axiom schema of Replacement can also be formulated in terms of the ranges of such set functions.

Finitude

One defines three distinct notions involving surjections. For a general set to be (Bishop-)finite shall mean there is a bijective function to a natural. If the existence of such a bijection is proven impossible, the set is called non-finite. Secondly, for a notion weaker than finite, to be finitely indexed (or Kuratowski-finite) shall mean that there is a surjection from a von Neumann natural number onto it. In programming terms, the element of such a set are accessible in a (ending) for-loop, and only those, while it may not be decidable whether repetition occurred. Thirdly, call a set subfinite if it is the subset of a finite set, which thus injects into that finite set. Here, a for-loop will access all of the set's members, but also possibly others. For another combined notion, one weaker than finitely indexed, to be subfinitely indexed with more elements.

Terminology for conditions of finiteness and infinitude may vary. Notably, subfinitely indexed sets (a notion necessarily involving surjections) are sometimes called subfinite (which can be defined without functions). The property of being finitely indexed could also be denoted "finitely countable", to fit the naming logic, but is by some authors also called finitely enumerable (which might be confusing as this suggest an injection in the other direction). Relatedly, the existence of a bijection with a finite set has not established, one may say a set is not finite, but this use of language is then weaker than to claim the set to be non-finite. The same issue applies to countable sets (not proven countable vs. proven non-countable), et cetera. A surjective map may also be called an enumeration.

Infinitude

. This validates the formulations of Dedekind-infinite. So more generally than the property of infinitude in the previous section on number bounds, one may call a set infinite may be called countably infinite. A set is Tarski-infinite and that theory does not prove all non-finite sets to be infinite in the injection existence sense, albeit it there holds when without any choice even permits cardinals aside the aleph numbers, and there can then be sets that negate both of the above properties, i.e. they are both non-Dedekind-infinite and non-finite (also called Dedekind-finite infinite sets).

Call an inhabited set countable onto it and subcountable. Call a set enumerable is trivially infinite, countable and enumerable, as witnessed by the identity function. Also here, in strong classical theories many of these notions coincide in general and, as a result, the naming conventions in the literature are inconsistent. An infinite, countable set is equinumeros.

's countable subsets gives another notion of uncountability. More properties of finiteness may be defined as negations of such properties, et cetera.

Characteristic functions

, one is now led to reason about classes such as

, one has

and so

may in generally not be decidable cannot be witnessed cannot be proven, then one cannot judge the comprehended collection to be total functional. Case in point: The classical derivation of Schröder–Bernstein relies on case analysis - but to constitute a function plus constructive principles. So to the extent that intuitionistic inference does not go beyond what is formalized here, there is no generic construction of a bijection from two injections in opposing directions.

" to be interpreted as a completed object that is also not necessarily given as lawlike sequence. Applications may be found in the common models for claims about probability, e.g. statements involving the notion of "being given" an unending random sequence of coin flips, even if many predictions can also be expressed in terms of spreadss.

, it is the characteristic function and

free) may be referred to as a .

if existence is actually decidable,

may be independent. This and the {\mathrm {LPO}}, is discussed below.

Witness of apartness

The identity of indiscernibles necessitates that all agree on them. And so if there exists a is proven, as soon it is established that not all, a logically negative condition.

define the logically positive apartness relation

Computable sets

on the numbers (say one defined from Kleene's T predicate), let again

, then

. There, one can obtain a bijective function. In this way, the class of functions in typical classical set theories is provenly rich, as it also contains objects that are beyond what we know to be effectively computable, or programmatically listable in praxis.

In computability theory, the computable sets are ranges of non-decreasing total functions in the recursive sense of the arithmetical hierarchy, and not higher. Deciding a predicate at that level amounts to solving the task of eventually finding a certificate. See also Kripke's schema. Note that bounded Separation nonetheless proves the more complicated arithmetical predicates to still constitute sets, the next level being the computably enumerable.

There is a large corpus of computability theory notions regarding how general subsets of naturals relate to one another. For example, one way to establish a bijection of two such sets is by relating them through a computable isomorphism, which is a computable permutation of all the naturals. The latter may in turn be established by a pair of particular injections in opposing directions.

Boundedness criteria

, the sequence

i.e.

that is bounded is then numerically capped as well, and in particular eventually does not exceed the identity function on its input indices. Formally,

(or an equivalent formulation of this property) is called pseudo-bounded). The related notion.

Choice functions

proves each union of a countable set of two-element sets to be countable again. Indeed, models have been defined that negate the countability of such a countable union of pairs. Assuming countable choice - A naive proof strategy for that statement fails at the accounting of infinitely many existential instantiations.

does \Pi_4^1-theorems, but it is strictly non-constructive, as shown below. The development here proceeds in a fashion agnostic to any of the variants described next.

Axiom of countable choice), as is implied by the constructive Church's thesis principle). The weak Kőnig's lemma and is itself sometimes viewed as capturing a form of countable choice. In the presence of a weak form of countable choice, the lemma becomes equivalent to the non-constructive principle of more logical flavor, {\mathrm {LLPO}}. Constructively, a weak form of choice is required for well-behaved Cauchy reals. Countable choice is not valid in the internal logic of a general elementary topos, which can be seen as models of constructive set theories.
Axiom of dependent choice, given any entire relation, but these do not have to be evaluated all together at once. It also holds in many realizability models. In the condition of the formally similar recursion theorem. Dependent choice does not imply that subsingleton domains have a choice function.
.
and its elements and which is closed by taking indexed sums and products (see dependent type.
Axiom of choice. Also, when restricted to the Borel algebra alone does not prove the existence of a function selecting a member from each non-empty such Lebesgue-measurable subset is the σ-algebra generated by the intervals-formulas, a non-constructive consequence not acceptable, for example, from a computability standpoint. Note that constructively, Zorn's lemma does not imply choice: When membership in function domains fails to be decidable, the extremal function granted by that principle is not provably always a choice function on the whole domain.

Full Choice implies PEM

To highlight the strength of full Choice and its relation to matters of intentionality, one should consider Diaconescu's theorem. Its proof first defines the classes

So full choice is non-constructive in set theory as defined here. The issue is that when propositions are part of set comprehension, the notion of their truth values are ramified into set terms of the theory. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the proposition to information about function values.

For computable semantics, set theory axioms postulating (total) function existence lead to the requirement for halting recursive functions. From their function graph in individual interpretations, one can infer the branches taken by the "if-clauses" that were undecided in the interpreted theory. But on the level of the synthetic frameworks, when they broadly become classical from adopting full choice, these extensional set theories theories contradict the constructive Church's rule.

Regularity implies PEM

. The axiom of regularity in the universal collection, there exists:

Demanding that the set of naturals is well-ordered. So the least number principle has the same non-constructive implication. As with the proof from Choice, the scope of propositions for which these results hold is governed by one's Separation axiom.

Arithmetic

Shortcomings of ECST

The four Peano axioms is decidable. Induction for arithmetic formulas is a theorem.

However, as discussed, when not assuming full mathematical induction (or stronger axioms like full Separation) in a set theory, there is a pitfall regarding the existence of arithmetic operations. The first-order theory of Heyting arithmetic has the same signature does actually not enable primitive recursion" here denotes the Cartesian product.

Arithmetic functions from recursion

In the next section, it is clarified which set theoretical axiom may be asserted to prove existence of the latter arithmetic functions as a function set, together with their desired relation to zero and successor.

Far beyond just the equality predicate, the obtained model of arithmetic then validates

and double-negation elimination is possible for any Harrop formula.

, the axiom granting definition. This iteration- or recursion principle is akin to the transfinite recursion theorem, except it is restricted to set functions and finite ordinal arguments, i.e. there is no clause about limit ordinals. It functions as the set theoretical equivalent of a natural numbers object in category theory in our set theory, including addition and multiplication functions.

are well-founded, in the sense of the inductive subsets formulation can then also be defined and its properties, like uniqueness and countability, be proven.

Recursion from set theory axioms

" is also commonly used with classes anyhow.)

, the function spaces

-defined classes.

, one may considerWith this axiom, any such space is now a set, or to n-fold Cartesian products, provably does preserve countability.

plus finite exponentiation, the recursion principle is a theorem. Moreover, enumerable forms of the pigeon hole principle can now also be proven, e.g. that on a finitely indexed set, every auto-injection is also a surjection. As a consequence, the cardinality are finite. Taking quotients or taking the binary union or Cartesian product of two sets preserve finiteness, sub-finiteness and being finitely indexed.

-predicates (with respect to the set theory language, and this then holds regardless of the decidability of their equality relations.)

Weak set theory variations

Induction without infinite sets

. The addition of numbers, considered as relation on triples, is an infinite collection, just like collection of natural numbers themselves. But note that induction schemas may be adopted (for sets, ordinals or in conjunction with a natural number sort), without ever postulating that the collection of naturals exists as a set. As noted, Heyting arithmetic is bi-interpretable with such a constructive set theory, in which all sets are postulated to be in bijection with an ordinal. The BIT predicate is a common means to encode sets in arithmetic.

This paragraph lists a few weak natural number induction principles studied in the proof theory of arithmetic theories with addition and multiplication in their signature. This is the framework where these principles are most well understood. The theories may be defined via bounded formulations or variations on induction schemas that may furthermore only allow for predicates of restricted complexity. On the classical first-order side, this leads to theories between the Robinson arithmetic and Peano arithmetic has full mathematical induction for arithmetical formulas and has \varepsilon_0, meaning the theory lets one encode ordinals of weaker theories as recursive relation on just the naturals. Theories may also include additional symbols for particular functions. Many of the well studied arithmetic theories are weak regarding proof of totality for some more fast growing functions. Some of the most basic examples of arithmetics include elementary function arithmetic, which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a proof theoretic ordinal (the least not provenly recursive well-ordering-conservative over primitive recursive arithmetic-induction is also part of the second-order reverse mathematics \mathsf{RCA}_0.

-induction schema. Lack of stronger induction schemas means, for example, that some unbounded versions of the pigeon hole principle are unprovable. One relatively weak one being the Ramsey theorem type claim here expressed as follows: is not ever the mappings return value anymore.'s, beyond which the function would still have to attain some color value. More specifically, the strength of the required bounding principle is strictly between validates the former so called infinite pigeon hole principle, which concerns unbounded domains, and so is about mappings with infinitely many inputs.

It is worth noting that in the program of predicative arithmetic, even the mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals.

Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory-formulas. It also has Axiom schema of Set Induction, which enables theorems involving the class of ordinals. The theory has the disjunction property.

. The theory is especially weak when studied without Infinity.

Stronger subtheories of ZF

Exponentiation

without the Powerset axiom has natural models in classes of sets of hereditary size less than certain uncountable cardinals. In particular, it is still consistent with all existing sets (including sets holding reals) being subcountable, and there even countable. Such a theory essentially amounts to second-order arithmetic. All sets being subcountable can constructively be consistent even in the present of uncountable sets, as introduced now.

: of all functions is, in fact, also a set. This is certainly required, for example, to formalize the object map of an internal hom-functor

. This examples shows that the Exponentiation axiom not only enriches the domain of sets directly, but via separation also enables the derivation of yet more sets, and this then furthermore also strengthens other axioms.

Notably, these bounded quantifiers now range over function spaces that are provably uncountable of points underlying the Cantor space, is uncountable, by Cantor's diagonal argument, just to avoid conflation of cardinal- with ordinal exponentiation.) Roughly, classically uncountable sets, like for example these function spaces, tend to not have computably decidable equality.

Unions and countability

With Exponentiation, the theory proves the existence of any primitive recursive function as discussed, and thus encode ordinals in the arithmetic. One then furthermore obtains the ordinal, the counted set of words over an infinite alphabet being the union of a countable set of countable sets.

The list here is by no means complete. Many theorems about the various function existence predicates hold, especially when assuming countable choice - which as noted is never implicitly assumed in this discussion.

At last, with Exponentiation, any finitely indexed union of a family of subfinitely indexed resp. subcountable sets is itself subfinitely indexed resp. subcountable as well. The theory also proves the collection of all the countable.

The class of all subsets of a set

. But notably, in a mathematical set theory framework, the collection of all subsets of a set is defined not in a bottom-up construction from its constituents but via a comprehension over all itself \Pi_1, which makes the axiom of powerset impredicative.

of course holds any subset. Over classical logic, this furthermore means that Exponentiation turns the power class into a set.

is a field of sets, for it to form a σ-algebra is continuous from below of the function's values at finite unions.

Apart from the class of detachable sets, also various other subclasses of any powerclass are now provenly sets. For example, the theory also proves this for the collection of all the countable subsets of any set.

, is called the truth value algebra and does not necessarily provenly have only two elements.

also.

is true in a theory is contingent on a simple disjunction:

, bounded excluded middle in fact already turns set theory classical, as discussed further below.)

in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.

. See continuum hypothesis and the related Easton's theorem.

Category and type theoretic notions

So in this context with Exponentiation, first-order arithmetic has a model and all function spaces between sets exist. The latter are more accessible than the classes containing all subsets of a set, as is the case with exponential objects resp. subobjects in category theory. In category theoretical essentially corresponds to constructively well-pointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an elementary topos. corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any coequalizer of two nonintersecting monomorphisms has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically.

" exists on its own and denotes function spaces, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying, an adjunction, none have the property of being a surjection.

Constructive set theories are also studied in the context of applicative axioms.

Metalogic

minus Regularity. So this would thus lead to a theory beyond the strength of typical type theory.

to be not enumerable, in the sense of injections out of it. Without further axioms, intuitionistic mathematics has models in recursive functions but also forms of hypercomputation.

Analysis

is elaborated on. For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive. Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which choice, induction and comprehension principles are silently assumed. See also the related constructive analysis, feasible analysis and computable analysis.

The theory so far proves uniqueness of Archimedean, Dedekind complete (pseudo-)ordered fields, with equivalence by a unique isomorphism. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable. This result is relevant assuming complete such models exist as sets.

Topology

. Consider a counter-example to the constructive provability of the well-orderedness of the naturals, but now embedded in the reals. Say

for example, may constructively fail to provably exist. More generally, this locatedness property of subsets governs the well-developed constructive metric space theory.

Whether Cauchy or Dedekind reals, among others, also fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.

Cauchy sequences

. So this enables speaking of Cauchy sequences.

Cauchy reals

constructed with respect to an equivalence relation. Exponentiation together with bounded separation prove the collection of Cauchy reals to be a set, thus somewhat simplifying the logically treatment of the reals.

with a strengthened form of Collection, the Cauchy reals are poorly behaved when not assuming a form of countable choice suffices for most results. This concerns completeness of equivalence classes of such sequences, equivalence of the whole set to the Dedekind reals, existence of a modulus of convergence for all Cauchy sequences and the preservation of such a modulus when taking limits. An alternative approach that is slightly better behaved is to work a collection of Cauchy reals together a choice of modulus, i.e. not with just the real numbers but with a set of pairs, or even with a fixed modulus shared by all real numbers.

Towards the Dedekind reals

As in the classical theory, Dedekind cuts given by

The theory given by the axioms so far validates that a pseudo-ordered or Powerset, countable choice into finite sets is assumed to prove the uncountability of the set of all Dedekind reals.

Constructive schools

, as defined in the second section on number bounds. Here are some other propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic:

), first one has Markov's principle, which is a form of proof by contradiction motivated by (unbound memory capacity) computable search. This has notable impact on statements about real numbers, as touched upon below. In this school one further even has the anti-classical constructive Church's thesis principle in the arithmetical hierarchy into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently.
So on another end, on the Brouwerian intuitionist), there are bar induction, the decidable fan theorem countable), or even Brouwer's anti-classical continuity principle, determining return values of what is established a function on unending sequences already through just finite initial segments.

, explained below. The independence of premise rule plus the countability of all subsets of the naturals. These combinations are then naturally also not consistent with further anti-classical principles.

Indecomposability

indecomposable,

are the trivial properties. This is well studied in intuitionistic analysis.

says that it cannot be decidable over all sets.

and discussed below.

Non-constructive principles

and many principles defining intermediate logics for just negated propositions, can be presented as De Morgan's rules. Note that in the context of Exponentiation, such proposition on sets are now set-bound.

Particularly valuable in the study of constructive analysis may not be. As is known from the incompleteness theorem proves the disjunction of the two axiomatically.)

, a most prominent non-constructive, essentially logical statement goes by the name limited principle of omniscience-fashion, i.e. of Goldbach-type: Goldbach conjecture, Fermat's Last Theorem but also the Riemann hypothesis.

-sentences generally hint at equivalent formulations deciding apartness of any two reals is decidable (dichotomy). It is then also equivalent to the statement that if the product of two reals is zero, then either of the reals is zero - again without a witness. Indeed, formulations of the three omniscience principles are then each equivalent to theorems of the apartness, equality or order of two reals in this way. Yet more can be said about the Cauchy sequences that are augmented with a modulus of convergence.

A famous source of computable undecidability - and in turn also of a broad range of undecidable propositions - is the predicate expressing a computer program to be total.

Infinite trees

Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of reverse mathematics concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets

with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so-called Weak Kőnig's lemma for which no computable such path through it exists. To prove this, one enumerates the partial computable everywhere, which by construction is incompatible with any total computable path.

is also equivalent to the Brouwer fixed point theorem and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, but always be aware that these claims may depend on the formulation, as the classical theorems about encoded reals can translate to different variants when expressed in a constructive context.

, and some variants thereof, concerns infinite graphs and so its contrapositives gives a condition for finiteness. Again to connect to analysis, over the \mathsf{RCA}_0 is for example equivalent to the Borel compactness.

Induction

Mathematical induction

to be the set to all its inductive subclasses. As in the classical theory, it is also implied when passing to the impredicative full Separation schema. As stated in the section on Choice, induction principles such as this are also implied by various forms of choice principles.

). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to exponentiation principles., not even for all predicatively defined sets is the equality to such a finite von Neumann ordinal necessarily decidable.

Set Induction

Going beyond the previous induction principles, one has full set induction, which is to be compared to well-founded induction. Like mathematical induction above, the following axiom is formulated as a schema in terms of predicates, and thus has a different character than induction principles proven from predicative set theory axioms. A variant of the axiom just for bounded formulas is also studied independently and may be derived from other axioms. in the standard framework. This (as well as natural number induction) may again be restricted to just the bounded set formulas, in which case arithmetic is not impacted.

, the axiom proves induction in transitive sets-formulation. Set induction in turn enables ordinal arithmetic in this sense. It further allows definitions of class functions by transfinite recursion. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak strengths. This also holds for their counterparts in type theory. Replacement is not required to prove induction over the set of naturals from set induction, but that axiom is necessary for their arithmetic modeled within the set theory.

The axiom of regularity, induction reads

Via the contrapositive, set induction implies all instances of regularity but only with double-negated existence in the conclusion. In the other direction, given enough transitive sets, regularity implies each instance of set induction.

Metalogic

with its collection axioms discarded in favour of the weaker Replacement and Exponentiation axioms. It proves the Cauchy reals to be a set, but not the class of Dedekind reals.

" among its members is trichotomous" and thus that of a set theory, as was the motivation for the principle in the 20's. But the constructive theory here does not prove a trichotomy for all ordinals, while the trichotomous ordinals are not well behaved with respect to the notion of successor and rank.

and proves the same functions recursive. Specifically, its proof-theoretic large countable ordinal is the Bachmann–Howard ordinal. This is also the ordinal of classical or intuitionistic Kripke–Platek set theory.

Aczel was also one of the main developers or Non-well-founded set theory, which rejects set induction.

Relation to ZF

The theory also constitutes a presentation of Zermelo–Fraenkel set theory now exactly leads into the classical theory.

also proves there exists such a number.

Strong Collection

So firstly, one may reflect upon the strength of the axiom of replacement, which have ever deeper rank. This is also not a subset of any previously established set.

Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema it is equivalent to Replacement, unless the powerset axiom is dropped. In the current context the strong axiom presented supersedes Replacement, due to not requiring the binary relation definition to be functional, but possibly multi-valued. and thus the axiom is also expressing some power akin to a Separation procedure. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.

Weak collection and predicative separation.

Metalogic

with its subset collection schema below, it has the existence property.

Constructive Zermelo–Fraenkel

Binary refinement

, implies that this is indeed possible.

plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left Dedekind cuts (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all characteristic function.

Subset Collection

adopts the axioms of the previous sections plus a stronger form of Exponentiation. It is by adopting the following alternative to Exponentiation, which can again be seen as a constructive version of the Power set axiom:An alternative that is not a schema is elaborated on below.

Fullness

be the class of all total relations. This class is given as

represents the space of "non-unique-valued functions" or "multivalued functions.

being a set would imply the Powerset axiom.

, there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large set..

The Fullness axiom, as well as dependent choice, is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated category theoretically.

Metalogic of CZF

has the numerical existence property and the disjunctive property lacks the existence property due to the Subset Collection Schema or Fullness axiom. The schema can also be an obstacle for realizability models. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom is adopted instead. The latter is in general lacking a constructive interpretation.

Unprovable claims

, for that matter) are part of the principles listed above, in the sections on constructive schools in analysis, on the Cauchy construction and on non-constructive principles. What follows concerns set theoretical concepts:

, this is the set of hereditarily countable sets even constitutes a set, even when countable choice is assumed.

. Also, neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The circumstance that ordinals are better behaved in the classical than in the constructive context manifests in a different theory of large set existence postulates.

Variants of the stages of the von Neumann hierarchy may be defined with respect to given sets of truth values, but these constructively also fail to exhibit the full classical structure.

Finally, the theory also does not prove that all function spaces formed from sets in the constructible universe are sets inside.

Ordinal analysis

. Adding back just mathematical induction gives a theory with proof theoretic ordinal, which is the first common fixed point of the Veblen functions and is below the Feferman–Schütte ordinal).

Being related to inductive definitions or bar induction.

Models

-pretopos. Without diverging into topos theory. The effective topos based on maps characterized by certain good subcountability properties.

for sets) is validated in some effective topos models, meaning the axiom does not spoil cornerstones of the restrictive recursive school.

can still be interpreted in Martin-Löf type theory, using the propositions-as-types. plus the choice principle, and also together with choice, have the existence property for a broad class of sets in common mathematics. Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

Soundness and Completeness theorems, with respect to realizability, have been established.

Breaking with ZF

One may of course add a Church's thesis.

One may postulate the subcountability is then provenly not a set, by Cantor's diagonal argument. Subcountability is also in contradiction with various large set axioms and stronger.)

is closed under Troelstra's,

, as noted.

In 1989 Ingrid Lindström showed that non-well-founded sets with Aczel's anti-foundation axiom.-induction schema or relativized dependent choice, as well as the assertion that every set is member of a transitive set.

Intuitionistic Zermelo–Fraenkel

adopting both the standard Separation as well as Power set without , in place of Replacement, one may use theWhile the axiom of replacement requires the relation to be functional over the set (as in, for every in there is associated exactly one ), the Axiom of Collection does not. It merely requires there be associated at least one , and it asserts the existence of a set which collects at least one such for each such , the Collection schema implies the Axiom schema of replacement. When making use of Powerset (and only then), they can be shown to be classically equivalent.

is based on intuitionistic rather than classical logic, it is considered impredicative. It allows formation of sets via a power set operation and using the general Axiom of Separation with any proposition, including ones which contain quantifierss which are not bounded. Thus new sets can be formed in terms of the universe of all sets, distancing the theory from the bottom-up constructive perspective. So it is even easier to define sets with undecidable membership, namely by making use of undecidable predicates defined on a set. The power set axiom further implies the existence of a set of truth values are strong enough so that full is already implied by shall always be decidable, no matter the set.

Metalogic

to be a set. The theory has many of the nice numerical existence properties being subcountable. It also has the disjunctive property.

as formulated does not. The combination of schemas including full separation spoils it.

Even without , the proof theoretic strength-sentences.

Intuitionistic Z

On the weaker end, as with its historical counterpart Zermelo set theory but without Replacement, Collection or Induction.

Sorted theories

Constructive set theory

is a theory using constructive first-order logic with identity and two more sorts beyond sets, namely natural numbers and functionss. Its axioms are:

The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union.
The Axiom of restricted, or predicative, separation, which is a weakened form of the Separation axiom from classical set theory, requiring that any quantificationss be bounded to another set, as discussed.
A form of the Axiom of Infinity) is in fact a set.
The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the Axiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity.

And furthermore:

The usual Peano axioms for natural numbers.
Axioms asserting that the domain and range of a function are both sets. Additionally, an Axiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual Replacement axiom in classical set theory.

when comparing with the previous sections.

And finally the theory adopts

An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

Bishop style set theory

Set theory in the flavor of Errett Bishop's constructivist school mirrors that of Myhill, but is set up in a way that sets come equipped with relations that govern their discreteness. Commonly, Dependent Choice is adopted.

A lot of analysis and module theory has been developed in this context.

Category theories

), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of setss.

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section. For some good set theory, this may require enough projectives, an axiom about surjective "presentations" of set, implying Countable and Dependent Choice.