## Intuitionistic choice and classical logic

### Thierry Coquand and Erik Palmgren,
** Archive for Mathematical Logic, ** to appear

** 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.

Back to the list of publications.
Erik Palmgren,
November 10, 1999.