This category needs an editor. We encourage you to help if you are qualified.
Volunteer, or read more about what this involves.
Related categories

909 found
Order:
1 — 50 / 909
  1. Varieties of Three-Valued Heyting Algebras with a Quantifier.M. Abad, J. P. Díaz Varela, L. A. Rueda & A. M. Suardíaz - 2000 - Studia Logica 65 (2):181-198.
    This paper is devoted to the study of some subvarieties of the variety Qof Q-Heyting algebras, that is, Heyting algebras with a quantifier. In particular, a deeper investigation is carried out in the variety Q 3 of three-valued Q-Heyting algebras to show that the structure of the lattice of subvarieties of Qis far more complicated that the lattice of subvarieties of Heyting algebras. We determine the simple and subdirectly irreducible algebras in Q 3 and we construct the lattice of subvarieties (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2. The Philosophy of Alternative Logics.Andrew Aberdein & Stephen Read - 2009 - In Leila Haaparanta (ed.), The Development of Modern Logic. Oxford University Press. pp. 613-723.
    This chapter focuses on alternative logics. It discusses a hierarchy of logical reform. It presents case studies that illustrate particular aspects of the logical revisionism discussed in the chapter. The first case study is of intuitionistic logic. The second case study turns to quantum logic, a system proposed on empirical grounds as a resolution of the antinomies of quantum mechanics. The third case study is concerned with systems of relevance logic, which have been the subject of an especially detailed reform (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3. A Δ22 Well-Order of the Reals and Incompactness of L.Uri Abraham & Saharon Shelah - 1993 - Annals of Pure and Applied Logic 59 (1):1-32.
    A forcing poset of size 221 which adds no new reals is described and shown to provide a Δ22 definable well-order of the reals . The encoding of this well-order is obtained by playing with products of Aronszajn trees: some products are special while other are Suslin trees. The paper also deals with the Magidor–Malitz logic: it is consistent that this logic is highly noncompact.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  4. Binary Refinement Implies Discrete Exponentiation.Peter Aczel, Laura Crosilla, Hajime Ishihara, Erik Palmgren & Peter Schuster - 2006 - Studia Logica 84 (3):361-368.
    Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary refinement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary refinement implies that the class of detachable subsets of a set form a set. Binary refinement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was sufficient to prove that the (...)
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  5. On a Contraction-Less Intuitionistic Propositional Logic with Conjunction and Fusion.Romà J. Adillon & Ventura Verdú - 2000 - Studia Logica 65 (1):11-30.
    In this paper we prove the equivalence between the Gentzen system G LJ*\c , obtained by deleting the contraction rule from the sequent calculus LJ* (which is a redundant version of LJ), the deductive system IPC*\c and the equational system associated with the variety RL of residuated lattices. This means that the variety RL is the equivalent algebraic semantics for both systems G LJ*\c in the sense of [18] and [4], respectively. The equivalence between G LJ*\c and IPC*\c is a (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6. Classical Logic, Intuitionistic Logic, and the Peirce Rule.Henry Africk - 1992 - Notre Dame Journal of Formal Logic 33 (2):229-235.
    A simple method is provided for translating proofs in Grentzen's LK into proofs in Gentzen's LJ with the Peirce rule adjoined. A consequence is a simpler cut elimination operator for LJ + Peirce that is primitive recursive.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  7. A Bounded Translation of Intuitionistic Propositional Logic Into Basic Propositional Logic.Mojtaba Aghaei & Mohammad Ardeshir - 2000 - Mathematical Logic Quarterly 46 (2):195-206.
    In this paper we prove a bounded translation of intuitionistic propositional logic into basic propositional logic. Our new theorem, compared with the translation theorem in [1], has the advantage that it gives an effective bound on the translation, depending on the complexity of formulas.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  8. Intuitionistic Autoepistemic Logic.Luigia Aiello, Giambattista Amati, Fiora Pirri & Fondazione Ugo Bordoni - 1997 - Studia Logica 59.
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  9. Constructive Discursive Logic with Strong Negation.Seiki Akama, Jair Minoro Abe & Kazumi Nakamatsu - 2011 - Logique Et Analyse 54 (215):395-408.
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  10. A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
    A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  11. Intuitionistic Autoepistemic Logic.Giambattista Amati, Luigia Carlucci-Aiello & Fiora Pirri - 1997 - Studia Logica 59 (1):103-120.
    In this paper we address the problem of combining a logic with nonmonotonic modal logic. In particular we study the intuitionistic case. We start from a formal analysis of the notion of intuitionistic consistency via the sequent calculus. The epistemic operator M is interpreted as the consistency operator of intuitionistic logic by introducing intuitionistic stable sets. On the basis of a bimodal structure we also provide a semantics for intuitionistic stable sets.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  12. Review: M. I. Semenenko, Properties of Some Sublogics of the Classical and Intuitionistic Propositional Calculi. [REVIEW]Alan Ross Anderson - 1974 - Journal of Symbolic Logic 39 (2):351-352.
  13. Uniqueness of Normal Proofs in Implicational Intuitionistic Logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
    A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is provable without (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14. LK, LJ, Dual Intuitionistic Logic, and Quantum Logic.Hiroshi Aoyama - 2004 - Notre Dame Journal of Formal Logic 45 (4):193-213.
    In this paper, we study the relationship among classical logic, intuitionistic logic, and quantum logic . These logics are related in an interesting way and are not far apart from each other, as is widely believed. The results in this paper show how they are related with each other through a dual intuitionistic logic . Our study is completely syntactical.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  15. A Translation of Intuitionistic Predicate Logic Into Basic Predicate Logic.Mohammad Ardeshir - 1999 - Studia Logica 62 (3):341-352.
    Basic Predicate Logic, BQC, is a proper subsystem of Intuitionistic Predicate Logic, IQC. For every formula in the language {, , , , , , }, we associate two sequences of formulas 0,1,... and 0,1,... in the same language. We prove that for every sequent , there are natural numbers m, n, such that IQC , iff BQC n m. Some applications of this translation are mentioned.
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  16. Intuitionistic Open Induction and Least Number Principle and the Buss Operator.Mohammad Ardeshir & Mojtaba Moniri - 1998 - Notre Dame Journal of Formal Logic 39 (2):212-220.
    In "Intuitionistic validity in -normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory , that of all -normal Kripke structures for which he gave an r.e. axiomatization. In the language of arithmetic and denote PA plus Open Induction or Open LNP, and are their intuitionistic deductive closures. We show is recursively axiomatizable and , while . If proves PEM but not totality of a classically provably total Diophantine function of , then and so . A (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  17. The Double Negation of the Intermediate Value Theorem.Mohammad Ardeshir & Rasoul Ramezanian - 2010 - Annals of Pure and Applied Logic 161 (6):737-744.
    In the context of intuitionistic analysis, we consider the set consisting of all continuous functions from [0,1] to such that =0 and =1, and the set consisting of ’s in where there exists x[0,1] such that . It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have . However, there exists no satisfying answer to . We try to answer to this question by reducing it to a schema about intuitionistic (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  18. Intuitionistic Axiomatizations for Bounded Extension Kripke Models.Mohammad Ardeshir, Wim Ruitenburg & Saeed Salehi - 2003 - Annals of Pure and Applied Logic 124 (1-3):267-285.
    We present axiom systems, and provide soundness and strong completeness theorems, for classes of Kripke models with restricted extension rules among the node structures of the model. As examples we present an axiom system for the class of cofinal extension Kripke models, and an axiom system for the class of end-extension Kripke models. We also show that Heyting arithmetic is strongly complete for its class of end-extension models. Cofinal extension models of HA are models of Peano arithmetic.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  19. Ardeshir, M., Ruitenburg, W. And Salehi, S., Intuitionistic.C. Areces, P. Blackburn, M. Marx, S. Cook, A. Kolokolova, T. Coquand, G. Sambin, J. Smith, S. Valentini & P. Dybjer - 2003 - Annals of Pure and Applied Logic 124:301.
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  20. The Ontology of Justifications in the Logical Setting.Sergei N. Artemov - 2012 - Studia Logica 100 (1-2):17-30.
    Justification Logic provides an axiomatic description of justifications and delegates the question of their nature to semantics. In this note, we address the conceptual issue of the logical type of justifications: we argue that justifications in the logical setting are naturally interpreted as sets of formulas which leads to a class of epistemic models that we call modular models . We show that Fitting models for Justification Logic naturally encode modular models and can be regarded as convenient pre-models of the (...)
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  21. The Basic Intuitionistic Logic of Proofs.Sergei Artemov & Rosalie Iemhoff - 2007 - Journal of Symbolic Logic 72 (2):439 - 451.
    The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  22. Discovering Knowability: A Semantic Analysis.Sergei Artemov & Tudor Protopopescu - 2013 - Synthese 190 (16):3349-3376.
    In this paper, we provide a semantic analysis of the well-known knowability paradox stemming from the Church–Fitch observation that the meaningful knowability principle /all truths are knowable/, when expressed as a bi-modal principle F --> K♢F, yields an unacceptable omniscience property /all truths are known/. We offer an alternative semantic proof of this fact independent of the Church–Fitch argument. This shows that the knowability paradox is not intrinsically related to the Church–Fitch proof, nor to the Moore sentence upon which it (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  23. Algebraic Proofs of Cut Elimination.Jeremy Avigad - manuscript
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24. Interpreting Classical Theories in Constructive Ones.Jeremy Avigad - 2000 - Journal of Symbolic Logic 65 (4):1785-1812.
    A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.
    Remove from this list   Direct download (12 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  25. A Non-Deterministic View on Non-Classical Negations.Arnon Avron - 2005 - Studia Logica 80 (2-3):159-194.
    We investigate two large families of logics, differing from each other by the treatment of negation. The logics in one of them are obtained from the positive fragment of classical logic (with or without a propositional constant ff for “the false”) by adding various standard Gentzen-type rules for negation. The logics in the other family are similarly obtained from LJ+, the positive fragment of intuitionistic logic (again, with or without ff). For all the systems, we provide simple semantics which is (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  26. Topological Completeness for Higher-Order Logic.S. Awodey & C. Butz - 2000 - Journal of Symbolic Logic 65 (3):1168-1182.
    Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.
    Remove from this list   Direct download (13 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27. Quantified Propositional Gödel Logics.Matthias Baaz, Agata Ciabattoni & Richard Zach - 2000 - In Andrei Voronkov & Michel Parigot (eds.), Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000. Berlin: Springer. pp. 240-256.
    It is shown that Gqp↑, the quantified propositional Gödel logic based on the truth-value set V↑ = {1 - 1/n : n≥1}∪{1}, is decidable. This result is obtained by reduction to Büchi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of Gqp↑ as the intersection of all finite-valued quantified propositional Gödel logics.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  28. On Skolemization in Constructive Theories.Matthias Baaz & Rosalie Iemhoff - 2008 - Journal of Symbolic Logic 73 (3):969-998.
    In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  29. Gentzen Calculi for the Existence Predicate.Matthias Baaz & Rosalie Iemhoff - 2006 - Studia Logica 82 (1):7-23.
    We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  30. The Skolemization of Existential Quantifiers in Intuitionistic Logic.Matthias Baaz & Rosalie Iemhoff - 2006 - Annals of Pure and Applied Logic 142 (1):269-295.
    In this paper an alternative Skolemization method is introduced that, for a large class of formulas, is sound and complete with respect to intuitionistic logic. This class extends the class of formulas for which standard Skolemization is sound and complete and includes all formulas in which all strong quantifiers are existential. The method makes use of an existence predicate first introduced by Dana Scott.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  31. Bi-Simulating in Bi-Intuitionistic Logic.Guillermo Badia - 2016 - Studia Logica 104 (5):1037-1050.
    Bi-intuitionistic logic is the result of adding the dual of intuitionistic implication to intuitionistic logic. In this note, we characterize the expressive power of this logic by showing that the first order formulas equivalent to translations of bi-intuitionistic propositional formulas are exactly those preserved under bi-intuitionistic directed bisimulations. The proof technique is originally due to Lindstrom and, in contrast to the most common proofs of this kind of result, it does not use the machinery of neither saturated models nor elementary (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  32. Some Results on Kripke Models Over an Arbitrary Fixed Frame.Seyed Mohammad Bagheri & Morteza Moniri - 2003 - Mathematical Logic Quarterly 49 (5):479-484.
    We study the relations of being substructure and elementary substructure between Kripke models of intuitionistic predicate logic with the same arbitrary frame. We prove analogues of Tarski's test and Löwenheim-Skolem's theorems as determined by our definitions. The relations between corresponding worlds of two Kripke models [MATHEMATICAL SCRIPT CAPITAL K] ⪯ [MATHEMATICAL SCRIPT CAPITAL K]′ are studied.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  33. Diagram Construction in Intuitionistic Logic.Seyed Bagheri & Massoud Pourmahdian - 2006 - Logic Journal of the IGPL 14 (6):889-901.
    Every classical first order structure is coded in its diagram consisting of atomic sentences it satisfies. We study diagrams for the class of constant domain Kripke models and use it to define notions of submodel, reduction, expansion and ultraproduct for a ceratin subclass of it. In particular, we study conditions under which forcing is preserved by reductions and expansions.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  34. Review: Dana Scott, Some Definitional Suggestions for Automata Theory. [REVIEW]Robert F. Barnes - 1975 - Journal of Symbolic Logic 40 (4):615-616.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  35. Carnielli, Walter (ed.). Logic and Philosophy of the Formal Sciences: A Festscrift for Itala M. Loffredo D´ Ottaviano. São Paulo: Centro de Lógica, Epistemología e Historia da Ciência, UNICAMP (Número especial de Manuscrito, Revista Internacional de Filosofia, vol. 28, n. 2, jul-dez.) pp. 191-591.(2005). [REVIEW]Tomás Barrero - 2006 - Ideas Y Valores 55 (132):124-126.
  36. A Reduction Theorem for the Kripke–Joyal Semantics: Forcing Over an Arbitrary Category Can Always Be Replaced by Forcing Over a Complete Heyting Algebra. [REVIEW]Imants Barušs & Robert Woodrow - 2013 - Logica Universalis 7 (3):323-334.
    It is assumed that a Kripke–Joyal semantics \({\mathcal{A} = \left\langle \mathbb{C},{\rm Cov}, {\it F},\Vdash \right\rangle}\) has been defined for a first-order language \({\mathcal{L}}\) . To transform \({\mathbb{C}}\) into a Heyting algebra \({\overline{\mathbb{C}}}\) on which the forcing relation is preserved, a standard construction is used to obtain a complete Heyting algebra made up of cribles of \({\mathbb{C}}\) . A pretopology \({\overline{{\rm Cov}}}\) is defined on \({\overline{\mathbb{C}}}\) using the pretopology on \({\mathbb{C}}\) . A sheaf \({\overline{{\it F}}}\) is made up of sections of (...)
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  37. Natural Deduction for Non-Classical Logics.David Basin, Seán Matthews & Luca Viganò - 1998 - Studia Logica 60 (1):119-160.
    We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and (...)
    Remove from this list   Direct download (8 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  38. Review: E.-W. Beth, General Logic and Semiotics. [REVIEW]Charles A. Baylis - 1950 - Journal of Symbolic Logic 15 (3):233-233.
  39. Review: G. T. Kneebone, Philosophy and Mathematics. [REVIEW]Charles A. Baylis - 1948 - Journal of Symbolic Logic 13 (2):124-124.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  40. The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals.Michael Beeson - 1976 - Journal of Symbolic Logic 41 (1):18-24.
  41. The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations.Michael J. Beeson - 1975 - Journal of Symbolic Logic 40 (3):321-346.
  42. Intuitionistic Negation.W. Russell Belding - 1971 - Notre Dame Journal of Formal Logic 12 (2):183-187.
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  43. Hilbert’s Varepsilon -Operator in Intuitionistic Type Theories.John L. Bell - 1993 - Mathematical Logic Quarterly 39 (1):323--337.
    We investigate Hilbert’s varepsilon -calculus in the context of intuitionistic type theories, that is, within certain systems of intuitionistic higher-order logic. We determine the additional deductive strength conferred on an intuitionistic type theory by the adjunction of closed varepsilon -terms. We extend the usual topos semantics for type theories to the varepsilon -operator and prove a completeness theorem. The paper also contains a discussion of the concept of “partially defined‘ varepsilon -term. MSC: 03B15, 03B20, 03G30.
    Remove from this list  
     
    Export citation  
     
    Bookmark   1 citation  
  44. On an Intuitionistic Logic for Pragmatics.Gianluigi Bellin, Massimiliano Carrara & Daniele Chiffi - 2015 - Journal of Logic and Computation:doi: 10.1093/logcom/exv036.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  45. On Not Strengthening Intuitionistic Logic.N. D. Belnap, H. Leblanc & R. H. Thomason - 1963 - Notre Dame Journal of Formal Logic 4 (4):313-320.
    tic sequenzen-kalkul of Gentzen, into rules for PCc, the classical sequenzenkalkul. We shall limit ourselves here to sequenzen or turnstile statements of the form A„A„..., A„ I- B, where A„A„..., A„(n ~ 0), and B are wffs consisting of propositional variables, zero or more of the connectives '5', "v', ' ', ')', and '=', and zero or more parentheses. One can pass from PCi to PCc by amending the intelim rules for ' a result of long standing, or by amending (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  46. Review: E. W. Beth, History of Logic. [REVIEW]Albert A. Bennett - 1946 - Journal of Symbolic Logic 11 (3):96-96.
  47. The Information in Intuitionistic Logic.Johan Benthem - 2009 - Synthese 167 (2):251-270.
    Issues about information spring up wherever one scratches the surface of logic. Here is a case that raises delicate issues of 'factual' versus 'procedural' information, or 'statics' versus 'dynamics'. What does intuitionistic logic, perhaps the earliest source of informational and procedural thinking in contemporary logic, really tell us about information? How does its view relate to its 'cousin' epistemic logic? We discuss connections between intuitionistic models and recent protocol models for dynamic-epistemic logic, as well as more general issues that emerge.
    Remove from this list   Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  48. Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
    In the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic. All results included here, but a part of the proposition (a) below, are new. This work is, ideally, (...)
    Remove from this list   Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  49. Krivine's Intuitionistic Proof of Classical Completeness.Stefano Berardi & Silvio Valentini - 2004 - Annals of Pure and Applied Logic 129 (1-3):93-106.
    In 1996, Krivine applied Friedman's A-translation in order to get an intuitionistic version of Gödel completeness result for first-order classical logic and countable languages and models. Such a result is known to be intuitionistically underivable 559), but Krivine was able to derive intuitionistically a weak form of it, namely, he proved that every consistent classical theory has a model. In this paper, we want to analyze the ideas Krivine's remarkable result relies on, ideas which where somehow hidden by the heavy (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  50. Review: A. Heyting, L'Axiomatique Intuitionniste. [REVIEW]Paul Bernays - 1958 - Journal of Symbolic Logic 23 (3):343-344.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 909