The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational implementation. Voevodsky has proposed such a program, including a new axiom with both geometric and logical significance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to homotopy (...) type theory. It also gives the new system of foundations a distinctly structural character. (shrink)
A comprehensive reference to category theory for students and researchers in mathematics, computer science, logic, cognitive science, linguistics, and philosophy. Useful for self-study and as a course text, the book includes all basic definitions and theorems, as well as numerous examples and exercises.
This paper is the first in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)
From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in this (...) case 2.In the present work, we generalize the entire arrangement from propositional to first-order logic, using a representation result of Butz and Moerdijk. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed primarily in the form of a contravariant adjunction, is established by homming into a common dualizing object, now Sets, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology.The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we give an elementary proof of Butz and Moerdijkʼs result in logical terms. (shrink)
Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired (...) by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in [20]. (shrink)
This brief article is intended to introduce the reader to the field of algebraic set theory, in which models of set theory of a new and fascinating kind are determined algebraically. The method is quite robust, applying to various classical, intuitionistic, and constructive set theories. Under this scheme some familiar set theoretic properties are related to algebraic ones, while others result from logical constraints. Conventional elementary set theories are complete with respect to algebraic models, which arise in a variety of (...) ways, including topologically, type-theoretically, and through variation. Many previous results from topos theory involving realizability, permutation, and sheaf models of set theory are subsumed, and the prospects for further such unification seem bright. (shrink)
of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has dependent types x : (...) A B(x), which are regarded as indexed families of types. There are simple type forming operations A × B and A → B, as well as operations on dependent types, including in particular the sum x:A B(x) and product x:A B(x) types (see the appendix for details). The Curry-Howard interpretation of the operations A × B and A → B is as propositional conjunction and.. (shrink)
This paper is the second in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)
The failed criterion of logical truth proposed by Carnap in the Logical Syntax of Language was based on the determinateness of all logical and mathematical statements. It is related to a conception which is independent of the specifics of the system of the Syntax, hints of which occur elsewhere in Carnap’s writings, and those of others. What is essential is the idea that the logical terms are invariant under reinterpretation of the empirical terms, and are therefore semantically determinate. A certain (...) objection to Carnap’s version of the invariance conception has been repeated several times in the literature. It is based on Gödel incompleteness, which is puzzling, since Carnap’s Syntax is otherwise quite careful to take account of Gödel. We show here that, in fact, the objection is invalid and is based on a confusion about determinacy. Sorting this out is worthwhile not only for the purpose of better understanding Carnap’s thinking in the Syntax, though. The invariance conception is also related to recent work in the philosophy of logic regarding “logicality”—the characterization of logical concepts—following a proposal of Tarski’s. It is even connected to some very recent developments in the foundations of mathematics. (shrink)
In this paper the machinery and results developed in [Awodey et al, 2004] are extended to the study of constructive set theories. Specifically, we introduce two constructive set theories BCST and CST and prove that they are sound and complete with respect to models in categories with certain structure. Specifically, basic categories of classes and categories of classes are axiomatized and shown to provide models of the aforementioned set theories. Finally, models of these theories are constructed in the category of (...) ideals. (shrink)
As McKinsey and Tarski showed, the Stone representation theorem for Boolean algebras extends to algebras with operators to give topological semantics for propositional modal logic, in which the “necessity” operation is modeled by taking the interior of an arbitrary subset of a topological space. In this article, the topological interpretation is extended in a natural way to arbitrary theories of full first-order logic. The resulting system of S4 first-order modal logic is complete with respect to such topological semantics.
This thesis is intended t0 help develop the theory 0f coalgebras by, Hrst, taking classic theorems in the theory 0f universal algebras amd dualizing them and, second, developing an interna] 10gic for categories 0f coalgebras. We begin with an introduction t0 the categorical approach t0 algebras and the dual 110tion 0f coalgebras. Following this, we discuss (c0)a,lg€bra.s for 2. (c0)monad and develop 2. theory 0f regular subcoalgebras which will be used in the interna] logic. We also prove that categories 0f (...) coalgebras are completc, under reasonably weak conditions, and simultaneously prove the wellknown dual result for categories 0f algebras. We dose the second chapter with 2. discussion 0f bisimulations in which we introduce a weaker 110tion 0f bisimulaticn than is current in the literature, but which is w€H—b€ha.v€d and reduces t0 the standard defmition under the assumption 0f choice. (shrink)
We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions . As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...) axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo-Fraenkel set theory. (shrink)
We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. In addition, we show that the full (...) axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo—Fraenkel set theory (IZF). (shrink)
This paper is the first in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)
This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting (...) framework is intended as a setting for the logical and categorical study of relative computability. (shrink)
We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E. In contrast to the well-known interpretation of higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE, but rather by a suitable complete Heyting algebra H. The canonical map relating H and ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such structures arise from surjective geometric morphisms (...) f : F → E, where H = f∗ΩF. The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are not longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion. (shrink)
This paper constructs models of intuitionistic set theory in suitable categories. First, a Basic Intuitionistic Set Theory (BIST) is stated, and the categorical semantics are given. Second, we give a notion of an ideal over a category, using which one can build a model of BIST in which a given topos occurs as the sets. And third, a sheaf model is given of a Basic Intuitionistic Class Theory conservatively extending BIST. The paper extends the results in [2] by introducing a (...) new and perhaps more natural notion of ideal, and in the class theory of part three. (shrink)
This paper is the second in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)
Moerdijk has introduced a topos of sheaves on a category of filters. Following his suggestion, we prove that its double negation subtopos is the topos of sheaves on the subcategory of ultrafilters - the ultrasheaves. We then use this result to establish a double negation translation of results between the topos of ultrasheaves and the topos on filters.
In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.
Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. We give rules for bracket types in dependent type theory and provide complete semantics using (...) regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally Cartesian closed categories. We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic, in the sense that a formula from the fragment is derivable in intuitionistic first-order logic if, and only if, its interpretation in dependent type theory is inhabited. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete, in the same sense, for all of classical first-order logic. (shrink)
We introduce a new sheaf-theoretic construction called the ideal completion of a category and investigate its logical properties. We show that it satisfies the axioms for a category of classes in the sense of Joyal and Moerdijk [17], so that the tools of algebraic set theory can be applied to produce models of various elementary set theories. These results are then used to prove the conservativity of different set theories over various classical and constructive type theories.
The notion of a continuously variable quantity can be regarded as a generalization of that of a particular (constant) quantity, and the properties of such quantities are then akin to, and derived from, the..
We investigate a certain system of intuitionistic set theory from three points of view: an elementary set theory with bounded separation, a topos with distinguished inclusions, and a category of classes with a system of small maps. The three presentations are shown to be equivalent in a strong sense.
The [lambda]-calculus can be represented topologically by assigning certain spaces to the types and certain continuous maps to the terms. Using a recent result from category theory, the usual calculus of [lambda]-conversion is shown to be deductively complete with respect to such topological semantics. It is also shown to be functionally complete, in the sense that there is always a ‘minimal’ topological model in which every continuous function is [lambda]-definable. These results subsume earlier ones using cartesian closed categories, as well (...) as those employing so-called Henkin and Kripke [lambda]-models. (shrink)
The notion of a continuously variable quantity can be regarded as a generalization of that of a particular quantity, and the properties of such quantities are then akin to, and derived from, the properties of constants. For example, the continuous, real-valued functions on a topological space behave like the field of real numbers in many ways, but instead form a ring. Topos theory permits one to apply this same idea to logic, and to consider continuously variable sets . In this (...) expository paper, such applications are explained to the non-specialist. Some recent results are mentioned, including a new completeness theorem for higher-order logic. (shrink)
Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby. In order to stay focused on the “big picture”, we merely sketch the overall form of each construction, referring to the (...) literature for details. Each of the three steps considered below is based on more recent logical research than the preceding one. The first step from sets to types is essentially the familiar idea of set theoretic semantics for a syntactic system, i.e. giving a model; we take a brief glance at this step from the current point of view, mainly just to fix ideas and notation. The second step from types to categories is known to categorical logicians as the construction of a “syntactic category”; we give some specifics for the benefit of the reader who is not familiar with it. The third step from categories to sets is based on quite recent work, but captures in a precise way an intuition from the early days of foundational studies. With these pieces in place, we can then draw some conclusions regarding the differences between the three schemes, and their relative merits. In particular, it is possible to state more precisely why the methods of category theory are more appropriate to philosophical structuralism. (shrink)
The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π, and intensional identity types Id, as used in (...) homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: they should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory. (shrink)
