Strong Normalization Theorem for a Constructive Arithmetic with Definition by Transfinite Recursion and Bar Induction

Notre Dame Journal of Formal Logic 38 (3):350-373 (1997)
  Copy   BIBTEX

Abstract

We prove the strong normalization theorem for the natural deduction system for the constructive arithmetic TRDB (the system with Definition by Transfinite Recursion and Bar induction), which was introduced by Yasugi and Hayashi. We also establish the consistency of this system, applying the strong normalization theorem

Categories

Keywords

Reprint years

DOI

10.1305/ndjfl/1039700743

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,227

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Some new double induction and superinduction principles.Raymond M. Smullyan - 1990 - Studia Logica 49 (1):23 - 30.
On the strength of könig's duality theorem for countable bipartite graphs.Stephen G. Simpson - 1994 - Journal of Symbolic Logic 59 (1):113-123.
The role of parameters in bar rule and bar induction.Michael Rathjen - 1991 - Journal of Symbolic Logic 56 (2):715-730.
Ordinal inequalities, transfinite induction, and reverse mathematics.Jeffry L. Hirst - 1999 - Journal of Symbolic Logic 64 (2):769-774.
Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis.W. A. Howard & G. Kreisel - 1966 - Journal of Symbolic Logic 31 (3):325-358.
Primitive Recursion and the Chain Antichain Principle.Alexander P. Kreuzer - 2012 - Notre Dame Journal of Formal Logic 53 (2):245-265.
Ordinal analysis without proofs.Jeremy Avigad - manuscript
On the proof of Solovay's theorem.Dick Jongh, Marc Jumelet & Franco Montagna - 1991 - Studia Logica 50 (1):51 - 69.
General arithmetic.Andrew Boucher - manuscript
A note on Goodman's theorem.Ulrich Kohlenbach - 1999 - Studia Logica 63 (1):1-5.
Recursion theory for metamathematics.Raymond Merrill Smullyan - 1993 - New York: Oxford University Press.
Tarski's fixed-point theorem and lambda calculi with monotone inductive types.Ralph Matthes - 2002 - Synthese 133 (1-2):107 - 129.
Model-theoretic properties characterizing peano arithmetic.Richard Kaye - 1991 - Journal of Symbolic Logic 56 (3):949-963.

Analytics

Added to PP
2010-08-24

Downloads
12 (#1,090,149)

6 months
3 (#984,770)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The Trend of Logic and Foundation of Mathematics in Japan in 1991 to 1996.Yuzuru Kakuda, Kanji Namba & Nobuyoshi Motohashi - 1997 - Annals of the Japan Association for Philosophy of Science 9 (2):95-110.

Add more citations

References found in this work

The machinery of consistency proofs.Mariko Yasugi - 1989 - Annals of Pure and Applied Logic 44 (1-2):139-152.

Add more references