Simplified cut elimination for Kripke-Platek set theory

Jäger, Gerhard (2022). Simplified cut elimination for Kripke-Platek set theory. In: Ferreira, Fernando; Kahle, Reinhard; Sommaruga, Giovanni (eds.) Axiomatic Thinking II (pp. 9-34). Springer 10.1007/978-3-030-77799-9_2

Text 978-3-030-77799-9_2.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (294kB) | Request a copy

The purpose of this article is to present a new and simplified cut elimination procedure for KP. We start off from the basic language of set theory and add constants for all elements of the constructible hierarchy up to the Bachmann-Howard ordinal ψ(εΩ+1). This enriched language is then used to set up an infinitary proof system IP whose ordinal-theoretic part is based on a specific notation system C(εΩ+1,0) due to Buchholz and his idea of operator controlled derivations. KP is embedded into IP and complete cut elimination for IP is proved.

Interest & Impact

Downloads

2 since deposited on 25 Jan 2023
2 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item