Document type
Book chapters
Title
On some semi-constructive theories related to Kripke–Platek set theory
Participants in the publication
Fernando Ferreira (Author)
Dep. Matemática
CMAFcIO
Summary
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 of Markov’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-11 reflection. The key idea of the extended analysis is to treat second-order (class) quantifiers as bounded quantifiers and strict-11 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.
Editor(s)
Gerhard Jaeger, Wilfried Sieg
Institution
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA
Where published
Feferman on Foundations
Publication Identifiers
ISSN - 2211-2758
eISSN - 2211-2766
ISBN - 9783319633329,9783319633343
Publisher
Springer International Publishing
Collection
Outstanding Contributions to Logic
Number of pages
38
Starting page
347
Last page
384
Document Identifiers
URL -
http://dx.doi.org/10.1007/978-3-319-63334-3
DOI -
https://doi.org/10.1007/978-3-319-63334-3
Keywords
Functional Interpretations
Power Kripke-Platek set theory
Strict pi-11 reflection
Sigma-ordinal
Intuitionistic Kripke-Platek set theory
Notes
This is a refereed research paper in mathematical logic. It is an invited paper to a volume of the collection "Outstanding Contributions to Logic" dedicated to the eminent logician Solomon Feferman.
Download