Elementary Constructive Operational Set Theory
Andrea Cantini, Laura Crosilla · 2010
We introduce a theory of constructive sets and operations. One motivation behind constructive operational set theory is to merge a constructive notion of set (in the sense of Aczel) with some aspects which are typical of Feferman's so-called "explicit mathematics". In particular, one has non-extensional operations (or rules) alongside with 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, finitely axiomatised system of constructive sets and operations, which is shown to be as strong as the system of intuitionistic elementary number theory.