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. 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.
Erik Palmgren, November 10, 1999.