Explicit mathematics

Script error: No such module "AfC submission catcheck".

In the field of logic and set theory, American mathematician and philosopher Solomon Feferman developed explicit mathematics, which is a collection of axiomatic systems related to constructive mathematics. It consists of a set of fundamental logical systems based on mathematical logic. A second type of class is added to a first-order logic of partial terms axiomatizing combinatory algebra. Alternative names: classifications, or types are sometimes used. The aim of explicit mathmetics was to have a straightforward and principled transfer of the notions of indescribable cardinals from set theory to admissible ordinals, yet the approach leaves open the question as to what is the proper analogue for admissible ordinals — if any — of a cardinal κ being $\Pi _{n}^{m}$ -indescribable for m > 1.

Description and history[edit]

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.

Idea and goal[edit]

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.

${\mathsf {T_{0}}}$ (the classical variant)
${\mathsf {T_{0}^{i}}}$ (the intuitionistic variant)

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

Definition[edit]

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

We utilise the common abbreviation $s\simeq t$ to represent $(s\downarrow \land t\downarrow \rightarrow s=t)$ in the logic of partial terms. The basic axioms and natural numbers for the operation are:

$kab=a$ ,
$sab\downarrow \land sabc\simeq ac(bc)$ .
$p_{0}(a,b)=a\land p_{1}(a,b)=b$
$0\in N\land (\forall x\in N)(s_{N}x\in N)$
$(\forall x\in N)(s_{N}x\neq 0\land p_{N}(s_{N}x)=x)$
$(\forall x\in N)(x\neq 0\rightarrow s_{N}(p_{N}x)=x)$
$a\in N\land b\in N\land a=b\rightarrow d_{N}uvab=u$
$a\in N\land b\in N\land a\neq b\rightarrow d_{N}uvab=v$

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

Extensions[edit]

Elementary comprehension[edit]

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 $\in$ of the binary relation for membership and a symbol of binary relationship for names ${\mathfrak {R}}$ , where ${\mathfrak {R}}{\textrm {(s,U)}}$ means that ${\textrm {s}}$ is a name for the class ${\textrm {U}}$ ; we use the abbreviation ${\mathfrak {R}}{\textrm {(s)}}:\leftrightarrow \exists {\textrm {U}}{\mathfrak {R}}{\textrm {(s,U)}}$ , indicating that ${\textrm {s}}$ is a name, are added.

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

${\mathfrak {R}}{\textrm {(nat)}}\land \forall x(x\in ^{-}{\textrm {nat}}\leftrightarrow N(x))$
${\mathfrak {R}}{\textrm {(id)}}\land \forall x(x\in ^{-}{\textrm {id}}\leftrightarrow \exists y(x=(y,y)))$
${\mathfrak {R}}(a)\rightarrow {\mathfrak {R}}({\textrm {co}}(a))\land \forall x(x\in ^{-}{\textrm {co}}(a)\leftrightarrow \neg x\in ^{-}a)$
${\mathfrak {R}}(a)\land {\mathfrak {R}}(b)\rightarrow {\mathfrak {R}}({\textrm {int}}(a,b))\land \forall x(x\in ^{-}{\textrm {int}}(a,b))\leftrightarrow x\in ^{-}a\land x\in ^{-}b$
${\mathfrak {R}}(a)\rightarrow {\mathfrak {R}}({\textrm {dom}}(a))\land \forall x(x\in ^{-}{\textrm {dom}}(a)\leftrightarrow \exists y((x,y)\in ^{-}a))$
${\mathfrak {R}}(a)\rightarrow {\mathfrak {R}}({\textrm {inv}}(a,f))\land \forall x(x\in ^{-}{\textrm {inv}}(a,f)\leftrightarrow fx\in ^{-}a)$

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

Join and inductive generation[edit]

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 ${\mathsf {T_{0}}}$ 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. ${\mathsf {T}}$ is a slightly stronger, second-order variant of ${\mathsf {T_{0}}}$ which has elementary comprehension, join, inductive generation, full induction over the natural numbers and the full second-order induction scheme.

References[edit]

This article "Explicit mathematics" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Explicit mathematics. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.