Published online by Cambridge University Press: 24 October 2008
It has been known for some time ((6), p. 270; (4), theorem 9·19) that if is a Boolean topos, then the full subcategory
Kf of Kuratowski-finite objects in
is again a topos. For a non-Boolean topos
, however,
Kf need not be a topos, as can be seen when
is the Sierpinski topos ((1), example 7·1); on the other hand, two other full subcategories of
, coinciding with
Kf when
is Boolean, suggest themselves as candidates for a subtopos of finite objects. Of one of these, the category
dKf of decidable K-finite objects in
, the Main Theorem of (1) asserts that it is always a (Boolean) topos. The other is the category
sKf of
-subobjects of K-finite objects. The inclusions
dKf ⊆
Kf ⊆
sKf are clear.
are clear.