scholarly journals On the complexity of propositional quantification in intuitionistic logic

1997 ◽  
Vol 62 (2) ◽  
pp. 529-544 ◽  
Author(s):  
Philip Kremer
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Natural Extension ◽  
Second Order ◽  
Modal Systems ◽  
Propositional Quantification

AbstractWe define a propositionally quantified intuitionistic logic Hπ+ by a natural extension of Kripke's semantics for propositional intuitionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π+, S4π+, S4.2π+, K4π+, Tπ+, Kπ+ and Bπ+, studied by Fine.

On storage operators

1998 ◽  
Author(s):  
Karim Nour
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Input Data ◽  
Type System ◽  
Second Order ◽  
Data Type ◽  
Simple Type ◽  
Output Data ◽  
Major Drawback ◽  
Proof Rules

λ-calculus as such is not a computational model. A reduction strategy is needed. In this paper, we consider λ-calculus with the left reduction. This strategy has many advantages: it always terminates when applied to a normalizable λ-term and it seems more economic since we compute λ-term only when we need it. But the major drawback of this strategy is that a function must compute its argument every time it uses it. This is the reason why this strategy is not really used. In 1990 Krivine (1990b) introduced the notion of storage operators in order to avoid this problem and to simulate call-by-value when necessary. The AF2 type system is a way of interpreting the proof rules for second-order intuitionistic logic plus equational reasoning as construction rules for terms. Krivine (1990b) has shown that, by using Gödel translation from classical to intuitionistic logic (denoted byg), we can find in system AF2 a very simple type for storage operators. Historically the type was discovered before the notion of storage operator itself. Krivine (1990a) proved that as far as totality of functions is concerned second-order classical logic is conservative over second-order intuitionistic logic. To prove this, Krivine introduced the following notions: A[x] is an input (resp. output) data type if one can prove intuitionistically A[x] → Ag[x] (resp. Ag[x] → ⇁⇁A[x]). Then if A[x] is an input data type and B[x] is an output data type, then if one can prove A[x] → B[x] classically one can prove it intuitionistically. The notion of storage operator was discovered by investigating the property of all λ-terms of type Ng[x] → ⇁⇁N[x] where N[x] is the type of integers. Parigot (1992) and Krivine (1994) have extended the AF2 system to classical logic. The method of Krivine is very simple: it consists of adding a new constant, denoted by C, with the declaration С: ∀X{⇁⇁ X → X} which axiomatizes classical logic over intuitionistic logic. For the constant C, he adds a new reduction rule which is a particular case of a rule given by Felleisen (1987) for control operator.

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.

The undecidability of second order linear logic without exponentials

1996 ◽  
Vol 61 (2) ◽  
pp. 541-548 ◽  
Author(s):  
Yves Lafont
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Logic ◽  
Classical Case ◽  
Second Order ◽  
Order Linear ◽  
Phase Semantics ◽  
Counter Machines ◽  
Intuitionistic Linear Logic

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

scholarly journals On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im
Keyword(s):  
Programming Languages ◽  
Intuitionistic Logic ◽  
Reference Point ◽  
Classical Logic ◽  
Proof System ◽  
Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

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.

An embedding of classical logic in S4

1970 ◽  
Vol 35 (4) ◽  
pp. 529-534 ◽  
Author(s):  
Melvin Fitting
Keyword(s):  
Intuitionistic Logic ◽  
Model Theory ◽  
Classical Logic ◽  
First Order ◽  
Barcan Formula ◽  
Complete Sequences

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].

On epistemic and ontological interpretations of intuitionistic and paraconsistent paradigms

2020 ◽  
Author(s):  
Walter Carnielli ◽  
Abilio Rodrigues
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Point Of View ◽  
Constructive Proof ◽  
Technical Point ◽  
Preservation Of Evidence ◽  
Epistemic Approach ◽  
Epistemic Interpretation ◽  
Excluded Middle

Abstract From the technical point of view, philosophically neutral, the duality between a paraconsistent and a paracomplete logic (for example intuitionistic logic) lies in the fact that explosion does not hold in the former and excluded middle does not hold in the latter. From the point of view of the motivations for rejecting explosion and excluded middle, this duality can be interpreted either ontologically or epistemically. An ontological interpretation of intuitionistic logic is Brouwer’s idealism; of paraconsistency is dialetheism. The epistemic interpretation of intuitionistic logic is in terms of preservation of constructive proof; of paraconsistency is in terms of preservation of evidence. In this paper, we explain and defend the epistemic approach to paraconsistency. We argue that it is more plausible than dialetheism and allows a peaceful and fruitful coexistence with classical logic.

On the intuitionistic strength of monotone inductive definitions

2004 ◽  
Vol 69 (3) ◽  
pp. 790-798 ◽  
Author(s):  
Sergei Tupailo
Keyword(s):  
Classical Logic ◽  
Second Order ◽  
Double Negation ◽  
Inductive Definitions ◽  
Intuitionistic Theory

Abstract.We prove here that the intuitionistic theory T0↾ + UMIDN. or even EETJ↾ + UMIDN, of Explicit Mathematics has the strength of –CA0. In Section 1 we give a double-negation translation for the classical second-order μ-calculus, which was shown in [Mö02] to have the strength of –CA0. In Section 2 we interpret the intuitionistic μ-calculus in the theory EETJ↾ + UMIDN. The question about the strength of monotone inductive definitions in T0 was asked by S. Feferman in 1982, and — assuming classical logic — was addressed by M. Rathjen.

Sign in / Sign up

Export Citation Format

Share Document