Results for 'Homotopy Type Theory'

964 found
Order:
  1.  37
    Does Homotopy Type Theory Provide a Foundation for Mathematics?Stuart Presnell & James Ladyman - 2018 - British Journal for the Philosophy of Science 69 (2):377-420.
    Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  2. Homotopy Type Theory and Structuralism.Teruji Thomas - 2014 - Dissertation, University of Oxford
    I explore the possibility of a structuralist interpretation of homotopy type theory (HoTT) as a foundation for mathematics. There are two main aspects to HoTT's structuralist credentials. First, it builds on categorical set theory (CST), of which the best-known variant is Lawvere's ETCS. I argue that CST has merit as a structuralist foundation, in that it ascribes only structural properties to typical mathematical objects. However, I also argue that this success depends on the adoption of a (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  3.  26
    Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy.David Corfield - 2020 - Oxford, England: Oxford University Press.
    Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy provides a reasonably gentle introduction to this new logic, thoroughly motivated by intuitive explanations of the need for all of its component parts, and illustrated through innovative applications of the calculus.
  4. Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
    Homotopy Type Theory is a putative new foundation for mathematics grounded in constructive intensional type theory that offers an alternative to the foundations provided by ZFC set theory and category theory. This article explains and motivates an account of how to define, justify, and think about HoTT in a way that is self-contained, and argues that, so construed, it is a candidate for being an autonomous foundation for mathematics. We first consider various questions (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  5. The Hole Argument in Homotopy Type Theory.James Ladyman & Stuart Presnell - 2020 - Foundations of Physics 50 (4):319-329.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  6.  74
    Natural models of homotopy type theory.Steve Awodey - unknown
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  7. Identity in Homotopy Type Theory, Part I: The Justification of Path Induction.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
    Homotopy Type Theory is a proposed new language and foundation for mathematics, combining algebraic topology with logic. An important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory's types, tokens, and identities as spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. In this paper we give a (...)
    Direct download (13 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  8.  90
    Modal Homotopy Type Theory. The Prospect of a New Logic for Philosophy. [REVIEW]A. Klev & C. Zwanziger - 2022 - History and Philosophy of Logic 44 (3):337-342.
    1. The theory referred to by the—perhaps intimidating—main title of this book is an extension of Per Martin-Löf's dependent type theory. Much philosophical work pertaining to dependent type theory...
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  9. Universes and univalence in homotopy type theory.James Ladyman & Stuart Presnell - 2019 - Review of Symbolic Logic 12 (3):426-455.
    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 (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  10.  46
    Modal homotopy type theory.David Corfield - unknown
  11. Mathesis Universalis and Homotopy Type Theory.Steve Awodey - 2019 - In Stefania Centrone, Sara Negri, Deniz Sarikaya & Peter M. Schuster, Mathesis Universalis, Computability and Proof. Cham, Switzerland: Springer Verlag.
     
    Export citation  
     
    Bookmark  
  12.  95
    Does Homotopy Type Theory Provide a Foundation for Mathematics.James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science.
  13.  25
    Reviewed Work: Homotopy Type Theory: Univalent Foundations of Mathematics, http://homotopytypetheory.org/book, Institute for Advanced Study The Univalent Foundations Program.Review by: Jaap van Oosten - 2014 - Bulletin of Symbolic Logic 20 (4):497-500,.
  14.  43
    (1 other version)Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT.James Ladyman & Stuart Presnell - 2016 - Philosophia Mathematica:nkw023.
  15. Expressing ‘the structure of’ in homotopy type theory.David Corfield - 2017 - Synthese 197 (2):681-700.
    As a new foundational language for mathematics with its very different idea as to the status of logic, we should expect homotopy type theory to shed new light on some of the problems of philosophy which have been treated by logic. In this article, definite description, and in particular its employment within mathematics, is formulated within the type theory. Homotopy type theory has been proposed as an inherently structuralist foundational language for mathematics. (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  16.  26
    The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013, vii + 583 pp. [REVIEW]Jaap van Oosten - 2014 - Bulletin of Symbolic Logic 20 (4):497-500.
  17.  59
    A cubical model of homotopy type theory.Steve Awodey - 2018 - Annals of Pure and Applied Logic 169 (12):1270-1294.
  18.  48
    Voevodsky’s Univalence Axiom in Homotopy Type Theory.Steve Awodey, Alvaro Pelayo & Michael A. Warren - unknown
    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.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  19. Type Theory and Homotopy.Steve Awodey - 2012 - In Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm, Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Dordrecht, Netherland: Springer. pp. 183-201.
    The purpose of this informal survey article is to introduce the reader to a new and surprising connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Per Martin-Löf into homotopy theory and higher-dimensional category theory.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  20.  20
    From multisets to sets in homotopy type theory.Håkon Robbestad Gylterud - 2018 - Journal of Symbolic Logic 83 (3):1132-1146.
  21.  34
    Correction to: Expressing ‘the structure of’ in homotopy type theory.David Corfield - 2020 - Synthese 197 (2):701-701.
    The original article has been corrected. The article is published with Open Access but was missing Open Access information. This has been added.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  22.  25
    Homotopy limits in type theory.Jeremy Avigad, Krzysztof Kapulkin & Peter Lefanu Lumsdaine - unknown
    Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23. Naive cubical type theory.Bruno Bentzen - 2021 - Mathematical Structures in Computer Science 31:1205–1231.
    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, (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  24.  45
    Should Type Theory Replace Set Theory as the Foundation of Mathematics?Thorsten Altenkirch - 2023 - Axiomathes 33 (1):1-13.
    Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25.  41
    Homotopy model theory.Brice Halimi - 2021 - Journal of Symbolic Logic 86 (4):1301-1323.
    Drawing on the analogy between any unary first-order quantifier and a "face operator," this paper establishes several connections between model theory and homotopy theory. The concept of simplicial set is brought into play to describe the formulae of any first-order language L, the definable subsets of any L-structure, as well as the type spaces of any theory expressed in L. An adjunction result is then proved between the category of o-minimal structures and a subcategory of (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  26.  26
    Models of Martin-Löf Type Theory From Algebraic Weak Factorisation Systems.Nicola Gambino & Marco Federico Larrea - 2023 - Journal of Symbolic Logic 88 (1):242-289.
    We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that the comprehension category associated with a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid and cubical sets models, as well (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  27. What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
    In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  28. Higher Schreier Theory in Cubical Agda.David Jaz Myers & Zyad Yasser - forthcoming - Journal of Symbolic Logic:1-17.
    Homotopy type theory (HoTT) enables reasoning about groups directly as the types of symmetries (automorphisms) of mathematical structures. The HoTT approach to groups—first put forward by Buchholtz, van Doorn, and Rijke—identifies a group with the type of objects of which it is the symmetries. This type is called the “delooping” of the group, taking a term from algebraic topology. This approach naturally extends the group theory to higher groups which have symmetries between symmetries, and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  29.  74
    Combinatorial realizability models of type theory.Pieter Hofstra & Michael A. Warren - 2013 - Annals of Pure and Applied Logic 164 (10):957-988.
    We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  30. Homotopy theoretic models of identity types.Steve Awodey & Michael Warren - 2009 - Mathematical Proceedings of the Cambridge Philosophical Society 146:45–55.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   27 citations  
  31.  1
    Epimorphisms and Acyclic Types in Univalent Foundations.Ulrik Buchholtz, Tom de Jong & Egbert Rijke - forthcoming - Journal of Symbolic Logic.
    We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory as developed in univalent foundations. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with 0-connected, pointed 1-types. Many of our results are formalized as part of the agda-unimath library.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  32. Constructive mathematics and equality.Bruno Bentzen - 2018 - Dissertation, Sun Yat-Sen University
    The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' (...)
     
    Export citation  
     
    Bookmark   1 citation  
  33.  22
    Non-Trivial Higher Homotopy of First-Order Theories.Tim Campion & Jinhe Ye - forthcoming - Journal of Symbolic Logic:1-7.
    Let T be the theory of dense cyclically ordered sets with at least two elements. We determine the classifying space of $\mathsf {Mod}(T)$ to be homotopically equivalent to $\mathbb {CP}^\infty $. In particular, $\pi _2(\lvert \mathsf {Mod}(T)\rvert )=\mathbb {Z}$, which answers a question in our previous work. The computation is based on Connes’ cycle category $\Lambda $.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34.  22
    First-Order Homotopical Logic.Joseph Helfer - forthcoming - Journal of Symbolic Logic:1-63.
    We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from [8] that any Grothendieck fibration of the kind being considered can automatically be upgraded to a two-dimensional fibration, after which the invariance (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35. Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.) - 2019 - Springer Verlag.
    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 (...)
  36.  18
    The Theory of an Arbitrary Higher λ\lambda-Model.Daniel Martinez & Ruy J. G. B. de Queiroz - 2023 - Bulletin of the Section of Logic 52 (1):39-58.
    One takes advantage of some basic properties of every homotopic λ\lambda-model (e.g. extensional Kan complex) to explore the higher βη\beta\eta-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher λ\lambda-terms, whose equality rules would be contained in the theory of any λ\lambda-homotopic model.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37.  61
    The Hole Argument, take n.John Dougherty - 2020 - Foundations of Physics 50 (4):330-347.
    I apply homotopy type theory to the hole argument as formulated by Earman and Norton. I argue that HoTT gives a precise sense in which diffeomorphism-related Lorentzian manifolds represent the same spacetime, undermining Earman and Norton’s verificationist dilemma and common formulations of the hole argument. However, adopting this account does not alleviate worries about determinism: general relativity formulated on Lorentzian manifolds is indeterministic using this standard of sameness and the natural formalization of determinism in HoTT. Fixing this (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  38. Pregeometry, Formal Language and Constructivist Foundations of Physics.Xerxes D. Arsiwalla, Hatem Elshatlawy & Dean Rickles - manuscript
    How does one formalize the structure of structures necessary for the foundations of physics? This work is an attempt at conceptualizing the metaphysics of pregeometric structures, upon which new and existing notions of quantum geometry may find a foundation. We discuss the philosophy of pregeometric structures due to Wheeler, Leibniz as well as modern manifestations in topos theory. We draw attention to evidence suggesting that the framework of formal language, in particular, homotopy type theory, provides the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  39.  10
    Axiomatic Method in Contemporary Science and Technology.С.П Ковалев & А.В Родин - 2016 - Epistemology and Philosophy of Science 47 (1):153-169.
    In 1900 David Hilbert announced his famous list of then-opened mathematical problems; the problem number 6 in this list is axiomatization of physical theories. Since then a lot of systematic efforts have been invested into solving this problem. However the results of these efforts turned to be less successful than the early enthusiasts of axiomatic method expected. The existing axiomatizations of physical and biological theories provide a valuable logical analysis of these theories but they do not constitute anything like their (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  40.  56
    Representation and Spacetime: The Hole Argument Revisited.Aboutorab Yaghmaie, Bijan Ahmadi Kakavandi, Saeed Masoumi & Morteza Moniri - 2022 - International Studies in the Philosophy of Science 35 (2):171-188.
    Ladyman and Presnell have recently argued that the Hole argument is naturally resolved when spacetime is represented within homotopy type theory rather than set theory. The core idea behind their proposal is that the argument does not confront us with any indeterminism, since the set-theoretically different representations of spacetime involved in the argument are homotopy type-theoretically identical. In this article, we will offer a new resolution based on ZFC set theory to the argument. (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  41. Categorical harmony and path induction.Patrick Walsh - 2017 - Review of Symbolic Logic 10 (2):301-321.
    This paper responds to recent work in the philosophy of Homotopy Type Theory by James Ladyman and Stuart Presnell. They consider one of the rules for identity, path induction, and justify it along ‘pre-mathematical’ lines. I give an alternate justification based on the philosophical framework of inferentialism. Accordingly, I construct a notion of harmony that allows the inferentialist to say when a connective or concept is meaning-bearing and this conception unifies most of the prominent conceptions of harmony (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  42. Cognitivism about Epistemic Modality and Hyperintensionality.David Elohim - manuscript
    This essay aims to vindicate the thesis that cognitive computational properties are abstract objects implemented in physical systems. I avail of Voevodsky's Univalence Axiom and function type equivalence in Homotopy Type Theory, in order to specify an abstraction principle for epistemic (hyper-)intensions. The homotopic abstraction principle for epistemic (hyper-)intensions provides an epistemic conduit for our knowledge of (hyper-)intensions as abstract objects. Higher observational type theory might be one way to make first-order abstraction principles defined (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  43.  34
    Univalent polymorphism.Benno van den Berg - 2020 - Annals of Pure and Applied Logic 171 (6):102793.
    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 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44.  65
    Introduction to Special Issue: Foundations of Mathematical Structuralism.Georg Schiemer & John Wigglesworth - 2020 - Philosophia Mathematica 28 (3):291-295.
    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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45. A Hyperintensional Two-Dimensionalist Solution to the Access Problem.David Elohim - manuscript
    I argue that the two-dimensional hyperintensions of epistemic topic-sensitive two-dimensional truthmaker semantics provide a compelling solution to the access problem. -/- I countenance an abstraction principle for two-dimensional hyperintensions based on Voevodsky's Univalence Axiom and function type equivalence in Homotopy Type Theory. The truth of my first-order abstraction principle for two-dimensional hyperintensions is grounded in its being possibly recursively enumerable i.e. Turing computable and the Turing machine being physically implementable. I apply, further, modal rationalism in modal (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  46. Structuralism, Invariance, and Univalence.Steve Awodey - 2014 - Philosophia Mathematica 22 (1):1-11.
    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 (...)
    Direct download (12 more)  
     
    Export citation  
     
    Bookmark   38 citations  
  47.  70
    What inductive explanations could not be.John Dougherty - 2018 - Synthese 195 (12):5473-5483.
    Marc Lange argues that proofs by mathematical induction are generally not explanatory because inductive explanation is irreparably circular. He supports this circularity claim by presenting two putative inductive explanantia that are one another’s explananda. On pain of circularity, at most one of this pair may be a true explanation. But because there are no relevant differences between the two explanantia on offer, neither has the explanatory high ground. Thus, neither is an explanation. I argue that there is no important asymmetry (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  48.  26
    Axiomatic Method in Contemporary Science and Technology.Sergei Kovalyov & Andrei Rodin - 2016 - Epistemology and Philosophy of Science 47 (1):153-169.
    In 1900 David Hilbert announced his famous list of then-opened mathematical problems; the problem number 6 in this list is axiomatization of physical theories. Since then a lot of systematic efforts have been invested into solving this problem. However the results of these efforts turned to be less successful than the early enthusiasts of axiomatic method expected. The existing axiomatizations of physical and biological theories provide a valuable logical analysis of these theories but they do not constitute anything like their (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  49. A meaning explanation for HoTT.Dimitris Tsementzis - 2020 - Synthese 197 (2):651-680.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  50. The Lean Theorem Prover.Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn & Jakob von Raumer - unknown
    Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
1 — 50 / 964