Automorphisms of partial combinatory algebras and realizability models of constructive set theory

In this thesis we investigate automorphisms of partial combinatory algebras and construct realizability models of constructive set theory. After some introductory and background material in chapters 1 and 2, we define in chapter 3 a generalisation of Kripke and realizability models of intuitionistic...

Full description

Bibliographic Details
Main Author: Swan, Andrew Wakelin
Published: University of Leeds 2012
Subjects:
Online Access:http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.590459
Description
Summary:In this thesis we investigate automorphisms of partial combinatory algebras and construct realizability models of constructive set theory. After some introductory and background material in chapters 1 and 2, we define in chapter 3 a generalisation of Kripke and realizability models of intuitionistic logic that we call Kripke realizability models. In chapters 4, 6 and 7 we then develop various realizability models of constructive set theory. We show in chapter 5 how to use these techniques to investigate the automorphisms of some partial combinatory algebras. In chapter 8 we use a Kripke realizability model to show that a property known as the existence property does not hold for the set theory CZF.