1. Description and History

What is explicit mathematics? For the systematic logical study of higher mathematics, explicit mathematics is a flexible, unified context in which existence evidence ensures computability or definibility with the means of what is shown to exist. In view of the ubiquity of the existence of evidence in modern mathematics, it would seem that such parts of mathematics must be relatively limited, and no method is known to produce the objects claimed to exist.

Indeed, the main parts of mathematics covered by the explicit mathematical framework are referred to as constructive, predictive and descriptive and were originally pursued based on the philosophic principles that, in the majority of cases, were not considered to be persuasive and confined to practise. In current work, the logical analysis of the framework show that, despite its philosophical and methodological limitations, the uniform explanations of solutions do not pay much for the functionality and mathematical scope of these approaches. In particular, all scientifically applicable mathematics are already taken into account in a weak predictive system.

2. Idea and Goal

Most modern mathematics based on non-constructive set-theoretical principles, but in fact little is actually used (other than, obviously, the theory itself) of what is implicit in them. For example, in a finite type structure over natural numbers N, a large proportion of the mathematical analysis may be developed—and indeed within type three. In the set theory, transfinite types occur through the transfinite iteration of the operation. However, where such iteration is used only for operations in a given type in the analysis.This is reflected in recent results on the determinateness of Borel games. Practice can be considered deficient in the fact that it does not pursue potential resources of transfinite types.

The classes of explicit mathematics are not the same as the classes of set theory, nor are they the same as the types of type theory. They are similar to the former in that they represent certain collections of the underlying first-order model, but they differ in that they have names that can be used to create new ones. The systems are available in intuitionistic or classical logic flavours. One advantage is that they allow for the smooth axiomatization of strong notions of universes, as discussed below.

• [math]\displaystyle{ \mathsf{T_0} }[/math] (the classical variant)
• [math]\displaystyle{ \mathsf{T^i_0} }[/math] (the intuitionistic variant)

These two systems were the original ones invented by Feferman, and also the strongest.

3. Definition

The systems' first-order parts deal with an applicative universe in the sense of combinatory algebra. It includes the constants [math]\displaystyle{ k }[/math] and [math]\displaystyle{ s }[/math] (combinators); [math]\displaystyle{ p }[/math], [math]\displaystyle{ p_0 }[/math]and [math]\displaystyle{ p_1 }[/math] (pairing and projection); [math]\displaystyle{ 0 }[/math], [math]\displaystyle{ s_N }[/math] and [math]\displaystyle{ p_N }[/math] (zero, successor, and predecessor), and [math]\displaystyle{ d_N }[/math] (definition by natural number cases), as well as possibly other applicative constants. There is a binary function-symbol [math]\displaystyle{ \cdot }[/math], a unary relationship-symbol [math]\displaystyle{ \downarrow }[/math], a unique relationship-symbol [math]\displaystyle{ \textrm{N} }[/math], and the binary equality relationship [math]\displaystyle{ = }[/math].

We utilise the common abbreviation [math]\displaystyle{ s \simeq t }[/math] to represent [math]\displaystyle{ (s \downarrow \and t \downarrow \rightarrow s = t) }[/math] in the logic of partial terms. The basic axioms and natural numbers for the operation are:

• [math]\displaystyle{ kab = a }[/math],
• [math]\displaystyle{ sab \downarrow \and sabc \simeq ac(bc) }[/math].
• [math]\displaystyle{ p_0(a, b) = a \and p_1(a, b) = b }[/math]
• [math]\displaystyle{ 0 \in N \and (\forall x \in N)(s_Nx \in N) }[/math]
• [math]\displaystyle{ (\forall x \in N)(s_Nx \neq 0 \and p_N(s_Nx) = x) }[/math]
• [math]\displaystyle{ (\forall x \in N)(x \neq 0 \rightarrow s_N(p_Nx) = x) }[/math]
• [math]\displaystyle{ a \in N \and b \in N \and a = b \rightarrow d_Nuvab = u }[/math]
• [math]\displaystyle{ a \in N \and b \in N \and a \neq b \rightarrow d_Nuvab = v }[/math]

We have lambda and fixed point combinator from the first two axioms. To these axioms, in order to get the theory [math]\displaystyle{ \textrm{BON+(L}-\textrm{Ind}_N) }[/math], we add the system of induction over natural numbers. Theoretically, this is comparable to first order Peano arithmetic, PA, across both interpretations. In PA, [math]\displaystyle{ \textrm{BON+(L}-\textrm{Ind}_N) }[/math] can be interpreted by coding operations, employing Kleene's T and U predicates, as indices of recursive functions.

