About this topic
Summary Type theory is a family of formal systems based on Russell's doctrine that every mathematical object must have a type and every mathematical operation must be restricted to objects of certain types. Like set theory and category theory, it is one of the most common foundation for mathematics today. In addition, type theory can also be understood as the study of type systems in programming languages. In this sense, it is a branch of theoretical computer science.
Key works The doctrine of types is first contemplated in Appendix B of Russell 1903 as a solution for the contradictions in the foundations of mathematics. The idea is later systematically implemented by Whitehead & Russell 1910 in the form of a ramified theory of types. Ramsey 1926 proposes a deramification of the type structure, resulting in a simple type theory. Its most notable formulation is in the simply-typed lambda calculus of Church 1940. Curry & Feys 1958 and Howard 1980 discovered a correspondence between types and propositions of intuitionistic logic systems. Martin-Löf 1975, 1982, 1980 develops a constructive type theory serving as a foundation for Bishop's brand of constructive mathematics. Homotopy type theory is a recent further development of constructive type theory proposed in The Univalent Foundations Program 2013.
Introductions Textbooks include Nederpelt & Geuvers 2014, Pierce 2002, Harper 2012. For a more philosophical introduction, see Nordström et al 1990 and Nordström et al 2001. Martin-Löf's original works are surprisingly accessible and collections are available online at https://pml.flu.cas.cz/ and https://github.com/michaelt/martin-lof. The SEP entry by Coquand 2008 is a very accessible introduction. A collection of resources for learning type theory can be found on https://github.com/jozefg/learn-tt.
Related

