Recent zbMATH articles in MSC 03B20https://www.zbmath.org/atom/cc/03B202021-04-16T16:22:00+00:00WerkzeugThe stories of logics.https://www.zbmath.org/1456.030122021-04-16T16:22:00+00:00"Kapsner, Andreas"https://www.zbmath.org/authors/?q=ai:kapsner.andreasSummary: In this paper, I investigate in how far we can use fictional stories to learn about logic. How can we engage with fiction in order to come to find out what logical principles are actually valid? Is that possible at all? I claim that it is, and I propose two case studies to make the point.Stable formulas in intuitionistic logic.https://www.zbmath.org/1456.030522021-04-16T16:22:00+00:00"Bezhanishvili, Nick"https://www.zbmath.org/authors/?q=ai:bezhanishvili.nick"de Jongh, Dick"https://www.zbmath.org/authors/?q=ai:de-jongh.dick-h-jSummary: \textit{A. Visser} et al. [``NNIL, a study in intuitionistic propositional logic'', in: Modal logics and process algebra: a bisimulation perspective. 289--326 (1994)] introduced NNIL-formulas, showing that these are (up to provable equivalence) exactly the formulas preserved under taking submodels of Kripke models. In this article we show that NNIL-formulas are up to frame equivalence the formulas preserved under taking subframes of (descriptive and Kripke) frames, that NNIL-formulas are subframe formulas, and that subframe logics can be axiomatized by NNIL-formulas. We also define a new syntactic class of ONNILLI-formulas. We show that these are (up to frame equivalence) the formulas preserved in monotonic images of (descriptive and Kripke) frames and that ONNILLI-formulas are stable formulas as introduced by \textit{G. Bezhanishvili} and \textit{N. Bezhanishvili} [Rev. Symb. Log. 5, No. 4, 731--762 (2012; Zbl 1314.03020)]. Thus, ONNILLI is a syntactically defined set of formulas axiomatizing all stable logics. This resolves a problem left open in 2013.A linear/producer/consumer model of classical linear logic.https://www.zbmath.org/1456.031042021-04-16T16:22:00+00:00"Paykin, Jennifer"https://www.zbmath.org/authors/?q=ai:paykin.jennifer"Zdancewic, Steve"https://www.zbmath.org/authors/?q=ai:zdancewic.steveSummary: This paper defines a new proof- and category-theoretic framework for \textit{classical linear logic} that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the LPC structure. The paper's meta-theoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model.On displaying negative modalities.https://www.zbmath.org/1456.030362021-04-16T16:22:00+00:00"Drobyshevich, Sergey"https://www.zbmath.org/authors/?q=ai:drobyshevich.sergei-andreevichSummary: We extend \textit{T. Onishi}'s result [Australas. J. Log. 12, No. 4, 177--203 (2015; Zbl 1330.03053)] on displaying substructural negations by formulating display calculi for non-normal versions of impossibility and unnecessity operators, called \textit{regular} and \textit{co-regular negations}, respectively, by \textit{D. Vakarelov} [in: Paraconsistent logic. Essays on the inconsistent. München etc.: Philosophia Verlag. 328--363 (1989; Zbl 0692.03016)]. We make a number of connections between Onishi's work [loc. cit.] and Vakarelov's study [loc. cit.] of negation. We also prove a decidability result for our display calculus, which can be naturally extended to obtain decidability results for a large number of display calculi for logics with negative modal operators.Mackey-complete spaces and power series -- a topological model of differential linear logic.https://www.zbmath.org/1456.031002021-04-16T16:22:00+00:00"Kerjean, Marie"https://www.zbmath.org/authors/?q=ai:kerjean.marie"Tasson, Christine"https://www.zbmath.org/authors/?q=ai:tasson.christineSummary: In this paper, we describe a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted as bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we use a notion of power series between Mackey-complete spaces, generalizing entire functions in \(\mathbb{C}\). Finally, we get a quantitative model of Intuitionist Differential Linear Logic, with usual syntactic differentiation and where interpretations of proofs decompose as a Taylor expansion.On the unification of classical, intuitionistic and affine logics.https://www.zbmath.org/1456.031012021-04-16T16:22:00+00:00"Liang, Chuck"https://www.zbmath.org/authors/?q=ai:liang.chuckSummary: This article presents a \textit{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 \(\lambda\mu\) calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.Relating sequent calculi for bi-intuitionistic propositional logic.https://www.zbmath.org/1456.030222021-04-16T16:22:00+00:00"Pinto, Luís"https://www.zbmath.org/authors/?q=ai:pinto.luis-f"Uustalu, Tarmo"https://www.zbmath.org/authors/?q=ai:uustalu.tarmoSummary: Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic.
In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-left inferences to be single-conclusion resp. single-assumption and is incomplete without the cut rule, (2) the calculus with nested sequents by \textit{R. Goré} et al. [in: Advances in modal logic. Vol. 7. Proceedings of the 7th conference (AiML 2008), Nancy, France, September 9--12, 2008. London: College Publications. 43--66 (2008; Zbl 1244.03157)], where a complete class of cuts is encapsulated into special ``unnest'' rules and (3) a cut-free labelled sequent calculus derived from the Kripke semantics of the logic. We show that these calculi can be translated into each other and discuss the ineliminable cuts of the standard-style sequent calculus.
For the entire collection see [Zbl 1391.03011].On various negative translations.https://www.zbmath.org/1456.030892021-04-16T16:22:00+00:00"Ferreira, Gilda"https://www.zbmath.org/authors/?q=ai:ferreira.gilda"Oliva, Paulo"https://www.zbmath.org/authors/?q=ai:oliva.pauloSummary: Several proof translations of classical mathematics into intuitionistic mathematics have been proposed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Among those, the most commonly cited are translations due to Kolmogorov, Gödel, Gentzen, Kuroda and Krivine (in chronological order). In this paper we propose a framework for explaining how these different translations are related to each other. More precisely, we define a notion of a (modular) simplification starting from Kolmogorov translation, which leads to a partial order between different negative translations. In this derived ordering, Kuroda and Krivine are minimal elements. Two new minimal translations are introduced, with Godel and Gentzen translations sitting in between Kolmogorov and one of these new translations.
For the entire collection see [Zbl 1391.03011].Syllogistic logic with ``most''.https://www.zbmath.org/1456.030212021-04-16T16:22:00+00:00"Endrullis, Jörg"https://www.zbmath.org/authors/?q=ai:endrullis.jorg"Moss, Lawrence S."https://www.zbmath.org/authors/?q=ai:moss.lawrence-sSummary: We add \textsf{Most} \(X\) are \(Y\) to the syllogistic logic of \textsf{All} \(X\) are \(Y\) and \textsf{Some} \(X\) are \(Y\). We prove soundness, completeness, and decidability in polynomial time. Our logic has infinitely many rules, and we prove that this is unavoidable.