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.

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 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.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

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.

Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic

1991 ◽  
Vol 56 (4) ◽  
pp. 1403-1451 ◽  
Author(s):  
V. Michele Abrusci
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Commutative Monoid ◽  
Structural Rules ◽  
Exchange Rule ◽  
Phase Semantics ◽  
Correct Program ◽  
Image Position

The linear logic introduced in [3] by J.-Y. Girard keeps one of the so-called structural rules of the sequent calculus: the exchange rule. In a one-sided sequent calculus this rule can be formulated asThe exchange rule allows one to disregard the order of the assumptions and the order of the conclusions of a proof, and this means, when the proof corresponds to a logically correct program, to disregard the order in which the inputs and the outputs occur in a program.In the linear logic introduced in [3], the exchange rule allows one to prove the commutativity of the multiplicative connectives, conjunction (⊗) and disjunction (⅋). Due to the presence of the exchange rule in linear logic, in the phase semantics for linear logic one starts with a commutative monoid. So, the usual linear logic may be called commutative linear logic.The aim of the investigations underlying this paper was to see, first, what happens when we remove the exchange rule from the sequent calculus for the linear propositional logic at all, and then, how to recover the strength of the exchange rule by means of exponential connectives (in the same way as by means of the exponential connectives ! and ? we recover the strength of the weakening and contraction rules).

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 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).

Sign in / Sign up

Export Citation Format

Share Document