Abstract
We introduce an operational set theory in the style of [5] and [16].
The theory we develop here is a theory of constructive sets and operations.
One motivation behind constructive operational set theory is to merge a constructive
notion of set ([1], [2]) with some aspects which are typical of explicit
mathematics [14]. In particular, one has non-extensional operations (or rules)
alongside extensional constructive sets. Operations are in general partial and a
limited form of self{application is permitted. The system we introduce here is
a fully explicit, nitely axiomatised system of constructive sets and operations,
which is shown to be as strong as HA.