- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Explaining the Gentzen–Takeuti reduction steps: a second-order system
Archive for Mathematical Logic 40 (4):255-272 (2001)
Abstract
Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π1 1-CA) in terms of the more perspicious infinitary approach from [BS88]My notes
Similar books and articles
Review: Wilfried Buchholz, Notation Systems for Infinitary Derivations ; Wilfried Buchholz, Explaining Gentzen's Consistency Proof within Infinitary Proof Theory ; Sergei Tupailo, Finitary Reductions for Local Predicativity, I: Recursively Regular Ordinals. [REVIEW]Toshiyasu Arai - 2002 - Bulletin of Symbolic Logic 8 (3):437-439.
Consistency proof via pointwise induction.Toshiyasu Arai - 1998 - Archive for Mathematical Logic 37 (3):149-165.
A reduction rule for Peirce formula.Sachio Hirokawa, Yuichi Komori & Izumi Takeuti - 1996 - Studia Logica 56 (3):419 - 426.
Gentzen’s consistency proof without heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A simple relationship between Buchholz's new system of ordinal notations and Takeuti's system of ordinal diagrams.Mitsuhiro Okada - 1987 - Journal of Symbolic Logic 52 (3):577-581.
Resolution calculus for the first order linear logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
NP-Completeness of a Combinator Optimization Problem.M. S. Joy & V. J. Rayward-Smith - 1995 - Notre Dame Journal of Formal Logic 36 (2):319-335.
A direct independence proof of Buchholz's Hydra Game on finite labeled trees.Masahiro Hamano & Mitsuhiro Okada - 1998 - Archive for Mathematical Logic 37 (2):67-89.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.
A Buchholz Derivation System for the Ordinal Analysis of KP + Π₃-Reflection.Markus Michelbrink - 2006 - Journal of Symbolic Logic 71 (4):1237 - 1283.
Analytics
Added to PP
2013-12-01
Downloads
30 (#521,181)
6 months
6 (#512,819)
2013-12-01
Downloads
30 (#521,181)
6 months
6 (#512,819)
Historical graph of downloads
Citations of this work
Does reductive proof theory have a viable rationale?Solomon Feferman - 2000 - Erkenntnis 53 (1-2):63-96.
Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The no-counterexample interpretation.W. W. Tait - 2005 - Bulletin of Symbolic Logic 11 (2):225-238.
A Buchholz Rule for Modal Fixed Point Logics.Gerhard Jäger & Thomas Studer - 2011 - Logica Universalis 5 (1):1-19.
Reading Gentzen's Three Consistency Proofs Uniformly.Ryota Akiyoshi & Yuta Takahashi - 2013 - Journal of the Japan Association for Philosophy of Science 41 (1):1-22.
Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-7c76586df8-5tf24 uwo