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,881

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

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.
Typability in Partial Applicative Structures.Inge Bethke & Piet Rodenburg - 2011 - Journal of Logic, Language and Information 20 (2):161-168.
A Confutation of the Pessimistic Induction.Seungbae Park - 2010 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 42 (1):75-84.
The Suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories.Gerhard Jäger & Dieter Probst - 2011 - Annals of Pure and Applied Logic 162 (8):647-660.
Remarks on applicative theories.Andrea Cantini - 2005 - Annals of Pure and Applied Logic 136 (1-2):91-115.
Totality in applicative theories.Gerhard Jäger & Thomas Strahm - 1995 - Annals of Pure and Applied Logic 74 (2):105-120.
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.
A Pessimistic Induction against Scientific Antirealism.Seungbae Park - 2014 - Organon F: Medzinárodný Časopis Pre Analytickú Filozofiu 21 (1):3-21.
A theory of rules for enumerated classes of functions.Andreas Schlüter - 1995 - Archive for Mathematical Logic 34 (1):47-63.
On the quantifier complexity of Δ n+1 (T)– induction.A. Cordón-Franco, A. Fernández-Margarit & F. F. Lara-Martín - 2004 - Archive for Mathematical Logic 43 (3):371-398.
Peirce's and Lewis's theories of induction.Chung-Ying Cheng - 1969 - The Hague,: Martinus Nijhoff.

Analytics

Added to PP
2014-01-16

Downloads
17 (#868,760)

6 months
7 (#430,521)

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 12 references / Add more references