On Feferman's operational set theory \textsf{OST} (Q2463480)

The author provides a proof-theoretic analysis of the operational set theory \textsf{OST}, introduced by S.~Feferman, and some of its extensions. The language of \textsf{OST} extends the one of usual set theory by operations which mimic the applicative structure of Feferman's explicit mathematics. It contains, in particular, operations for separation (for definite operations), replacement, and choice. It can be strengthened by a power set operation \(\mathbb{P}\) and an operator for unbounded quantification \(\mathbf{E}\). The theories \textsf{OST} and \textsf{OST}\(^r({\mathbf{E}},\mathbb{P})\) are shown to be equiconsistent with \textsf{KP}\(\omega\) and \textsf{ZFC}, respectively; the exact strength of \textsf{OST}\((\mathbb{P})\) is still unknown, but is shown to be between \textsf{KP}\((\mathcal{P})\) and \textsf{KP}\((\mathcal{P}) + (V = L)\) (where \textsf{KP}\((\mathcal{P})\) is Kripke-Platek set theory for power admissible sets).