Portal de Periódicos da CAPES

On Some Semi-constructive Theories Related to Kripke–Platek Set Theory

2017; Springer International Publishing; Linguagem: Inglês

10.1007/978-3-319-63334-3_13

2211-2766

Fernando Ferreira,

Advanced Algebra and Logic

We consider some very robust semi-constructive theories related to Kripke–Platek set theory, with and without the powerset operation. These theories include the law of excluded middle for bounded formulas, a form ofMarkov, Andrei Markov’s principleMarkov’s principle, the unrestricted collection scheme and, also, the classical contrapositive of the bounded collection scheme. We analyse these theories using forms of a functional interpretation which work in tandem with the constructible hierarchy (or the cumulative hierarchy, if the powerset operation is present). The main feature of these functional interpretations is to treat bounded quantifications as “computationally empty.” Our analysis is extended to a second-order setting enjoying some forms of class comprehension, including strict- $$\Pi ^1_1$$ reflection. The key idea of the extended analysis is to treat second-order (class) quantifiers as bounded quantifiers and strict- $$\Pi ^1_1$$ reflection as a form of collection. We will be able to extract some effective bounds from proofs in these systems in terms of the constructive tree ordinals up to the Bachmann–Howard ordinal.