A CORRECT POLYNOMIAL TRANSLATION OF S4 INTO INTUITIONISTIC LOGIC

2019 ◽  
Vol 84 (02) ◽  
pp. 439-451
Author(s):  
RAJEEV GORÉ ◽  
JIMMY THOMSON
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Intuitionistic Propositional Logic ◽  
Normal Modal Logic ◽  
Modal Logic S4 ◽  
Polynomial Translation

AbstractWe show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernández is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.

scholarly journals On density of truth of the intuitionistic logic in one variable

2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
Propositional Variable ◽  
Intuitionistic Propositional Logic ◽  
International Audience

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

The decidability of the Kreisel-Putnam system

1970 ◽  
Vol 35 (3) ◽  
pp. 431-437 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Finite Model ◽  
Model Property ◽  
Intuitionistic Propositional Logic ◽  
Disjunction Property ◽  
Finite Model Property ◽  
Image Position

The intuitionistic propositional logic I has the following disjunction property This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiomhas the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom:In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.

scholarly journals COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS

2018 ◽  
Vol 11 (3) ◽  
pp. 507-518
Author(s):  
PHILIP KREMER
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
Second Order ◽  
Topological Semantics ◽  
First Order ◽  
Propositional Modal Logic ◽  
Propositional Quantifiers ◽  
Modal Logic S4 ◽  
Natural Way

AbstractWe add propositional quantifiers to the propositional modal logic S4 and to the propositional intuitionistic logic H, introducing axiom schemes that are the natural analogs to axiom schemes typically used for first-order quantifiers in classical and intuitionistic logic. We show that the resulting logics are sound and complete for a topological semantics extending, in a natural way, the topological semantics for S4 and for H.

Explicit Provability and Constructive Semantics

2001 ◽  
Vol 7 (1) ◽  
pp. 1-36 ◽  
Author(s):  
Sergei N. Artemov
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Modal Logics ◽  
Combinatory Logic ◽  
Underlying Structure ◽  
Intuitionistic Propositional Logic ◽  
Intuitionistic Modal Logics

AbstractIn 1933 Gödel introduced a calculus of provability (also known as modal logicS4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logicLPof propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection ofLP. This also achieves Gödel's objective of defining intuitionistic propositional logicIntvia classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics forIntwhich resisted formalization since the early 1930s.LPmay be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

Logical connectives for intuitionistic propositional logic

1971 ◽  
Vol 36 (1) ◽  
pp. 15-20 ◽  
Author(s):  
Dean P. McCullough
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Classical Type ◽  
Classical Propositional Logic ◽  
Intuitionistic Propositional Logic ◽  
Truth Function ◽  
Logical Connectives ◽  
Complete Set ◽  
Complete Sets

In classical propositional logic it is well known that {7, ⊃ } is a functionally complete set with respect to a two-valued truth function modeling. I.e. all definable logical connectives are definable from 7 and ⊃. Other modelings of classical type propositional logics may have different functionally complete sets; for example, multivalued truth function modelings.This paper examines the question of a functionally complete set of logical connectives for intuitionistic propositional logic with respect to S. Kripke's modeling for intuitionistic logic.

Propositional quantification in the monadic fragment of intuitionistic logic

1998 ◽  
Vol 63 (1) ◽  
pp. 269-300 ◽  
Author(s):  
Tomasz Połacik
Keyword(s):  
Intuitionistic Logic ◽  
Metric Space ◽  
Propositional Logic ◽  
Second Order ◽  
Intuitionistic Propositional Logic ◽  
Topological Interpretation ◽  
Propositional Quantifiers ◽  
Propositional Quantification

AbstractWe study the monadic fragment of second order intuitionistic propositional logic in the language containing the standard propositional connectives and propositional quantifiers. It is proved that under the topological interpretation over any dense-in-itself metric space, the considered fragment collapses to Heyting calculus. Moreover, we prove that the topological interpretation over any dense-in-itself metric space of fragment in question coincides with the so-called Pitts' interpretation. We also prove that all the nonstandard propositional operators of the form q ↦ ∃p (q ↔ F(p)), where F is an arbitrary monadic formula of the variable p, are definable in the language of Heyting calculus under the topological interpretation of intuitionistic logic over sufficiently regular spaces.

scholarly journals An Alternative Natural Deduction for the Intuitionistic Propositional Logic

2016 ◽  
Vol 45 (1) ◽  
Author(s):  
Mirjana Ilić
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Intuitionistic Propositional Logic ◽  
Deduction System ◽  
Natural Deduction System

A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.

FORMULAS IN MODAL LOGIC S4

2010 ◽  
Vol 3 (4) ◽  
pp. 600-627
Author(s):  
KATSUMI SASAKI
Keyword(s):  
Normal Form ◽  
Modal Logic ◽  
Propositional Logic ◽  
Normal Forms ◽  
Classical Propositional Logic ◽  
Mutual Relation ◽  
Grzegorczyk Logic ◽  
Modal Logic S4 ◽  
Normal Modal Logics ◽  
Finite Method

Here, we provide a detailed description of the mutual relation of formulas with finite propositional variables p1, …, pm in modal logic S4. Our description contains more information on S4 than those given in Shehtman (1978) and Moss (2007); however, Shehtman (1978) also treated Grzegorczyk logic and Moss (2007) treated many other normal modal logics. Specifically, we construct normal forms, which behave like the principal conjunctive normal forms in the classical propositional logic. The results include finite and effective methods to find a normal form equivalent to a given formula A by clarifying the behavior of connectives and giving a finite method to list all exact models.

scholarly journals CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION

2018 ◽  
Vol 83 (04) ◽  
pp. 1680-1682
Author(s):  
ROY DYCKHOFF
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Major Result ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic

AbstractWe present a much-shortened proof of a major result (originally due to Vorob’ev) about intuitionistic propositional logic: in essence, a correction of our 1992 article, avoiding several unnecessary definitions.

Sign in / Sign up

Export Citation Format

Share Document