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

Abstract The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T 1 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.