A flexible type system for the small Veblen ordinal

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

[img] Text
FIT-2.pdf - Accepted Version
Restricted to registered users only until 1 September 2020.
Available under License Publisher holds Copyright.

Download (811kB) | Request a copy
[img] Text
Ranzi-Strahm2019_Article_AFlexibleTypeSystemForTheSmall.pdf - Published Version
Restricted to registered users only
Available under License Publisher holds Copyright.

Download (743kB) | Request a copy

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 and 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 Oct 2019 11:12

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 Edit item
Provide Feedback