Understanding uniformity in Fefermanʹs explicit mathematics Original Research Article

The aim of this paper is the analysis of uniformity in Fefermanʹs explicit mathematics. The proof-strength of those systems for constructive mathematics is determined by reductions to subsystems of second-order arithmetic: If uniformity is absent, the method of standard structures yields that the strength of the join axiom collapses. Systems with uniformity and join are treated via cut elimination and asymmetrical interpretations in standard structures.