Foundations of Explicit Mathematics

Explicit mathematics was introduced by Feferman around 1975. The three basic papers which illuminate explicit mathematics from various angles are

S. Feferman: A language and axioms for explicit mathematics , Algebra and Logic (J.N. Crossley, editor), Lecture Notes in Mathematics, vol. 450, Springer, 1975, pp. 87–139
S. Feferman: Recursion theory and set theory: a marriage of convenience, Oslo 1977 (J. E. Fenstad, R. O. Gandy, and G. E. Sacks, editors), North-Holland, 1978, pp. 55-98
S. Feferman: Constructive theories of functions and classes, Logic Colloquium ’78 (M. Boffa, D. van Dalen, and K. McAloon, editors), North-Holland, 1979, pp. 159–224

The original aim of explicit mathematics was to provide a natural formal framework for Bishop-style constructive mathematics. Soon it turned out, however, that the range of applications of explicit mathematics is much wider and includes, for example, also the following subjects:

Reductive proof theory

Systems of explicit mathematics play an important role in studying the relationship between subsystems of analysis, subsystems of set theory and theories for inductive definitions and for the reduction of classical theories to constructively (better) justified formalisms.

Abstract recursion theory

Several of its basic first order features (λ abstraction, fixed point theorem) are recursion-theoretic in nature, which are not tied to any specific structure; it is also a good tool in developing a proof theory of higher order functionals; cf., e.g.,

S. Feferman and G. Jäger: Systems of explicit mathematics with non-constructive μ-operator. Part I, Annals of Pure and Applied Logic, vol. 65 (1993), no. 3, pp. 243–263
S. Feferman and G. Jäger: Systems of explicit mathematics with non-constructive $\mu$-operator. Part II, Annals of Pure and Applied Logic, vol. 79 (1996), no. 1, pp. 37-52
G. Jäger and T. Strahm: The proof-theoretic strength of the Suslin operator in applicative theories, Reflections on the Foundations of Mathematics: Essays in honor of Solomon Feferman (W. Sieg, R. Sommer, C. Talcott - editors), A K Peters, 2002, pp. 270-292

Type systems

Flexible (polymorphic) type systems find a natural place in explicit mathematics; the most practically needed type constructs can be modeled in systems of low proof-theoretic strength; cf., e.g.,

S. Feferman: Polymorphic typed lambda-calculi in a type-free axiomatic framework, Logic and Computation (W. Sieg, editor), Contemporary Mathematics, vol. 106, American Mathematical Society, 1990, pp. 101–136
G. Jäger: Type theory and explicit mathematics, Logic Colloquium ’87 (H.-D. Ebbinghaus, J. Fernandez-Prida, M. Garrido, M. Lascar, and M. Rodriguez Artalejo, editors), North-Holland, 1989, pp. 117–135

Programming

Explicit mathematics also provides an abstract framework for dealing with certain aspects of functional and object-oriented programming; cf., e.g.,

S. Feferman: Logics for termination and correctness of functional programs, Logic from Computer Science (Y. N. Moschovakis, editor), Springer, 1991, pp. 95–127,
S. Feferman: Logics for termination and correctness of functional programs II: Logics of strength PRA, Proof Theory (P. Aczel, H. Simmons, and S. S. Wainer, editors), Cambridge University Press, 1992, pp. 195–225
T. Studer: A semantics for $\lambda^{\{\}}$: a calculus with overloading and late-binding, Journal of Logic and Computation 11(4), , 2001, pp. 527-544
T. Studer: Constructive Foundations for Featherweight Java, Proof Theory in Computer Science, volume 2183 of LNCS (R. Kahle, P. Schroeder-Heister, R. Stärk, editors), Springer, 2001, pp. 202-238

One possible formulation of explicit mathematics is based on the following ontology:

individuals are explicitly given and can be interpreted as objects, operations, (constructive) functions, programs and the like;
self-application is possible; we define new operations (terms) by means of principles such as $\lambda$ abstraction and the fixed point theorem;
induction is then often used in order to show that these new operations have the desired properties.

Types (sometimes also called classes) are abstractly defined collections of operations; they have names and are addressed via these names. The focus of explicit mathematics is on the explicit presentation of operations rather than their constructive justification; it is possible to be explicit without being constructive (and vice versa). Our current research activities in the context of explicit mathematics and related formal frameworks can be summarized as follows; with each topic, we list some recent relevant publications:

Operational set theory

G. Jäger: On Feferman's operational set theory OST, Annals of Pure and Applied Logic 150, 2007, pp. 10-39
G. Jäger: Full operational set theory with unbounded existential quantification and power set, Annals of Pure and Applied Logic 160, 2009, pp. 33–52

Strong higher type functionals in applicative theories

G. Jäger, D. Probst: The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories, Annals of Pure and Applied logic 162(8), 2011, pp. 647-660

Universes and reflection principles in explicit mathematics

G. Jäger, T. Strahm: Reflections on reflections in explicit mathematics, Annals of Pure and Applied Logic 136(1-2), 2005, pp. 116-133

Weak systems of explicit mathematics and partial truth

T. Strahm: Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297
D. Spescha, T. Strahm: Elementary explicit types and polynomial time operations, Mathematical Logic Quarterly 55(3), 2009, pp. 245-258,
T. Strahm: Weak theories of operations and types, Ways of Proof Theory (R.Schindler, editor), Ontos Verlag, 2010, pp. 441-468

Unfolding schematic formal systems

S. Feferman, T. Strahm: Unfolding finitist arithmetic, Review of Symbolic Logic 3(4), 2010, pp. 665-689

You are here