Vlll
INTRODUCTION
theoretic notion of a generic subset of a poset is actually classified by
the topos of double negation sheaves. More precisely, if C is a poset,
G** AC described above reduces to the fuctor G(c) = {c'ectc* £ c} .
G=* AC is mclosed iff 11topology on Cop is subcanonical. If C
has a least element, and a sup of each two compatible elements,
Q
Shjj(C)c* S classifies the theory of a "generic subset of C" in the
standard settheoretic sense. Sh,, (C) is equivalent as a category to the
topos of sheaves on a cBa RO(Cop) .
Iterations of this construction through the ordinals are considered
in the second part of chapter 3. There we prove another of our main new
results, that iterated forcing in set theory (in particular, the one given
by Solovay and Tennenbaum, cf. e.g. [Ku]) and Grothendieck1s construction
of a lax limit of a fibred topos in [SGA 4], Exp. VI, §§68 (which was
motivated by notions and problems in algebraic geometry and algebraic
topology), are the same up to Godel's negative interpretation of classical
into intuitionistic logic. This suggests possibilities of interapplica
tions between logic, and algebraic geometry and algebraic topology.
For concreteness, we consider the SolovayTennenbaum iterated forcing
although a general iterated forcing construction (cf. e.g. [Ku, chapter
VIII] is an example of the lax limit of a fibred topos.
More precisely, let B be a cBa in a topos of sheaves on a cBa B .
It then follows from a general sheafrepresentation theorem [FSo] that
the set r(8) of global sections of 8 is a complete Heyting algebra,
(and here it is in fact a cBa), that
sh
Sh(B)
*B*

sh^r^B))
r
an d
that
B** T(8) is a complete Boolean inclusion. If A is a limit ordinal,
and Bn ** B.. «*...«• B  . . . (aA) are complete Boolean inclusions, let
E, be the lax limit of the fibred topos Sh(B„ )TTZS\\ (B.. )!7T^. . . TT^Sh(B )tTl
A 0 1 a
... (aA) . Then shj(E,) ^ Sh(B,) , where B, is the Boolean com
pletion of U B
aA
Applications to intuitionistic systems are given in chapter 4. In
section 4.1 we extend a model of secondorder intuitionistic arithmetic
given in [Kr] to a symmetric extension of a Heytingvalued model of intui
tionistic set theory ZFI with Collection (roughly speaking, a topos
localic over a topos of continuous Hsets), showing that ZFI is consistent