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.

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.

AGGREGATION AND IDEMPOTENCE

2013 ◽  
Vol 6 (4) ◽  
pp. 680-708 ◽  
Author(s):  
LLOYD HUMBERSTONE
Keyword(s):  
Propositional Logic ◽  
Consequence Relations ◽  
Classical Propositional Logic ◽  
Intuitionistic Propositional Logic ◽  
Sentential Context ◽  
Consequence Relation ◽  
Intermediate Logics ◽  
Conservative Operation ◽  
The One

AbstractA 1-ary sentential context is aggregative (according to a consequence relation) if the result of putting the conjunction of two formulas into the context is a consequence (by that relation) of the results of putting first the one formula and then the other into that context. All 1-ary contexts are aggregative according to the consequence relation of classical propositional logic (though not, for example, according to the consequence relation of intuitionistic propositional logic), and here we explore the extent of this phenomenon, generalized to having arbitrary connectives playing the role of conjunction; among intermediate logics, LC, shows itself to occupy a crucial position in this regard, and to suggest a characterization, applicable to a broader range of consequence relations, in terms of a variant of the notion of idempotence we shall call componentiality. This is an analogue, for the consequence relations of propositional logic, of the notion of a conservative operation in universal algebra.

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 A Weakly-Intuitionistic Logic I1

2015 ◽  
Vol 21 (2) ◽  
pp. 53-60 ◽  
Author(s):  
Я. Чючюра
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Classical Propositional Logic ◽  
Translation Function ◽  
Definition Of

In 1995, Sette and Carnielli presented a calculus, $I1$, which is intended to be dual to the paraconsistent calculus $P1$. The duality between $I1$ and $P1$ is reflected in the fact that both calculi are maximal with respect to classical propositional logic and they behave in a special, non-classical way, but only at the level of variables. Although some references are given in the text, the authors do not explicitly define what they mean by ‘duality’ between the calculi. For instance, no definition of the translation function from the language of $I1$ into the language of $P1$ (or from $P1$ to $I1$) was provided (see [4], pp. 88–90) nor was it shown that the calculi were functionally equivalent (see [13], pp. 260–261). The purpose of this paper is to present a new axiomatization of $I1$ and briefly discuss some results concerning the issue of duality between the calculi.

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 Control effects as a modality

2009 ◽  
Vol 19 (1) ◽  
pp. 17-26 ◽  
Author(s):  
HAYO THIELECKE
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
The Other ◽  
Classical Propositional Logic ◽  
Double Negation ◽  
Other Hand

AbstractWe combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.

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