The Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule was introduced by W. Buchholz to give an ordinal-free proof of cut-elimination for a subsystem of analysis with Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-comprehension. W. Buchholz’s proof provides cut-free derivations by familiar rules only for arithmetical sequents. When second-order quantifiers are present, they are introduced by the Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule and some residual cuts are not (...) eliminated. In the present paper, we introduce an extension of the Ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Omega $$\end{document}-rule and prove the complete cut-elimination by the same method as W. Buchholz: any derivation of arbitrary sequent is transformed into its cut-free derivation by the standard rules. In fact we treat the subsystem of Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-CA that W. Buchholz used for his explanation of G. Takeuti’s finite reductions. Extension to full Π11\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi ^{1}_{1}$$\end{document}-CA is planned for another paper. (shrink)

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...) CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Π02 theorems of arithmetic. (shrink)

The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.