The proof-theoretic analysis of the Suslin operator in applicative theories

In this article we introduce the Suslin quantification functional El into the framework of Feferman's explicit mathematics and analyze it from the point of view of proof theory. More precisely, we work in the first order part of explicit mathematics augmented by appropriate axioms for E-1. Then we establish the exact proof-theoretic relationship between these applicative theories and (subsystems of) the second order theory (Delta(2)(1)-CA), depending on the induction principles permitted.