The Univalent Foundations of Mathematics provide not only an entirely non-Cantorian conception of the basic objects of mathematics but also a novel account of how foundations ought to relate to mathematical practice. In this paper, I intend to answer the question: In what way is UF a new foundation of mathematics? I will begin by connecting UF to a pragmatist reading of the structuralist thesis in the philosophy of mathematics, which I will use to define a criterion (...) that a formal system must satisfy if it is to be regarded as a “structuralist foundation.” I will then explain why both set-theoretic foundations like ZFC and category-theoretic foundations like ETCS satisfy this criterion only to a very limited extent. Then I will argue that UF is better-able to live up to the proposed criterion for a structuralist foundation than any currently available foundational proposal. First, by showing that most criteria of identity in the practice of mathematics can be formalized in terms of the preferred criterion of identity between the basic objects of UF. Second, by countering several objections that have been raised against UF’s capacity to serve as a foundation for the whole of mathematics. (shrink)

The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not (...) immediately clear how these principles are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine. (shrink)

This edited work presents contemporary mathematical practice in the foundational mathematical theories, in particular set theory and the univalent foundations. It shares the work of significant scholars across the disciplines of mathematics, philosophy and computer science. Readers will discover systematic thought on criteria for a suitable foundation in mathematics and philosophical reflections around the mathematical perspectives. The first two sections focus on the two most prominent candidate theories for a foundation of mathematics. Readers may trace current research in (...) set theory, which has widely been assumed to serve as a framework for foundational issues, as well as new material elaborating on the univalent foundations, considering an approach based on homotopy type theory (HoTT). The further sections then build on this and are centred on philosophical questions connected to the foundations of mathematics. Here, the authors contribute to discussions on foundational criteria with more general thoughts on the foundations of mathematics which are not connected to particular theories. This book shares the work of some of the most important scholars in the fields of set theory (S. Friedman), non-classical logic (G. Priest) and the philosophy of mathematics (P. Maddy). The reader will become aware of the advantages of each theory and objections to it as a foundation, following the latest and best work across the disciplines and it is therefore a valuable read for anyone working on the foundations of mathematics or in the philosophy of mathematics. (shrink)

The persistent challenge of formulating ontic structuralism in a rigorous manner, which prioritizes structures over the entities they contain, calls for a transformation of traditional logical frameworks. I argue that Univalent Foundations (UF), which feature the axiom that all isomorphic structures are identical, offer such a foundation and are more attractive than other proposed structuralist frameworks. Furthermore, I delve into the significance in the case of the hole argument and, very briefly, the nature of symmetries.

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.

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)

The Univalence axiom, due to Vladimir Voevodsky, is often taken to be one of the most important discoveries arising from the Homotopy Type Theory research programme. It is said by Steve Awodey that Univalence embodies mathematical structuralism, and that Univalence may be regarded as ‘expanding the notion of identity to that of equivalence’. This article explores the conceptual, foundational and philosophical status of Univalence in Homotopy Type Theory. It extends our Types-as-Concepts interpretation of HoTT to Universes, and offers an account (...) of the Univalence axiom in such terms. We consider Awodey’s informal argument that Univalence is motivated by the principle that reasoning should be invariant under isomorphism, and we examine whether an autonomous and rigorous justification along these lines can be given. We consider two problems facing such a justification. First, there is a difference between equivalence and isomorphism and Univalence must be formulated in terms of the former. Second, the argument as presented cannot establish Univalence itself but only a weaker version of it, and must be supplemented by an additional principle. The article argues that the prospects for an autonomous justification of Univalence are promising. (shrink)

The Univalent Foundations of mathematics take the point of view that all of mathematics can be encoded in terms of spatial notions like "point" and "path". We will argue that this new point of view has important implications for philosophy, and especially for those parts of analytic philosophy that take set theory and first-order logic as their benchmark of rigor. To do so, we will explore the connection between foundations and philosophy, outline what is distinctive about the (...) logic of the Univalent Foundations, and then describe new philosophical theses one can express in terms of this new logic. (shrink)

