Proof theory of reflection
type: Item
instance of: scholarly article
title: Proof theory of reflection
zbMATH Open document ID: 0813.03037
DOI: 10.1016/0168-0072(94)90074-4
author: Michael Rathjen
published in: Annals of Pure and Applied Logic
publication date: 1995-06-07T00:00:00Z
review text: This is a well-written paper. Its final product is the determination of the proof-theoretic ordinal of \(\text{KP}+ \Pi_ 3\)-Ref, i.e. Kripke- Platek set theory with \(\Pi_ 3\)-reflection. To reach there, the author gives motivations, intuitions, backgrounds, future visions, etc., making the paper accessible and almost self-contained. First, he develops a powerful ordinal notation system, \(T(K)\), composed of \(0\), \(K\), \(+\), \(\varphi\), \(\Omega\), \(\Xi\), \(\Psi\), and the ordering \(<\). According to him, ``nude ordinal notation systems without any set-theoretic interpretation tend to be hard to grasp'', and so he reminds ``the reader some set-theoretical notions'', first. Indeed, \(K\) is a weakly compact cardinal, \(\varphi\) is the Veblen function, etc. Then an infinitary proof system, \(RS(K)\), of ramified set theory is presented. Here, the subject of investigation is the initial segment, given by \(T(K)\), of the constructible set hierarchy. Since each set is named, infinitary rules here are counter-parts of the \(\omega\)-rule in Peano arithmetic. Cut- elimination is achieved by means of \(H\)-controlled derivations, and then KP-set theory is embedded into \(RS(K)\), thus determining its ordinal. Of course, \(\Pi_ 3\)-reflection is just a beginning: ``the idea is that \(\Pi^ 1_ 2\)-comprehension can be fathomed by going through transfinite levels of reflection: and thus an ordinal analysis for it should be attainable via an, admittedly, considerable extension of the machinery laid out in this paper''. \{Being given quite a few inches, one wants an ell: the author could have spent 2, 3 sentences in explaining the Veblen function \(\varphi\), what its connection with \(\varepsilon\)- numbers is, and what \(\alpha= _{\text{NF}} \varphi \beta \gamma\) means. A few more words might not have been wasted on collapsing functions as well as on \(H\)-controlled derivations, perhaps. Apparently, proof-reading was done a bit hastily: among others, p. 190, footn…
Mathematics Subject Classification ID: 03F15
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03E20
zbMATH DE Number: 633655
zbMATH Keywords: cut-elimination
zbMATH Keywords: proof-theoretic ordinal
zbMATH Keywords: Kripke-Platek set theory with \(\Pi_ 3\)-reflection
zbMATH Keywords: ordinal notation system
zbMATH Keywords: infinitary proof system
zbMATH Keywords: ramified set theory
zbMATH Keywords: constructible set hierarchy
zbMATH Keywords: ordinal analysis
MaRDI profile type: Publication
full work available at URL: 0168-0072(94)90074-4
OpenAlex ID: W2033008594
cites work: Q4079598
cites work: Second order arithmetic and related topics
cites work: Q4075450
cites work: Notation systems for infinitary derivations
cites work: Q3138829
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q4040375
cites work: Systems of predicative analysis, II: Representations of ordinals
cites work: Q4146722
cites work: Q3778746
cites work: Q3852172
cites work: Q4742775
cites work: Proof theory. An introduction
cites work: Proof theory and ordinal analysis
cites work: Ordinal notations based on a weakly Mahlo cardinal
cites work: Proof-theoretic analysis of KPM
cites work: How to develop Proof‐Theoretic Ordinal Functions on the basis of admissible ordinals
cites work: Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
cites work: Q4143279
cites work: Consistency proofs of subsystems of classical analysis
cites work: Proof theory. 2nd ed
cites work: Q4773683
description: scientific article; zbMATH DE number 633655