Systems of explicit mathematics with non-constructive μ-operator and join

Annals of Pure and Applied Logic 82 (2):193-219 (1996)
  Copy   BIBTEX


The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics.



    Upload a copy of this work     Papers currently archived: 91,998

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Can constructive mathematics be applied in physics?Douglas S. Bridges - 1999 - Journal of Philosophical Logic 28 (5):439-453.
Realisability in weak systems of explicit mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
Intentional mathematics.Stewart Shapiro (ed.) - 1985 - New YorK, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Weak-operator Continuity and the Existence of Adjoints.Douglas Bridges & Luminita Dediu - 1999 - Mathematical Logic Quarterly 45 (2):203-206.
Varieties of constructive mathematics.D. S. Bridges - 1987 - New York: Cambridge University Press. Edited by Fred Richman.
On power set in explicit mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
Questioning Constructive Reverse Mathematics.I. Loeb - 2012 - Constructivist Foundations 7 (2):131-140.


Added to PP

18 (#833,659)

6 months
14 (#179,755)

Historical graph of downloads
How can I increase my downloads?