The present thesis investigates the validity of some interesting principles such as
the Axiom of Choice, AC, in the general extensional realizability structure V(A)
for an arbitrary applicative structure, A, generalising the result by Rathjen established for the specific realizability model V(K_1), the Fan Theorem, FT,
and the principle of Bar Induction, BI, in the particular realizability structures
over the Graph Model, V(P(omega)), and over the Scott D1 Model, V(D_infty), since, in the
literature, little is known about these realizability models and most investigations
are carried out in the realizability models built over Kleene's first and second models.
After an introduction and some background material, given in the first two
chapters, I introduce the notion of extensional realizability over an arbitrary
applicative structure, A, and I show that variants of the axiom of choice hold in
V(A). Next, the focus switches from considering the general realizability structure
V(A) generated on an arbitrary applicative structure, A, to the specific realizability
universes, V(D_infty) and V(P(omega)) to investigate some interesting properties including
the validity of FT and BI in these universes.
For the remainder of the thesis, a proof of the soundness of realizability with
truth, as it leads to different applications than that without truth, for the theories
CZF and CZF + REA, is given and an investigation of many choice principles
is carried out in the truth realizability universe V*(A) for an arbitrary applicative
structure, A.
