Foundations of Explicit Mathematics
Explicit mathematics was introduced by Feferman around 1975. The three basic papers which illuminate explicit mathematics from various angles are
- 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 :
- 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 :
- Constructive theories of functions and classes, Logic Colloquium ’78 (M. Boffa, D. van Dalen, and K. McAloon, editors), North-Holland, 1979, pp. 159–224 :
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.,- Systems of explicit mathematics with non-constructive μ-operator. Part I, Annals of Pure and Applied Logic, vol. 65 (1993), no. 3, pp. 243–263 :
- 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 :
- 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.,- 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 :
- 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.,- Logics for termination and correctness of functional programs, Logic from Computer Science (Y. N. Moschovakis, editor), Springer, 1991, pp. 95–127, :
- 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 :
- A semantics for $\lambda^{\{\}}$: a calculus with overloading and late-binding, Journal of Logic and Computation 11(4), , 2001, pp. 527-544 :
- 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 :
- 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.
Operational set theory
- On Feferman's operational set theory OST, Annals of Pure and Applied Logic 150, 2007, pp. 10-39 :
- 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
- 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
- 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
- Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297 :
- Elementary explicit types and polynomial time operations, Mathematical Logic Quarterly 55(3), 2009, pp. 245-258, :
- Weak theories of operations and types, Ways of Proof Theory (R.Schindler, editor), Ontos Verlag, 2010, pp. 441-468 :
Unfolding schematic formal systems
- Unfolding finitist arithmetic, Review of Symbolic Logic 3(4), 2010, pp. 665-689 :