Categorical Logic

Abstract

In this section we present some basic results concerning the theory of elementary topoi and sheaves. A topos is a special kind of a category defined by axioms which allow that certain constructions with sets can be done in this category too. The original notion of a topos is closely connected with the notion of the category of sheaves over topological spaces, which was introduced for use in algebraic geometry. For our purposes this aspect and the origin of topos theory is not so important. We are interested in aspects in which a logic is predominant and which enable us to think of topoi as models of a theory. The introduction of topos theory as a generalization of set theory is revolutionary. The basic new idea depends on the fact that for the investigation and definition of some objects we use the relations between objects instead of the elements of these objects. Surely, this idea has its origin in category theory and basically utilizes methods of this theory.