Document Zbl 0433.18001

Finiteness and decidability: I. (English) Zbl 0433.18001

Applications of sheaves, Proc. Res. Symp., Durham 1977, Lect. Notes Math. 753, 80-100 (1979).

The possibility of treating elementary toposes as ”models” of various versions of intuitionistic set theory - the objects of the topos being the sets of the model - makes it natural to investigate the meanings in topos theory of the various set-theoretic definitions of finiteness. The present paper focuses attention on the decidable (objects for which the equality predicate satisfies the tertium non datur) Kuratowski-finite (objects satisfying the internalization of the condition that they are non-isomorphic to all their proper subobjects) objects. The full subcategory formed by these, denoted \( E_{d x f} \), in the topos \( E \) is shown to be a topos satisfying the intrinsinc axiom of choice. Hence it is boolean. Its subobject classifier is the complemented-subobject classifier \( 1+1 \) of \( E \), and it is closed under exponentiation, finite limits and finite coproducts, and the inclusion functor \( E_{d k} \rightarrow E \) is logical if and only if \( E \) is boolean. Moreover, such inclusion functors are respected by the inverseimage part of any geometric morphism between toposes. In the final section of the paper the Sierpinski topos \( S \overrightarrow{ }{ }^{\vec{n}} \) is shown to be an example where the full subcategory of all Kuratowski-finite objects is not a topos. It is also shown that such objects in a topos of set-valued presheaves on a small category \( C \) form a topos if and only if \( C \) has the property \( C(A, B) \neq \emptyset \Rightarrow C(B, A) \neq \emptyset \). In this case all the Kuratowski-finite presheaves are decidable. The paper does not take up the study of possible connections between the existence of a naturalnumber-object, an object-classifier, and an internalization in \( E \) of \( E_{d} K_{1} \).

This review text is based on a scanned copy of the printed version. It was converted to LaTeX using MathPix and a specifically developed LLM to assign the text parts to the metadata. It may contain errors, misassignments, or gaps; in particular, the reviewer signature has not yet been extracted reliably in general. If you notice any errors, please report them directly to our editorial team via the Contact Form.