nLab
explicit mathematics

Explicit mathematics

Idea

Explicit mathematics is a programme initiated by Solomon Feferman which is related to constructive mathematics.

It is also a range of foundational logical systems based on the logic of partial terms?. Starting from a first-order logic of partial terms axiomatizing combinatory algebra, a second sort of classes is added. Sometimes, the alternative names classifications or types are used.

The classes of explicit mathematics are not like the classes of set theory, but also not like types of type theory. They are like the former in that they represent certain collections of the underlying first-order model, but they are like the latter in that they have names that can be operated on to construct new ones.

The systems come in flavors with either intuitionistic or classical logic. On benefit is that they allow for smooth axiomatization of strong notions of universes, see below.

The primary systems are called T 0T_0 (the classical variant) and T 0 iT_0^i (the intuitionistic variant).

In the 1980s there was a proof assistant and program extraction tool called PX based on a version of T 0T_0 relative to the Lisp programming language.

The basic theory of operations and numbers

The first-order part of the systems treat an applicative universe in the sense of combinatory algebra. It includes constants k\mathrm{k} and s\mathrm{s} (combinators), p\mathrm{p}, p 0\mathrm{p}_0, and p 1\mathrm{p}_1 (pairing and projection), 00, s N\mathrm{s}_N, and p N\mathrm{p}_N (zero, successor, and predecessor), and d N\mathrm{d}_N (definition by cases on the natural numbers), and possibly further applicative constants.

There is one binary function symbol {\cdot} for application (usual just indicated by juxtaposition), one unary relation symbol \downarrow for being defined, one unary relation symbol N\mathrm{N} for natural numbers, as well the binary equality relation.

In the logic of partial terms, we use the usual abbreviation st(sts=t)s \simeq t \leftrightarrow ({s\downarrow} \wedge {t\downarrow} \to s=t). The basic axioms for the operations and natural numbers are:

  1. kab=a\mathrm{k} a b = a,
  2. sabsabcac(bc)\mathrm{s} a b \downarrow \wedge \mathrm{s} a b c \simeq a c(b c),
  3. p 0(a,b)=ap 1(a,b)=b\mathrm{p}_0(a,b)=a \wedge \mathrm{p}_1(a,b) = b,
  4. 0N(xN)(s NxN)0\in N \wedge (\forall x\in N)(\mathrm{s}_N x \in N),
  5. (xN)(s Nx0p N(s Nx)=x)(\forall x\in N)(\mathrm{s}_N x \ne 0 \wedge \mathrm{p}_N(\mathrm{s}_N x)=x),
  6. (xN)(x0s N(p Nx)=x)(\forall x\in N)(x\ne0 \to \mathrm{s}_N(\mathrm{p}_N x) = x),
  7. aNbNa=bd Nuvab=ua\in N \wedge b\in N \wedge a=b \to \mathrm{d}_N u v a b = u,
  8. aNbNabd Nuvab=va\in N \wedge b\in N \wedge a\ne b \to \mathrm{d}_N u v a b = v.

From the first two axioms we get lambda-definability and a fixed-point combinator.

To these axioms we add the scheme of induction over the natural numbers to obtain the theory BON+(LInd N)BON + (\mathrm{L}{-}Ind_N). This is proof-theoretically equivalent to first-order Peano arithmetic, PAPA, via interpretations both ways. We can interpret BON+(LInd N)BON + (\mathrm{L}{-}Ind_N) in PAPA by coding operations as indices for recursive functions using Kleene’s TT and UU predicates.

Elementary comprehension

When we go from the purely applicative theory to the theories of classes and names, we add a second sort (for classes) as well as several new constants, a binary relation symbol \in (for membership) and a binary relation symbol for names \Re, where (s,U)\Re(s, U) means that ss is a name for the class UU. We use the abbreviation (s):U(s,U)\Re(s) :\leftrightarrow \exists U \Re(s,U), indicating that ss is a name.

The basic axioms regarding classes and names state that every class has a name, that there are no homonyms, and that \Re respects extensional equality.

The names of classes corresponding to elementary comprehension are generated from natnat (natural numbers) and idid (the equality relation) using coco (complements), intint (intersections), domdom (domains), and invinv (inverse images). [These are for the classical systems. The intuitionistic systems are slightly different. Todo: look this up]

Using the abbreviation s˙t:U((t,U)sU)s\dot\in t :\leftrightarrow \exists U(\Re(t,U) \wedge s\in U), the axioms are:

  1. (nat)x(x˙natN(x))\Re(nat) \wedge \forall x(x \dot\in nat \leftrightarrow N(x)),
  2. (id)x(x˙idy(x=(y,y)))\Re(id) \wedge \forall x(x \dot\in id \leftrightarrow \exists y(x = (y,y))),
  3. (a)(co(a))x(x˙co(a)¬x˙a)\Re(a) \to \Re(co(a)) \wedge \forall x(x \dot\in co(a) \leftrightarrow \neg x\dot\in a),
  4. (a)(b)(int(a,b))x(x˙int(a,b)x˙ax˙b)\Re(a) \wedge \Re(b) \to \Re(int(a,b)) \wedge \forall x(x \dot\in int(a,b) \leftrightarrow x \dot\in a \wedge x \dot\in b),
  5. (a)(dom(a))x(x˙dom(a)y((x,y)˙a))\Re(a) \to \Re(dom(a)) \wedge \forall x(x \dot\in dom(a) \leftrightarrow \exists y((x,y) \dot\in a)),
  6. (a)(inv(a,f))x(x˙inv(a,f)fx˙a)\Re(a) \to \Re(inv(a,f)) \wedge \forall x(x \dot\in inv(a,f) \leftrightarrow f x \dot\in a).

Again we add some induction over the natural numbers to obtain theories EC+(CInd N)EC + (\mathrm{C}{-}Ind_N) (induction axiom for classes) and EC+(LInd N)EC + (\mathrm{L}{-}Ind_N) (induction schema for all formulas). These correspond proof-theoretically to the subsystems of second-order arithmetic ACA 0ACA_0 and ACAACA, respectively.

Join and inductive generation

The join of classes gives disjoint unions of classes, and thus corresponds to the Σ\Sigma-types of type theory. The inductive generation operation provides accesible parts of classes coding binary relations.

[todo: the axioms for join and inductive generation.]

The theory T 0T_0 has elementary comprehension, join, inductive generation, and full induction over the natural numbers. It has the same proof-theoretic strength as CZF plus REAREA, the regular extension axiom. Further equivalences are listed at ordinal analysis.

Universes in explicit mathematics

[todo]

References

Last revised on January 6, 2018 at 13:26:44. See the history of this page for a list of all contributions to it.