FORCING AND CLASSIFYING TOPOI

3

of morphisms in E , natural in Z,Y „ Equivalently, for

each object X , the functor (-)*X: E •+ E has a right

adjoint (-)X: E + E .

(iii) E has a subobject classifier, i.e. an object ft and

a morphism 1 — * ft (called "true") such that, for each

monomorphism Y *- * X in E , there is a unique morphism

4 : X-*•ftin £ (the classifying map of a ) making

Y c *X

1

1 —^-* ft

a pullback diagram.

[Jo1 , §1.1] gives an outline of the proof that each presheaf category

Eop

S is an elementary topos.

A natural number object in an elementary topos E is an object N

c s

together with morphisms 1 —*N—*N such that for any diagram

x u f

1 - * X - * X in E , there exists a unique N -» • X such that the following

diagram commutes:

0 s

X ^

N

„N

;f ! f

X

(Eop

In a presheaf topos S , the natural object is given by the con-

stant presheaf U .

In an elementary topos E , the lattice of subobjects of each object

is a Heyting algebra. If, in addition, for every A1-* B in E there is

A1 «-* B with AAA'= 0 , AvA' = B (so the lattice of subobjects of each

object of E is a Boolean algebra), we say that E is a Boolean topos.

0.4. Presheaf Semantics.

Any elementary topos interprets intuitionistic higher-order logic,

and any elementary topos with a natural number object interprets intuition-

istic higher-order arithmetic (Boolean topoi interpret classical logic)