Presheaf Toposes and Propositional Logic
| Autor: | Squire, Richard |
|---|---|
| Rok vydání: | 2010 |
| Předmět: | |
| Druh dokumentu: | Diplomová práce |
| Popis: | 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: v v ד v ε L([symbol removed]) iff C is a groupoid. The presheaf topos [symbol removed], of actions of a single idempotent, whose i.p.l. is given by: φ ε L([symbol removed]) iff ד u v v v (v → u) ꜔ φ, 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]). 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]. This theorem has as particular cases: (1) [symbols removed] (2) [symbols removed] (3) [symbols removed] Doctor of Philosophy (PhD) |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|