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.

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.

Gentzen sequent calculi for some intuitionistic modal logics

2019 ◽  
Vol 27 (4) ◽  
pp. 596-623
Author(s):  
Zhe Lin ◽  
Minghui Ma
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Modal Logics ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Intuitionistic Propositional Logic ◽  
Propositional Language ◽  
Intuitionistic Modal Logics ◽  
Subformula Property ◽  
Gentzen Sequent Calculus

Abstract Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond ,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond ,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

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.

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.

scholarly journals Maximality of bi-intuitionistic propositional logic

2021 ◽  
Author(s):  
Grigory Olkhovikov ◽  
Guillermo Badia
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Expressive Power ◽  
Formal Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Intuitionistic Propositional Logic ◽  
Abstract Logic ◽  
First Order ◽  
Work Done

Abstract In the style of Lindström’s theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of the previous work done by the authors for intuitionistic logic (Badia and Olkhovikov, 2020, Notre Dame Journal of Formal Logic, 61, 11–30).

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.

Admissibility of structural rules for contraction-free systems of intuitionistic logic

2000 ◽  
Vol 65 (4) ◽  
pp. 1499-1518 ◽  
Author(s):  
Roy Dyckhoff ◽  
Sara Negri
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Direct Proof ◽  
Intuitionistic Propositional Logic ◽  
Structural Rules

AbstractWe give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs, i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

Sign in / Sign up

Export Citation Format

Share Document