Recent zbMATH articles in MSC 03Bhttps://www.zbmath.org/atom/cc/03B2021-04-16T16:22:00+00:00WerkzeugRelating 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].Natural deduction for Post's logics and their duals.https://www.zbmath.org/1456.030472021-04-16T16:22:00+00:00"Petrukhin, Yaroslav"https://www.zbmath.org/authors/?q=ai:petrukhin.yaroslav-igorevichSummary: In this paper, we introduce the notion of dual Post's negation and an infinite class of Dual Post's finitely-valued logics which differ from Post's ones with respect to the definitions of negation and the sets of designated truth values. We present adequate natural deduction systems for all Post's \(k\)-valued \((k\geqslant 3)\) logics as well as for all Dual Post's \(k\)-valued logics.Another plan for negation.https://www.zbmath.org/1456.030492021-04-16T16:22:00+00:00"Francez, Nissim"https://www.zbmath.org/authors/?q=ai:francez.nissimSummary: The paper presents a plan for negation, proposing a paradigm shift from the Australian plan for negation, leading to a family of contra-classical logics. The two main ideas are the following:
\begin{itemize}
\item[1.] Instead of shifting points of evaluation (in a frame), shift the evaluated formula.
\item[2.] Introduce an incompatibility set for every atomic formula, extended to any compound formula, and impose the condition on valuations that a formula evaluates to true iff all the formulas in its incompatibility set evaluate to false. Thus, atomic sentences are not independent in their truth-values.
\item[3.] The resulting negation, in addition to excluding the negated formula, provides a positive alternative
\item[4.] to the negated formula.
\end{itemize}
I also present a sound and complete natural deduction proof systems for those logics. In addition, the kind of negation considered in this paper is shown to provide an innovative notion of grounding negation.The 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.Boulesic-doxastic logic.https://www.zbmath.org/1456.030322021-04-16T16:22:00+00:00"Rönnedal, Daniel"https://www.zbmath.org/authors/?q=ai:ronnedal.danielSummary: In this paper, I will develop a set of boulesic-doxastic tableau systems and prove that they are sound and complete. Boulesic-doxastic logic consists of two main parts: a boulesic part and a doxastic part. By `boulesic logic' I mean `the logic of the will', and by `doxastic logic' I mean `the logic of belief'. The first part deals with `boulesic' concepts, expressions, sentences,
arguments and theorems. I will concentrate on two types of boulesic expression: 'individual \(x\)
wants it to be the case that' and `individual \(x\) accepts that it is the case that'. The second part deals with `doxastic' concepts, expressions, sentences, arguments and theorems. I will concentrate on two types of doxastic expression: `individual \(x\) believes that' and `it is imaginable to individual \(x\) that'. Boulesic-doxastic logic investigates how these concepts are related to each other. Boulesic logic is a new kind of logic. Doxastic logic has been around for a while, but the approach to this branch of logic in this paper is new. Each system is combined with modal logic with two kinds of modal operators for historical and absolute necessity and predicate logic with necessary identity and `possibilist' quantifiers. I use a kind of possible world semantics to describe the systems semantically. I also sketch out how our basic language can be extended with propositional quantifiers. All the systems developed in this paper are new.Comparing some substructural strategies dealing with vagueness.https://www.zbmath.org/1456.030082021-04-16T16:22:00+00:00"Cobreros, Pablo"https://www.zbmath.org/authors/?q=ai:cobreros.pablo"Egré, Paul"https://www.zbmath.org/authors/?q=ai:egre.paul"Ripley, David"https://www.zbmath.org/authors/?q=ai:ripley.david"van Rooij, Robert"https://www.zbmath.org/authors/?q=ai:van-rooy.robertSummary: It is well-known that in combination with further premises that look less controversial, the tolerance principle -- the constraint that if \(Pa\) holds, and \(a\) and \(b\) are similar in \(P\)-relevant respects, \(Pb\) holds as well -- leads to contradiction, namely to the sorites paradox. According to many influential views of the sorites paradox (e.g. Williamson 1994), we therefore ought to reject the principle of tolerance as unsound.
For the entire collection see [Zbl 1385.68004].Logic, reasoning, argumentation: insights from the wild.https://www.zbmath.org/1456.030192021-04-16T16:22:00+00:00"Zenker, Frank"https://www.zbmath.org/authors/?q=ai:zenker.frankSummary: This article provides a brief selective overview and discussion of recent research into natural language argumentation that may inform the study of human reasoning on the assumption that an episode of argumentation issues an invitation to accept a corresponding inference. As this research shows, arguers typically seek to establish new consequences based on prior information. And they typically do so vis-à-vis a real or an imagined opponent, or an opponent-position, in ways that remain sensitive to considerations of context, audiences, and goals. Deductively valid inferences remain a limiting case of such reasoning. In view of these insights, it may appear less surprising that allegedly ``irrational'' behavior can regularly be produced in experimental settings that expose subjects to standardized reasoning tasks.Relevant implication and ordered geometry.https://www.zbmath.org/1456.030422021-04-16T16:22:00+00:00"Urquhart, Alasdair"https://www.zbmath.org/authors/?q=ai:urquhart.alasdairSummary: This paper shows that model structures for \(\mathbf{R}^+\), the system of positive
relevant implication, can be constructed from ordered geometries. This extends earlier results building such model structures from projective spaces. A final section shows how such models can be extended to models for the full system \(\mathbf{R}\).A non-transitive relevant implication corresponding to classical logic consequence.https://www.zbmath.org/1456.030432021-04-16T16:22:00+00:00"Verdée, Petr"https://www.zbmath.org/authors/?q=ai:verdee.petr"De Bal, Inge"https://www.zbmath.org/authors/?q=ai:de-bal.inge"Samonek, Aleksandra"https://www.zbmath.org/authors/?q=ai:samonek.aleksandraSummary: In this paper we first develop a logic independent account of relevant implication. We propose a stipulative de nition of what it means for a multiset of premises to relevantly \textbf{L}-imply a multiset of conclusions, where \textbf{L} is a Tarskian consequence relation: the premises relevantly imply the conclusions iff there is an abstraction of the pair \(\langle\mathrm{premises}, \mathrm{conclusions}\rangle\) such that the abstracted premises \textbf{L}-imply the abstracted conclusions and none of the abstracted premises or the abstracted conclusions can be omitted while still maintaining valid \textbf{L}-consequence.
Subsequently we apply this de nition to the classical logic (\textbf{CL}) consequence relation to obtain \textbf{NTR}-consequence, i.e., the relevant \textbf{CL}-consequence relation in our sense, and develop a sequent calculus that is sound and complete w.r.t. relevant \textbf{CL}-consequence. We
present a sound and complete sequent calculus for \textbf{NTR}. In a next step we add rules for an object language relevant implication to the sequent calculus. The object language implication reflects exactly the \textbf{NTR}-consequence relation. One can see the resulting logic \textbf{NTR}\(^\to\)
as a relevant logic in the traditional sense of the word.
By means of a translation to the relevant logic \textbf{R}, we show that the presented logic \textbf{NTR} is very close to relevance logics in the Anderson-Belnap-Dunn-Routley-Meyer tradition. However, unlike usual relevant logics, \textbf{NTR} is decidable for the full language, disjunctive syllogism (\(A\) and \(\neg A\vee B\) relevantly imply \(B\)) and adjunction (\(A\) and \(B\) relevantly imply \(A\wedge B\)) are valid, and neither Modus Ponens nor the cut rule are admissible.Incompactness of the \(\forall_1\) fragment of basic second order propositional relevant logic.https://www.zbmath.org/1456.030392021-04-16T16:22:00+00:00"Badia, Guillermo"https://www.zbmath.org/authors/?q=ai:badia.guillermoSummary: In this note we provide a simple proof of the incompactness over Routley-Meyer
\textbf{B}-frames of the \(\forall_1\) fragment of the second order propositional relevant language. Moreover, we observe that this fragment is clearly still recursively enumerable.Logical theory choice.https://www.zbmath.org/1456.030152021-04-16T16:22:00+00:00"Priest, Graham"https://www.zbmath.org/authors/?q=ai:priest.grahamSummary: There is at present a certain dispute about counterfactuals taking place. What is at issue is whether counterfactuals with necessarily false antecedents are all true. Some hold that such counterfactuals are vacuously true, appearances notwithstanding. Let us call such people vacuists. Others hold that some counterfactuals with necessarily false antecedents are true; some are false: it just depends on their contents. Let us call such people non-vacuists. As a notable representative of the vacuists, I will take Tim Williamson. On the other side, I will take the position defended by Berto, French, Priest, and Ripley. I will argue (unsurprisingly) that the better choice is non-vacuism. That, however, is a subsidiary aim of this paper. The main point is to illustrate the method of theory-choice.Berry's paradox\dots again.https://www.zbmath.org/1456.030142021-04-16T16:22:00+00:00"Priest, Graham"https://www.zbmath.org/authors/?q=ai:priest.grahamSummary: The paper is a discussion of whether Berry's pardox presupposes the principle of excluded middle, with particular reference to the work of Ross Brady.Reconfiguration over tree decompositions.https://www.zbmath.org/1456.681322021-04-16T16:22:00+00:00"Mouawad, Amer E."https://www.zbmath.org/authors/?q=ai:mouawad.amer-e"Nishimura, Naomi"https://www.zbmath.org/authors/?q=ai:nishimura.naomi"Raman, Venkatesh"https://www.zbmath.org/authors/?q=ai:raman.venkatesh"Wrochna, Marcin"https://www.zbmath.org/authors/?q=ai:wrochna.marcinSummary: A vertex-subset graph problem \(Q\) defines which subsets of the vertices of an input graph are feasible solutions. The reconfiguration version of a vertex-subset problem \(Q\) asks whether it is possible to transform one feasible solution for \(Q\) into another in at most \(\ell\) steps, where each step is a vertex addition or deletion, and each intermediate set is also a feasible solution for \(Q\) of size bounded by \(k\). Motivated by recent results establishing W[1]-hardness of the reconfiguration versions of most vertex-subset problems parameterized by \(\ell\), we investigate the complexity of such problems restricted to graphs of bounded treewidth. We show that the reconfiguration versions of most vertex-subset problems remain PSPACE-complete on graphs of treewidth at most \(t\) but are fixed-parameter tractable parameterized by \(\ell + t\) for all vertex-subset problems definable in monadic second-order logic (MSOL). To prove the latter result, we
introduce a technique which allows us to circumvent cardinality constraints and define reconfiguration problems in MSOL.
For the entire collection see [Zbl 1318.68014].Point-free foundation of geometry looking at laboratory activities.https://www.zbmath.org/1456.510092021-04-16T16:22:00+00:00"Gerla, Giangiacomo"https://www.zbmath.org/authors/?q=ai:gerla.giangiacomo"Miranda, Annamaria"https://www.zbmath.org/authors/?q=ai:miranda.annamariaThe authors propose a point-free axiomatization of Euclidean geometry, in which the notions of convexity and half-planes, and with them the Boolean algebra of regular closed subsets, regions, and \(n\)-dimensional prototypes are crucial, with the aim of providing an intuitively convincing axiomatization that could be used in an educational setting.
Reviewer: Victor V. Pambuccian (Glendale)Classical realizability and arithmetical formulæ.https://www.zbmath.org/1456.030262021-04-16T16:22:00+00:00"Guillermo, Mauricio"https://www.zbmath.org/authors/?q=ai:guillermo.mauricio"Miquey, Ètienne"https://www.zbmath.org/authors/?q=ai:miquey.etienneSummary: In this paper, we treat the specification problem in Krivine classical realizability
[\textit{J.-L. Krivine}, Panor. Synth. 27, 197--229 (2009; Zbl 1206.03017)], in the case of arithmetical formulæ. In the continuity of previous works from
[the first author, Jeux de réalisabilité en arithmétique classique. Paris: Université Paris 7 (PhD thesis) (2008);
the first author and \textit{A. Miquel}, Math. Struct. Comput. Sci. 26, No. 7, 1269--1303 (2016; Zbl 1425.03009)], we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first sections, we recall the definition of classical realizability, as well as a few technical results. In Section 5, we introduce in more details the specification problem and the intuition of the game-theoretic point of view we adopt later. We first present a game \(\mathbb{G}^1\), that we prove to be adequate and complete if the language contains no instructions `\texttt{quote}'
[\textit{J.-L. Krivine}, Theor. Comput. Sci. 308, No. 1--3, 259--276 (2003; Zbl 1169.03328)], using interaction constants to do substitution over execution threads. We then show that as soon as the language contain `\texttt{quote}', the game is no more complete, and present a second game \(\mathbb{G}^2\) that is both adequate and complete in the general case. In the last Section, we draw attention to a model-theoretic point of view and use our specification result to show that arithmetical formulæ are absolute for realizability models.A note on the relevance of semilattice relevance logic.https://www.zbmath.org/1456.030442021-04-16T16:22:00+00:00"Weiss, Yale"https://www.zbmath.org/authors/?q=ai:weiss.yaleSummary: A propositional logic has the \textit{variable sharing property} if
\(\phi\to\psi\) is a theorem only if \(\phi\) and \(\psi\) share some propositional variable(s). In
this note, I prove that positive semilattice relevance logic \((\mathbf{R}_u^+)\) and its extension with an involution negation \((\mathbf{R}_u^\neg)\) have the variable sharing property (as these systems are not subsystems of \(\mathbf{R}\), these results are not automatically entailed by the fact that \(\mathbf{R}\) satisfies the variable sharing property). Typical proofs of the variable sharing property rely on ad hoc, if clever, matrices. However, in this note, I exploit the properties of rather more intuitive arithmetical structures to establish the variable sharing property for the systems discussed.Superdeduction in \(\bar{\lambda}\mu\tilde{\mu}\).https://www.zbmath.org/1456.030862021-04-16T16:22:00+00:00"Houtmann, Clément"https://www.zbmath.org/authors/?q=ai:houtmann.clementSummary: Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on \textit{C. Urban}'s work on classical sequent calculus [Classical logic and computation. Cambridge: University of Cambridge (PhD Thesis) (2000)]. However the computational content of Christian Urban's calculus is not directly related to the (\(\lambda\)-calculus based) Curry-Howard correspondence. In contrast the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus is a \(\lambda\)-calculus for classical sequent calculus. This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the \(\bar{\lambda}\mu\tilde{\mu}\)-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].A characterisation of some \(\mathbf{Z}\)-like logics.https://www.zbmath.org/1456.030512021-04-16T16:22:00+00:00"Mruczek-Nasieniewska, Krystyna"https://www.zbmath.org/authors/?q=ai:mruczek-nasieniewska.krystyna"Nasieniewski, Marek"https://www.zbmath.org/authors/?q=ai:nasieniewski.marekSummary: In
[\textit{J.-Y. Béziau}, Log. Log. Philos. 15, No. 2, 99--111 (2006; Zbl 1134.03018)] a logic \(\mathbf{Z}\) was defined with the help of the modal logic \(\mathbf{S5}\). In it, the negation operator is understood as meaning `it is not necessary that'. The strong soundness-completeness result for \(\mathbf{Z}\) with respect to a version of Kripke semantics was also given there. Following the formulation of \(\mathbf{Z}\) we can talk about \(\mathbf{Z}\)-\textit{like logics} or \textit{Beziau-style logics} if we consider other modal logics instead of \(\mathbf{S5}\) -- such a possibility has been mentioned in
[Béziau, loc. cit.]. The correspondence result between modal logics and respective Beziau-style logics has been generalised for the case of normal logics naturally leading to soundness-completeness results
(see [\textit{J. Marcos}, Log. Anal., Nouv. Sér. 48, No. 189--192, 279--300 (2005; Zbl 1084.03015); the authors, Bull. Sect. Log., Univ. Łódź, Dep. Log. 34, No. 4, 229--248 (2005; Zbl 1117.03036)]). In
[the authors, Bull. Sect. Log., Univ. Łódź, Dep. Log. 37, No. 3--4, 185--196 (2008; Zbl 1286.03103); Bull. Sect. Log., Univ. Łódź, Dep. Log. 38, No. 3--4, 189--203 (2009; Zbl 1286.03104)] some partial results for non-normal cases are given. In the present paper we try to give similar but more general correspondence results for the non-normal-worlds case. To achieve this aim we have to enrich original Beziau's language with an additional negation operator understood as `it is necessary that not'.Kreisel's interests. On the foundations of logic and mathematics. Contributions of the conference, Salzburg, Austria, August 13--14, 2018.https://www.zbmath.org/1456.030052021-04-16T16:22:00+00:00"Weingartner, Paul (ed.)"https://www.zbmath.org/authors/?q=ai:weingartner.paul"Leeb, Hans-Peter (ed.)"https://www.zbmath.org/authors/?q=ai:leeb.hans-peterPublisher's description: The contributions to this volume are from participants of the international conference Kreisel's Interests -- On the Foundations of Logic and Mathematics, which took place from 13 to 14 August 2018 at the University of Salzburg in Salzburg, Austria. The contributions have been revised and partially extended. Among the contributors are Akihiro Kanamori, Göran Sundholm, Ulrich Kohlenbach, Charles Parsons, Daniel Isaacson, and Kenneth Derus. The contributions cover the discussions between Kreisel and Wittgenstein on philosophy of mathematics, Kreisel's Dictum, proof theory, the discussions between Kreisel and Gödel on philosophy of mathematics, some biographical facts, and a collection of extracts from Kreisel's letters.
The articles of this volume will be reviewed individually.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.Natural models of homotopy type theory.https://www.zbmath.org/1456.030232021-04-16T16:22:00+00:00"Awodey, Steve"https://www.zbmath.org/authors/?q=ai:awodey.steveSummary: The notion of a \textit{natural model} of type theory is defined in terms of that of a \textit{representable natural transfomation} of presheaves. It is shown that such models agree exactly with the concept of a \textit{category with families} in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums \(\Sigma\), dependent products \(\Pi\) and intensional identity types , as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.Realizability in ordered combinatory algebras with adjunction.https://www.zbmath.org/1456.030252021-04-16T16:22:00+00:00"Ferrer Santos, Walter"https://www.zbmath.org/authors/?q=ai:ferrer-santos.walter-ricardo"Guillermo, Mauricio"https://www.zbmath.org/authors/?q=ai:guillermo.mauricio"Malherbe, Octavio"https://www.zbmath.org/authors/?q=ai:malherbe.octavioSummary: In this work, we continue our consideration of the constructions presented in the paper \textit{Krivine's Classical Realizability from a Categorical Perspective} by \textit{T. Streicher} [Math. Struct. Comput. Sci. 23, No. 6, 1234--1256 (2013; Zbl 1326.03083)]. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented, \textit{mutatis mutandis}, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.A generalized Blakers-Massey theorem.https://www.zbmath.org/1456.180172021-04-16T16:22:00+00:00"Anel, Mathieu"https://www.zbmath.org/authors/?q=ai:anel.mathieu"Biedermann, Georg"https://www.zbmath.org/authors/?q=ai:biedermann.georg"Finster, Eric"https://www.zbmath.org/authors/?q=ai:finster.eric"Joyal, André"https://www.zbmath.org/authors/?q=ai:joyal.andreThe classical \textit{Blakers-Massey theorem} [\textit{A. L. Blakers} and \textit{W. S. Massey}, Proc. Natl. Acad. Sci. USA 35, 322--328 (1949; Zbl 0040.25801); Ann. Math. (2) 53, 161--205 (1951; Zbl 0042.17301); Ann. Math. (2) 55, 192--201 (1952; Zbl 0046.40604); Ann. Math. (2) 58, 409--417 (1953; Zbl 0053.12901)], aka the \textit{homotopy excision theorem}, is one of the most fundamental facts in homotopy theory, claiming that, given a homotopy pushout diagram of spaces
\[
\begin{array} [c]{ccc} A & \begin{array} [c]{c} g\\
\rightarrow\\
\end{array} & C\\
\begin{array} [c]{cc} f & \downarrow \end{array} & _{\lrcorner} & \downarrow\\
B & \rightarrow & D \end{array}
\]
such that the map \(f\)\ is \(m\)-connected and the map \(g\)\ is \(n\)-connected, the canonical map \(A\rightarrow B\times_{D}C\)\ to the homotopy pullback is in fact \(\left( m+n\right) \)-connected, giving rise to the \textit{Freudenthal suspension theorem} [\textit{H. Freudenthal}, Compos. Math. 5, 299--314 (1937; Zbl 0018.17705)] and therefore paving the way to \textit{stable homotopy theory}.
A new proof of this theorem [\textit{K.-B. Hou (Favonia)} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 565--574 (2016; Zbl 1395.55011)] was found in the context of \textit{homotopy type theory} providing an elementary axiomatization of homotopy-theoretic reasoning [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)], which is generally thought to serve as an internal language for the \(\infty\)-topoi as developed by Rezk [\url{https://faculty.math.illinois.edu/\symbol{126}rezk/homotopy-topos-sketch.pdf}] and [\textit{J. Lurie}, Higher topos theory. Princeton, NJ: Princeton University Press (2009; Zbl 1175.18001)]. The original proof in [\textit{K.-B. Hou (Favonia)} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 565--574 (2016; Zbl 1395.55011)] was translated into the language of higher category theory by Rezk [\url{https://faculty.math.illinois.edu/\symbol{126} rezk/freudenthal-and-blakers-massey.pdf}]. The main result of this paper is a much generalized theorem, applying not only to spaces, but to an arbitrary \(\infty\)-topos. Indeed, as was shown in [\textit{M. Anel} et al., J. Topol. 11, No. 4, 1100--1132 (2018; Zbl 1423.18009)], the generalized theorem is to be applied to an appropriate presheaf topos, yielding an analogue of the Blakers-Massey theorem in the context of Goodwille's calculus of functors.
The authors observe that the \(n\)-connected maps form the left class of a \textit{factorization system} \(\left( \mathfrak{L},\mathfrak{R}\right) \)\ on the category of spaces with the additional property that the left class \(\mathfrak{L}\) is stable under base change, referring to a factorization system obedient to this condition as a \textit{modality}. The main result of this paper goes as follows.
Theorem. Let \(\mathcal{E}\)\ be an \(\infty\)-topos and \(\left( \mathfrak{L} ,\mathfrak{R}\right) \) a modality on \(\mathcal{E}\). Write \(\Delta h:A\rightarrow A\times_{B}A\) for the diagonal of a map \(h:A\rightarrow B\in\mathcal{E}\) and \(-\square_{Z}-\)\ for the pushout product in the slice category \(\mathcal{E}_{/Z}\). Given a pushout square
\[
\begin{array} [c]{ccc} Z & \begin{array} [c]{c} g\\
\rightarrow\\
\end{array} & Y\\
\begin{array} [c]{cc} f & \downarrow \end{array} & _{\lrcorner} & \downarrow\\
X & \rightarrow & W \end{array}
\]
in \(\mathcal{E}\)\ with \(\Delta f\square_{Z}\Delta g\in\mathfrak{L}\), the canonical map \(\left( f,g\right) :Z\rightarrow X\times_{W}Y\) is also in \(\mathfrak{L}\).
A similar generalization of the Blakers-Massey theorem was obtained by \textit{W. Chachólski} et al. [Ann. Inst. Fourier 66, No. 6, 2641--2665 (2016; Zbl 1368.55006)], though their method involves the manipulation of \textit{weak cellular inequalities} of spaces, as introduced in [\textit{E. Dror Farjoun}, Cellular spaces, null spaces and homotopy localization. Berlin: Springer-Verlag (1995; Zbl 0842.55001)], whereas the authors focus on \(\infty \)-topos-theoretic tools such as descent.
A synopsis of the paper consisting of four sections goes as follows. \S 2 fixes higher-categorical conventions and recalls some elementary facts. \S 3 proceeds as follows.
\begin{itemize}
\item It begins by introducing the notion of a factorization system as well as the pushout product and pullback hom.
\item It then gives a short treatment of the \(n\)-connected/\(n\)-truncated factorization system in an \(\infty\)-topos.
\item It introduces the notion of a modality itself, providing a number of examples and deriving some elementary properties, including the dual Blakers-Massey theorem.
\item It concludes with the descent theorem for \(\mathfrak{L}\)-cartesian squares.
\end{itemize}
\S 4 turns to the proof of the generalized Blakers-Massey theorem itself, finishing with the derivation of the classical theorem as well as that of Chacholski-Scherner-Werndli.
Reviewer: Hirokazu Nishimura (Tsukuba)Logic script 2. Introduction to modal logic.https://www.zbmath.org/1456.030012021-04-16T16:22:00+00:00"Brendel, Elke"https://www.zbmath.org/authors/?q=ai:brendel.elkePublisher's description: Modal logic deals with inferences and arguments involving the notions of possibility and necessity. This introduction to the semantics and syntax of modal junction and quantifier logic explains the foundations of the theory of possible worlds and provides a calculus of natural reasoning for modal logic proof. It also discusses important philosophical applications of modal logic, as well as issues concerning the existence of possible, necessary, and fictional objects. The book lends itself to either self-study or as a textbook for a basic modal logic course in BA or MA philosophy courses. It is aimed primarily at those who already have an elementary knowledge of logic and wish to deepen it in an important area of philosophical logic.
For Vol. 1 see [Zbl 1376.03001].Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas.https://www.zbmath.org/1456.680242021-04-16T16:22:00+00:00"Ancona, Davide"https://www.zbmath.org/authors/?q=ai:ancona.davide"Lagorio, Giovanni"https://www.zbmath.org/authors/?q=ai:lagorio.giovanniSummary: In recent work we have shown how it is possible to define very precise type systems for object-oriented languages by abstractly compiling a program into a Horn formula \(f\). Then type inference amounts to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of \(f\).
Type systems defined in this way are idealized, since in the most interesting instantiations both the terms of the coinductive Herbrand universe and goal derivations cannot be finitely represented. However, sound and quite expressive approximations can be implemented by considering only regular terms and derivations. In doing so, it is essential to introduce a proper subtyping relation formalizing the notion of approximation between types.
In this paper we study a subtyping relation on coinductive terms built on union and object type constructors. We define an interpretation of types as set of values induced by a quite intuitive relation of membership of values to types, and prove that the definition of subtyping is sound w.r.t. subset inclusion between type interpretations. The proof of soundness has allowed us to simplify the notion of contractive derivation and to discover that the previously given definition of subtyping did not cover all possible representations of the empty type.
For the entire collection see [Zbl 1392.68028].Composition-nominative logics as institutions.https://www.zbmath.org/1456.030542021-04-16T16:22:00+00:00"Chentsov, Alexey"https://www.zbmath.org/authors/?q=ai:chentsov.alexey-a"Nikitchenko, Mykola"https://www.zbmath.org/authors/?q=ai:nikitchenko.mykola-sSummary: Composition-nominative logics (CNL) are program-oriented logics. They are based on algebras of partial predicates which do not have fixed arity. The aim of this work is to present CNL as institutions. Homomorphisms of first-order CNL are introduced, satisfaction condition is proved. Relations with institutions for classical first-order logic are considered. Directions for further investigation are outlined.\(\mathrm{Venn}_{i_{o1}} \): a diagram system for universe without boundary.https://www.zbmath.org/1456.030572021-04-16T16:22:00+00:00"Bhattacharjee, Reetu"https://www.zbmath.org/authors/?q=ai:bhattacharjee.reetu"Chakraborty, Mihir Kr."https://www.zbmath.org/authors/?q=ai:chakraborty.mihir-kumar"Choudhury, Lopamudra"https://www.zbmath.org/authors/?q=ai:choudhury.lopamudraSummary: A new diagram system \(\mathrm{Venn}_{i_{o1}}\) where properties are fundamental and an object exists only w.r.t a property is presented. This work modifies both in syntax and semantics the system \(\mathrm{Venn}_{i_o}\) proposed by Choudhury and Chakraborty to picturise and address issues connected with open universe. Semantics for the current system is given. Soundness and completeness w.r.t the semantics are established.Venn diagram with names of individuals and their absence: a non-classical diagram logic.https://www.zbmath.org/1456.030562021-04-16T16:22:00+00:00"Bhattacharjee, Reetu"https://www.zbmath.org/authors/?q=ai:bhattacharjee.reetu"Chakraborty, Mihir Kr."https://www.zbmath.org/authors/?q=ai:chakraborty.mihir-kumar"Choudhury, Lopamudra"https://www.zbmath.org/authors/?q=ai:choudhury.lopamudraSummary: Venn diagram system has been extended by introducing names of individuals and their absence. Absence gives a kind of negation of singular propositions. We have offered here a non-classical interpretation of this negation. Soundness and completeness of the present diagram system have been established with respect to this interpretation.Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search.https://www.zbmath.org/1456.030242021-04-16T16:22:00+00:00"Espírito Santo, José"https://www.zbmath.org/authors/?q=ai:espirito-santo.jose|espirito-santo.jose-carlos"Matthes, Ralph"https://www.zbmath.org/authors/?q=ai:matthes.ralph"Pinto, Luís"https://www.zbmath.org/authors/?q=ai:pinto.luis-fSummary: A new approach to inhabitation problems in simply typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda terms. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and produces simple, recursive decision procedures and counting functions. These allow to predict the number of inhabitants by testing the given type for syntactic criteria. This new approach is comprehensive and robust: based on the same syntactic representation, we also derive the state-of-the-art coherence theorems ensuring uniqueness of inhabitants.Mathematics for computer science. Basic concepts, structures and their applications. 3rd expanded and updated edition.https://www.zbmath.org/1456.680022021-04-16T16:22:00+00:00"Berghammer, Rudolf"https://www.zbmath.org/authors/?q=ai:berghammer.rudolfThis is the third edition of this textbook. For a review of the first edition see [Zbl 1309.00001].
The second edition added two new chapters and an
elaborate appendix giving a formal and complete introduction to the natural numbers based on Peano structures. With these two chapters, important aspects of computer science are addressed, namely those that concern the programming of algorithms. Keywords for the first of these chapters are program specification and verification, Hoare-calculus, loop-invariants and program construction; the second one focuses on generic programming, which is exemplified by several graph-theoretic algorithms, thus also extending concepts of graph theory from a former chapter. The third edition finally adds solutions to all exercises except those for the new chapters, which are available online.
The presentation of the topics is always detailed and in full mathematical rigour, starting with motivating examples and naive concepts, which are
then gradually conducted to full formalization. The reader will find many topics and detailed proofs not often found in other introductory
textbooks. The book is especially valuable for those students of computer science who are interested in a rigorous mathematical foundation.
Reviewer: Dieter Riebesehl (Lüneburg)Quantifying over events in probability logic: an introduction.https://www.zbmath.org/1456.030462021-04-16T16:22:00+00:00"Speranski, Stanislav O."https://www.zbmath.org/authors/?q=ai:speranski.stanislav-oSummary: In this article we describe a bunch of \textit{probability logics with quantifiers over events}, and develop primary techniques for proving computational complexity results (in terms of \(m\)-degrees) about these logics, mainly over discrete probability spaces. Also the article contains a comparison with some other probability logics and a discussion of interesting analogies with research in the metamathematics of Boolean algebras, demonstrating a number of attractive features and intuitive advantages of the present proposal.A categorical reconstruction of quantum theory.https://www.zbmath.org/1456.180142021-04-16T16:22:00+00:00"Tull, Sean"https://www.zbmath.org/authors/?q=ai:tull.seanThis paper lies in the long-standing tradition of \textit{reconstruction theorems}. To mention a notable few, we have
\begin{itemize}
\item The so-called \textit{Veblen-Young theorem} [\textit{O. Veblen} and \textit{J. W. Young}, Am. J. Math. 30, 347--380 (1908; JFM 39.0606.01); Bull. Sci. Math., II. Sér. 44, 105--112 (1920; JFM 47.0582.08); Projective Geometry. Vol. I. Boston and London: Ginn and Comp (1910; JFM 41.0606.06); Projective geometry. Vol. I, II. New York-Toronto-London: Blaisdell Publishing Company (1965; Zbl 0127.37604)] claims that a \textit{projective space} of dimension at least $3$ can be constructed as the projective space associated to a vector space over a division ring. Geometry of linear subspaces of a projective space or \textit{projective geometry} in short was axiomatized lattice-theoretically as finite-dimensional complemented modular lattices. \textit{G. Birkhoff} [Lattice theory. New York: American Mathematical Society (AMS) (1940; Zbl 0063.00402)] has shown that every complemented modular lattice of finite dimension is the direct product of lattices associated with projective geometries of finite dimension. \textit{J. von Neumann} [Proc. Natl. Acad. Sci. USA 22, 92--100 (1936; Zbl 0014.22307); Continuous geometry. Princeton, N.J.: Princeton University Press (1960; Zbl 0171.28003)] generalized these considerations to continuous geometry under the name of \textit{coordination theorems}.
\item Quantum mechanics was formulated by orthomodular lattices. It was \textit{C. Piron} [Helv. Phys. Acta 37, 439--468 (1964; Zbl 0141.23204)] who succeeded in establishing the coordination theorem. See Theorem 7.44 in [\textit{V. S. Varadarajan}, Geometry of quantum theory. Vol. I. Princeton, N.J.-Toronto-London-Melbourne: D. van Nostrand Company, Inc. (1968; Zbl 0155.56802)] for its details.
\item The category of modules was axiomatized categorically as \textit{abelian categories}. The so-called \textit{Freyd-Mitchell embedding theorem} [\textit{P. Freyd}, Abelian categories. An introduction to the theory of functors. New York-Evanston-London: Harper and Row, Publishers (1964; Zbl 0121.02103); \textit{B. Mitchell}, Theory of categories. New York and London: Academic Press (1965; Zbl 0136.00604)] claims that every abelian category is a full subcategory of a category of modules over some ring $R$ and that the embedding is an exact functor.
\item Grothendieck toposes were axiomatized categorically as \textit{elementary toposes} by Lawvere and Tierney during the year 1969--1970.
It was \textit{J. Giraud} [Cohomologie non abélienne. Berlin-Heidelberg-New York: Springer-Verlag (1971; Zbl 0226.14011)] who succeeded in categorically characterizing elementary toposes for which one can reconstruct Grothendieck toposes.
\end{itemize}
This paper presents a genuinely categorical formalism of quantum mechanics based on dagger categories, establishing its coordination theorem to recover something like the standard Hilber-space formalism [\textit{D. Hilbert} et al., Math. Ann. 98, 1--30 (1927; JFM 53.0849.03)].
Reviewer: Hirokazu Nishimura (Tsukuba)Parity, relevance, and gentle explosiveness in the context of Sylvan's mate function.https://www.zbmath.org/1456.030402021-04-16T16:22:00+00:00"Ferguson, Thomas Macaulay"https://www.zbmath.org/authors/?q=ai:ferguson.thomas-macaulayThis paper presents an investigation into a `mate function' introduced by Richard Routley to serve as a ``relaxed or generalized version'' of a star operator used for defining negation in relevance logics. A first-degree model with a mate function is defined as a triple \(\langle G, K, \cdot^M \rangle\), where \(K\) is a nonempty collection of atomic set-ups, \(G \in K\) is a distinguished set-up, and \(\cdot^M : K \rightarrow K\) is a unary \emph{mate function} such that for all \(H \in K\), there exists a set-up \(I \in K\) such that \(H^M = I\). The main intended purpose of this construction is the truth condition for negation, which is defined as follows: \(H \Vdash {\sim}\varphi\) iff \(H^M \not\Vdash \varphi\). Moreover, the paper is concentrated on the mate functions which turn out to be \emph{cyclical} (with some period \(n\)), i.e., which is subject to the following condition: for all \(H \in K \setminus \{G\}\): \(H^{M_n} = H^M\). It is shown how the set of first-degree models with cyclical mate functions of any period \(n\) can be characterized by a countably infinite collection of distinct sound and complete proof systems. It is observed that these systems can be naturally divided into two distinct partitions and that this division is ``tightly correlated with the parity of mate functions, so that the logics in which mate functions have even parity differ [\dots] from those systems whose mate functions have odd parity.'' In particular, ``logics corresponding to mate functions of even parity are exactly the systems that are relevant logics while logics corresponding to functions with odd parity are exactly the class of logics that are \emph{gently explosive}.''
Reviewer: Yaroslav Shramko (Kryvyi Rih)Transport of finiteness structures and applications.https://www.zbmath.org/1456.031082021-04-16T16:22:00+00:00"Tasson, Christine"https://www.zbmath.org/authors/?q=ai:tasson.christine"Vaux, Lionel"https://www.zbmath.org/authors/?q=ai:vaux.lionelSummary: We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: These include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.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.In defence of dialetheism: a reply to Beziau and Tkaczyk.https://www.zbmath.org/1456.030502021-04-16T16:22:00+00:00"Martin, Ben"https://www.zbmath.org/authors/?q=ai:martin.ben|martin.benjamin-m-sSummary: In recent editions of this journal, \textit{J.-Y. Beziau} [ibid. 25, No. 1, 51--56 (2016; Zbl 1384.03017)] and \textit{M. Tkaczyk} [ibid. 25, No. 2, 203--224 (2016; Zbl 1384.03077)] have criticised a prominent dialetheic logic and common arguments for dialetheism, respectively. While Beziau argues that Priest's logic \textbf{LP} commits the dialetheist to trivialism, the thesis that all propositions are true, Tkaczyk maintains that the arguments traditionally proposed for dialetheism are faulty and ultimately that dialetheism should be rejected as self-refuting. This paper shows that both are mistaken in their contentions. Beziau's argument conflates \textit{truth-in-an-interpretation} with truth \textit{simpliciter} and Tkaczyk misconstrues the substance of dialetheic arguments. In the process of identifying these weaknesses of both arguments, the paper clarifies elements of both dialetheic logics and dialetheism which these discussions demonstrate are still misunderstood within the literature.Maximality of the minimal \(\mathcal R\)-logic.https://www.zbmath.org/1456.030532021-04-16T16:22:00+00:00"Karczewska, Anna Maria"https://www.zbmath.org/authors/?q=ai:karczewska.anna-mariaSummary: The minimal system of the connective of realization -- \textit{T. Jarmużek} and \textit{A. Pietruszczak}'s [Log. Log. Philos. 13, 147--162 (2004; Zbl 1117.03328)] \textsf{MR} -- is examined. The single-index rule is defined. Then it is claimed that if a single- index rule non-derivable in \textsf{MR} is derivable in a strengthening of \textsf{MR}, then the strengthening is inconsistent. This property may be called the \textit{single-index maximality}.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.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.Proof nets for multiplicative cyclic linear logic and Lambek calculus.https://www.zbmath.org/1456.030922021-04-16T16:22:00+00:00"Abrusci, V. Michele"https://www.zbmath.org/authors/?q=ai:abrusci.vito-michele"Maieli, Roberto"https://www.zbmath.org/authors/?q=ai:maieli.robertoSummary: This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.Reasoning: games, cognition, logic. Proceedings of the Poznań reasoning week multi-conference, Poznań, Poland, September 11--15, 2018.https://www.zbmath.org/1456.030042021-04-16T16:22:00+00:00"Urbański, Mariusz (ed.)"https://www.zbmath.org/authors/?q=ai:urbanski.mariusz"Skura, Tomasz (ed.)"https://www.zbmath.org/authors/?q=ai:skura.tomasz-f"Łupkowski, Paweł (ed.)"https://www.zbmath.org/authors/?q=ai:lupkowski.pawelPublisher's description: This volume contains papers presented at the Poznań reasoning week multi-conference held in Poznań in September 11--15, 2018.
PRW aims at bringing together experts whose research offers a broad range of perspectives on systematic analyses of reasoning processes and their formal modelling. The 2018 edition consisted of three conferences, which addressed the following topics:
\begin {itemize}
\item (i) games in reasoning research,
\item (ii) the interplay of logic and cognition, and
\item (iii) refutation systems. The papers collected in this volume address all these topics.
\end {itemize}
The articles of this volume will be reviewed individually.Natural deduction for four-valued both regular and monotonic logics.https://www.zbmath.org/1456.030482021-04-16T16:22:00+00:00"Petrukhin, Yaroslav"https://www.zbmath.org/authors/?q=ai:petrukhin.yaroslav-igorevichSummary: The development of recursion theory motivated Kleene to create regular three-valued logics. Remove it taking his inspiration from the computer science, Fitting later continued to investigate regular three-valued logics and defined them as monotonic ones. Afterwards, Komendantskaya proved that there are four regular three-valued logics and in the three-valued case the set of regular logics coincides with the set of monotonic logics. Next, Tomova showed that in the four-valued case regularity and monotonicity do not coincide. She counted that there are 6400 four-valued regular logics, but only six of them are monotonic. The purpose of this paper is to create natural deduction systems for them. We also describe some functional properties of these logics.Temporal alethic dyadic deontic logic and the contrary-to-duty obligation paradox.https://www.zbmath.org/1456.030342021-04-16T16:22:00+00:00"Rönnedal, Daniel"https://www.zbmath.org/authors/?q=ai:ronnedal.danielSummary: A contrary-to-duty obligation (sometimes called a reparational duty) is a conditional obligation where the condition is forbidden, e.g. ``if you have hurt your friend, you should apologise'', ``if he is guilty, he should confess'', and ``if she will not keep her promise to you, she ought to call you''. It has proven very difficult to find plausible formalisations of such obligations in most deontic systems. In this paper, we will introduce and explore a set of temporal alethic dyadic deontic systems, i.e., systems that include temporal, alethic and dyadic deontic operators. We will then show how it is possible to use our formal apparatus to symbolise contrary-to-duty obligations and to solve the so-called contrary-to-duty (obligation) paradox, a problem well known in deontic logic. We will argue that this response to the puzzle has many attractive features. Semantic tableaux are used to characterise our systems proof theoretically and a kind of possible world semantics, inspired by the so-called \(\mathrm{T}\times\mathrm{W}\) semantics, to characterise them semantically. Our models contain several different accessibility relations and a preference relation between possible worlds, which are used in the definitions of the truth conditions for the various operators. Soundness results are obtained for every tableau system and completeness results for a subclass of them.S (for syllogism) revisited. ``The revolution devours its children''.https://www.zbmath.org/1456.030412021-04-16T16:22:00+00:00"Meyer, Robert K."https://www.zbmath.org/authors/?q=ai:meyer.robert-k.1"Martin, Errol P."https://www.zbmath.org/authors/?q=ai:martin.errol-peterSummary: In 1978, the authors began a paper, [``S (for Syllogism)'', Preprint] intended as a philosophical companion piece to the technical solution [the authors, J. Symb. Log. 47, 869--887 (1982; Zbl 0498.03011)] of the Anderson-Belnap \(\mathrm{P}-\mathrm{W}\) problem. [the authors, Preprint, loc. cit.] has gone through a number of drafts, which have been circulated among close friends. Meanwhile other authors have failed to see the point of the semantics which we introduced in [the authors, 1982, loc. cit]. It will accordingly be our purpose here to revisit that semantics, while giving our present views on syllogistic matters past, present and future, especially as they relate to not begging the question via such dubious theses as \(A\to A\). We shall investigate in particular a paraconsistent attitude toward such theses.Expressing the behavior of three very different concurrent systems by using natural extensions of separation logic.https://www.zbmath.org/1456.681162021-04-16T16:22:00+00:00"Daylight, Edgar G."https://www.zbmath.org/authors/?q=ai:daylight.edgar-g"Shukla, Sandeep K."https://www.zbmath.org/authors/?q=ai:shukla.sandeep-kumar"Sergio, Davide"https://www.zbmath.org/authors/?q=ai:sergio.davideSummary: Separation Logic is a non-classical logic used to verify pointer-intensive code. In this paper, however, we show that Separation Logic, along with its natural extensions, can also be used as a specification language for concurrent-system design. To do so, we express the behavior of three very different concurrent systems: a Subway, a Stopwatch, and a \(2\times 2\) Switch. The Subway is originally implemented in \texttt{LUSTRE}, the Stopwatch in \texttt{Esterel}, and the \(2\times 2\) Switch in \texttt{Bluespec}.
For the entire collection see [Zbl 1415.68026].Complexity of translations from resolution to sequent calculus.https://www.zbmath.org/1456.030872021-04-16T16:22:00+00:00"Reis, Giselle"https://www.zbmath.org/authors/?q=ai:reis.giselle"Woltzenlogel Paleo, Bruno"https://www.zbmath.org/authors/?q=ai:woltzenlogel-paleo.brunoSummary: Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.\(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads.https://www.zbmath.org/1456.030272021-04-16T16:22:00+00:00"Honsell, Furio"https://www.zbmath.org/authors/?q=ai:honsell.furio"Liquori, Luigi"https://www.zbmath.org/authors/?q=ai:liquori.luigi"Maksimovic, Petar"https://www.zbmath.org/authors/?q=ai:maksimovic.petar"Scagnetto, Ivan"https://www.zbmath.org/authors/?q=ai:scagnetto.ivanSummary: We extend the constructive dependent type theory of the Logical Framework \(\mathsf{LF}\) with \textit{monadic, dependent} type constructors indexed with predicates over judgements, called \textit{Locks}. These monads capture various possible \textit{proof attitudes} in establishing the judgment of the object logic encoded by an \(\mathsf{LF}\) type. Standard examples are \textit{factoring-out} the verification of a \textit{constraint} or \textit{delegating} it to an \textit{external oracle}, or supplying some \textit{non-apodictic} epistemic evidence, or simply \textit{discarding} the proof witness of a precondition deeming it irrelevant. This new framework, called \textit{Lax Logical Framework}, \(\mathsf{LLF}_{\mathcal P}\), is a conservative extension of \(\mathsf{LF}\), and hence it is the appropriate metalanguage for dealing formally with \textit{side-conditions} in rules or \textit{external evidence} in logical systems. \(\mathsf{LLF}_{\mathcal P}\) arises once the \textit{monadic} nature of the \textit{lock} type-constructor, \(\mathcal L^{\mathcal{P}}_{M,\sigma}[\cdot]\), introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, \(\mathcal U^{\mathcal{P}}_{M,\sigma}[\cdot]\), in place of Moggi's monadic \(let_T\), thus simplifying the equational theory. The rules for \(\mathcal U^{\mathcal{P}}_{M,\sigma}[\cdot]\) permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of \(\mathsf{LLF}_{\mathcal{P}}\) by a novel indirect method based on the encoding of \(\mathsf{LLF}_{\mathcal{P}}\) in \(\mathsf{LF}\). We discuss encodings in \(\mathsf{LLF}_{\mathcal{P}}\) of call-by-value \(\lambda\)-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.Automorphisms of types in certain type theories and representation of finite groups.https://www.zbmath.org/1456.030282021-04-16T16:22:00+00:00"Soloviev, Sergei"https://www.zbmath.org/authors/?q=ai:soloviev.sergei-vladimirovich|solovev.sergei-i|solovyev.sergey-alexandrovichSummary: The automorphism groups of types in several systems of type theory are studied. It is shown that in simply typed \(\lambda\)-calculus \(\lambda^1\beta\eta\) and in its extension with surjective pairing and terminal object these groups correspond exactly to the groups of automorphisms of finite trees. In second-order \(\lambda\)-calculus and in Luo's framework (LF) with dependent products, any finite group may be represented.Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions.https://www.zbmath.org/1456.680972021-04-16T16:22:00+00:00"Dima, Cătălin"https://www.zbmath.org/authors/?q=ai:dima.catalin"Enea, Constantin"https://www.zbmath.org/authors/?q=ai:enea.constantin"Guelev, Dimitar"https://www.zbmath.org/authors/?q=ai:guelev.dimitar-pSummary: We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for identifying states whose histories are indistinguishable to the considered coalition.
For the entire collection see [Zbl 1392.68028].A correspondence between maximal abelian sub-algebras and linear logic fragments.https://www.zbmath.org/1456.031052021-04-16T16:22:00+00:00"Seiller, Thomas"https://www.zbmath.org/authors/?q=ai:seiller.thomasSummary: We show a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by \textit{J. Dixmier} [Ann. Math. (2) 59, 279--286 (1954; Zbl 0055.10702)] and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction [\textit{J.-Y. Girard}, Theor. Comput. Sci. 412, No. 20, 1860--1883 (2011; Zbl 1230.03093)]. The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation. We also unveil the essential role played by MASAs in previous geometry of interaction constructions.Semantics of a typed algebraic lambda-calculus.https://www.zbmath.org/1456.030292021-04-16T16:22:00+00:00"Valiron, Benoît"https://www.zbmath.org/authors/?q=ai:valiron.benoitSummary: Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We sketch the relation with two established vectorial lambda-calculi. Then we study the problems arising from the addition of a fixed point combinator and how to modify the equational theory to solve them. We sketch an algebraic vectorial PCF and its possible denotational interpretations.
For the entire collection see [Zbl 1445.68010].Probabilistic logic over equations and domain restrictions.https://www.zbmath.org/1456.030452021-04-16T16:22:00+00:00"Mordido, Andreia"https://www.zbmath.org/authors/?q=ai:mordido.andreia"Caleiro, Carlos"https://www.zbmath.org/authors/?q=ai:caleiro.carlosSummary: We propose and study a probabilistic logic over an algebraic basis, including equations and domain restrictions. The logic combines aspects from classical logic and equational logic with an exogenous approach to quantitative probabilistic reasoning. We present a sound and weakly complete axiomatization for the logic, parameterized by an equational specification of the algebraic basis coupled with the intended domain restrictions. We show that the satisfiability problem for the logic is decidable, under the assumption that its algebraic basis is given by means of a convergent rewriting system, and, additionally, that the axiomatization of domain restrictions enjoys a suitable subterm property. For this purpose, we provide a polynomial reduction to Satisfiability Modulo Theories. As a consequence, we get that validity in the logic is also decidable. Furthermore, under the assumption that the rewriting system that defines the equational basis underlying the logic is also subterm convergent, we show that the resulting satisfiability problem is \textsf{NP}-complete, and thus the validity problem is \textsf{coNP}-complete. We test the logic with meaningful examples in information security, namely by verifying and estimating the probability of the existence of offline guessing attacks to cryptographic protocols.Modal logic and the approximation induction principle.https://www.zbmath.org/1456.681172021-04-16T16:22:00+00:00"Gazda, Maciej"https://www.zbmath.org/authors/?q=ai:gazda.maciej-w"Fokkink, Wan"https://www.zbmath.org/authors/?q=ai:fokkink.willem-janSummary: We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators.
For the entire collection see [Zbl 1415.68026].Book review of: Lewis Carroll's diaries. The private journals of Charles Lutwidge Dodgson (Lewis Carroll); The logic pamphlets of Charles Lutwidge Dodgson and related pieces.https://www.zbmath.org/1456.000292021-04-16T16:22:00+00:00"Moktefi, Amirouche"https://www.zbmath.org/authors/?q=ai:moktefi.amiroucheReview of [Zbl 1239.01121].Almost linear Büchi automata.https://www.zbmath.org/1456.680952021-04-16T16:22:00+00:00"Babiak, Tomáš"https://www.zbmath.org/authors/?q=ai:babiak.tomas"Řehák, Vojtěch"https://www.zbmath.org/authors/?q=ai:rehak.vojtech"Strejček, Jan"https://www.zbmath.org/authors/?q=ai:strejcek.janSummary: We introduce a new fragment of linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Büchi automata studied in this context and we indicate possible applications.
For the entire collection see [Zbl 1415.68026].A public announcement separation logic.https://www.zbmath.org/1456.030302021-04-16T16:22:00+00:00"Courtault, J. R."https://www.zbmath.org/authors/?q=ai:courtault.jean-rene"van Ditmarsch, H."https://www.zbmath.org/authors/?q=ai:van-ditmarsch.hans-pieter"Galmiche, D."https://www.zbmath.org/authors/?q=ai:galmiche.didierSummary: We define a Public Announcement Separation Logic (PASL) that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying its semantics and illustrating its interest for modelling systems, we provide a sound and complete tableau calculus that deals with resource, agent and announcement constraints and give also a countermodel extraction method.Advances in modal logic. Vol. 13. Proceedings of the 13th conference (AiML 2020), Helsinki, Finland, virtual conference, August 24--28, 2020.https://www.zbmath.org/1456.030032021-04-16T16:22:00+00:00"Olivetti, Nicola (ed.)"https://www.zbmath.org/authors/?q=ai:olivetti.nicola"Verbrugge, Rineke (ed.)"https://www.zbmath.org/authors/?q=ai:verbrugge.rineke"Negri, Sara (ed.)"https://www.zbmath.org/authors/?q=ai:negri.sara"Sandu, Gabriel (ed.)"https://www.zbmath.org/authors/?q=ai:sandu.gabrielPublisher's description: Logic deals with the fundamental notions of truth and falsity. Modal logic arose from the philosophical study of ``modes of truth'' with the two most common modes being ``necessarily true'' and ``possibly true''.
Nowadays modal logic is used to reason about knowledge, about obligations, about programs and about time, among others.
Actual research in modal logic spans philosophy, computer science and mathematics using techniques from relational structures, universal algebra, topology, and proof theory.
These proceedings record the papers presented at the 2020 conference on advances in modal logic, a biennial conference series with an aim to report on important new developments in pure and applied modal logic.
The topics include decidability and complexity results, proof theory, model theory, interpolation, related problems in algebraic logic, as well as history of modal reasoning.
The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1398.03005].Normative consistency: an xstit account.https://www.zbmath.org/1456.030372021-04-16T16:22:00+00:00"Payette, Gillman"https://www.zbmath.org/authors/?q=ai:payette.gillmanSummary: In this paper we take inspiration from a couple of authors on how to think about normative (in)consistency, and then show how to conceive of normative inconsistency in an xstit framework. One view on normative inconsistency is from \textit{G. H. von Wright} [``Is there a logic of norms?'', Ratio Juris 4, No. 3, 265--283 (1991; \url{doi:10.1111/j.1467-9337.1991.tb00099.x})], and the other from \textit{C. L. Hamblin} [J. Philos. Log. 1, 74--85 (1972; Zbl 0225.02007)]. These two accounts share a conception of normative inconsistency, but their formal frameworks are very different. We propose a way to get the best of both views on normative inconsistency by using an xstit framework, mixed with a version of Anderson's reduction of deontic logic to alethic modal logic. We consider variations on those ideas and relate it to a work of \textit{R. B. Marcus} [``Moral dilemmas and consistency'', J. Philos. 77, No. 3, 121--136 (1980)].Epistemic erotetic search scenarios.https://www.zbmath.org/1456.030312021-04-16T16:22:00+00:00"Łupkowski, Paweł"https://www.zbmath.org/authors/?q=ai:lupkowski.pawel"Majer, Ondrej"https://www.zbmath.org/authors/?q=ai:majer.ondrej"Peliš, Michal"https://www.zbmath.org/authors/?q=ai:pelis.michal"Urbański, Mariusz"https://www.zbmath.org/authors/?q=ai:urbanski.mariuszSummary: The aim of this paper is to introduce erotetic search scenarios known from Inferential Erotetic Logic by using the framework of epistemic erotetic logic. The key notions used in this system are those of askability and epistemic erotetic implication. Scenarios are supposed to represent all rational strategies of an agent solving the problem posed by the initial question where the interaction with an external information source is seen as a series of updates of the agent's knowledge.Existential import and relations of categorical and modal categorical statements.https://www.zbmath.org/1456.030382021-04-16T16:22:00+00:00"Raclavský, Jiří"https://www.zbmath.org/authors/?q=ai:raclavsky.jiriSummary: I examine the familiar quadruple of categorical statements ``Every \(F\) is/is not \(G\)'', ``Some \(F\) is/is not \(G\)'' as well as the quadruple of their modal versions ``Necessarily, every \(F\) is/is not \(G\)'', ``Possibly, some \(F\) is/is not \(G\)''. I focus on their existential import and its impact on the resulting Squares of Opposition. Though my construal of existential import follows modern approach, I add some extra details which are enabled by framing my definition of existential import within expressively rich higher-order partial type logic. As regards the modal categorical statements, I find that so-called void properties bring existential import to them, so they are the only properties which invalidate subalternation, and thus also contrariety and subcontrariety, in the corresponding Square of Opposition.A semantics for nabla.https://www.zbmath.org/1456.030552021-04-16T16:22:00+00:00"Goubault-Larrecq, Jean"https://www.zbmath.org/authors/?q=ai:goubault-larrecq.jeanSummary: We give a semantics for a classical variant of Dale Miller and Alwen Tiu's logic \(FO \lambda^\nabla\). Our semantics validates the rule that nabla \(x\) implies exists \(x\), but is otherwise faithful to the authors' original intentions. The semantics is based on a category of so-called nabla sets, which are simply strictly increasing sequences of non-empty sets. We show that the logic is sound for that semantics. Assuming there is a unique base type \(\iota\), we show that it is complete for Henkin structures, incomplete for standard structures in general, but complete for standard structures in the case of \(\Pi_1\) formulae, and that includes all first-order formulae.Subexponentials in non-commutative linear logic.https://www.zbmath.org/1456.030992021-04-16T16:22:00+00:00"Kanovich, Max"https://www.zbmath.org/authors/?q=ai:kanovich.max-i"Kuznetsov, Stepan"https://www.zbmath.org/authors/?q=ai:kuznetsov.s-l"Nigam, Vivek"https://www.zbmath.org/authors/?q=ai:nigam.vivek"Scedrov, Andre"https://www.zbmath.org/authors/?q=ai:scedrov.andreSummary: Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.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.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.Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis.https://www.zbmath.org/1456.680992021-04-16T16:22:00+00:00"Morgenstern, Andreas"https://www.zbmath.org/authors/?q=ai:morgenstern.andreas"Schneider, Klaus"https://www.zbmath.org/authors/?q=ai:schneider.klaus.1Summary: The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent \(\omega\)-automaton and then compute a winning strategy for the corresponding \(\omega\)-regular game. To this end, the obtained \(\omega\)-automata have to be (pseudo)-determinized where typically a variant of Safra's determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implementations by replacing Safra's determinization by simpler determinization procedures. In particular, we exploit (1) the temporal logic hierarchy that corresponds to the well-known automata hierarchy consisting of safety, liveness, Büchi, and co-Büchi automata as well as their Boolean closures, (2) the non-confluence property of \(\omega\)-automata that result from certain translations of LTL formulas, and (3) symbolic implementations of determinization procedures for the Rabin-Scott and the Miyano-Hayashi breakpoint construction. In particular, we present convincing experimental results that demonstrate the practical applicability of our new synthesis procedure.
For the entire collection see [Zbl 1392.68028].Begin, after, and later: a maximal decidable interval temporal logic.https://www.zbmath.org/1456.030332021-04-16T16:22:00+00:00"Bresolin, Davide"https://www.zbmath.org/authors/?q=ai:bresolin.davide"Sala, Pietro"https://www.zbmath.org/authors/?q=ai:sala.pietro"Sciavicco, Guido"https://www.zbmath.org/authors/?q=ai:sciavicco.guidoSummary: Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous ITL studied so far is Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments have an undecidable satisfiability problem. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider different combinations of the interval relations begins (B), after (A), later (L) and their inverses \(\bar{\text{A}}\), \(\bar{\text{B}}\), and \(\bar{\text{L}}\). We know from previous works that the combination \(\text{AB}\bar{\text{B}}\bar{\text{A}}\) is decidable only when finite domains are considered (and undecidable elsewhere), and that \(\text{AB}\bar{\text{B}}\) is decidable over the natural numbers. We extend these results by showing that decidability of \(\text{AB}\bar{\text{B}}\) can be further extended to capture the language \(\text{AB}\bar{\text{B}}\bar{\text{L}}\), which lays in between \(\text{AB}\bar{\text{B}}\) and \(\text{AB}\bar{\text{B}}\bar{\text{A}}\), and that turns out to be maximal w.r.t decidability over strongly discrete linear orders (e.g. finite orders, the naturals, the integers). We also prove that the proposed decision procedure is optimal with respect to the EXPSPACE complexity class.
For the entire collection see [Zbl 1392.68028].On modal \(\mu\)-calculus over finite graphs with bounded strongly connected components.https://www.zbmath.org/1456.030352021-04-16T16:22:00+00:00"D'Agostino, Giovanna"https://www.zbmath.org/authors/?q=ai:dagostino.giovanna"Lenzi, Giacomo"https://www.zbmath.org/authors/?q=ai:lenzi.giacomoSummary: For every positive integer \(k\) we consider the class \(SCCk\) of all finite graphs whose strongly connected components have size at most \(k\). We show that for every \(k\), the Modal \(\mu\)-Calculus fixpoint hierarchy on \(SCCk\) collapses to the level \(\Delta_2=\Pi_2\cap\Sigma_2\), but not to \(\operatorname{Comp}(\Sigma_1,\Pi_1)\) (compositions of formulas of level \(\Sigma_1\) and \(\Pi_1)\). This contrasts with the class of all graphs, where \(\Delta_2=\operatorname{Comp}(\Sigma_1,\Pi_1)\).
For the entire collection see [Zbl 1392.68028].Deep inference and expansion trees for second-order multiplicative linear logic.https://www.zbmath.org/1456.031072021-04-16T16:22:00+00:00"Straßburger, Lutz"https://www.zbmath.org/authors/?q=ai:strassburger.lutzSummary: In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.Dialectica interpretation with marked counterexamples.https://www.zbmath.org/1456.030882021-04-16T16:22:00+00:00"Trifonov, Trifon"https://www.zbmath.org/authors/?q=ai:trifonov.trifon-aSummary: Goedel's functional ``Dialectica'' interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.
For the entire collection see [Zbl 1391.03011].