Switch to: References

Add citations

You must login to add citations.
  1. The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
    One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a (...)
    Download  
     
    Export citation  
     
    Bookmark   48 citations  
  • Type-theoretic interpretation of iterated, strictly positive inductive definitions.Erik Palmgren - 1992 - Archive for Mathematical Logic 32 (2):75-99.
    We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur only (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Interpreting Descriptions in Intensional Type Theory.Jesper Carlström - 2005 - Journal of Symbolic Logic 70 (2):488 - 514.
    Natural deduction systems with indefinite and definite descriptions (ε-terms and ι-terms) are presented, and interpreted in Martin-Löf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of 'the element such that the property holds' and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting descriptions by (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • On constructing completions.Laura Crosilla, Hajime Ishihara & Peter Schuster - 2005 - Journal of Symbolic Logic 70 (3):969-978.
    The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo—Fraenkel set theory. We deduce this statement from the principle of refinement, which we distill before from the axiom of fullness. Together with exponentiation, refinement is equivalent to fullness. None of the defining properties of an ordering is needed, and only refinement for two—element coverings is used. In particular, the Dedekind reals form a set; whence we have also refined an earlier result by Aczel and (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Frege's Judgement Stroke and the Conception of Logic as the Study of Inference not Consequence.Nicholas J. J. Smith - 2009 - Philosophy Compass 4 (4):639-665.
    One of the most striking differences between Frege's Begriffsschrift (logical system) and standard contemporary systems of logic is the inclusion in the former of the judgement stroke: a symbol which marks those propositions which are being asserted , that is, which are being used to express judgements . There has been considerable controversy regarding both the exact purpose of the judgement stroke, and whether a system of logic should include such a symbol. This paper explains the intended role of the (...)
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • A meaning explanation for HoTT.Dimitris Tsementzis - 2020 - Synthese 197 (2):651-680.
    In the Univalent Foundations of mathematics spatial notions like “point” and “path” are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory can be justified intuitively as a theory of shapes in the same way that ZFC can be justified intuitively as a theory of collections. I first clarify (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Concept Horse is a Concept.Ansten Klev - 2018 - Review of Symbolic Logic 11 (3):547-572.
    I offer an analysis of the sentence "the concept horse is a concept". It will be argued that the grammatical subject of this sentence, "the concept horse", indeed refers to a concept, and not to an object, as Frege once held. The argument is based on a criterion of proper-namehood according to which an expression is a proper name if it is so rendered in Frege's ideography. The predicate "is a concept", on the other hand, should not be thought of (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Seeming Interdependence Between the Concepts of Valid Inference and Proof.Dag Prawitz - 2019 - Topoi 38 (3):493-503.
    We may try to explain proofs as chains of valid inference, but the concept of validity needed in such an explanation cannot be the traditional one. For an inference to be legitimate in a proof it must have sufficient epistemic power, so that the proof really justifies its final conclusion. However, the epistemic concepts used to account for this power are in their turn usually explained in terms of the concept of proof. To get out of this circle we may (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • A pragmatic interpretation of intuitionistic propositional logic.Carlo Dalla Pozza & Claudio Garola - 1995 - Erkenntnis 43 (1):81-109.
    We construct an extension P of the standard language of classical propositional logic by adjoining to the alphabet of a new category of logical-pragmatic signs. The well formed formulas of are calledradical formulas (rfs) of P;rfs preceded by theassertion sign constituteelementary assertive formulas of P, which can be connected together by means of thepragmatic connectives N, K, A, C, E, so as to obtain the set of all theassertive formulas (afs). Everyrf of P is endowed with atruth value defined classically, (...)
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • Uniformly convex Banach spaces are reflexive—constructively.Douglas S. Bridges, Hajime Ishihara & Maarten McKubre-Jordens - 2013 - Mathematical Logic Quarterly 59 (4-5):352-356.
    We propose a natural definition of what it means in a constructive context for a Banach space to be reflexive, and then prove a constructive counterpart of the Milman-Pettis theorem that uniformly convex Banach spaces are reflexive.
    Download  
     
    Export citation  
     
    Bookmark  
  • In Defense of Logical Universalism: Taking Issue with Jean van Heijenoort.Philippe Rouilhan - 2012 - Logica Universalis 6 (3-4):553-586.
    Van Heijenoort's main contribution to history and philosophy of modern logic was his distinction between two basic views of logic, first, the absolutist, or universalist, view of the founding fathers, Frege, Peano, and Russell, which dominated the first, classical period of history of modern logic, and, second, the relativist, or model-theoretic, view, inherited from Boole, Schröder, and Löwenheim, which has dominated the second, contemporary period of that history. In my paper, I present the man Jean van Heijenoort (Sect. 1); then (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • What is neologicism?Bernard Linsky & Edward N. Zalta - 2006 - Bulletin of Symbolic Logic 12 (1):60-99.
    In this paper, we investigate (1) what can be salvaged from the original project of "logicism" and (2) what is the best that can be done if we lower our sights a bit. Logicism is the view that "mathematics is reducible to logic alone", and there are a variety of reasons why it was a non-starter. We consider the various ways of weakening this claim so as to produce a "neologicism". Three ways are discussed: (1) expand the conception of logic (...)
    Download  
     
    Export citation  
     
    Bookmark   24 citations  
  • Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
    In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...)
    Download  
     
    Export citation  
     
    Bookmark   116 citations  
  • Setting the Facts Straight.Mark Jago - 2011 - Journal of Philosophical Logic 40 (1):33-54.
    Substantial facts are not well-understood entities. Many philosophers object to their existence on this basis. Yet facts, if they can be understood, promise to do a lot of philosophical work: they can be used to construct theories of property possession and truthmaking, for example. Here, I give a formal theory of facts, including negative and logically complex facts. I provide a theory of reduction similar to that of the typed λ -calculus and use it to provide identity conditions for facts. (...)
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • A minimalist two-level foundation for constructive mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
    We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin.One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections.The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model.This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • “Inference versus consequence” revisited: inference, consequence, conditional, implication.Göran Sundholm - 2012 - Synthese 187 (3):943-956.
    Inference versus consequence , an invited lecture at the LOGICA 1997 conference at Castle Liblice, was part of a series of articles for which I did research during a Stockholm sabbatical in the autumn of 1995. The article seems to have been fairly effective in getting its point across and addresses a topic highly germane to the Uppsala workshop. Owing to its appearance in the LOGICA Yearbook 1997 , Filosofia Publishers, Prague, 1998, it has been rather inaccessible. Accordingly it is (...)
    Download  
     
    Export citation  
     
    Bookmark   30 citations  
  • Univalent foundations as structuralist foundations.Dimitris Tsementzis - 2017 - Synthese 194 (9):3583-3617.
    The Univalent Foundations of Mathematics provide not only an entirely non-Cantorian conception of the basic objects of mathematics but also a novel account of how foundations ought to relate to mathematical practice. In this paper, I intend to answer the question: In what way is UF a new foundation of mathematics? I will begin by connecting UF to a pragmatist reading of the structuralist thesis in the philosophy of mathematics, which I will use to define a criterion that a formal (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • A Proof‐Theoretic Account of the Miners Paradox.Ansten Klev - 2016 - Theoria 82 (4):351-369.
    By maintaining that a conditional sentence can be taken to express the validity of a rule of inference, we offer a solution to the Miners Paradox that leaves both modus ponens and disjunction elimination intact. The solution draws on Sundholm's recently proposed account of Fitch's Paradox.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Pretopologies and a uniform presentation of sup-lattices, quantales and frames.Giulia Battilotti & Giovanni Sambin - 2006 - Annals of Pure and Applied Logic 137 (1-3):30-61.
    We introduce the notion of infinitary preorder and use it to obtain a predicative presentation of sup-lattices by generators and relations. The method is uniform in that it extends in a modular way to obtain a presentation of quantales, as “sup-lattices on monoids”, by using the notion of pretopology.Our presentation is then applied to frames, the link with Johnstone’s presentation of frames is spelled out, and his theorem on freely generated frames becomes a special case of our results on quantales.The (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Steps Towards a Proof-Theoretical Semantics.Enrico Moriconi - 2012 - Topoi 31 (1):67-75.
    The aim of this paper is to reconsider several proposals that have been put forward in order to develop a Proof-Theoretical Semantics, from the by now classical neo-verificationist approach provided by D. Prawitz and M. Dummett in the Seventies, to an alternative, more recent approach mainly due to the work of P. Schroeder-Heister and L. Hallnäs, based on clausal definitions. Some other intermediate proposals are very briefly sketched. Particular attention will be given to the role played by the so-called Fundamental (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Offline and Online Data: on upgrading functional information to knowledge.Giuseppe Primiero - 2013 - Philosophical Studies 164 (2):371-392.
    This paper addresses the problem of upgrading functional information to knowledge. Functional information is defined as syntactically well-formed, meaningful and collectively opaque data. Its use in the formal epistemology of information theories is crucial to solve the debate on the veridical nature of information, and it represents the companion notion to standard strongly semantic information, defined as well-formed, meaningful and true data. The formal framework, on which the definitions are based, uses a contextual version of the verificationist principle of truth (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Dedekind and Hilbert on the foundations of the deductive sciences.Ansten Klev - 2011 - Review of Symbolic Logic 4 (4):645-681.
    We offer an interpretation of the words and works of Richard Dedekind and the David Hilbert of around 1900 on which they are held to entertain diverging views on the structure of a deductive science. Firstly, it is argued that Dedekind sees the beginnings of a science in concepts, whereas Hilbert sees such beginnings in axioms. Secondly, it is argued that for Dedekind, the primitive terms of a science are substantive terms whose sense is to be conveyed by elucidation, whereas (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Dialogue structure and logical expressivism.Paul Piwek - 2011 - Synthese 183 (S1):33-58.
    This paper aims to develop the implications of logical expressivism for a theory of dialogue coherence. I proceed in three steps. Firstly, certain structural properties of cooperative dialogue are identified. Secondly, I describe a variant of the multi-agent natural deduction calculus that I introduced in Piwek (J Logic Lang Inf 16(4):403–421, 2007 ) and demonstrate how it accounts for the aforementioned structures. Thirdly, I examine how the aforementioned system can be used to formalise an expressivist account of logical vocabulary that (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • From the Knowability Paradox to the existence of proofs.W. Dean & H. Kurokawa - 2010 - Synthese 176 (2):177 - 225.
    The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed (...)
    Download  
     
    Export citation  
     
    Bookmark   13 citations  
  • A characterization of ML in many-sorted arithmetic with conditional application.M. D. G. Swaen - 1992 - Journal of Symbolic Logic 57 (3):924 - 953.
    In this paper we discuss an interpretation of intuitionistic type theory in many-sorted arithmetic with so-called conditional application. Via the formulas-as-types correspondence the arithmetical system in turn can be embedded in ML, resulting in a characterization of strong Σ-elimination by an axiom of conditional choice.
    Download  
     
    Export citation  
     
    Bookmark  
  • Recent advances in ordinal analysis: Π 21-CA and related systems.Michael Rathjen - 1995 - Bulletin of Symbolic Logic 1 (4):468 - 485.
    §1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].Ordinal-theoretic proof theory (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  • A construction of non-well-founded sets within Martin-löf's type theory.Ingrid Lindström - 1989 - Journal of Symbolic Logic 54 (1):57-64.
    In this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löf's theory of types. A system is a type W together with an assignment of ᾱ ∈ U and α̃ ∈ ᾱ → W to each α ∈ W. We show that for any system W we can define an equivalence relation = w such that α = w β ∈ U and = w is the maximal bisimulation. Aczel's proof (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • On the unusual effectiveness of logic in computer science.Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi & Victor Vianu - 2001 - Bulletin of Symbolic Logic 7 (2):213-236.
    In 1960, E. P. Wigner, a joint winner of the 1963 Nobel Prize for Physics, published a paper titled On the Unreasonable Effectiveness of Mathematics in the Natural Sciences [61]. This paper can be construed as an examination and affirmation of Galileo's tenet that “The book of nature is written in the language of mathematics”. To this effect, Wigner presented a large number of examples that demonstrate the effectiveness of mathematics in accurately describing physical phenomena. Wigner viewed these examples as (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  • Variable Handling and Compositionality: Comparing DRT and DTS.Yukiko Yana, Koji Mineshima & Daisuke Bekki - 2019 - Journal of Logic, Language and Information 28 (2):261-285.
    This paper provides a detailed comparison between discourse representation theory and dependent type semantics, two frameworks for discourse semantics. Although it is often stated that DRT and those frameworks based on dependent types are mutually exchangeable, we argue that they differ with respect to variable handling, more specifically, how substitution and other operations on variables are defined. This manifests itself in two recalcitrant problems posed for DRT; namely, the overwrite problem and the duplication problem. We will see that these problems (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On the collection of points of a formal space.Giovanni Curi - 2006 - Annals of Pure and Applied Logic 137 (1-3):126-146.
    On the collection of points of a formal space.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Between constructive mathematics and PROLOG.Gerhard Jäger - 1991 - Archive for Mathematical Logic 30 (5-6):297-310.
    Download  
     
    Export citation  
     
    Bookmark  
  • Empirical Negation.Michael De - 2013 - Acta Analytica 28 (1):49-69.
    An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation (‘It is unwarranted that. . . ’) and intuitionistic negation (‘It is refutable that. . . ’). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • The assertion-candidate and the meaning of mood.Maria van der Schaar - 2007 - Synthese 159 (1):61-82.
    The meaning of a declarative sentence and that of an interrogative sentence differ in their aspect of mood. A semantics of mood has to account for the differences in meaning between these sentences, and it also has to explain that sentences in different moods may have a common core. The meaning of the declarative mood is to be explained not in terms of actual force (contra Dummett), but in terms of potential force. The meaning of the declarative sentence (including its (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Inverse Linking, Possessive Weak Definites and Haddock Descriptions: A Unified Dependent Type Account.Justyna Grudzińska & Marek Zawadowski - 2019 - Journal of Logic, Language and Information 28 (2):239-260.
    This paper proposes a unified dependent type analysis of three puzzling phenomena: inversely linked interpretations, weak definite readings in possessives and Haddock-type readings. We argue that the three problematic readings have the same underlying surface structure, and that the surface structure postulated can be interpreted properly and compositionally using dependent types. The dependent type account proposed is the first, to the best of our knowledge, to formally connect the three phenomena. A further advantage of our proposal over previous analyses is (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • The Neglect of Epistemic Considerations in Logic: The Case of Epistemic Assumptions.Göran Sundholm - 2019 - Topoi 38 (3):551-559.
    The two different layers of logical theory—epistemological and ontological—are considered and explained. Special attention is given to epistemic assumptions of the kind that a judgement is granted as known, and their role in validating rules of inference, namely to aid the inferential preservation of epistemic matters from premise judgements to conclusion judgement, while ordinary Natural Deduction assumptions serve to establish the holding of consequence from antecedent propositions to succedent proposition.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • The Justification of the Logical Laws Revisited.Patrizio Contu - 2006 - Synthese 148 (3):573-588.
    The proof-theoretic analysis of logical semantics undermines the received view of proof theory as being concerned with symbols devoid of meaning, and of model theory as the sole branch of logical theory entitled to access the realm of semantics. The basic tenet of proof-theoretic semantics is that meaning is given by some rules of proofs, in terms of which all logical laws can be justified and the notion of logical consequence explained. In this paper an attempt will be made to (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Semantic Values for Natural Deduction Derivations.Göran Sundholm - 2006 - Synthese 148 (3):623-638.
    Drawing upon Martin-Löf’s semantic framework for his constructive type theory, semantic values are assigned also to natural-deduction derivations, while observing the crucial distinction between consequence among propositions and inference among judgements. Derivations in Gentzen’s format with derivable formulae dependent upon open assumptions, stand, it is suggested, for proof-objects, whereas derivations in Gentzen’s sequential format are proof-acts.
    Download  
     
    Export citation  
     
    Bookmark   12 citations  
  • Truth as an Epistemic Notion.Dag Prawitz - 2012 - Topoi 31 (1):9-16.
    What is the appropriate notion of truth for sentences whose meanings are understood in epistemic terms such as proof or ground for an assertion? It seems that the truth of such sentences has to be identified with the existence of proofs or grounds, and the main issue is whether this existence is to be understood in a temporal sense as meaning that we have actually found a proof or a ground, or if it could be taken in an abstract, tenseless (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Tychonoff's theorem in the framework of formal topologies.Sara Negri & Silvio Valentini - 1997 - Journal of Symbolic Logic 62 (4):1315-1332.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Canonical naming systems.Leon Horsten - 2004 - Minds and Machines 15 (2):229-257.
    This paper outlines a framework for the abstract investigation of the concept of canonicity of names and of naming systems. Degrees of canonicity of names and of naming systems are distinguished. The structure of the degrees is investigated, and a notion of relative canonicity is defined. The notions of canonicity are formally expressed within a Carnapian system of second-order modal logic.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • 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 which is (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Innovations in computational type theory using Nuprl.S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo & E. Moran - 2006 - Journal of Applied Logic 4 (4):428-469.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Reflections on reflections in explicit mathematics.Gerhard Jäger & Thomas Strahm - 2005 - Annals of Pure and Applied Logic 136 (1-2):116-133.
    We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Knowledge of proofs.Peter Pagin - 1994 - Topoi 13 (2):93-100.
    If proofs are nothing more than truth makers, then there is no force in the standard argument against classical logic (there is no guarantee that there is either a proof forA or a proof fornot A). The standard intuitionistic conception of a mathematical proof is stronger: there are epistemic constraints on proofs. But the idea that proofs must be recognizable as such by us, with our actual capacities, is incompatible with the standard intuitionistic explanations of the meanings of the logical (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • A Construction of Type: Type in Martin-Lof's Partial Type Theory with One Universe.Erik Palmgren - 1991 - Journal of Symbolic Logic 56 (3):1012-1015.
    Download  
     
    Export citation  
     
    Bookmark  
  • A constructive manifestation of the Kleene–Kreisel continuous functionals.Martín Escardó & Chuangjie Xu - 2016 - Annals of Pure and Applied Logic 167 (9):770-793.
    Download  
     
    Export citation  
     
    Bookmark  
  • Constructive belief reports.Bartosz Więckowski - 2015 - Synthese 192 (3):603-633.
    The paper develops a proof-theoretic semantics for belief reports by extending the constructive type-theoretical formalism presented in Więckowski with a specific kind of set-forming operator suited for the representation of belief attitudes. The extended formalism allows us to interpret constructions which involve, e.g., iteration of belief, quantifying into belief contexts, and anaphora in belief reports. Moreover, constructive solutions to canonical instances of the problem of hyperintensionality are suggested. The paper includes a discussion of Ranta’s constructive account of belief reports.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Polynomial-time Martin-Löf type theory.L. Pe Joseph - 1992 - Archive for Mathematical Logic 32 (2):137-150.
    Fragments of extensional Martin-Löf type theory without universes,ML 0, are introduced that conservatively extend S.A. Cook and A. Urquhart'sIPV ω. A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, some examples in group theory are considered.
    Download  
     
    Export citation  
     
    Bookmark  
  • (1 other version)An interpretation of martin‐löf's constructive theory of types in elementary topos theory.Anne Preller - 1992 - Mathematical Logic Quarterly 38 (1):213-240.
    We give a formal interpretation of Martin-Löf's Constructive Theory of Types in Elementary Topos Theory which is presented as a formalised theory with intensional equality of objects. Types are interpreted as arrows and variables as sections of their types. This is necessary to model correctly the working of the assumption x ∈ A. Then intensional equality interprets equality of types. The normal form theorem which asserts that the interpretation of a type is intensional equal to the pullback of its “alignment” (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On the existence of Stone-Čech compactification.Giovanni Curi - 2010 - Journal of Symbolic Logic 75 (4):1137-1146.
    Download  
     
    Export citation  
     
    Bookmark   4 citations