
handle: 2158/355571
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.
set; operation; cut elimination; constructivism
set; operation; cut elimination; constructivism
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 6 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
