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

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.