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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,888

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.
Remarks on applicative theories.Andrea Cantini - 2005 - Annals of Pure and Applied Logic 136 (1-2):91-115.
Notes on bounded induction for the compositional truth predicate.Bartosz Wcisło & Mateusz Łełyk - 2017 - Review of Symbolic Logic 10 (3):455-480.
A note on Goodman's theorem.Ulrich Kohlenbach - 1999 - Studia Logica 63 (1):1-5.
Quick cut-elimination for strictly positive cuts.Toshiyasu Arai - 2011 - Annals of Pure and Applied Logic 162 (10):807-815.
Totality in applicative theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
Inaccessibility in constructive set theory and type theory.Michael Rathjen, Edward R. Griffor & Erik Palmgren - 1998 - Annals of Pure and Applied Logic 94 (1-3):181-200.
Intuitionistic fixed point theories over set theories.Toshiyasu Arai - 2015 - Archive for Mathematical Logic 54 (5-6):531-553.
Lindenbaum algebras of intuitionistic theories and free categories.Peter Freyd, Harvey Friedman & Andre Scedrov - 1987 - Annals of Pure and Applied Logic 35 (C):167-172.
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
18 (#1,111,327)

6 months
4 (#1,247,093)

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.
The theory of the Gödel functionals.Nicolas D. Goodman - 1976 - Journal of Symbolic Logic 41 (3):574-582.

View all 11 references / Add more references