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

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im

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.

2009 ◽  
Vol 19 (1) ◽  
pp. 17-26 ◽  
Author(s):  
HAYO THIELECKE

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.


2000 ◽  
Vol 65 (2) ◽  
pp. 788-802 ◽  
Author(s):  
A. Avron

AbstractWe describe a method for obtaining classical logic from intuitionistic logic which does not depend on any proof system, and show that by applying it to the most important implicational relevance logics we get relevance logics with nice semantical and proof-theoretical properties. Semantically all these logics are sound and strongly complete relative to classes of structures in which all elements except one are designated. Proof-theoretically they correspond to cut-free hypersequential Gentzen-type calculi. Another major property of all these logics is that the classical implication can faithfully be translated into them.


2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka

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.


2021 ◽  
pp. 103-106
Author(s):  
Stephen Read

This chapter is a short note, co-written with Stephen Read, reacting to Hilary Putnam’s observation in his ‘Vagueness and Alternative Logic’ that intuitionistic logic would block the transition from the negation of the usual universally quantified conditional form of major premise for a Sorites to the assertion of a sharp boundary to the target predicate in the series concerned, and would thus allow the paradox to be reconceived as a straightforward reductio of its major premise. It is pointed out that a Sorites need not employ that form of major premise but can instead proceed, in intuitionistic logic, from the negation of the existential claim that the series in question contains a sharp boundary and that, while an intuitionistically suspect double negation elimination step would still be needed to enforce the unpalatable conclusion that the predicate in question indeed has a sharp boundary, nothing like the semantic motivation that the Intuitionists have favoured in mathematics for a restriction on double negation elimination can be operative in this context.


Author(s):  
G.M. Bierman

Linear logic was introduced by Jean-Yves Girard in 1987. Like classical logic it satisfies the law of the excluded middle and the principle of double negation, but, unlike classical logic, it has non-degenerate models. Models of logics are often given only at the level of provability, in that they provide denotations of formulas. However, we are also interested in models which provide denotations of deductions, or proofs. Given such a model two proofs are said to be equivalent if their denotations are equal. A model is said to be ‘degenerate’ if there are no formulas for which there exist at least two non-equivalent proofs. It is easy to see that models of classical logic are essentially degenerate because any formula is either true or false and so all proofs of a formula are considered equivalent. The intuitionist approach to this problem involves altering the meaning of the logical connectives but linear logic attacks the very connectives themselves, replacing them with more refined ones. Despite this there are simple translations between classical and linear logic. One can see the need for such a refinement in another way. Both classical and intuitionistic logics could be said to deal with static truths; both validate the rule of modus ponens: if A→B and A, then B; but both also validate the rule if A→B and A, then A∧B. In mathematics this is correct since a proposition, once verified, remains true – it persists. Many situations do not reflect such persistence but rather have an additional notion of causality. An implication A→B should reflect that a state B is accessible from a state A and, moreover, that state A is no longer available once the transition has been made. An example of this phenomenon is in chemistry where an implication A→B represents a reaction of components A to yield B. Thus if two hydrogen and one oxygen atoms bond to form a water molecule, they are consumed in the process and are no longer part of the current state. Linear logic provides logical connectives to describe such refined interpretations.


1970 ◽  
Vol 35 (4) ◽  
pp. 529-534 ◽  
Author(s):  
Melvin Fitting

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


Author(s):  
Walter Carnielli ◽  
Abilio Rodrigues

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.


2004 ◽  
Vol 69 (3) ◽  
pp. 790-798 ◽  
Author(s):  
Sergei Tupailo

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.


Studia Logica ◽  
2005 ◽  
Vol 80 (1) ◽  
pp. 95-104
Author(s):  
Witold A. Pogorzelski ◽  
Piotr Wojtylak
Keyword(s):  

Author(s):  
Peter Pagin

The law of excluded middle (LEM) says that every sentence of the form A∨¬A (‘A or not A’) is logically true. This law is accepted in classical logic, but not in intuitionistic logic. The reason for this difference over logical validity is a deeper difference about truth and meaning. In classical logic, the meanings of the logical connectives are explained by means of the truth tables, and these explanations justify LEM. However, the truth table explanations involve acceptance of the principle of bivalence, that is, the principle that every sentence is either true or false. The intuitionist does not accept bivalence, at least not in mathematics. The reason is the view that mathematical sentences are made true and false by proofs which mathematicians construct. On this view, bivalence can be assumed only if we have a guarantee that for each mathematical sentence, either there is a proof of the truth of the sentence, or a proof of its falsity. But we have no such guarantee. Therefore bivalence is not intuitionistically acceptable, and then neither is LEM. A realist about mathematics thinks that if a mathematical sentence is true, then it is rendered true by the obtaining of some particular state of affairs, whether or not we can know about it, and if that state of affairs does not obtain, then the sentence is false. The realist further thinks that mathematical reality is fully determinate, in that every mathematical state of affairs determinately either obtains or does not obtain. As a result, the principle of bivalence is taken to hold for mathematical sentences. The intuitionist is usually an antirealist about mathematics, rejecting the idea of a fully determinate, mind-independent mathematical reality. The intuitionist’s view about the truth-conditions of mathematical sentences is not obviously incompatible with realism about mathematical states of affairs. According to Michael Dummett, however, the view about truth-conditions implies antirealism. In Dummett’s view, a conflict over realism is fundamentally a conflict about what makes sentences true, and therefore about semantics, for there is no further question about, for example, the existence of a mathematical reality than as a truth ground for mathematical sentences. In this vein Dummett has proposed to take acceptance of bivalence as actually defining a realist position. If this is right, then both the choice between classical and intuitionistic logic and questions of realism are fundamentally questions of semantics, for whether or not bivalence holds depends on the proper semantics. The question of the proper semantics, in turn, belongs to the theory of meaning. Within the theory of meaning Dummett has laid down general principles, from which he argues that meaning cannot in general consist in bivalent truth-conditions. The principles concern the need for, and the possibility of, manifesting one’s knowledge of meaning to other speakers, and the nature of such manifestations. If Dummett’s argument is sound, then bivalence cannot be justified directly from semantics, and may not be justifiable at all.


Sign in / Sign up

Export Citation Format

Share Document