Conservativity of transitive closure over weak constructive operational set theory

Constructive set theory a' la Myhill–Aczel has been extended in previous papers by the authors to incorporate a notion of (partial, non–extensional) operation. Constructive operational set theory is a constructive and predicative analogue of Beeson’s Inuitionistic set theory with rules and of Feferman’s Operational set theory. This paper is concerned with an extension of constructive operational set theory by a uniform operation of Transitive Closure. We show that the resulting theory is conservative over Peano Arithmetic.