Structuralism, the view that mathematics is the science of structures, can be characterized as a philosophical response to a general structural turn in modern mathematics. Structuralists aim to understand the ontological, epistemological, and semantical implications of this structural approach in mathematics. Theories of structuralism began to develop following the publication of Paul Benacerraf’s paper ‘What numbers could not be’ in 1965. These theories include non-eliminative approaches, formulated in a background ontology of sui generis structures, such as Stewart Shapiro’s ante rem (...) structuralism and Michael Resnik’s pattern structuralism. In contrast, there are also eliminativist accounts of structuralism, such as Geoffrey Hellman’s modal structuralism, which avoids sui generis structures. These research projects have guided a more systematic focus on philosophical topics related to mathematical structuralism, including the identity criteria for objects in structures, dependence relations between objects and structures, and also, more recently, structural abstraction principles. Parallel to these developments are approaches that describe mathematical structure in category-theoretic terms. Category-theoretic approaches have been further developed using tools from homotopy type theory. Here we find a strong relationship between mathematical structuralism and the univalent foundations project, an approach to the foundations of mathematics based on higher category theory. (shrink)

It’s often said that set theory provides a foundation for classical mathematics because every classical mathematical object can be modeled as a set and every classical mathematical theorem can be proved from the axioms of set theory. This is obviously a remarkable mathematical fact, but it isn’t obvious what makes it ‘foundational’. This paper begins with a taxonomy of the jobs set theory does that might reasonably be regarded as foundational. It then moves on to category-theoretic and univalent (...) class='Hi'>foundations, exploring to what extent they do these same jobs, and to what extent they might do other jobs also reasonably regarded as foundational. (shrink)

In this paper I will review the developments in the foundations of mathematics in the last 150 years in such a way as to show that they have delivered something of a rather different kind: mathematical pluralism.

This note opens with brief evaluations of classical foundationalist endeavors – those of Frege, Russell, Brouwer and Hilbert. From there we proceed to some pluralist approaches to foundations, focusing on Putnam and Wittgenstein, making a note of what enables their pluralism. Then, I bring up approaches that find foundations potentially harmful, as expressed by Rav and Lakatos. I conclude with a brief discussion of a late medieval Indian case study in order to show what an “unfounded” mathematics could (...) look like. The general purpose is to re-evaluate the desiderata of foundational programs in mathematics. (shrink)

The search for a synthesis between formalism and constructivism, and meditation on Gödel incompleteness, leads in a natural way to conceive mathematics as dynamic and plural, that is the result of a human achievement, rather than static and unique, that is given truth. This foundational attitude, called dynamic constructivism, has been adopted in the actual development of topology and revealed some deep structures that had remained hidden under other views. After motivations for and a brief introduction to dynamic constructivism, an (...) overview is given of the changes it induces in the practice of mathematics and in its foundation, and of the new results it allows to obtain. (shrink)

Presents outstanding translations of the Greek philosopher's works by leading British and American scholars of the last century.

This work has been selected by scholars as being culturally important, and is part of the knowledge base of civilization as we know it. This work was reproduced from the original artifact, and remains as true to the original work as possible. Therefore, you will see the original copyright references, library stamps (as most of these works have been housed in our most important libraries around the world), and other notations in the work. This work is in the public domain (...) in the United States of America, and possibly other nations. Within the United States, you may freely copy and distribute this work, as no entity (individual or corporate) has a copyright on the body of the work.As a reproduction of a historical artifact, this work may contain missing or blurred pages, poor pictures, errant marks, etc. Scholars believe, and we concur, that this work is important enough to be preserved, reproduced, and made generally available to the public. We appreciate your support of the preservation process, and thank you for being an important part of keeping this knowledge alive and relevant. (shrink)

