Topoi and logic

Abstract

This thesis surveys the theory of those categories called elementary topoi, with particular emphasis on the relationship between topoi and mathematical logic. Sections 1.1 and 1.2 introduce the elementary topos, which has several equivalent definitions: as a finitely complete and cocomplete category ε with exponentiation and a representor for the subobject functor Sub: εop→ ε as a cartesian closed category with a subobject representor; and as a finitely complete category with a representor for each functor Rel(A,-) = Sub(A -): εop→ε In section 1.3, a number of technical results are developed, to be used later in the thesis. The notion of "mathematics in a topos" is examined in section 1.4: topos theory has arisen partly from attempts to put set theory (and hence mathematics) on a categorical foundation, and various theories in the language of category theory have been proposed as axiomatisations of the "theory of the category of sets". The axioms for a topos are included in each of these theories and so a topos is in a sense a generalisation of the category of sets and functions; the category Set of "naive" sets and functions is a topos. In section 1.4, some of these "theories of the category of sets" are described briefly, and the idea of a topos as a generalisation of Set is illustrated by a number of examples of mathematical constructions which "lift" to an arbitrary topos. Chapter two is concerned with a body of results often called the "internal logic of a topos". After a brief resume of some results in the theory of Heyting algebras (section 2.1), section 2.2 shows how the partially ordered sets Sub(A) of subobjects of a given object A of a topos has the structure of a Heyting algebra. These Heyting algebras, of course, generalise the Boolean algebras of subsets of a set. Some set-theoretic notions, however, have two generalisations to an arbitrary topos; for instance, the power set of a set A has as generalisations to an arbitrary topos both the set Sub(A) and the power-object P(A), that is, the representor of the functor Rel(A,-). One speaks of the set Sub (A) as being "external" and of the power object P(A) as being "internal"; section 2.3 explains this external/internal dichotomy a little more and examines some "internal versions" of the Heyting algebra operations on the Heyting algebras Sub(A) of a topos. In a sense explained in section 2.3, these "internal operations" make Ω, the subobject representor, a "Heyting algebra-object". Section 2.4 surveys a number of "quantifier-arrows" defined in a topos, and explains how in the category Set they really do quantify. In chapter three, I attempt to make precise the somewhat vague notion of "internal logic of a topos" by defining a "first order semantics in a topos" and a notion of " ε-validity" for a topos ε. It is shown that all intuitionistic theorems are ε-valid for any topos ε although this is not true of all classical theorems unless the topos satisfies a certain"axiom of Boolean-ness", and a topos ε is given for which ε -validity characterizes intuitionistic theorem-hood. This particular ε -semantics turns out to be essentially the semantics of S.A. Kripke.