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.
[2] A set theory does not only express theorems about numbers, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed.
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.
, this totality constitutes an undecidable subset of indices, highlighting that the recursive world of functions between the naturals is already captured by a set dominated by
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
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.
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.
does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical
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
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.
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.
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.