Classifying Topoi and Preservation of Higher Order Logic by Geometric Morphisms.

[摘要] Topoi are categories which have enough structure to interpret higher order logic.They admit two notions of morphism: logical morphisms which preserve all of the structure and therefore the interpretation of higher order logic, and geometric morphisms which only preserve only some of the structure and therefore only some of the interpretation of higher order logic.The question then arises: what kinds of higher order theories are preserved by geometric morphisms?It is known that certain first order theories called internal geometric theories are preserved by geometric morphisms, and these admit what are known as classifying topoi.Briefly, a classifying topos for an internal geometric theory T in a topos E is a topos E[T] such that models of T in any topos F with a geometric morphism to E are in one to one correspondence with geometric morphisms from F to E[T] over E.One useful technique for showing that a higher order theory Tau is preserved by geometric morphisms is to define an internal geometric theory T of ;;bad sets;; for Tau and show that Tau is equivalent to the higher order theory which says ;;the classifying topos for T is degenerate;;.We set up a deduction calculus for internal geometric theories and show that it proves a contradiction if and only if the classifying topos of that theory is degenerate. We use this result to study a variant of the higher order theory of Dedekind finite objects and the higher order theory of field objects considered as ring objects with no non-trivial ideals.

[发布机构] University of Michigan

[效力级别] Geometric Morphisms

[关键词] Topos Theory;Geometric Morphisms;Higher Order Logic;Mathematics;Science;Mathematics