In this paper we present some metapredicative subsystems of analysis. We deal with reflection principles, $\omega-model$ existence axioms (limit axioms) and axioms asserting the existence of hierarchies. We show several equivalences among the introduced subsystems. In particular we prove the equivalence of $\sum_1^1$ transfinite dependent choice and $\prod_2^1$ reflection on $\omega-models$ of $\sum_1^1-DC$.

This article provides an ordinal analysis of Σ11 transfinite dependent choice.

In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.

In this paper it is shown that the intuitionistic .xed point theory equation image for α times iterated fixed points of strictly positive operator forms is conservative for negative arithmetic and equation image sentences over the theory equation image for α times iterated arithmetic comprehension without set parameters.This generalizes results previously due to Buchholz [5] and Arai [2].

A new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA0, those in second order set theory extending NBG are. In this article, we establish the equivalence between Δ01-LFP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Delta^1_0\mbox{\bf-LFP}}$$\end{document} and Δ01-FP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Delta^1_0\mbox{\bf-FP}}$$\end{document}, which assert the existence of a least and of a fixed point, respectively, for positive elementary operators. Our proof also shows (...) the equivalence between ID1 and ID^1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\widehat{\it ID}_1}$$\end{document}, both of which are defined in the standard way but with the starting theory PA replaced by ZFC. (shrink)

By forcing, we give a direct interpretation of into Avigad's. To the best of the author's knowledge, this is one of the simplest applications of forcing to “real problems”.