4. Extensions

4.1. Elementary Comprehension

When we shift from just applicatory theory to class theory with names, a second class (for classes) as well as numerous additional constants, a symbol [math]\displaystyle{ \in }[/math] of the binary relation for membership and a symbol of binary relationship for names [math]\displaystyle{ \mathfrak{R} }[/math], where [math]\displaystyle{ \mathfrak{R}\textrm{(s, U)} }[/math] means that [math]\displaystyle{ \textrm{s} }[/math] is a name for the class [math]\displaystyle{ \textrm{U} }[/math]; we use the abbreviation [math]\displaystyle{ \mathfrak{R}\textrm{(s)}: \leftrightarrow \exists \textrm{U}\mathfrak{R}\textrm{(s, U)} }[/math], indicating that [math]\displaystyle{ \textrm{s} }[/math] is a name, are added.

Each class has its own name, no homonyms and [math]\displaystyle{ \mathfrak{R} }[/math] maintains extensive equality in the core axioms relating classes and names. The class names of the basic understanding are produced using [math]\displaystyle{ \textrm{co} }[/math] (complements), [math]\displaystyle{ \textrm{int} }[/math] (intersections), [math]\displaystyle{ \textrm{dom} }[/math] (domains), [math]\displaystyle{ \textrm{inv} }[/math] (inverse images), [math]\displaystyle{ \textrm{nat} }[/math] (natural numbers) and [math]\displaystyle{ \textrm{id} }[/math] (equality ratios). Classical systems are concerned with this. The intuitional systems differ slightly. Using the abbreviation [math]\displaystyle{ s \in^- t }[/math] to represent [math]\displaystyle{ \exists\textrm{U}(\mathfrak{R}\textrm{(t, U)} \and s \in U) }[/math], the axioms in elementary comprehension are as follows:

• [math]\displaystyle{ \mathfrak{R}\textrm{(nat)} \and \forall x(x \in^- \textrm{nat} \leftrightarrow N(x)) }[/math]
• [math]\displaystyle{ \mathfrak{R}\textrm{(id)} \and \forall x(x \in^- \textrm{id} \leftrightarrow \exists y(x = (y, y))) }[/math]
• [math]\displaystyle{ \mathfrak{R}(a) \rightarrow \mathfrak{R}(\textrm{co}(a)) \and \forall x(x \in^- \textrm{co}(a) \leftrightarrow \neg x \in^- a) }[/math]
• [math]\displaystyle{ \mathfrak{R}(a) \and \mathfrak{R}(b) \rightarrow \mathfrak{R}(\textrm{int}(a, b)) \and \forall x(x \in^- \textrm{int}(a, b)) \leftrightarrow x \in^- a \and x \in^- b }[/math]
• [math]\displaystyle{ \mathfrak{R}(a) \rightarrow \mathfrak{R}(\textrm{dom}(a)) \and \forall x(x \in^- \textrm{dom}(a) \leftrightarrow \exists y((x, y) \in^- a)) }[/math]
• [math]\displaystyle{ \mathfrak{R}(a) \rightarrow \mathfrak{R}(\textrm{inv}(a, f)) \and \forall x(x \in^- \textrm{inv}(a, f) \leftrightarrow fx \in^- a) }[/math]

We add some induction to get the [math]\displaystyle{ \textrm{EC}+(\textrm{C-Ind}_N) }[/math], the induction axiom for the classes, and [math]\displaystyle{ \textrm{EC}+(\textrm{L-Ind}_N) }[/math], the induction schema for all formulas, theories by using natural numbers. Basic explicit mathematics with elementary comprehension ([math]\displaystyle{ \mathsf{EM}_0 }[/math]) is theoretically consistent with the second-order arithmetic subsystem [math]\displaystyle{ \mathsf{ACA}_0 }[/math].

4.2. Join and Inductive Generation

The combination of classes provides disjoined class unions, and therefore corresponds to type theory types. The inductive operation generates accessible parts of the binary relationship coding classes. The theory [math]\displaystyle{ \mathsf{T_0} }[/math] has elementary comprehension, join, inductive generation, and full induction over the natural numbers. It has the same proof-theoretic strength as CZF plus REA, the regular extension axiom. Further equivalences are listed at ordinal analysis. [math]\displaystyle{ \mathsf{T} }[/math] is a slightly stronger, second-order variant of [math]\displaystyle{ \mathsf{T_0} }[/math] which has elementary comprehension, join, inductive generation, full induction over the natural numbers and the full second-order induction scheme.