This bold and lively essay is one of those rarest of intellectual achievements, a big small book. In its short length are condensed enormous erudition and impressive analytical scope. With verve and self-assurance, it addresses a broad, central question: How can we improve our understanding of the large-scale processes and structures that transformed the world of the nineteenth century and are transforming our world today? Tilly contends that twentieth-century social theories have been encumbered by a nineteenth century heritage of “pernicious (...) postulates.” He subjects each misleading belief to rigorous criticism, challenging many standard social science paradigms and methodologies. As an alternative to those timeless, placeless models of social change and organization, Tilly argues convincingly for a program of concrete, historically grounded analysis and systematic comparison. To illustrate the strategies available for such research, Tilly assesses the works of several major practitioners of comparative historical analysis, making skillful use of this selective review to offer his own speculative, often unconventional accounts of our recent past. Historically oriented social scientists will welcome this provocative essay and its wide-ranging agenda for comparative historical research. Other social scientists, their graduate and undergraduate students, and even the interested general reader will find this new work by a major scholar stimulating and eminently readable. This is the second of five volumes commissioned by the Russell Sage Foundation to mark its seventy-fifth anniversary. "In this short, brilliant book Tilly suggests a way to think about theories of historical social change....This book should find attentive readers both in undergraduate courses and in graduate seminars. It should also find appreciative readers, for Tilly is a writer as well as a scholar." —Choice. (shrink)

In the Univalent Foundations of mathematics spatial notions like “point” and “path” are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory can be justified intuitively as a theory of shapes in the same way that ZFC can be justified intuitively as a theory of collections. I (...) first clarify what such an “intuitive justification” should be by distinguishing between formal and pre-formal “meaning explanations” in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like “shape”, “path” etc. (shrink)

Society has historically not taken a benign view of genetic disease. The laws permitting sterilization of the mentally re tarded~ and those proscribing consanguineous marriages are but two examples. Indeed as far back as the 5th-10th centuries, B.C.E., consanguineous unions were outlawed (Leviticus XVIII, 6). Case law has traditionally tended toward the conservative. It is reactive rather than directive, exerting its influence only after an individual or group has sustained injury and brought suit. In contrast, state legislatures have not been (...) inhibited in enacting statutes. Many of their products can be characterized as hasty, unnecessary, ill-conceived, and based on the heart rather than the head. Moreover the lack of expert consultation sought has also been remarkable. One state legislature, for example, has advocated immunization for sickle cell anemia! Many others have enacted laws for the screening of inborn errors of metabolism, e.g., phenylketon uria, but have poorly defined the lines of responsibility to secure compliance. A spate of specific disease-related bills has emerged in the u.S. Congress, each seeking recognition and appropriations. Sickle cell anemia, hemophilia, Cooley's anemia and Tay-Sachs disease have been among the front-runners for support. Finally, in 1975, Congress has begun to examine an omnibus bill concerning all forms of genetic disease. The bill, termed the National Genetic Diseases Act is, however, still far from being enacted. (shrink)

This paper focuses on the significance of the concept of noise for cognition and computation. The concept of noise was massively transformed in the twentieth century with the advent of information theory, cybernetics, and computer science, all of which provide formal accounts of information and noise centrally concerned with contingency. We show how the concept has changed from these classical formulations, through developments in mathematics (topology and topos theory), computing (interactive computing and univalent foundations), and cognitive science (predictive (...) processing and cognitive morphodynamics). Ultimately it argues for the central importance of noise not only within a topological conception of cognition and computation, but also in the transcendental-empirical torsion of image schemata and the social interactive elaboration of freedom. (shrink)

Structuralist foundations of mathematics aim for an ‘invariant’ conception of mathematics. But what should be their basic objects? Two leading answers emerge: higher groupoids or higher categories. I argue in favor of the former over the latter. First, I explain why to choose between them we need to ask the question of what is the correct ‘categorified’ version of a set. Second, I argue in favor of groupoids over categories as ‘categorified’ sets by introducing a pre-formal understanding of groupoids (...) as abstract shapes. This conclusion lends further support to the perspective taken by the Univalent Foundations of mathematics. (shrink)

This note argues that, insofar as contemporary mathematics is concerned, there is overwhelming evidence that if mathematical objects are structures, then isomorphism should not be taken as their identity condition. This goes against a common version of structuralism in the philosophical literature. Four areas are presented in which identifying isomorphic structures or objects leads to contradiction or inadequacy. This is followed by a philosophical discussion on possible ways to approach the distinction, and a section on the possibility of proceeding intensionally, (...) as is done in e.g.\ the Univalent Foundations program. (shrink)

