Ranzi, Florian; Strahm, Thomas (2019). A flexible type system for the small Veblen ordinal. Archive for mathematical logic, 58(5-6), pp. 711-751. Springer-Verlag 10.1007/s00153-019-00658-x
|
Text
FIT-2.pdf - Accepted Version Available under License Publisher holds Copyright. Download (811kB) | Preview |
|
|
Text
Ranzi-Strahm2019_Article_AFlexibleTypeSystemForTheSmall.pdf - Published Version Available under License Publisher holds Copyright. Download (743kB) | Preview |
We introduce and analyze two theories for typed (accessible part) inductive definitions
and establish their proof-theoretic ordinal to be the small Veblen ordinal \theta\Omega^\omega. We investigate
on the one hand the applicative theory FIT of functions, (accessible part) inductive
definitions, and types. It includes a simple type structure and is a natural generalization
of S. Feferman’s system QL(F0-IRN). On the other hand, we investigate the arithmetical
theory TID of typed (accessible part) inductive definitions, a natural subsystem of ID_1,
and carry out a wellordering proof within TID that makes use of fundamental sequences
for ordinal notations in an ordinal notation system based on the finitary Veblen functions.
The essential properties for describing the ordinal notation system are worked out.
Item Type: |
Journal Article (Original Article) |
|---|---|
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: |
Ranzi, Florian, Strahm, Thomas Adrian |
Subjects: |
000 Computer science, knowledge & systems 500 Science > 510 Mathematics |
ISSN: |
0933-5846 |
Publisher: |
Springer-Verlag |
Language: |
English |
Submitter: |
Nenad Savic |
Date Deposited: |
15 Oct 2019 14:14 |
Last Modified: |
31 Jan 2023 00:25 |
Publisher DOI: |
10.1007/s00153-019-00658-x |
BORIS DOI: |
10.7892/boris.133882 |
URI: |
https://boris.unibe.ch/id/eprint/133882 |
Actions (login required)
 |
Edit item |