On the Strength of some Semi-Constructive Theories
Solomon Feferman · 2012
Most axiomatizations of set theory that have been treated metamathematically have been based either entirely on classical logic or entirely on intuitionistic logic. But a natural conception of the set- theoretic universe is as an indenite (or \potential) totality, to which intuitionistic logic is more appropriately applied, while each set is taken to be a denite (or \completed) totality, for which classical logic is ap- propriate; so on that view, set theory should be axiomatized on some correspondingly mixed basis. Similarly, in the case of predicative analy- sis, the natural numbers are considered to form a denite totality, while the universe of sets (or functions) of natural numbers are viewed as an indenite totality, so that, again, a mixed semi-constructive logic should be the appropriate one to treat the two together. Various such semi- constructive systems of analysis and set theory are formulated here and their proof-theoretic strength is characterized. Interestingly, though the logic is weakened, one can in compensation strengthen certain principles in a way that could be advantageous for mathematical applications. 1