The article is devoted to the comparison of two types of proofs in mathematical practice, the methodological differences of which go back to the difference in the understanding of the nature of mathematics by Descartes and Leibniz. In modern philosophy of mathematics, we talk about conceptual and formal proofs in connection with the so-called Hilbert Thesis, according to which every proof can be transformed into a logical conclusion in a suitable formal system. The analysis of the arguments of the proponents (...) and opponents of the Thesis, “conceptualists” and “formalists”, is presented respectively by the two main antagonists – Y. Rav and J. Azzouni. The focus is on the possibility of reproducing the proof of “interesting” mathematical theorems in the form of a strict logical conclusion, in principle feasible by a mechanical procedure. The argument of conceptualists is based on pointing out the importance of other aspects of the proof besides the logical conclusion, namely, in introducing new concepts, methods, and establishing connections between different sections of meaningful mathematics, which is often illustrated by the case of proving Fermat’s Last Theorem (Y. Rav). Formalists say that a conceptual proof “points” to the formal logical structure of the proof (J. Azzouni). The article shows that the disagreement is based on the assumption of asymmetry of mutual translation of syntactic and semantic structures of the language, as a result of which the formal proof loses important semantic factors of proof. In favor of a formal proof, the program of univalent foundations of mathematics In. Vojevodski, according to which the future of mathematical proofs is associated with the availability of computer verification programs. In favor of conceptual proofs, it is stated (A. Pelc) that the number of steps in the supposed formal logical conclusion when proving an “interesting” theorem exceeds the cognitive abilities of a person. The latter circumstance leads the controversy beyond the actual topic of mathematical proof into the epistemological sphere of discussions of “mentalists” and “mechanists” on the question of the supposed superiority of human intelligence over the machine, initiated by R. Penrose in his interpretation of the Second Theorem of Goedel, among whose supporters, as it turned out, was Goedel himself. (shrink)

_Stefania Centrone, Deborah Kant_, and _Deniz Sarikaya_, eds, _ Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory, and General Thoughts _. Studies in Epistemology, Logic, Methodology, and Philosophy of Science; 407. Springer, 2019. Pp. xxviii + 494. ISBN: 978-3-030-15654-1 ; 978-3-030-15655-8. doi.org/10.1007/978-3-030-15655-8† †.

The article is devoted to the nature of the topological intuition and disclosure of the specifics of topological heuristics in the framework of philosophical theory of knowledge. As we know, intuition is a one of the support categories of the theory of knowledge, the driving force of scientific research. Great importance is mathematical intuition for the solution of non-standard problems, for which there is no algorithm for such a solution. In such cases, the mathematician addresses the so-called heuristics, built on (...) the basis of guesswork, obtained by intuition. The author substantiates the conclusion that topological intuition significantly specific compared to a traditional mathematical intuitions of Euclidean geometry. Today topology is a rapidly developing field of modern mathematics, integrates nicely with other sections of mathematical science. In its most general form of the topology can be defined as the branch of mathematics that studies the properties of spatial figures, does not change under deformations. The topological intuition is an instrument for development of topology on the basis of typological heuristics, which is the result of applying topological intuition to the objects topology. The author demonstrates in detail providing with the examples the specificity of topological heuristics and establishes its interconnection with Euclidean geometry. The author draws the conclusion about the fundamentality of topological intuition, and that it, perhaps, is primary in relation to traditionally understood mathematical intuition. (shrink)

The Hole Argument is primarily about the meaning of general covariance in general relativity. As such it raises many deep issues about identity in mathematics and physics, the ontology of space–time, and how scientific representation works. This paper is about the application of a new foundational programme in mathematics, namely homotopy type theory, to the Hole Argument. It is argued that the framework of HoTT provides a natural resolution of the Hole Argument. The role of the Univalence Axiom in the (...) treatment of the Hole Argument in HoTT is clarified. (shrink)

This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation (...) to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality. (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)

We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category EFF. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category EFF one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this (...) class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets. (shrink)