Intuitionistic choice and classical logic

Archive for Mathematical Logic 39 (1):53-74 (2000)
  Copy   BIBTEX


. The effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we can directly extract effective content from $\Pi_2^0$ -statements true in the model. All the arguments of the present paper can be formalised in Martin-Löf's constructive type theory with generalised inductive definitions



    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

Similar books and articles

Intuitionistic completeness for first order classical logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
Choice principles and constructive logics.David Dedivi - 2004 - Philosophia Mathematica 12 (3):222-243.
Intuitionistic Choice and Restricted Classical Logic.Ulrich Kohlenbach - 2001 - Mathematical Logic Quarterly 47 (4):455-460.
Axioms for classical, intuitionistic, and paraconsistent hybrid logic.Torben Braüner - 2006 - Journal of Logic, Language and Information 15 (3):179-194.
Some axioms for constructive analysis.Joan Rand Moschovakis & Garyfallia Vafeiadou - 2012 - Archive for Mathematical Logic 51 (5-6):443-459.
Forcing in proof theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
Models of intuitionistic TT and N.Daniel Dzierzgowski - 1995 - Journal of Symbolic Logic 60 (2):640-653.


Added to PP

49 (#317,389)

6 months
2 (#1,232,442)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.
Heyting-valued interpretations for constructive set theory.Nicola Gambino - 2006 - Annals of Pure and Applied Logic 137 (1-3):164-188.
On the Strength of some Semi-Constructive Theories.Solomon Feferman - 2012 - In Ulrich Berger, Hannes Diener, Peter Schuster & Monika Seisenberger (eds.), Logic, Construction, Computation. De Gruyter. pp. 201-226.
A Boolean model of ultrafilters.Thierry Coquand - 1999 - Annals of Pure and Applied Logic 99 (1-3):231-239.

View all 6 citations / Add more citations

References found in this work

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
Developments in constructive nonstandard analysis.Erik Palmgren - 1998 - Bulletin of Symbolic Logic 4 (3):233-272.
A Boolean model of ultrafilters.Thierry Coquand - 1999 - Annals of Pure and Applied Logic 99 (1-3):231-239.

Add more references