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).
Previous Page Next Page