scholarly journals A modal logic amalgam of classical and intuitionistic propositional logic

2015 ◽  
Vol 27 (1) ◽  
pp. 201-212 ◽  
Author(s):  
Steffen Lewitzka
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Intuitionistic Propositional Logic

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.

scholarly journals From intuitionism to Brouwer’s modal logic

2020 ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Main Idea ◽  
Intuitionistic Propositional Logic ◽  
Strict Implication

We try to translate the intuitionistic propositional logic INT into Brouwer’s modal logic KTB. Our translation is motivated by intuitions behind Brouwer’s axiom p →☐◊p as discussed in [4]. The main idea is to interpret intuitionistic implication as modal strict implication, whereas variables and other positive sen-tences remain as they are. The proposed translation preserves fragments of the Rieger-Nishimura lattice which is the Lindenbaum algebra of monadic formulas in INT. Unfortunately, INT is not embedded by this mapping into KTB.

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.

scholarly journals An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

2019 ◽  
Author(s):  
Camillo Fiorentini
Keyword(s):  
Propositional Logic ◽  
Answer Set Programming ◽  
Kripke Model ◽  
Kripke Semantics ◽  
Minimal Models ◽  
Intuitionistic Propositional Logic ◽  
Answer Set

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

Sign in / Sign up

Export Citation Format

Share Document