The role of parameters in bar rule and bar induction
- 1 June 1991
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 56 (2), 715-730
- https://doi.org/10.2307/2274713
Abstract
For several subsystems of second order arithmeticTwe show that the proof-theoretic strength ofT+ (bar rule) can be characterized in terms ofT+ (bar induction)□, where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that,ACA0+ (bar rule) andACA0+ (bar induction)□prove the same-sentences.Keywords
This publication has 9 references indexed in Scilit:
- Jean-Yves Girard. Proof theory and logical complexity. Volume I. Studies in proof theory, no. 1. Bibliopolis, Naples 1987, also distributed by Humanities Press, Atlantic Highlands, N.J., 503 pp.The Journal of Symbolic Logic, 1989
- Which set existence axioms are needed to prove the separable Hahn-Banach theorem?Annals of Pure and Applied Logic, 1986
- Countable algebra and set existence axiomsAnnals of Pure and Applied Logic, 1983
- Inductive definitions and subsystems of analysisPublished by Springer Science and Business Media LLC ,1981
- Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical StudiesLecture Notes in Mathematics, 1981
- A MORE PERSPICUOUS FORMAL SYSTEM FOR PREDICATIVITYPublished by Walter de Gruyter GmbH ,1978
- Recursion-Theoretic HierarchiesPublished by Springer Science and Business Media LLC ,1978
- Theories of Finite Type Related to Mathematical PracticePublished by Elsevier BV ,1977
- Proof TheoryPublished by Springer Science and Business Media LLC ,1977