([SGA4],[Jo 1]), i.e. a geometric theory T_ classified by the sheaf
category E*-• S . The object one is looking for is then (a subobject of
the associated sheaf of) G = Z Hom(c,-) . Due to genericity, G may
satisfy further, non-geometric properties (e.g. preservation of cardinals
in forcing in set theory). As a simplicial set, G is the positive part of
the augmented complex Dec (Nerv(C)) (for simplicial methods, cf. [Dus]).
A generic object G thus constructed may not fall into cumulative hier-
archy 0 ^ P(0) - » P(P(0))*-• ...«#• lim Pn(0) = PW(0) *• . . . •* Pa(0) * ...
in the classifying topos E . However, working in E , one can force G
into cumulative hierarchy in a topos over E by constructing a generic
embedding G*^P (0) for a large enough. E.g. to construct G^-* 2
one looks at the poset [N,G;2] of finite partial functions f: N*G *2
as forcing conditions in E ordered by inclusion, with an appropriate
Grothendieck topology which enables properties of G in E to be
inherited to G as a subobject of 2 in a topos over E . E.g., one
can look at sheaves over 2 in S , or at 11-topology on [N,G;2] in
E . In this way, consistency and independence results w.r.t. higher-order
arithmetic (i.e. type theory) are strengthened to ones w.r.t. ZF set
As first examples, we construct two classifying topoi by using our
general forcing method. In both examples, instances of a very general
duality are used to compute categories of forcing conditions. This duality
is important in applications to model theory as well.
Permutation models are recently being studied with renewed interest
as (atomic) topoi ([BD],[Fre 1]). In chapter 2 we use our general method
of forcing to study them as classifying topoi. In particular, all examples
in [BD] are shown to be of one kind, i.e. topoi of continuous H-sets for
various topological groups H . (General features of these topoi are used
in chapter 4 in applications to models of intuitionistic set theory). In
particular, in one of those examples, we show how to construct the etale
topos by forcing.
We also reexamine forcing in set theory (chapter 3). Our main new
result there (which goes beyond [Ti 1], and [F]) is that the standard set-