Intuitionistic logic freed of all metarules

2007 ◽  
Vol 72 (4) ◽  
pp. 1204-1218 ◽  
Author(s):  
Giovanna Corsi ◽  
Gabriele Tassi
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Proof Search ◽  
Subformula Property

AbstractIn this paper we present two calculi for intuitionistic logic. The first one. IG, is characterized by the fact that every proof-search terminates and termination is reached without jeopardizing the subformula property. As to the second one, SIC, proof-search terminates, the subformula property is preserved and moreover proof-search is performed without any recourse to metarules, in particular there is no need to back-track. As a consequence, proof-search in the calculus SIC is accomplished by a single tree as in classical logic.

scholarly journals Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus

2008 ◽  
Vol 48 ◽  
Author(s):  
Romas Alonderis
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Proof Search

In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.

scholarly journals Dialogues for proof search

10.29007/5t86 ◽  
2018 ◽  
Author(s):  
Jesse Alama
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Dialogue Games ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

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.

scholarly journals Deep Proof Search in MELL

10.29007/p1fd ◽  
2018 ◽  
Author(s):  
Ozan Kahramanogullari
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Proof Search ◽  
Proof Construction ◽  
Deep Inference ◽  
Speed Up

The deep inference presentation of multiplicative exponential linear logic (MELL) benefits from a rich combinatoric analysis with many more proofs in comparison to its sequent calculus presentation. In the deep inference setting, all the sequent calculus proofs are preserved. Moreover, many other proofs become available, and some of these proofs are much shorter. However, proof search in deep inference is subject to a greater nondeterminism, and this nondeterminism constitutes a bottleneck for applications. To this end, we address the problem of reducing nondeterminism in MELL by refining and extending our technique that has been previously applied to multiplicative linear logic and classical logic. We show that, besides the nondeterminism in commutative contexts, the nondeterminism in exponential contexts can be reduced in a proof theoretically clean manner. The method conserves the exponential speed-up in proof construction due to deep inference, exemplified by Statman tautologies. We validate the improvement in accessing the shorter proofs by experiments with our implementations.

Sign in / Sign up

Export Citation Format

Share Document