Tipo
Capítulo em Livro
Título
On some semi-constructive theories related to Kripke–Platek set theory
Participantes na publicação
Fernando Ferreira (Author)
Dep. Matemática
CMAFcIO
Resumo
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
Gerhard Jaeger, Wilfried Sieg
Instituição
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA
Suporte
Feferman on Foundations
Identificadores da Publicação
ISSN - 2211-2758
eISSN - 2211-2766
ISBN - 9783319633329,9783319633343
Editora
Springer International Publishing
Coleção
Outstanding Contributions to Logic
Número de Páginas
38
Página Inicial
347
Página Final
384
Identificadores do Documento
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
Anotações
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