Extended bar induction in applicative theories

Annals of Pure and Applied Logic 50 (2):139-189 (1990)
  Copy   BIBTEX

Abstract

TAPP is a total applicative theory, conservative over intuitionistic arithmetic. In this paper, we first show that the same holds for TAPP+ the choice principle EAC; then we extend TAPP with choice sequences and study the principle EBIa0. The resulting theories are used to characterise the arithmetical fragment of EL +EBIa0. As a digression, we use TAPP to show that P. Martin-Löf's basic extensional theory ML0 is conservative over intuitionistic arithmetic.

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(90)90047-6

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

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

Extended bar induction in applicative theories.Gerard R. Renardel de Lavalette - 1990 - Annals of Pure and Applied Logic 50 (2):139-189.
Totality in applicative theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
Remarks on applicative theories.Andrea Cantini - 2005 - Annals of Pure and Applied Logic 136 (1-2):91-115.
N \hbox{\sf n} -strictness in applicative theories.Reinhard Kahle - 2000 - Archive for Mathematical Logic 39 (2):125-144.
Truth in applicative theories.Reinhard Kahle - 2001 - Studia Logica 68 (1):103-128.
Universes over Frege structures.Reinhard Kahle - 2003 - Annals of Pure and Applied Logic 119 (1-3):191-223.
On the proof theory of type two functionals based on primitive recursive operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
Minimal truth and interpretability.Martin Fischer - 2009 - Review of Symbolic Logic 2 (4):799-815.
Structure and definability in general bounded arithmetic theories.Chris Pollett - 1999 - Annals of Pure and Applied Logic 100 (1-3):189-245.
A note on Goodman's theorem.Ulrich Kohlenbach - 1999 - Studia Logica 63 (1):1-5.
Applicative theories for the polynomial hierarchy of time and its levels.Reinhard Kahle & Isabel Oitavem - 2013 - Annals of Pure and Applied Logic 164 (6):663-675.
Intuitionistic Open Induction and Least Number Principle and the Buss Operator.Mohammad Ardeshir & Mojtaba Moniri - 1998 - Notre Dame Journal of Formal Logic 39 (2):212-220.
Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
A feasible theory of truth over combinatory algebra.Sebastian Eberhard - 2014 - Annals of Pure and Applied Logic 165 (5):1009-1033.
Provably recursive functions of constructive and relatively constructive theories.Morteza Moniri - 2010 - Archive for Mathematical Logic 49 (3):291-300.

Analytics

Added to PP
2014-04-02

Downloads
7 (#1,356,784)

6 months
4 (#790,687)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Extensional realizability.Jaap van Oosten - 1997 - Annals of Pure and Applied Logic 84 (3):317-349.
On Goodman Realizability.Emanuele Frittaion - 2019 - Notre Dame Journal of Formal Logic 60 (3):523-550.
About Goodmanʼs Theorem.Thierry Coquand - 2013 - Annals of Pure and Applied Logic 164 (4):437-442.

Add more citations

References found in this work

Formal systems for some branches of intuitionistic analysis.G. Kreisel - 1970 - Annals of Mathematical Logic 1 (3):229.
Proof-theoretical analysis: weak systems of functions and classes.L. Gordeev - 1988 - Annals of Pure and Applied Logic 38 (1):1-121.

View all 11 references / Add more references