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
![[img]](https://boris.unibe.ch/style/images/fileicons/text.png) |
Text
978-3-030-77799-9_2.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (294kB) |
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.
Item Type: |
Book Section (Book Chapter) |
|---|---|
Division/Institute: |
08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) |
UniBE Contributor: |
Jäger, Gerhard Max |
Subjects: |
000 Computer science, knowledge & systems 500 Science > 510 Mathematics |
ISBN: |
978-3-030-77798-2 |
Publisher: |
Springer |
Language: |
English |
Submitter: |
Atefeh Rohani |
Date Deposited: |
25 Jan 2023 11:24 |
Last Modified: |
25 Jan 2023 23:28 |
Publisher DOI: |
10.1007/978-3-030-77799-9_2 |
BORIS DOI: |
10.48350/177369 |
URI: |
https://boris.unibe.ch/id/eprint/177369 |
Actions (login required)
 |
Edit item |