Contents
645 found
Order:
1 — 50 / 645
  1. Copredication in homotopy type theory.Hamidreza Bahramian - manuscript
    This paper applies homotopy type theory to formal semantics of natural languages and proposes a new model for the linguistic phenomenon of copredication. Copredication refers to sentences where two predicates which assume different requirements for their arguments are asserted for one single entity, e.g., "the lunch was delicious but took forever". This paper is particularly concerned with copredication sentences with quantification, i.e., cases where the two predicates impose distinct criteria of quantification and individuation, e.g., "Fred picked up and mastered three (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  2. Cognitivism about Epistemic Modality.David Elohim - manuscript
    This paper aims to vindicate the thesis that cognitive computational properties are abstract objects implemented in physical systems. I avail of the equivalence relations countenanced in Homotopy Type Theory, in order to specify an abstraction principle for epistemic intensions. The homotopic abstraction principle for epistemic intensions provides an epistemic conduit into our knowledge of intensions as abstract objects. I examine, then, how intensional functions in Epistemic Modal Algebra are deployed as core models in the philosophy of mind, Bayesian perceptual psychology, (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  3. 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 via inference rules, although not higher-order (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  4. 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 epistemology to solve the (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  5. Type Theoretic Interpretation of Theories and Syntax-Semantics Debate in Philosophy of Science.Morteza Moniri - manuscript
    In this paper, we discuss some proposed ways of defining the notions of structure and isomorphism between structures in the absence of formal language. We discuss Halvorson’s arguments against the semantic view conception of the notion of structure and Glymour and Lutz’s criticisms of Halvorson’s view. We suggest a new look at structures suggested by homotopy type theory (HoTT). This approach is consistent with both the syntactic and semantic views in the philosophy of science.
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  6. Minimal Type Theory (MTT).P. Olcott - manuscript
    Minimal Type Theory (MTT) is based on type theory in that it is agnostic about Predicate Logic level and expressly disallows the evaluation of incompatible types. It is called Minimal because it has the fewest possible number of fundamental types, and has all of its syntax expressed entirely as the connections in a directed acyclic graph.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  7. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - forthcoming - Journal of Logic and Computation.
    In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8. 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 $.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  9. Stefania Centrone, Deborah Kant, Deniz Serikaya, Reflections on the Foundations of Mathematics. Univalent Foundations, Set Theory and General Thoughts, vol. 407 of Synthese Library, Springer, 2019, pp. 494+xxviii; ISBN: 978-3-030-15654-1 (Hardcover) 149.79€, ISBN: 978-3-030-15655-8 (eBook). [REVIEW]Matteo de Ceglie - forthcoming - Studia Logica:1-7.
  10. Mathematical Structures Within Simple Type Theory.Samuel González-Castillo - forthcoming - Studia Logica:1-30.
    We present an extension of simple type theory that incorporates types for any kind of mathematical structure (of any order). We further extend this system allowing isomorphic structures to be identified within these types thanks to some syntactical restrictions; for this purpose, we formally define what it means for two structures to be isomorphic. We model both extensions in NFU set theory in order to prove their relative consistency.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  11. 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 property is reduced to an (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  12. Propositions as types.Ansten Klev - forthcoming - In Hilary Nesi & Petar Milin (eds.), International Encyclopedia of Language and Linguistics. Elsevier.
    Treating propositions as types allows for a unified presentation of logic and type theory. Both fields thereby gain in expressive and deductive power. This chapter introduces the reader to a system of type theory where propositions are types. The system will be presented as an extension of the simple theory of types. Philosophical and historical observations are made along the way. A linguistic example is given at the end.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  13. Critical Studies/Book Reviews.Hans-Christoph Kotzsch - forthcoming - Philosophia Mathematica:nkab026.
    _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† †.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14. Constructive Validity of a Generalized Kreisel–Putnam Rule.Ivo Pezlar - forthcoming - Studia Logica.
    In this paper, we propose a computational interpretation of the generalized Kreisel–Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry–Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  15. Embedding the Calendar and Time Type System in Temporal Type Theory.Georgios V. Pitsiladis & Costas D. Koutras - forthcoming - Journal of Applied Non-Classical Logics:1-48.
    Temporal Type Theory (TTT) has been recently introduced as a topos-theoretic approach to understanding the behaviour of systems over time. A truly innovative point of TTT is that it makes truth inherently dependent on time; this is to be contrasted with the classical approach in which past, present and future are related via logical operators. Further on this line of research, the notion of truth is substituted by the ‘time duration’ over which a proposition is true, giving rise to the (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  16. Ordinal Type Theory.Jan Plate - forthcoming - Inquiry: An Interdisciplinary Journal of Philosophy.
    Higher-order logic, with its type-theoretic apparatus known as the simple theory of types (STT), has increasingly come to be employed in theorizing about properties, relations, and states of affairs—or ‘intensional entities’ for short. This paper argues against this employment of STT and offers an alternative: ordinal type theory (OTT). Very roughly, STT and OTT can be regarded as complementary simplifications of the ‘ramified theory of types’ outlined in the Introduction to Principia Mathematica (on a realist reading). While STT, understood as (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  17. Prospectus to a Homotopic Metatheory of Language.Eric Schmid - forthcoming - Chicago: Edition Erich Schmid.
    Due to the wide scope of (in particular linear) homotopy type theory (using quantum natural language processing), a metatheory can be applied not just to theorizing the metatheory of scientific progress, but ordinary language or any public language defined by sociality/social agents as the precondition for the realizability of (general) intelligence via an inferential network from which judgement can be made. How this metatheory of science generalizes to public language is through the recent advances of quantum natural language processing, but (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  18. Equiconsistency of the Minimalist Foundation with its classical version.Maria Emilia Maietti & Pietro Sabelli - 2025 - Annals of Pure and Applied Logic 176 (2):103524.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  19. Propositional Type Theory of Indeterminacy.Víctor Aranda, Manuel Martins & María Manzano - 2024 - Studia Logica 112 (6):1409-1438.
    The aim of this paper is to define a partial Propositional Type Theory. Our system is partial in a double sense: the hierarchy of (propositional) types contains partial functions and some expressions of the language, including formulas, may be undefined. The specific interpretation we give to the undefined value is that of Kleene’s strong logic of indeterminacy. We present a semantics for the new system and prove that every element of any domain of the hierarchy has a name in the (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  20. Analyticity and Syntheticity in Type Theory Revisited.Bruno Bentzen - 2024 - Review of Symbolic Logic 17 (4).
    I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function type (x : (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  21. Univalence and Ontic Structuralism.Lu Chen - 2024 - Foundations of Physics 54 (3):1-27.
    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.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  22. Constructive Type Theory, an appetizer.Laura Crosilla - 2024 - In Peter Fritz & Nicholas K. Jones (eds.), Higher-Order Metaphysics. Oxford University Press.
    Recent debates in metaphysics have highlighted the significance of type theories, such as Simple Type Theory (STT), for our philosophical analysis. In this chapter, I present the salient features of a constructive type theory in the style of Martin-Löf, termed CTT. My principal aim is to convey the flavour of this rich, flexible and sophisticated theory and compare it with STT. I especially focus on the forms of quantification which are available in CTT. A further aim is to argue that (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  23. Martin-Löf’s Type Theorу: Between Phenomenology and Analytical Philosophy.Oleg Domanov - 2024 - HORIZON. Studies in Phenomenology 13 (1):33-56.
    Martin-Löf’s type theory stems simultaneously from Frege and Russell’s logic-ontological ideas and Husserl’s phenomenology. The article examines this intermediate status of type theory using as examples Martin-Löf ’s syntactical-semantic method and the role of evidence and canonical objects in his approach. Martin-Löf borrows the syntactical-semantic method from Frege and extends it drawing on Husserl’s theory of meaning. In type theory this method leads to the identity (isomorphism) of syntax and semantics (formal logic and formal ontology). Unlike traditional formal logic the (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  24. The Architecture and Archaeology of Modern Logic. Studies dedicated to Göran Sundholm.Ansten Klev (ed.) - 2024 - Cham: Springer.
  25. Aspects of a logical theory of assertion and inference.Ansten Klev - 2024 - Theoria 90 (5):534-555.
    The aim here is to investigate assertion and inference as notions of logic. Assertion will be explained in terms of its purpose, which is to give interlocutors the right to request the assertor to do a certain task. The assertion is correct if, and only if, the assertor knows how to do this task. Inference will be explained as an assertion equipped with what I shall call a justification profile, a strategy for making good on the assertion. The inference is (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  26. The purely iterative conception of set.Ansten Klev - 2024 - Philosophia Mathematica 32 (3):358-378.
    According to the iterative conception of set, sets are formed in stages. According to the purely iterative conception of set, sets are formed by iterated application of a set-of operation. The cumulative hierarchy is a mathematical realization of the iterative conception of set. A mathematical realization of the purely iterative conception can be found in Peter Aczel’s type-theoretic model of constructive set theory. I will explain Aczel’s model construction in a way that presupposes no previous familiarity with the theories on (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  27. Martin-Löf on the Validity of Inference.Ansten Klev - 2024 - In Antonio Piccolomini D'Aragona (ed.), Perspectives on Deduction: Contemporary Studies in the Philosophy, History and Formal Theories of Deduction. Springer Verlag. pp. 171-185.
    An inference is valid if it guarantees the transferability of knowledge from the premisses to the conclusion. If knowledge is here understood as demonstrative knowledge, and demonstration is explained as a chain of valid inferences, we are caught in an explanatory circle. In recent lectures, Per Martin-Löf has sought to avoid the circle by specifying the notion of knowledge appealed to in the explanation of the validity of inference as knowledge of a kind weaker than demonstrative knowledge. The resulting explanation (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  28. One Mathematic(s) or Many? Foundations of Mathematics in Twentieth-Century Mathematical Practice.Andrei Rodin - 2024 - In Bharath Sriraman (ed.), Handbook of the History and Philosophy of Mathematical Practice. Cham: Springer. pp. 2339-2364.
    The received Hilbert-style axiomatic foundations of mathematics has been designed by Hilbert and his followers as a tool for metatheoretical research. Foundations of mathematics of this type fail to satisfactory perform more basic and more practically oriented functions of theoretical foundations such as verification of mathematical constructions and proofs. Using alternative foundations of mathematics such as the univalent foundations is compatible with using the received set-theoretic foundations for metamathematical purposes provided the two foundations are mutually interpretable. Changes in foundations of (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  29. Does Identity Make Sense?Andrei Rodin - 2024 - Manuscrito 47 (1):2024-0073.
    In this paper we present novel conceptions of identity arising in and motivated by a recently emerged branch of mathematical logic, namely, Homotopy Type theory (HoTT). We consider an established 2013 version of HoTT as well as its more recent generalised version called Directed HoTT or Directed Type theory (DTT), which at the time of writing remains a work in progress. In HoTT, and in particular in DTT, identity is not just a relation but a mathematical structure which admits for (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  30. 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.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31. A Philosophical Introduction to Higher-order Logics.Andrew Bacon - 2023 - Routledge.
    This is the first comprehensive textbook on higher order logic that is written specifically to introduce the subject matter to graduate students in philosophy. The book covers both the formal aspects of higher-order languages -- their model theory and proof theory, the theory of λ-abstraction and its generalizations -- and their philosophical applications, especially to the topics of modality and propositional granularity. The book has a strong focus on non-extensional higher-order logics, making it more appropriate for foundational metaphysics than other (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  32. Frege’s Theory of Types.Bruno Bentzen - 2023 - Manuscrito 46 (4):2022-0063.
    It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church’s simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose and defend an alternative interpretation of first-level (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  33. Extensional Realizability and Choice for Dependent Types in Intuitionistic Set Theory.Emanuele Frittaion - 2023 - Journal of Symbolic Logic 88 (3):1138-1169.
    In [17], we introduced an extensional variant of generic realizability [22], where realizers act extensionally on realizers, and showed that this form of realizability provides inner models of $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory), that further validate $\mathsf {AC}_{\mathsf {FT}}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding $\mathsf {AC}_{\mathsf {FT}}$. We then show that adding (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34. 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 as new models based on normal (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35. Lambek–Grishin Calculus: Focusing, Display and Full Polarization.Giuseppe Greco, Michael Moortgat, Valentin D. Richard & Apostolos Tzimoulis - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 877-915.
    Focused sequent calculi are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbb {FP.LG}$$\end{document} for Lambek–Grishin logic by generalizing the theory of multi-type calculi and their (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  36. Verified completeness in Henkin-style for intuitionistic propositional logic.Huayu Guo, Dongheng Chen & Bruno Bentzen - 2023 - In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.), Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou. College Publications. pp. 36-48.
    This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  37. Under Lock and Key: A Proof System for a Multimodal Logic.G. A. Kavvos & Daniel Gratzer - 2023 - Bulletin of Symbolic Logic 29 (2):264-293.
    We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  38. Spiritus Asper versus Lambda: On the Nature of Functional Abstraction.Ansten Klev - 2023 - Notre Dame Journal of Formal Logic 64 (2):205-223.
    The spiritus asper as used by Frege in a letter to Russell from 1904 bears resemblance to Church’s lambda. It is natural to ask how they relate to each other. An alternative approach to functional abstraction developed by Per Martin-Löf some thirty years ago allows us to describe the relationship precisely. Frege’s spiritus asper provides a way of restructuring a unary function name in Frege’s sense such that the argument place indicator occurs all the way to the right. Martin-Löf’s alternative (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  39. 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.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  40. The Axiom of Choice is False Intuitionistically (in Most Contexts).Charles Mccarty, Stewart Shapiro & Ansten Klev - 2023 - Bulletin of Symbolic Logic 29 (1):71-96.
    There seems to be a view that intuitionists not only take the Axiom of Choice (AC) to be true, but also believe it a consequence of their fundamental posits. Widespread or not, this view is largely mistaken. This article offers a brief, yet comprehensive, overview of the status of AC in various intuitionistic and constructivist systems. The survey makes it clear that the Axiom of Choice fails to be a theorem in most contexts and is even outright false in some (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  41. Core Type Theory.Emma van Dijk, David Ripley & Julian Gutierrez - 2023 - Bulletin of the Section of Logic 52 (2):145-186.
    Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related, and determines the same consequence relation. The difference, however, matters for (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. Topos of Noise.Inigo Wilkins - 2023 - Angelaki 28 (3):144-162.
    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 (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  43. Propositional Forms of Judgemental Interpretations.Tao Xue, Zhaohui Luo & Stergios Chatzikyriakidis - 2023 - Journal of Logic, Language and Information 32 (4):733-758.
    In formal semantics based on modern type theories, some sentences may be interpreted as judgements and some as logical propositions. When interpreting composite sentences, one may want to turn a judgemental interpretation or an ill-typed semantic interpretation into a proposition in order to obtain an intended semantics. For instance, an incorrect judgement $$a:A$$ may be turned into its propositional form $$\textsc {is}(A,a)$$ and an ill-typed application p(a) into $$\textsc {do}(p,a)$$, so that the propositional forms can take part in logical compositions (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  44. Type Theory with Opposite Types: A Paraconsistent Type Theory.Juan C. Agudelo-Agudelo & Andrés Sicard-Ramírez - 2022 - Logic Journal of the IGPL 30 (5):777-806.
    A version of intuitionistic type theory is extended with opposite types, allowing a different formalization of negation and obtaining a paraconsistent type theory (⁠|$\textsf{PTT} $|⁠). The rules for opposite types in |$\textsf{PTT} $| are based on the rules of the so-called constructible falsity. A propositions-as-types correspondence between the many-sorted paraconsistent logic |$\textsf{PL}_\textsf{S} $| (a many-sorted extension of López-Escobar’s refutability calculus presented in natural deduction format) and |$\textsf{PTT} $| is proven. Moreover, a translation of |$\textsf{PTT} $| into intuitionistic type theory is (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45. Higher-Order Logic and Type Theory.John L. Bell - 2022 - Cambridge University Press.
    This Element is an exposition of second- and higher-order logic and type theory. It begins with a presentation of the syntax and semantics of classical second-order logic, pointing up the contrasts with first-order logic. This leads to a discussion of higher-order logic based on the concept of a type. The second Section contains an account of the origins and nature of type theory, and its relationship to set theory. Section 3 introduces Local Set Theory, an important form of type theory (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark   1 citation  
  46. Propositions as (Flexible) Types of Possibilities.Nate Charlow - 2022 - In Chris Tillman & Adam Murray (eds.), The Routledge Handbook of Propositions. Routledge. pp. 211-230.
    // tl;dr A Proposition is a Way of Thinking // -/- This chapter is about type-theoretic approaches to propositional content. Type-theoretic approaches to propositional content originate with Hintikka, Stalnaker, and Lewis, and involve treating attitude environments (e.g. "Nate thinks") as universal quantifiers over domains of "doxastic possibilities" -- ways things could be, given what the subject thinks. -/- This chapter introduces and motivates a line of a type-theoretic theorizing about content that is an outgrowth of the recent literature on epistemic (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  47. The entanglement of logic and set theory, constructively.Laura Crosilla - 2022 - Inquiry: An Interdisciplinary Journal of Philosophy 65 (6).
    ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  48. Boolean Types in Dependent Theories.Itay Kaplan, Ori Segel & Saharon Shelah - 2022 - Journal of Symbolic Logic 87 (4):1349-1373.
    The notion of a complete type can be generalized in a natural manner to allow assigning a value in an arbitrary Boolean algebra $\mathcal {B}$ to each formula. We show some basic results regarding the effect of the properties of $\mathcal {B}$ on the behavior of such types, and show they are particularity well behaved in the case of NIP theories. In particular, we generalize the third author’s result about counting types, as well as the notion of a smooth type (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  49. 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...
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark  
  50. Stefania Centrone, Deborah Kant, and Deniz Sarikaya, eds, Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory, and General Thoughts.Hans-Christoph Kotzsch - 2022 - Philosophia Mathematica 30 (1):88-102.
1 — 50 / 645