Filters and congruences in sectionally pseudocomplemented lattices and posets

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

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

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.

A bilateral Hilbert-style investigation of 2-intuitionistic logic

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.

On the unification of classical, intuitionistic and affine 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.

Linear logic

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.

A Remark on Maksimova's Variable Separation Property in Super-Bi-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.