This paper presents two types of realizability models for intuitionistic set theories. The point of departure for every notion of realizability will be a domain of computation, called a
partial combinatory algebra
. To put it roughly, the role of a
in the first type of realizability is to furnish a concrete instantiation of the Brouwer-Heyting-Kolmogorov interpretation of the logical connectives. In a sense, partial combinatory algebras can lay claim to be of equal importance to models of intuitionistic set theory as partial orderings are to forcing models of classical set theory.
Among other things, these models can be used to extract computational information from proofs. Their main employment here, however, will be to provide consistency, equiconsistency, and independence results. Relinquishing classical logic can bring forth considerable profits. It allows for axiomatic freedom in that one can adopt new axioms that are true in realizability models but utterly false classically.