A bilateral Hilbert-style investigation of 2-intuitionistic logic

2019 ◽  
Vol 29 (5) ◽  
pp. 665-692
Author(s):  
Sergey Drobyshevich
Keyword(s):  
Intuitionistic Logic ◽  
Primitive Notion ◽  
Signed Formulas ◽  
Intuitionistic Logics

Abstract We develop a bilateral Hilbert-style calculus for 2-intuitionistic logic of Heinrich Wansing. This calculus is defined over signed formulas of two types: formulas signed with plus correspond to assertions, while formulas signed with minus correspond to rejections. In this way, the provided system is a Hilbert-style calculus, which does take rejection seriously by considering it a primitive notion on par with assertion. We show that this presentation is not trivial and provide two equivalent axiomatizations obtained by extending intuitionistic and dual intuitionistic logics, respectively. Finally, we show that 2-intuitionistic logic is in some sense definitionally equivalent to a variant of Nelson’s logic with constructible falsity.

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

Model existence theorems for modal and intuitionistic logics

1973 ◽  
Vol 38 (4) ◽  
pp. 613-627 ◽  
Author(s):  
Melvin Fitting
Keyword(s):  
Existence Theorem ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Existence Theorems ◽  
Compactness Theorem ◽  
Infinitary Logic ◽  
Consistency Property ◽  
Model Existence ◽  
Model Existence Theorem ◽  
Intuitionistic Logics

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it.In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.

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.

scholarly journals A Remark on Maksimova's Variable Separation Property in Super-Bi-Intuitionistic Logics

2017 ◽  
Vol 14 (1) ◽  
Author(s):  
Guillermo Badia
Keyword(s):  
Intuitionistic Logic ◽  
Separation Property ◽  
Algebraic Characterization ◽  
Variable Separation ◽  
Intuitionistic Logics

We provide a sucient frame-theoretic condition for a super bi-intuitionistic logic to have Maksimova's variable separation property. We conclude that bi-intuitionistic logic enjoys the property. Furthermore, we offer an algebraic characterization of the super-bi-intuitionistic logics with Maksimova's property.

A Passage Theory of Time

2018 ◽  
Author(s):  
Martin A. Lipman
Keyword(s):  
Necessary Conditions ◽  
Fragmented Structure ◽  
The World ◽  
Real Change ◽  
Primitive Notion

This paper proposes a theory of time that takes the notion of passage as its basic primitive. Any notion of passage that is worthy of that name should make for real change across time. It is argued that real change across time in turn requires the obtaining of incompatible facts. The proposed theory will therefore be a form of fragmentalism, which makes room for the obtaining of incompatible facts by taking the world to exhibit a type of fragmented structure. The preferred form of fragmentalism and the primitive notion of passage are elucidated in some detail. It is argued that the resulting picture resolves the problem of change and meets the puzzling yet necessary conditions for the reality of passage

Crime as Prime

2018 ◽  
Author(s):  
Richard Holton
Keyword(s):  
The State ◽  
Mens Rea ◽  
Attempted Murder ◽  
State Of Mind ◽  
Actus Reus ◽  
Mental Element ◽  
Primitive Notion

This paper develops an account of core criminal terms like ‘murder’ that parallels Williamson’s account of knowledge. It is argued that while murder requires that the murderer killed, and that they did so with a certain state of mind, murder cannot be regarded as the conjunction of these two elements (the action, the actus reus, and the associated mental element, the mens rea). Rather, murder should be seen as a primitive notion, which entails each of them. This explains some of the problems around criminal attempt. Attempted murder cannot be seen simply as involving the state of mind of murder minus success; rather, it has to be seen as a self-standing offence, that of attempting to commit the murder.

scholarly journals Filters and congruences in sectionally pseudocomplemented lattices and posets

2021 ◽  
Author(s):  
Ivan Chajda ◽  
Helmut Länger
Keyword(s):  
Algebraic Semantics ◽  
Basic Properties ◽  
Algebraic Constructions ◽  
Pseudocomplemented Lattices ◽  
Intuitionistic Logics

AbstractTogether with J. Paseka we introduced so-called sectionally pseudocomplemented lattices and posets and illuminated their role in algebraic constructions. We believe that—similar to relatively pseudocomplemented lattices—these structures can serve as an algebraic semantics of certain intuitionistic logics. The aim of the present paper is to define congruences and filters in these structures, derive mutual relationships between them and describe basic properties of congruences in strongly sectionally pseudocomplemented posets. For the description of filters in both sectionally pseudocomplemented lattices and posets, we use the tools introduced by A. Ursini, i.e., ideal terms and the closedness with respect to them. It seems to be of some interest that a similar machinery can be applied also for strongly sectionally pseudocomplemented posets in spite of the fact that the corresponding ideal terms are not everywhere defined.

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.

Sign in / Sign up

Export Citation Format

Share Document