where f(&i) denotes F(f)(ai), the value of the mapping F(C) - F(Cf)
at a. . The higher-order aspect of the language is interpreted as
follows: the sort Q is the power-sort of the sort F .
We say that a sentence $ is true in S , and write S t= (J ,
if C II - (J ) at each object C of C . The truth-value | | f | f of a
formula f(x1,...,x ) is the subfunctor | | J11"* C ' Fn given by
Il4)| l (C) = {ai,...,an e Fn(C)lC lhf)(x1/.../xn)[a1,]} .
When ( C is the trivial one-object category, the presheaf semantics
in S specializes to the ordinary Tarski semantics.
0.5. Grothendieck Topologies. Sheaves. Grothendieck Topoi.
Let E be a small category. A Grothendieck topology on ( C is
defined by specifying a set J(X) of sieves on X (i.e. subfunctors
of hY ) called coverinq sieves of the topology, for each object X of
( C , such that:
(i) For any X , the maximal sieve {a| codomain (a) = X}
is an element of J(X) .
(ii) If R e J(X) , and Y * X is a morphism of E , then the
f*(R) = {Z + Y|fa e R}
is an element of J(Y) (closure under pullbacks).
(iii) If R G J(X) , and S is a sieve on X such that for each
Y I X in R we have f*(S) e J(Y) , then S e J(X) .
A small category equipped with a Grothendieck topology is called a site.
The following lemma is useful in the applications.
Lemma (folklore). Let K be a family of sieves in a small category E ,
and assume K is closed under pullbacks. Then the Grothendieck topology
J generated by K is the smallest family f sieves in C D that includes
K and satisfies (i) and (iii) above.
Let ((E,J) be a site, F a presheaf on E . We say that F is a
sheaf (for the topology J ), if for every object X of C , and every
R e J(X) :
Previous Page Next Page