4 ANDREJ S^EDROV

[Jo 1 ,§5.4] [BJ],[Os]. A particular case of this interpretation, for a

topos of presheaves, merits attention, and which when C E is a poset,

reduces to the Kripke semantics for higher-order intuitionistic theories.

Eop

Let E be a small category. Each object of S is considered as

a sort of the language. For each object C of ( C , formula f (x., . . . ,x )

of the language (whose free variables are among x,,...,x of sorts

F,,...,F , respectively), and a choice of elements a. eF.(C) , 1 • i £ n,

we define "C forces (|(x,,...,x ) for (a,,...,a ) ", written as:

C |h f (x1, .. . ,xn)[alf. . . ,anl ,

by i n d u c t i o n on th e c o m p l e x i t y o f j . For s i m p l i c i t y , l e t us assume

FT

= F

0

= . . . = F = F .

1 2 n

0) C \\- T , CjK JL .

1) For each n-any predicate symbol P(x,,...,x ) let P ^ F

be a given subfunctor of the n-fold cartesian product F

Then Cll-P(x1,...,xn)[a1,...,an] iff alf...,a e P(C) .

2) C If - x, = x2 [a,,a2] iff a, = a2 as element of F(C) .

,al

•,an].

.,an].

3) C lh (fAip) (x1,...,xn) [a1,...,an] iff C lhMx^ . . . ,xn)[a^ .

and C Ihip (xlf.. . ,xR) [a1,.,an],

4) C lh (fvij ) (xx,.. .,xn) [aL,. . .,an] iff c IH (x^ . . . ,xn) [a^

or clhip(x1# . . .,xR) [a1# .

5) C lh (J-H0(x.,. . . ,x )[a1,...,a ] iff for each morphism C'-»C

in ( C , if

C'lh(|)(x1,...,xn) [fta,),...,(aj],n1

1 n

then

C » l h ^ ( x

1

, . . . , x

n

) [ f (

a i

) . . . f ( a

n

) ]

(th e meaning o f f ( a . ) w i l l be

e x p l a i n e d b e l o w ) .

6) Clh3yJ(x1, . . . , x

n

, y ) [ a

1

, . . . , a

n

] i f f fo r some b e F(C) ,

ClhJ ( x

x

, . . . / X

n

, y ) [ a

r

. . ^

n

, b ] .

7) ClK Vy| (x^, . . . , x ,y ) [ a , , . . . , a ] i f f fo r eac h morphism C—-C i n

C C , and eac h b e F ( C ' ) , C'lh 4 ( x

r

. . . , x

R

, y ) [f ( a ^ , . . .,f (a

R

) ,b ] ,