Search results for 'Type theory' (try it on Scholar)

1000+ found
Order:
  1.  93
    Salvatore Florio & Stewart Shapiro (2014). Set Theory, Type Theory, and Absolute Generality. 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 (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  2. Giuseppe Primiero & Mariarosiaria Taddeo (2012). A Modal Type Theory for Formalizing Trusted Communications. 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 (...)
    Translate
     
     
    Export citation  
     
    My bibliography   4 citations  
  3.  20
    Iris Loeb (2014). Towards Transfinite Type Theory: Rereading Tarski's Wahrheitsbegriff. 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  
  4. P. B. Andrews (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 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  
  5.  25
    Johan Georg Granström (2011). Treatise on Intuitionistic Type Theory. 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.  57
    Maria van der Schaar (2011). The Cognitive Act and the First-Person Perspective: An Epistemology for Constructive Type Theory. [REVIEW] 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 (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  7.  9
    Maria van der Schaar (2011). Assertion and Grounding: A Theory of Assertion for Constructive Type Theory. 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.  26
    André Fuhrmann (2010). Russell´s Early Type Theory and the Paradox of Propositions. Principia 5 (1-2):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  
  9.  6
    G. Longo (2000). Prototype Proofs in Type Theory. 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  
  10.  13
    Erik Palmgren (2012). Proof-Relevance of Families of Setoids and Identity in Type Theory. 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  
  11.  31
    Maria Schaar (2011). Assertion and Grounding: A Theory of Assertion for Constructive Type Theory. 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  
  12.  15
    Christoph Benzmüller & Lawrence C. Paulson (2013). Quantified Multimodal Logics in Simple Type Theory. 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  
  13.  9
    Erik Palmgren (1995). The Friedman‐Translation for Martin‐Löf's Type Theory. 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  
  14.  7
    Silvio Valentini (1996). Decidability in Intuitionistic Type Theory is Functionally Decidable. 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  
  15. Giuseppe Primiero (2012). A Contextual Type Theory with Judgemental Modalities for Reasoning From Open Assumptions. 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.  54
    Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano (2013). Completeness in Hybrid Type Theory. 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.  5
    Giovanni Sambin & Jan M. Smith (eds.) (1998). Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995. 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
    Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano (2012). Hybrid Type Theory: A Quartet in Four Movements. Principia 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 (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  19.  1
    P. B. Andrews (1965). A Transfinite Type Theory with Type Variables. Amsterdam, North-Holland Pub. Co..
    No categories
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  20.  2
    Andrey A. Kuzichev (1992). The Ambiguous Type Theory is Hereditarily Undecidable. Mathematical Logic Quarterly 38 (1):299-300.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  21.  6
    Paolo Galeazzi & Emiliano Lorini (forthcoming). Epistemic Logic Meets Epistemic Game Theory: A Comparison Between Multi-Agent Kripke Models and Type Spaces. Synthese:1-31.
    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 (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  22.  18
    Fairouz Kamareddine (1995). A Type Free Theory and Collective/Distributive Predication. 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  
  23.  12
    Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. 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  
  24. M. Schroder (2004). Spaces Allowing Type-2 Complexity Theory Revisited. Mathematical Logic Quarterly 50 (4):443.
    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  
  25. David Steiner & Thomas Strahm (2006). On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations. 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 (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  26.  37
    James Ladyman & Stuart Presnell (2015). Identity in Homotopy Type Theory, Part I: The Justification of Path Induction. 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  
  27.  18
    Georg Schiemer & Erich H. Reck (2013). Logic in the 1930s: Type Theory and Model Theory. 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 (2 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  28.  49
    Steve Awodey, Type Theory and Homotopy.
    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  
  29.  16
    Robin Cooper, Austinian Truth, Attitudes and Type Theory ∗.
    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 (...)
    No categories
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography   3 citations  
  30.  17
    James Ladyman & Stuart Presnell, Does Homotopy Type Theory Provide a Foundation for Mathematics?
    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 paper explains and motivates an account of how to define, justify and think about HoTT in a way that is self-contained, and argues that it can serve as an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics (...)
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  31.  8
    Anton Setzer (2000). Extending Martin-Löf Type Theory by One Mahlo-Universe. 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  
  32.  1
    Michael Rathjen & Sergei Tupailo (2006). Characterizing the Interpretation of Set Theory in Martin-Löf Type Theory. 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  
  33.  8
    Pieter Hofstra & Michael A. Warren (2013). Combinatorial Realizability Models of Type Theory. 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  
  34. Graham Stevens (2003). Re-Examining Russell's Paralysis: Ramified Type-Theory and Wittgenstein's Objection to Russell's Theory of Judgment. Russell 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  
  35.  11
    Michael Rathjen (2000). The Strength of Martin-Löf Type Theory with a Superuniverse. Part I. 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   4 citations  
  36.  5
    Anton Setzer (1998). Well-Ordering Proofs for Martin-Löf Type Theory. 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   5 citations  
  37.  12
    Michael Rathjen (2003). Realizing Mahlo Set Theory in Type Theory. 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  
  38.  3
    Hajime Ishihara & Erik Palmgren (2006). Quotient Topologies in Constructive Set Theory and Type Theory. 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   2 citations  
  39.  8
    Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. 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 (6 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  40.  3
    Leonardo de Moura, Jeremy Avigad, Soonho Kong & Cody Roux, Elaboration in Dependent Type Theory.
    To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  41.  24
    Steve Awodey, Natural Models of Homotopy Type Theory.
    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  
  42.  26
    J. Michael Dunn (1979). A Theorem in 3-Valued Model Theory with Connections to Number Theory, Type Theory, and Relevant Logic. 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   4 citations  
  43.  19
    Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. 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  
  44.  6
    Michael Rathjen (2001). The Strength of Martin-Löf Type Theory with a Superuniverse. Part II. 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   1 citation  
  45.  2
    Robert S. Fudge (2015). The Art Type Theory of Art. Philosophical Papers 44 (3):321-343.
    The theory I present and defend in this paper—what I term the art type theory— holds that something is a work of art iff it belongs to an established art type. Something is an established art type, in turn, either because its paradigmatic instances standardly satisfy eight art-making conditions, or because the art world has seen fit to enfranchise it as such. It follows that the art status of certain objects is independent of what any (...)
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  46.  24
    Edward N. Zalta (1982). Meinongian Type Theory and its Applications. Studia Logica 41 (2-3):297-307.
    In this paper I propose a fundamental modification of standard type theory, produce a new kind of type theoretic language, and couch in this language a comprehensive theory of abstract individuals and abstract properties and relations of every type. I then suggest how to employ the theory to solve the four following philosophical problems: the identification and ontological status of Frege's Senses; the deviant behavior of terms in propositional attitude contexts; the non-identity of necessarily (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  47.  37
    J. Lambek & P. J. Scott (1981). Intuitionist Type Theory and Foundations. Journal of Philosophical Logic 10 (1):101 - 115.
    A version of intuitionistic type theory is presented here in which all logical symbols are defined in terms of equality. This language is used to construct the so-called free topos with natural number object. It is argued that the free topos may be regarded as the universe of mathematics from an intuitionist's point of view.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  48.  1
    William M. Farmer (1993). 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] 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   1 citation  
  49.  11
    Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. Journal of Symbolic Logic 49 (3):730-753.
    We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  50.  23
    Zofia Kostrzycka & Marek Zaionc (2008). Asymptotic Densities in Logic and Type Theory. 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 (5 more)  
     
    Export citation  
     
    My bibliography  
1 — 50 / 1000