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 ] ,
Previous Page Next Page