We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a …
We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a special form. The main result is that the class of models of a generalized geometric theory is set-generated . Here, a class $\mathcal{X}$ of subsets of a set is set-generated if there exists a subset G of $\mathcal{X}$ such that for each α ∈ $\mathcal{X}$ , and finitely enumerable subset τ of α there exists a subset β ∈ G such that τ ⊆ β ⊆ α. We show the main result in the constructive Zermelo–Fraenkel set theory ( CZF ) with an additional axiom, called the set generation axiom which is derivable in CZF , both from the relativized dependent choice scheme and from a regular extension axiom. We give some applications of the main result to algebra, topology and formal topology.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of …
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of …
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Loef's intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on the problem whether there are (enough) injective sets in CZF.
We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that there are strongly enough injective sets. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory.
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of …
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Loef's intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on the problem whether there are (enough) injective sets in CZF. We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that there are strongly enough injective sets. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory.
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic …
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic phenomenon: let H be an endofunctor such that for every object X a final coalgebra, TX, of H(_) + X exists. Then TX is an object-part of a monad which is completely iterative. Moreover, a similar contruction of a "completely iterative monoid" is possible in every monoidal category satisfying mild side conditions.
The notion of a recursive density type (R.D.T.) was introduced by Medvedev and developed by Pavlova (1961). More recently the algebra of R.D.T.'s was initiated by Gonshor and Rice (1969). …
The notion of a recursive density type (R.D.T.) was introduced by Medvedev and developed by Pavlova (1961). More recently the algebra of R.D.T.'s was initiated by Gonshor and Rice (1969). The R.D.T.'s are equivalence classes of sets of integers, similar in many respects to the R.E.T.'s. They may both be thought of as effective analogues of the cardinal numbers. While the equivalence relationfor R.E.T.'s is defined in terms of partial recursive functions, that for R.D.T.'s may be characterized in terms of recursively bounded partial functions (see 4.22a).
Bachmann, in [2] shows how certain ordinals < Ω ( Ω = Ω 1 where Ω ξ is the (1 + ξ )th infinite initial ordinal) may be described from …
Bachmann, in [2] shows how certain ordinals < Ω ( Ω = Ω 1 where Ω ξ is the (1 + ξ )th infinite initial ordinal) may be described from below using suitable descriptions of ordinals < Ω 2 . The aim of this paper is to consider another approach to describing ordinal < Ω and compare it with the Bachmann method. Our approach will use functionals of transfinite type based on Ω . The Bachmann method consists in denning a hierarchy of normal functions ϕ δ : Ω → Ω (i.e. continuous and strictly increasing) for δ ≤ η 0 < Ω 2 , starting with ϕ 0 ( λ ) = ω 1 + λ . The definition of depends on a suitable description of the ordinals ≤ η 0 . This is obtained by defining a hierarchy 〈 F δ ∣ δ ≤ Ω 2 〉 of normal functions F δ : Ω 2 → Ω 2 analogously to the definition of the initial segment 〈ϕ δ ∣ δ ≤ Ω 〉 of . The ordinal η 0 is . Note . Our description of Bachmann's hierarchies will differ slightly from those in Bachmann's paper. Let and denote the hierarchies in [2]. Then as Bachmann's normal functions are not defined at 0 we let for λ, δ < Ω 2 . Bachmann defines for 0 < λ < Ω 2 but it seems more natural to omit this so that we let . The situation is analogous for and leads to the following definitions: where n < ω and ξ is a limit number of cofinality Ω , and
Abstract The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo–Fraenkel set theory. We deduce this statement from the principle of refinement, which we …
Abstract The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo–Fraenkel set theory. We deduce this statement from the principle of refinement, which we distill before from the axiom of fullness. Together with exponentiation, refinement is equivalent to fullness. None of the defining properties of an ordering is needed, and only refinement for two–element coverings is used. In particular, the Dedekind reals form a set: whence we have also refined an earlier result by Aczel and Rathjen, who invoked the full form of fullness. To further generalise this, we look at Richman's method to complete an arbitrary metric space without sequences, which he designed to avoid countable choice. The completion of a separable metric space turns out to be a set even if the original space is a proper class: in particular, every complete separable metric space automatically is a set.
One of the main goals of this paper is to give a construction of realizability models for predicative constructive set theories in a predicative metatheory. We will use the methods …
One of the main goals of this paper is to give a construction of realizability models for predicative constructive set theories in a predicative metatheory. We will use the methods of algebraic set theory, in particular the results on exact completion from van den Berg and Moerdijk (2008) [5]. Thus, the principal results of our paper are concerned with the construction of an extension of a category with small maps by a category of assemblies, again equipped with a class of maps, and to show that this extension construction preserves those axioms for a class of maps necessary to produce models of the relevant set theories in the exact completion of this category of assemblies.
Abstract This paper explores the set theoretic assumptions used in the current published proof of Fermat's Last Theorem, how these assumptions figure in the methods Wiles uses, and the currently …
Abstract This paper explores the set theoretic assumptions used in the current published proof of Fermat's Last Theorem, how these assumptions figure in the methods Wiles uses, and the currently known prospects for a proof using weaker assumptions.
We study the connection between the axiom of choice and the principles of existence of enough projective and injective abelian groups. We also introduce a weak choice principle that says, …
We study the connection between the axiom of choice and the principles of existence of enough projective and injective abelian groups. We also introduce a weak choice principle that says, roughly, that the axiom of choice is violated in only a set of different ways. This principle holds in all ordinary Fraenkel-Mostowski-Specker and Cohen models where choice fails, and it implies, among other things, that there are enough injective abelian groups. However, we construct an inner model of an Easton extension with no nontrivial injective abelian groups. In the presence of our weak choice principle, the existence of enough projective sets is as strong as the full axiom of choice, and the existence of enough free projective abelian groups is nearly as strong. We also prove that the axiom of choice is equivalent to “all free abelian groups are projective” and to “all divisible abelian groups are injective."
Zusammenfassung P. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole …
Zusammenfassung P. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander (mit trivialen Funktionen als Ausgangspunkt). Abstract P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand-point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other (starting with trivial functions).
We show that the category of basic pairs ( BP ) and the category of concrete spaces ( CSpa ) are both small-complete and small-cocomplete in the framework of constructive …
We show that the category of basic pairs ( BP ) and the category of concrete spaces ( CSpa ) are both small-complete and small-cocomplete in the framework of constructive Zermelo–Frankel set theory extended with the set generation axiom. We also show that CSpa is a coreflective subcategory of BP .
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle …
Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad.
1. Introduction and summary. The theory of hierarchies deals with the classification of objects according to some measure of their complexity. Such classifications have been fruitful in several areas of …
1. Introduction and summary. The theory of hierarchies deals with the classification of objects according to some measure of their complexity. Such classifications have been fruitful in several areas of mathematics: analysis (descriptive set theory), recursion theory, and the theory of models. Although much of the hierarchy theory of each of these areas was developed independently of the others, Addison, in the series of papers [Ad 1-6], has shown not only that there are deep-seated analogies among these theories, but that indeed many of their results can be derived from those of a general theory of hierarchies. Toward a further consolidation of these theories, this paper will study the relationships and analogies between certain classical hierarchies of descriptive set theory and their counterparts in recursion theory. The roots of modern hierarchy theory lie in the investigations of Baire, Borel, Lebesgue, and others around the turn of the century. As analysts with a concern for the foundations of their subject, they felt that constructions effected by means of the axiom of choice or the set of all countable ordinals were less secure than those carried out by more elementary means. They sought to discover what role these suspect constructions played in analysis and whether or not they could be avoided altogether. Thus descriptive set theory arose with the goal of identifying, classifying, and studying those sets (of real numbers) which were of interest for analysis and for which an construction could be given. Needless to say, there was vigorous disagreement as to just what constituted an explicit construction. The first large class of sets studied were the Borel sets. Since each Borel set can be constructed by iteration of the elementary operations of countable union and
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new …
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
Introduction.The theory of recursive density types was introduced by Medvedev [1] and studied by Pavlova [2], [3].Rice [4] made use of the concept in order to characterize B*, the class …
Introduction.The theory of recursive density types was introduced by Medvedev [1] and studied by Pavlova [2], [3].Rice [4] made use of the concept in order to characterize B*, the class of recursively bounded orders.In this paper we shall develop an algebra of recursive density types (called densities for short) analogous to Dekker's theory of recursive equivalence types.In order to keep this work self-contained, theorems probably proved by Pavlova [3] in her paper which was unavailable to us will be proved here.It will be seen that interesting phenomena occur here which do not occur in more traditional cardinality theories.As far as possible, Dekker's notation for numbers, sets, and classes will be used.In addition the following notations will be adopted.If a is an infinite set, then a(n) is the function enumerating a in order of size.Sometimes a will be used to represent the function providing there is no danger of confusion.Also n(a, x) will denote the number of elements in a not greater than x. Definition and elementary properties of densities. Definition ß ^ a <-> (3 recursive h){ix){n[ß, h(x)] ^ n(a, x)}.Several consequences follow immediately from the definition.(1) « may be taken to be strictly increasing.(2) It is sufficient to require the inequality only for all x^x0 where x0 is fixed.(3) If a and ß have finite cardinality, then /? ä a <-> card ßï;card a.If a has finite cardinality and ß does not, then ß^a but -,(a^ß).(4) For infinite a and ß the definition can be expressed equivalently in function language asRemarks analogous to (1) and (2) hold here also; in fact, it is advisable to use (1) in proving the equivalence of (4) and the original definition.(5) a^ß-^ß^a.(Vn)[ß(n)^a(n)]-+ ß^a.Since by (3) the behavior of finite sets is as trivially expected we shall be concerned primarily with infinite sets and thus (4) will be applicable.^ is a reflexive and transitive relation, hence by partially ordered set theory, if a~ß is defined as "a^ß and ß}ta", then ~ is an equivalence relation and the
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic …
The algebra of infinite trees is, as proved by C. Elgot, completely iterative, i.e., all ideal recursive equations are uniquely solvable. This is proved here to be a general coalgebraic phenomenon: let H be an endofunctor such that for every object X a final coalgebra, TX, of H(_) + X exists. Then TX is an object-part of a monad which is completely iterative. Moreover, a similar contruction of a "completely iterative monoid" is possible in every monoidal category satisfying mild side conditions.
This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject. Part …
This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject. Part I §1. Conceptions of sets. Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are …
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are not compelling.The fundamental theorem of algebra will serve as an example of where countable choice comes into play and how to proceed in its absence.Along the way, a notion of a complete metric space, suitable for a choiceless environment, is developed.
Varieties of F-algebras with respect to an endofunctor F on an arbitrary cocomplete category C are defined as equational classes admitting free algebras. They are shown to correspond precisely to …
Varieties of F-algebras with respect to an endofunctor F on an arbitrary cocomplete category C are defined as equational classes admitting free algebras. They are shown to correspond precisely to the monadic categories over C. Under suitable assumptions satisfied in particular by any endofunctor on Set and Setop the Birkhoff Variety Theorem holds. By dualization, covarieties over complete categories C are introduced, which then correspond to the comonadic categories over C, and allow for a characterization in dual terms of the Birkhoff Variety Theorem. Moreover, the well known conditions of accessibilitly and boundedness for Set-functors F, sufficient for the existence of cofree F-coalgebras, are shown to be equivalent.
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model …
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as …
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as small as possible (and thus, the type theory is as weak as possible). In particular, we will consider epimorphisms and disjoint sums. We show that, given the minimal type universe, all epimorphisms are surjections, and disjoint sums exist. Further, without universes, there are countermodels for these statements, and if we use the Logical Framework formulation of type theory, these statements are provably non-derivable.
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique …
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.
We give a construction of coequalisers in formal topology, a predicative ver- sion of locale theory. This allows for construction of quotient spaces and identification spaces in constructive topology.
We give a construction of coequalisers in formal topology, a predicative ver- sion of locale theory. This allows for construction of quotient spaces and identification spaces in constructive topology.
Completely iterative monads of Elgot et al. are the monads such that every guarded iterative equation has a unique solution. Free completely iterative monads are known to exist on every …
Completely iterative monads of Elgot et al. are the monads such that every guarded iterative equation has a unique solution. Free completely iterative monads are known to exist on every iteratable endofunctor H, i.e., one with final coalgebras of all functors H(_) + X. We show that conversely, if H generates a free completely iterative monad, then it is iteratable.
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose …
Bishop's informal set theory is briefly discussed and compared to Lawvere's Elementary Theory of the Category of Sets (ETCS). We then present a constructive and predicative version of ETCS, whose standard model is based on the constructive type theory of Martin-Lof. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.
In this paper we continue the investigations begun in [2] of equivalence classes of (denumerable) well-orderings under one-one partial recursive, order-preserving maps (recursive isotonisms). The numbering and notation are continued …
In this paper we continue the investigations begun in [2] of equivalence classes of (denumerable) well-orderings under one-one partial recursive, order-preserving maps (recursive isotonisms). The numbering and notation are continued from [2] except that we now use lower case Greek letters for classical ordinals and upper case Roman letters for sets and we slightly modify the definition of (see §IX.3). In section IX, after proving some lemmata which we use repeatedly in this paper, we establish the existence of Cantor Normal Forms for all co-ordinals less than a co-ordinal of the form W A ( a fortiori for all co-ordinals less than a principal number for exponentiation).
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower …
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing …
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as …
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.