FORCING AND CLASSIFYING TOPOI

7

F(X) = {aeG(X)l3R e J(X).V(Y " X) e R.a(a) e F(Y)} ,

where the meaning of a(a) is as in 0.4. above.

We say that F is a J-closed subobject of G in S iff F = F .

It is easy to see that a closed subobject of a sheaf is a sheaf. Moreover,

an important example of a Grothendieck topos is the category of canonical

sheaves on a complete Heyting algebra (i.e. locale) (cf. [FSo]). More

precisely, R-* h is a covering iff p = yR in the complete Heyting

algebra structure. Every topos of sheaves on a poset is equivalent as a

category to a topos of (canonical) sheaves on a locale (cf. e.g. [Jo 1 ,

§5.37] .

0.6. Sheaf Semantics.

To describe the elementary topos semantics for intuitionistic higher-

order arithmetic in the case of a topos of sheaves, one needs to recon-

sider the presheaf semantics. We are now interested in sentences true

"locally", "on a cover". To this purpose, the clauses 1), 2), 4), and 6)

for the presheaf semantics are modified as below, and the clauses 0),3),

5), and 7) are left intact. Furthermore, only sheaves are allowed as sorts

of the language.

1) C IH P(x-,...,x )[a,,...,a 1 iff

l n i n

.1R e J(C).V(C S c) e R.a(ax) ,...,a(a ) e P(C) ,

where the meaning of a (a.) is as in 0.4. above.

2) C ih xx = x2[a1,a2] iff ] R e J(C).V(C + C) e R.afa^ = a(a2) .

4) C IM$vt) (x1,...,xn)[a1,...,an] iff

I R E J(C).V(C £ C) e R. C if - * (x-,...,x ) [a(a,) ,.. . ,a(aJ ]

l n 1 n

or CMl-^(x1,.. . ,xn) [a(a1),.. .,a(an)].

6) C!!-3y^(x1,...,xn) [a1,...,an] iff

dR e J(C).V(C •* • C) e R.3b c F (Cf) .C'lh f ) (x^ . . . ,*n,y)

[aia^),...,a(an),b] .

Fourman [F] and Hayashi have given extensions of this interpretation to

ZF set theory (in a Grothendieck topos).