Results for 'Type theory'

1000+ found
Order:
  1. Set Theory, Type Theory, and Absolute Generality.Salvatore Florio & Stewart Shapiro - 2014 - Mind 123 (489):157-174.
    In light of the close connection between the ontological hierarchy of set theory and the ideological hierarchy of type theory, Øystein Linnebo and Agustín Rayo have recently offered an argument in favour of the view that the set-theoretic universe is open-ended. In this paper, we argue that, since the connection between the two hierarchies is indeed tight, any philosophical conclusions cut both ways. One should either hold that both the ontological hierarchy and the ideological hierarchy are open-ended, (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  2.  77
    A Modal Type Theory for Formalizing Trusted Communications.Giuseppe Primiero & Mariarosiaria Taddeo - 2012 - Journal of Applied Logic 10 (1):92-114.
    This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  3. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof.P. B. Andrews - 2002 - Kluwer Academic Publishers.
    This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  4.  29
    Towards Transfinite Type Theory: Rereading Tarski's Wahrheitsbegriff.Iris Loeb - 2014 - Synthese 191 (10):2281-2299.
    In his famous paper Der Wahrheitsbegriff in den formalisierten Sprachen (Polish edition: Nakładem/Prace Towarzystwa Naukowego Warszawskiego, wydzial, III, 1933), Alfred Tarski constructs a materially adequate and formally correct definition of the term “true sentence” for certain kinds of formalised languages. In the case of other formalised languages, he shows that such a construction is impossible but that the term “true sentence” can nevertheless be consistently postulated. In the Postscript that Tarski added to a later version of this paper (Studia Philosophica, (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  5.  26
    Treatise on Intuitionistic Type Theory.Johan Georg Granström - 2011 - Springer.
    Prolegomena It is fitting to begin this book on intuitionistic type theory by putting the subject matter into perspective. The purpose of this chapter is to ...
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  6.  93
    The Cognitive Act and the First-Person Perspective: An Epistemology for Constructive Type Theory.Schaar Maria van der - 2011 - Synthese 180 (3):391 - 417.
    The notion of cognitive act is of importance for an epistemology that is apt for constructive type theory, and for epistemology in general. Instead of taking knowledge attributions as the primary use of the verb 'to know' that needs to be given an account of, and understanding a first-person knowledge claim as a special case of knowledge attribution, the account of knowledge that is given here understands first-person knowledge claims as the primary use of the verb 'to know'. (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  7.  25
    Assertion and Grounding: A Theory of Assertion for Constructive Type Theory.Maria van der Schaar - 2011 - Synthese 183 (2):187-210.
    Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of demonstration. (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  8.  49
    Assertion and Grounding: A Theory of Assertion for Constructive Type Theory.Maria Schaar - 2011 - Synthese 183 (2):187-210.
    Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of demonstration. (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  9.  10
    Decidability in Intuitionistic Type Theory is Functionally Decidable.Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):300-304.
    In this paper we show that the usual intuitionistic characterization of the decidability of the propositional function B prop [x : A], i. e. to require that the predicate ∨ ¬ B) is provable, is equivalent, when working within the framework of Martin-Löf's Intuitionistic Type Theory, to require that there exists a decision function ψ: A → Boole such that = Booletrue) ↔ B). Since we will also show that the proposition x = Booletrue [x: Boole] is decidable, (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  10.  32
    Russell´s Early Type Theory and the Paradox of Propositions.André Fuhrmann - 2010 - Principia: An International Journal of Epistemology 5 (1):19-42.
    The paradox of propositiOns, presented in Appenclix B of Russell's The Principies of Mathernatics (1903), is usually taken as Russell's principal motive, at the time, for moving from a simple to a ramified theory of types. I argue that this view is mistaken. A closer study of Russell's correspondence with Frege reveals that Russell carne to adopt a very different resolution of the paradox, calling into question not the simplicity of his early type theory but the simplicity (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  11.  6
    Prototype Proofs in Type Theory.G. Longo - 2000 - Mathematical Logic Quarterly 46 (2):257-266.
    The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ-calculus and act as “proof-schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type (...), i. e. Girard's system F, where type-quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context. (shrink)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  12.  17
    Proof-Relevance of Families of Setoids and Identity in Type Theory.Erik Palmgren - 2012 - Archive for Mathematical Logic 51 (1-2):35-47.
    Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  13.  20
    Quantified Multimodal Logics in Simple Type Theory.Christoph Benzmüller & Lawrence C. Paulson - 2013 - Logica Universalis 7 (1):7-20.
    We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  14.  11
    The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
    In this note we show that Friedman's syntactic translation for intuitionistic logical systems can be carried over to Martin-Löf's type theory, inlcuding universes provided some restrictions are made. Using this translation we show that the theory is closed under a higher type version of Markov's rule.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  15. A Contextual Type Theory with Judgemental Modalities for Reasoning From Open Assumptions.Giuseppe Primiero - 2012 - Logique and Analyse 220:579-600.
    Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive verification and (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  16.  63
    Completeness in Hybrid Type Theory.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2013 - Journal of Philosophical Logic (2-3):1-30.
    We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of (...) $a$ that rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  17.  10
    Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995.Giovanni Sambin & Jan M. Smith (eds.) - 1998 - Oxford University Press.
    This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  18.  12
    Hybrid Type Theory: A Quartet in Four Movements.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2011 - Principia: An International Journal of Epistemology 15 (2):225.
    Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  19.  2
    A Transfinite Type Theory with Type Variables.P. B. Andrews - 1965 - Amsterdam: North-Holland Pub. Co..
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  20.  2
    The Ambiguous Type Theory is Hereditarily Undecidable.Andrey A. Kuzichev - 1992 - Mathematical Logic Quarterly 38 (1):299-300.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  21.  18
    Epistemic Logic Meets Epistemic Game Theory: A Comparison Between Multi-Agent Kripke Models and Type Spaces.Paolo Galeazzi & Emiliano Lorini - 2016 - Synthese 193 (7):2097-2127.
    In the literature there are at least two main formal structures to deal with situations of interactive epistemology: Kripke models and type spaces. As shown in many papers :149–225, 1999; Battigalli and Siniscalchi in J Econ Theory 106:356–391, 2002; Klein and Pacuit in Stud Log 102:297–319, 2014; Lorini in J Philos Log 42:863–904, 2013), both these frameworks can be used to express epistemic conditions for solution concepts in game theory. The main result of this paper is a (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  22.  15
    A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
    In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  23.  58
    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 derivation of (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  24.  20
    A Type Free Theory and Collective/Distributive Predication.Fairouz Kamareddine - 1995 - Journal of Logic, Language and Information 4 (2):85-109.
    The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  25.  1
    Spaces Allowing Type-2 Complexity Theory Revisited.Matthias Schröder - 2004 - Mathematical Logic Quarterly 50 (45):443-459.
    The basic concept of Type-2 Theory of Effectivity to define computability on topological spaces or limit spaces are representations, i. e. surjection functions from the Baire space onto X. Representations having the topological property of admissibility are known to provide a reasonable computability theory. In this article, we investigate several additional properties of representations which guarantee that such representations induce a reasonable Type-2 Complexity Theory on the represented spaces. For each of these properties, we give (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  26. On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
    This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  27.  60
    Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - forthcoming - 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 that (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  28.  25
    Logic in the 1930s: Type Theory and Model Theory.Georg Schiemer & Erich H. Reck - 2013 - Bulletin of Symbolic Logic 19 (4):433-472.
    In historical discussions of twentieth-century logic, it is typically assumed that model theory emerged within the tradition that adopted first-order logic as the standard framework. Work within the type-theoretic tradition, in the style of Principia Mathematica, tends to be downplayed or ignored in this connection. Indeed, the shift from type theory to first-order logic is sometimes seen as involving a radical break that first made possible the rise of modern model theory. While comparing several early (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  29.  60
    Type Theory and Homotopy.Steve Awodey - unknown
    of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  30.  4
    The Justification of Identity Elimination in Martin-Löf’s Type Theory.Ansten Klev - forthcoming - Topoi:1-14.
    On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  31.  21
    Austinian Truth, Attitudes and Type Theory ∗.Robin Cooper - unknown
    This paper is part of a broader project whose aim is to present a coherent unified approach to natural language dialogue semantics using tools from type theory. Here we explore aspects of our approach which relate to situation theory and situation semantics. We first point out a relationship between type theory and the Austinian notion of truth. We then consider how records in type theory might be used to represent situations and how dependent (...)
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography   3 citations  
  32.  15
    The Strength of Martin-Löf Type Theory with a Superuniverse. Part I.Michael Rathjen - 2000 - Archive for Mathematical Logic 39 (1):1-39.
    Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   7 citations  
  33.  8
    Well-Ordering Proofs for Martin-Löf Type Theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
    We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   8 citations  
  34.  18
    Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT.James Ladyman & Stuart Presnell - forthcoming - Philosophia Mathematica:nkw023.
    Among the most interesting features of Homotopy Type Theory is the way it treats identity, which has various unusual characteristics. We examine the formal features of “identity types” in HoTT, and how they relate to its other features including intensionality, constructive logic, the interpretation of types as concepts, and the Univalence Axiom. The unusual behaviour of identity types might suggest that they be reinterpreted as representing indiscernibility. We explore this by defining indiscernibility in HoTT and examine its relationship (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  35.  11
    Extending Martin-Löf Type Theory by One Mahlo-Universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.
    We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjen's theory KPM. This is achieved by replacing the universe in Martin-Löf's Type Theory by a new universe V having the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe inside V closed under f. We show that the proof theoretical strength of MLM is $\geq \psi_{\Omega_1}\Omega_{{\rm M}+\omega}$ . (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  36.  1
    Characterizing the Interpretation of Set Theory in Martin-Löf Type Theory.Michael Rathjen & Sergei Tupailo - 2006 - Annals of Pure and Applied Logic 141 (3):442-471.
    Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  37. Re-Examining Russell's Paralysis: Ramified Type-Theory and Wittgenstein's Objection to Russell's Theory of Judgment.Graham Stevens - 2003 - Russell: The Journal of Bertrand Russell Studies 23 (1).
    It is well known that Russell abandoned his multiple-relation theory of judgment, which provided the philosophical foundations for PM 's ramified type-theory, in response to criticisms by Wittgenstein. Their exact nature has remained obscure. An influential interpretation, put forth by Sommerville and Griffin, is that Wittgenstein showed that the theory must appeal to the very hierarchy it is intended to generate and thus collapses into circularity. I argue that this rests on a mistaken interpretation of (...)-theory and suggest an alternative one to explain Russell's reaction. (shrink)
     
    Export citation  
     
    My bibliography   5 citations  
  38.  3
    Quotient Topologies in Constructive Set Theory and Type Theory.Hajime Ishihara & Erik Palmgren - 2006 - Annals of Pure and Applied Logic 141 (1):257-265.
    The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  39.  9
    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 (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  40.  31
    A Theorem in 3-Valued Model Theory with Connections to Number Theory, Type Theory, and Relevant Logic.J. Michael Dunn - 1979 - Studia Logica 38 (2):149 - 169.
    Given classical (2 valued) structures and and a homomorphism h of onto , it is shown how to construct a (non-degenerate) 3-valued counterpart of . Classical sentences that are true in are non-false in . Applications to number theory and type theory (with axiom of infinity) produce finite 3-valued models in which all classically true sentences of these theories are non-false. Connections to relevant logic give absolute consistency proofs for versions of these theories formulated in relevant logic (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  41.  16
    Realizing Mahlo Set Theory in Type Theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.
    After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-Löf type theory developed by A. Setzer.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  42.  11
    A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.Peter Dybjer - 2000 - Journal of Symbolic Logic 65 (2):525-549.
    The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á la Tarski. A set U 0 of codes for small sets is generated inductively at the same time as a function T 0 , which maps a code to the corresponding small set, is defined by recursion on the way the elements of U 0 are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  43.  26
    Asymptotic Densities in Logic and Type Theory.Zofia Kostrzycka & Marek Zaionc - 2008 - Studia Logica 88 (3):385-403.
    This paper presents a systematic approach for obtaining results from the area of quantitative investigations in logic and type theory. We investigate the proportion between tautologies (inhabited types) of a given length n against the number of all formulas (types) of length n. We investigate an asymptotic behavior of this fraction. Furthermore, we characterize the relation between number of premises of implicational formula (type) and the asymptotic probability of finding such formula among the all ones. We also (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  44.  6
    The Strength of Martin-Löf Type Theory with a Superuniverse. Part II.Michael Rathjen - 2001 - Archive for Mathematical Logic 40 (3):207-233.
    Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  45.  1
    On the Strength of Dependent Products in the Type Theory of Martin-Löf.Richard Garner - 2009 - Annals of Pure and Applied Logic 160 (1):1-12.
    One may formulate the dependent product types of Martin-Löf type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  46.  35
    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  
     
    My bibliography  
  47.  10
    Dialogical Harmony: Tonk, Constructive Type Theory and Rules for Anonymous Players.Juan Redmond & Shahid Rahman - unknown
    Recent literature on dialogical logic discusses the case of tonk and the notion harmony in the context of a rule-based theory of meaning. Now, since the publications of those papers, a dialogical version of constructive type theory has been developed. The aim of the present paper is to show that, from the dialogical point of view, the harmony of the CTT-rules is the consequence of a more fundamental level of meaning characterized by the independence of players. We (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  48.  4
    A Simple Type Theory with Partial Functions and subtypes11Supported by the MITRE-Sponsored Research Program. Presented at the 9th International Congress of Logic, Methodology and Philosophy of Science Held in Uppsala, Sweden, August 7-14, 1991. [REVIEW]William M. Farmer - 1993 - Annals of Pure and Applied Logic 64 (3):211-240.
    Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  49.  21
    The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
    Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  50.  6
    Denotational Semantics for Intuitionistic Type Theory Using a Hierarchy of Domains with Totality.Geir Waagbø - 1999 - Archive for Mathematical Logic 38 (1):19-60.
    A modified version of Normann's hierarchy of domains with totality [9] is presented and is shown to be suitable for interpretation of Martin-Löf's intuitionistic type theory. This gives an interpretation within classical set theory, which is natural in the sense that $\Sigma$ -types are interpreted as sets of pairs and $\Pi$ -types as sets of choice functions. The hierarchy admits a natural definition of the total objects in the domains, and following an idea of Berger [3] this (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
1 — 50 / 1000