In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable.
Apart from demands for computability and reservations regrading of impredicativity,[1] technical question regarding which non-logical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.
With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily.
A translation of Church's rule into the language of the theory itself may here read Kleene's T predicate together with the result extraction expresses that any input number
Taking the computable world seriously as ontology, a prime example of an anti-classical conception related the Markovian school is the permitted subcountability of various uncountable collections.
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 and
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.
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.
Due to the potential undecidability of general predicates, the notion of subset and subclass is automatically more elaborate in constructive set theories than in classical ones.
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.
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.
Via extensional identification, the second form expresses the claim using notation for subclass comprehension and the bracketed object on the right hand side may not even constitute a set.
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.
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.
Similarly, programs in the partial recursive sense may be unrolled to predicates and weak assumptions suffice so that such a translation respects equality of their return values.
So more generally than the property of infinitude in the previous section on number bounds, one may call a set infinite in the logically positive sense if one can inject
and that theory does not prove all non-finite sets to be infinite in the injection existence sense, albeit it there holds when further assuming countable choice.
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 spreads.
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.
A choice principle postulates that certain selections can always be made in a joint fashion in the sense that they are also manifested as a single set function in the theory.
The set theory axioms listed so far incorporates first-order arithemtic and suffices as formalized framework for a good portion of common mathematics.
However, also that axiom does not entail the full induction schema for formulas with unbound quantifiers over the domain of sets, nor a dependent choice principle.
A consequence of this is that for some statements of higher complexity or indirection, even if concrete instances of interest may well be provable, the theory may not prove the universal closure.
Higher indirection, than in induction for mere existential statements, is needed to formally reformulate such a negation (the Ramsey theorem type claim in the original formulation above) and prove it.
essentially corresponds to constructively well-pointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object.
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.
Particularly valuable in the study of constructive analysis are non-constructive claims commonly formulated in terms of the collection of all binary sequences and the characteristic functions
The recursion principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full mathematical induction schema over one's structure modeling the naturals (e.g.
Having discussed all the weakened forms of the classical set theory axioms, Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation, and in a way that is not going beyond
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.