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”.

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

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].

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 article we provide wellordering proofs for metapredicative systems of explicit mathematics and admissible set theory featuring suitable axioms about the Mahloness of the underlying universe of discourse. In particular, it is shown that in the corresponding theories EMA of explicit mathematics and KPm 0 of admissible set theory, transfinite induction along initial segments of the ordinal φω00, for φ being a ternary Veblen function, is derivable. This reveals that the upper bounds given for these two systems in the (...) paper Jager and Strahm [11] are indeed sharp. (shrink)