nLab Kleene-Vesley topos

Contents

Idea

The effective part of the function realizability topos $RT(\mathcal{K}_2)$ .

This construction in realizability goes back to

Stephen Kleene, R. E. Vesley, The foundations of intuitionistic mathematics,North-Holland (1965)

The Kleene-Vesley topos as such is discussed for instance in

Jaap van Oosten, page 279 of Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

Last revised on March 8, 2014 at 07:42:34. See the history of this page for a list of all contributions to it.