Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-23T14:38:08.412Z Has data issue: false hasContentIssue false

Wellfoundedness proofs by means of non-monotonic inductive definitions I: Π20-operators

Published online by Cambridge University Press:  12 March 2014

Toshiyasu Arai*
Affiliation:
Graduate School of Science and Technology, Kobe University, Rokko-Dai, Nada-Ku. Kobe 657-8501, Japan, E-mail: arai@kurt.scitec.kobe-u.ac.jp

Abstract.

In this paper, we prove the wellfoundedrtess of recursive notation systems for reflecting ordinals up to Π3-reflection by relevant inductive definitions.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2004

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Arai, T., Ordinal diagrams for Π3-reflection, this Journal, vol. 65 (2000), pp. 13751394.Google Scholar
[2]Arai, T., Ordinal diagrams for recursively Mahlo universes, Archive for Mathematical Logic, vol. 39 (2000), pp. 353391.CrossRefGoogle Scholar
[3]Arai, T., Proof theory for theories of ordinals I: Recursively Mahlo ordinals, Annals of Pure and Applied Logic, vol. 122 (2003), pp. 185.CrossRefGoogle Scholar
[4]Arai, T., Proof theory for theories of ordinals II: Π3-reflection, Annals of Pure and Applied Logic, to appear.Google Scholar
[5]Arai, T., Proof theory for reflecting ordinals III: ΠN-reflection, submitted.Google Scholar
[6]Arai, T., Wellfoundedness proofs by means of non-monotonic inductive definitions II: First order operators,submitted.Google Scholar
[7]Arai, T., Ordinal diagrams for ΠN-reflection, draft.Google Scholar
[8]Buchholz, W., Normalfunktionen und konstruktive Systeme von Ordinalzahlen, Proof Theory Symposion, Kiel 1974 (Diller, J. and Müller, G. H., editors), Lecture Notes in Mathematics, vol. 500, Springer, 1975, pp. 425.Google Scholar
[9]Buchholz, W., Review of the paper: A. Setzer, Well-ordering proofs for Martin-Löf type theory, The Bulletin of Symbolic Logic, vol. 6 (2000), pp. 478479.CrossRefGoogle Scholar
[10]Richter, W. H. and Aczel, P., Inductive definitions and reflecting properties of admissible ordinals, Generalized Recursion Theory, Studies in Logic, vol. 79, North-Holland, 1974, pp. 301381.Google Scholar