Abstract. 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.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received: 20 March 1997 / Revised version: 20 February 1998
Rights and permissions
About this article
Cite this article
Coquand, T., Palmgren, E. Intuitionistic choice and classical logic. Arch Math Logic 39, 53–74 (2000). https://doi.org/10.1007/s001530050003
Issue Date:
DOI: https://doi.org/10.1007/s001530050003