Abstract

Constructive set theory a' la Myhill-Aczel has been extended in (Cantini and Crosilla 2008, Cantini and Crosilla 2010) 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 (Beeson 1988, Feferman 2006, Jaeger 2007, Jaeger 2009, Jaeger 1009b). This paper is concerned with an extension of constructive operational set theory (Cantini and Crosilla 2010) by a uniform operation of Transitive Closure, \tau. Given a set a, \tau produces its transitive closure \tau a. We show that the theory ESTE of (Cantini and Crosilla 2010) augmented by \tau is still conservative over Peano Arithmetic.