Presheaf Toposes and Propositional Logic

Abstract

<p>To each non-degenerate topos [symbol removed] we associate L([symbol removed]), the intermediate propositional logic (i.p.l.) consisting of those polynomials, built up from variables, 0, 1, ʌ, v and →, which become valid when interpreted in the natural internal Heyting algebra structure of the subobject classifier of [symbol removed]. For various polynomials φ, we give first order characterizations for the class of small categories determined by the condition φ ε L([symbol removed]) - where [symbol removed] is the topos of sets and C ranges over small categories. A basic example is:</p> <p>v v ד v ε L([symbol removed]) iff C is a groupoid.</p> <p>The presheaf topos [symbol removed], of actions of a single idempotent, whose i.p.l. is given by:</p> <p>φ ε L([symbol removed]) iff ד u v v v (v → u) ꜔ φ,</p> <p>is used to exemplify a relativization of the basic example, to toposes. For each topos [symbol removed] we introduce r([symbol removed]), the set of all polynomials φ such that for all internal categories C of [symbol removed], if φ ε L([symbol removed]) then C is a groupoid. Using a theorem of Jankov's we can compute ɼ([symbol removed]) when M belongs to a certain class of finite monoids that includes semilattices; in particular: φ ε ɼ([symbol removed]) iff φ ꜔ u v (u → (v v ד v)). This polynomial - the cogenerator of ɼ([symbol removed]) - is strictly weaker than the generator of L([symbol removed]).</p> <p>We use the higher order type theoretical language of a topos ([symbol removed]), developed in the first half of the thesis, to establish that for an extensive class of polynomials, the condition φ ε ɼ([symbol removed]) can be internalized; that is, we can define a formula ([symbol removed]), of the language of [symbol removed], such that: φ ε ɼ([symbol removed]) iff [symbols removed].</p> <p>This theorem has as particular cases:</p> <p>(1) [symbols removed]</p> <p>(2) [symbols removed]</p> <p>(3) [symbols removed]</p>