INTRODUCTION

vil

([SGA4],[Jo 1]), i.e. a geometric theory T_ classified by the sheaf

Q

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

ce|c|

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) * ...

n

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

a N

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

N

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

theory.

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-