Seminar on Applied Mathematical Logic

The variable-sharing property (VSP) is regarded as a key feature of relevant logic, while the Craig interpolation property (CIP), formulated with respect to relevant implication, implies the VSP in constant-free propositional languages. However, to the best of our knowledge, no constant-free distributive relevant logic has previously been shown to enjoy the CIP. This absence of positive results has contributed to a widespread impression among relevant logicians that relevance and Craig interpolation are incompatible. In this work, we address this tension by proving that the negation-free fragment of basic relevant logic B, denoted B⁺, enjoys both properties. Our proofs are purely syntactic and is based on a novel nested sequent calculus featuring binary relevant blocks as primitive structural constructs. Unlike conventional nested sequent calculi, where unary nesting reflects the binary accessibility relation of Kripke semantics, our calculus employs a binary nesting operator that directly reflects the ternary relational structure of Routley–Meyer semantics. We establish soundness and cut-free completeness of the calculus, and then provide syntactic proofs of both the VSP and the CIP using a structural notion internalized in the nested sequents. The talk is based on joint work with Fabio De Martin Polo.

In one or another logic, and assuming the presence of the symbols ⊥ and ⊤ for falsity and truth, interpolation theorem IT is the following claim. If the formula φ→ψ is valid, as determined by the semantics of the logic in question, then there exists a formula μ, called interpolant of φ and ψ, such that φ→μ and μ→ψ are valid and μ is built up from the extralogical symbols that occur in both φ and ψ. In propositional logic extralogical symbols are just atoms, and examples of logics for which IT is true include classical logic and intuitionistic logic. In predicate logic extralogical symbols are free variables, function symbols and predicate symbols of the given language. Then IT is known to hold for classical logic with equality, in which = is considered a logical symbol and so it may occur in an interpolant no matter whether it is in φ and ψ. Some sources, like Takeuti, give a proof for predicate logic without equality, but they proceed under the additional assumption that there are no function symbols of nonzero arity. I will show that the above restriction can be dropped: the proof-theoretic proof of IT given in Takeuti's book can be adjusted so that it works in the presence of function symbols.

Petr Vopěnka's alternative set theory is an alternative to Cantor's set-theoretical foundations for mathematics, which rejects commitment to actually infinite sets. Despite this rejection, the theory does speak of infinite sets and classes, but Vopěnka contends that infinity in alternative set theory is merely potential. In the theory, the notion of infinity is tied to the notion of proper semisets, subclasses of sets that are not themselves sets. According to Vopěnka, proper classes and proper semisets represent indefinite collections, while sets represent definite collections. Infinite sets have an indefinite part that disappears beyond a metaphorical horizon. I will argue that the notion of potential infinity in alternative set theory can be understood in terms of this indefiniteness. However, on the level of logic, it would appear that both sets and classes are equally definite: both are extensional, they share the same membership relation, and both are governed by classical logic. I show how this distinction in definiteness between sets and classes can be brought out by considering multiple models at once, using modal logic and the de dicto/de re distinction. I will argue that infinite classes are indefinite in the sense that their extension may vary depending on the domain, while all sets are defined by their members. Proper semisets produce an immediate problem for my reading. How can an infinite set be definite if it includes an indefinite semiset as a proper part? Or, conversely, if an infinite set is defined by its members, how can a proper semiset be indefinite if it is a proper part of a set that is completely defined by its members? To solve this issue, I argue that while infinite sets are still defined by their members, the question of which proper semiset is a proper part of which set remains indefinite.

Semiring provenance, proposed in 2007 by Green, Kravounarakis and Tannen was introduced as a comprehensive framework to capture different forms of annotated databases. The central idea is to annotate the atomic facts in a database by the values in a naturally ordered commutative semiring, then extend these to database queries using the operations of the semiring. More recently, Grädel and Tannen proposed a new approach, semiring semantics which incorporates negative information by annotating literals subject to the model-defining restriction - exactly one of each literal pair takes value 0. This has become a recent thriving research area whose major focus is the extent to which classical model theory extends to semiring semantics. However, the proof theory has received less attention with little understanding of appropriate proof systems for the majority of the main semirings. Interestingly, semirings as algebraic structures are closely related to residauted lattices, many of the main absorptive semirings in applications can be expanded to residuated lattices - often one well studied in the literature. In particular these residuated lattices have well development proof systems and opening up the potential for an effective development of proof systems for semirings. via known results for their corresponding residuated lattice. In this talk, we present the early stages of just such an investigation. We discuss the development of calculi for three propositional semiring based logics and a predicate calculus for the especially well behaved lattice semirings.

The aim of this talk is to introduce a display calculus for first-order relevant logics (FORL). Departing from the conventional Tarskian interpretation of quantifiers, we adopt the Mares-Goldblatt relational semantics, as well as its algebraic counterpart, where quantifiers are treated as operations on a set of admissible propositions. These structures effectively preclude the semantic collapse of FORL into classical logic. By considering foundational results by N. Belnap concerning the properties of displayable logics, we exploit the algebraic residuation of the connectives to construct a display calculus that accommodates FORL. Within this framework, the operational rules for quantifiers are governed by “structural pre-quantifiers” functioning as standard adjoints, which precisely mirror the core behavior of the quantifiers as defined on MG structures. Finally, we discuss some results, establishing the display property, the cut elimination theorem, and soundness with respect to the underlying MG structures, alongside a syntactic proof of completeness. This work builds upon ongoing research conducted in collaboration with Nick Ferenz.

This talk investigates the pointed modal logic of reals, establishing its relational Kripke semantics with bounded valuations in the Abelian ℓ-group of real numbers equipped with the distinguished negative constant -1. To study this logic algebraically, we introduce the variety of negatively pointed modal Abelian ℓ-groups, focusing particularly on its strongly pointed members. By constructing complex algebras and canonical frames, we establish a Truth Lemma that directly connects the relational models with the algebraic structures.

Because finitary axiomatizations cannot fully capture the Kripke validities of the reals, we introduce further algebraic constraints. Specifically, we incorporate an infinitary Archimedean-style rule to manage bounded valuations and infinitely small elements within the radical of the algebras. The presentation concludes by proving a corresponding infinitary algebraic completeness theorem, demonstrating that validity in this real-valued modal logic is exactly characterized by the infinitary derivability relation of pointed modal Abelian ℓ-groups.

Joint work with Wolfgang Poiger.

Substructural logics are generalizations of classical and intuitionistic logic that are suitable for resource sensitive reasoning. Their algebraic semantics, residuated lattices, have an independent history rooted in classical and order algebra. Many residuated lattices admit an idempotent skeleton, so the study of idempotent algebras is useful in the general analysis of residuated lattices. We focus on a distinguished class of idempotent residuated chains (lower-involutive) and the variety that they generate. This variety is known to have the amalgamation property (AP) and we fully classify all of its varieties that enjoy the AP and the ones that fail the AP, showing in particular that there are uncountably-many of each type. Joint work with X. Zhuang.

Dynamic Epistemic Logic (DEL) extends modal logic to model both knowledge and its change through communication. A central example is Public Announcement Logic (PAL), where knowledge states are modeled by sets of possible worlds, and announcements update these models by eliminating worlds. Thus, DEL’s semantics is inherently dynamic. In this talk, I will present a method to proof-theoretically represent the dynamic character of announcements in a fully natural way and with only syntactical means. I will first introduce so-called “indexed dynamic hypersequents” that serve as a syntactic counterpart to epistemic models and their updates. I will introduce them step by step, starting from standard sequents, and highlight the underlying semantic intuitions. Within this framework, I construct a dynamic proof calculus for PAL which rules are fully natural when compared to the semantics of PAL and reflect the structural properties of updates through public announcements, in particular how updated models are constructed and how worlds are related across such models. The calculus enjoys strong structural properties such as admissibility of all its structural rules and syntactic cut-elimination. This makes the calculus suitable for proving important meta-properties and for extension to other dynamic epistemic logics.

The talk is based on a joint work with Francesca Poggiolesi.

The celebrated Beth definability theorem establishes that implicit and explicit definability coincide in first-order classical logic. In this talk, we investigate a similar phenomenon in certain classes of algebraic structures: the strong Beth definability property, which holds when every implicit operation of the class can be made explicit. An implicit operation is a partial function that is implicitly defined by a formula and preserved by homomorphisms. Typical examples include complementation in bounded distributive lattices and taking inverses in monoids. Implicit operations can be viewed as a hidden part of the algebraic structure that becomes explicit once it can be expressed as a composition of the basic operations.

Not every class of algebraic structures has the strong Beth definability property. We introduce the notion of a Beth companion, an optimal solution to the problem of completing a class into one with the strong Beth definability property. For example, the Beth companion of the class of bounded distributive lattices is the class of Boolean algebras, obtained by adding complementation as a basic operation and thereby making it explicit. We discuss structural properties of Beth companions and their applications, and review several examples from general algebra and algebraic logic. We conclude by mentioning connections with amalgamation, algebraic logic, automated reasoning, and anti-unification, as well as directions for future research. Most of the results presented in this talk can be found in [1].

References:
[1] L. Carai, M. Kurtzhals, and T. Moraschini. The theory of implicit operations. 2025. Available at https://arxiv.org/abs/2512.14326

Strong logics are extensions of first-order logic with added expressive capabilities, for example through infinitary boolean connectives or second-order or other additional quantifiers. Model-theoretic properties of strong logics - for instance, analogues of the Compactness or Löwenheim-Skolem Theorems - give rise to large cardinals. In particular the part of the large cardinal hierarchy up to Vopěnka's Principle is well-studied through this perspective: most of the important large cardinals in this region have model-theoretic characterisations.

Our aim is twofold. First, we give an overview of some of the results obtained over the last years that show that several important hierarchies of large cardinals can be obtained by demanding that some model-theoretic property holds for stronger and stronger logics. Vopěnka's Principle is a natural limit point of many of these efforts which begs the question whether large cardinals at the upper end of the hierarchy have model-theoretic characterisations. In the second part of the talk we present some ongoing work considering model-theoretic characterisations of large cardinals in the realm of the recently introduced exacting and ultraexacting cardinals, which are among the strongest known large cardinals consistent with the axiom of choice.

A non-symmetric binary connective in a logic is connexive iff it verifies Aristotle's Thesis and Boethius' Thesis. The latter definition can be made precise in several ways; however, none of them make any of the classical connectives connexive.

Initially, connexivity was understood as a property of implication, and several propositional logics were introduced to show how one can make implication connexive in a non-trivial way. One of them is logic C, originally introduced in [1], which is a close relative of Nelson's logic of strong negation N4 and, in particular, inherits from the latter its constructive character and its relation to the positive fragment of intuitionistic logic IL.

Since connexive theses fail in classical logic, C is contraclassical; in fact, it even proves some negation-inconsistencies despite being non-trivial, so that it is also paraconsistent in a very strong sense.

In this talk, we consider several expansions of the propositional logic C with modal and conditional operators. We will argue that connexivity is the source of all special properties of C and that its modal and conditional extensions, if correct, must reflect the connexivity profile of implication in C.

When considering these extensions we will briefly compare them to similar modal and conditional logics defined on the basis of IL and N4, respectively; we will also see how similar connexivity profiles of the extended logics induce the similarities between them and their base logic C when it comes to properties like constructivity, paraconsistency, and contraclassicality.

References

1. H. Wansing. Connexive modal logic. Advances in Modal Logic 5, 367-383 (2005)

An orthocomplemented lattice (OL) is a bounded lattice equipped with an order-inverting period two complementation. A monadic orthocomplemented lattice (mOL) is an OL equipped with a closure operator, known as a quantifier, whose closed elements form a sub-OL. Janowitz introduced quantifiers on OLs, which were later studied by Harding in the setting of Von Neumann algebras, by Harding, McDonald, and Peinado in the setting of completions and Stone spaces, and by Lin and McDonald in the setting of functional algebras. A cylindric orthocomplemented lattice (cOL) is an expansion of a mOL by means of a family of pairwise commuting quantifiers and a family of constants, known as the diagonal elements, satisfying certain equations. In this talk, I will discuss some recent work on the representation theory of cOLs from the algebraic perspective of completions as well as from the topological perspective of duality theory.

It is first shown that cOLs are closed under MacNeille and canonical completions. In each case, the completion of a cOL A is obtained by forming an associated dual space X that is a cylindric orthoframe. This is a set equipped with an orthogonality relation, a family of binary reflexive transitive relations satisfying certain conditions, as well as a family of distinguished subsets. For the MacNeille completion, X is formed from the non-zero elements of A. For the canonical completion, X is formed from the proper filters of A. The corresponding completion is then obtained by embedding A into the complete cOL of biorthogonally closed subsets of X. With the introduction of a spectral topology on a cylindric orthoframe along the lines of McDonald and Yamamoto, we obtain a dual equivalence between the category of cOLs and the category of cylindric upper Vietoris orthospaces. Time permitting, a topological construction of the canonical completion of a cylindric Boolean algebra will be provided by means of certain cylindric expansions of the upper Vietoris spaces introduced by Bezhanishvili and Holliday.

In the landscape of logics in computer science, Propositional Dynamic Logic (PDL) is a well-known multi-modal calculus used to reason about programs in order to formally verify their correctness. However, standard PDL merely describes the (qualitative) reachability between states, while in practice one may require additional quantitative assessments. Indeed, since computational systems operate under critical constraints on resources (such as time or memory), it is reasonable to consider formal frameworks to reason not only about program execution, but also about program efficiency.

In this talk, I introduce NPDL, a logic which incorporates discrete program costs into the PDL-framework. Here, programs correspond to weighted accessibility relations, where the weights are extended natural number modelling the (least) cost of reaching new states via program executions. Naturally, the sequential composition (and iteration) of programs is defined treating addition of natural numbers as cost combination. Thinking of 'cost zero' as standard accessibility and 'infinite cost' as standard inaccessibility, the program constructs of NPDL generalise those of standard PDL.

As a main result, I show that NPDL is decidable. The proof is basd on an adequate weighted adaptation of the (Fischer-Ladner) filtration technique. Other interesting questions about NPDL (e.g., completeness, complexity, interpolation, ...) remain, as of yet, open.

Conditionals are propositions expressed by natural language expressions of the form "if A then B", formalized as a binary operator (A > B) on top of a classical logical language. They have been a cornerstone in philosophy, logic, experimental psychology, and artificial intelligence due to their essential role in making predictions, inferring causal connections, and expressing hypothetical reasoning. In this talk, I will present recent advancements concerning the logic of conditionals and their uncertainty quantification. The presentation is structured into two main parts. In the first part, I will delve into the semantic foundations of conditionals. I will illustrate their equivalent algebraic semantics and the resulting topological dualities which have been recently developed. The main findings focus on the algebraizability (or lack thereof) of a large family of conditional logics, paralleling the algebraic investigation of modal logics. Furthermore, these results allow for a deeper understanding of the model-theoretic properties of relational semantic structures for conditionals, such as Kripke-style and neighborhood semantics. Finally, I will outline recent results on the structure of the lattice of conditional logics, including the characterization of Post-complete logics within this structure. In the second part (time permitting), I will focus on uncertainty quantification, especially the probability of conditionals. I will show how, via basic algebraic methods, we can resolve the long-standing problem of characterizing the probability naturally associated with conditional propositions and their relationship with conditional probability. Along these lines, I will present both characterization results and limitative results concerning what the probability of conditionals cannot be. To conclude, I will draw connections to open problems and possible philosophical applications of this investigation. (Based on joint works with Tommaso Flaminio, Sara Ugolini, Stefano Bonzio, Lluis Godo, Yale Weiss.)

The Finite Embeddability Property states that each algebra in a given class locally embeds, in a precise sense, into a finite algebra in that class. The FEP is perhaps the main algebraic tool for establishing the decidability of the universal theory of some class of algebras. A pair of fundamental results of Galatos and Jipsen from 2013 and 2017, whose proofs rely on the machinery of residuated frames, states that any variety of integral residuated lattices axiomatized by equations in the signature { v, *, 1 } has the FEP, and the same holds for varieties of distributive integral residuated lattices. We show that there is a clean universal algebraic perspective which unifies both of these results, which does not require introducing residuated frames, and which applies more generally to positive universal classes. Namely, each positive universal class of integral residuated algebras closed under nuclear and conuclear images has the FEP. Such positive universal classes (such varieties) can moreover be described syntactically as precisely those axiomatized by positive universal sentences (by equations) in the signature { v, *, 1 }. This yields an isomorphism between the lattice of positive universal classes (varieties) of integral join-semilattice ordered algebras and the lattice of positive universal classes (varieties) of integral residuated algebras closed under nuclear and conuclear images. This provides a precise formulation of the idea that the global structure of the lattice of varieties of integral residuated lattices is determined by the lattice of varieties of integral idempotent semirings.

Feder and Vardi famously conjectured in the nineties that a finite domain constraint satisfaction problem whose constraint relations are chosen from some predetermined template is either NP-complete or solvable in polynomial time. Bulatov, Jeavons, and Krokhin suggested a general algebraic criterion for determining the tractability of a finite domain CSP in terms of the polymorphism algebra of its template. The CSP dichotomy conjecture and the stronger algebraic CSP dichotomy conjecture initiated a fertile area of research connecting universal algebra to complexity theory.

While the algebraic dichotomy conjecture was proven true independently by Bulatov and Zhuk in 2017, there are still questions concerning the fine-grained classification of the fixed template CSPs within P, up to logspace reductions. For example, while the famous Bulatov-Dalmau algorithm does show every Maltsev CSP is tractable, it is still an open question whether every Maltsev CSP belongs to the complexity class NC.

By providing a new algorithm, we are able to show that every finite domain fixed template CSP possessing a conservative Maltsev polymorphism belongs to the complexity class Parity L (which is contained in NC), which consists of all problems that can be solved by a Turing machine with a work tape of logarithmic size in the sense that the positive instances of the problem are precisely those where the machine has an even number of accepting computation paths. In fact, conservative Maltsev CSPs are either in L or they are complete for Parity L, so we now have a full complexity classification up to logspace reductions for conservative Maltsev CSP.

This is joint work with Manuel Bodirsky.

I will discuss formalization work aimed at representing fragments of the theory of hereditarily finite sets in Isabelle/HOL. We have tried to collect and systematize some known facts and features of the theory, sometimes referred to as ZFfin. The focus of attention was on several principles of finiteness, which can be shown to be equivalent in certain contexts, and several ways of spelling out regularity, which again can be shown to be so equivalent. Isabelle/HOL provided a method of organizing the material, with fragments of the theory represented using the available locale construct. To render axiom schemata of the theory, an inductive definition of first-order definable predicates has been used. Some independence results have been included by defining suitable models. Joint work with Štěpán Holub.

The canonical extension is a fundamental construction in the algebraic theory of modal logics. It plays a key role in the proof of completeness via canonicity for a large class of axiomatic extensions of the basic normal modal logic, and it has allowed to generalize such results from the classical modal logic to a vast family of non-classical logics. In this talk we will discuss and elaborate on a presentation of canonical extensions as pertaining to a family of algebraic extensions that are parametrized by the sets of meets and joins of the original poset that one wants to preserve; we will discuss how, by varying these sets of meets and joins, different types of maps can be extended in a way that guarantees good properties (such as having adjoints, or preserving meets/joins). We will discuss how other completions such as the Dedekind MacNeille completion fit in this framework and discuss various case-studies. In particular, we will show how this construction can be used for logics such as PDL where certain infinite meets are preserved, and how the parametric notion of canonical extension can be used to generalize completeness results for presentations of PDL with rules with infinite assumptions. Finally, time permitting, we will discuss how these constructions can be generalized to the context of quantale-enriched categories.

Regular varieties have been extensively studied in universal algebra, notably by J. Płonka, A. B. Romanowska, J. D. H. Smith, and C. Bergman, among others. More recently, S. Szawiel and M. Zawadowski developed a categorical approach to regular varieties via Lawvere theories. In this talk, we explain how regular varieties can be characterized in categorical terms. We then introduce a functorial version of the Płonka sum, refining Zawadowski’s construction, and prove a categorical analogue of the Płonka decomposition theorem. This is joint work in progress with Alexander Kurz.

Gödel modal logics are defined via Gödel Kripke models, which generalize classical Kripke semantics by allowing truth values in the unit interval [0,1], both for propositional valuations at each world and for the accessibility relation. The minimal modal logics associated with Gödel Kripke models have been thoroughly studied in [2,3], while the corresponding logics over classical (crisp) Kripke frames, with a crisp accessibility relation, were investigated in [4]. Although these logics are known to be decidable, they generally fail to satisfy the finite model property with respect to their intended semantics.

In this talk, we provide axiomatizations for the modal logics determined by finite Gödel Kripke models. We treat both the case of models with a valued accessibility relation, as considered in [2], and the case of classical Kripke models, as in [4]. This resolves an open problem in the literature, for which only a partial solution had previously been proposed in [1]. We also show that the resulting axiomatization does not coincide with a conjecture put forward in [3], and we present some additional results concerning models complete with partially witnessed properties.

Ongoing joint work with Ricardo Rodriguez, from UBA.

[1] Ferrari, M., Fiorentini, C., Rodriguez, R.O. A Gödel Modal Logic over Witnessed Crisp Models. Proceedings of TABLEAUX 2025. LNCS, vol 15980.
[2] X. Caicedo and R.O. Rodriguez. Standard Gödel modal logics. Studia Logica, 94(2):189–214, 2010.
[3] X. Caicedo and R.O. Rodriguez. Bi-modal Gödel logic over [0,1]-valued Kripke frames. Journal of Logic and Computation, 25(1):37–55, 2015.
[4] R.O. Rodriguez and A. Vidal. Axiomatization of Crisp Gödel Modal Logic. Studia Logica, 109(2):367-395, 2021.

Unbounded Łukasiewicz logic Lu is a substructural logic that combines features of infinite-valued Łukasiewicz logic with those of Abelian logic. The logic is finitely strongly complete w.r.t. the additive l-group on the reals expanded with a distinguished element -1. In this talk, we show that satisfiability in Lu is NP-complete. We achieve this by constructing a polynomial-time translation to the satisfiability of existential formulas in standard Łukasiewicz logic. Our main technical tools will be linear programming and the Tseitin transformation.

Cylindric algebras, introduced by A. Tarski, J. D. Monk, and L. Henkin, provide an algebraic framework for classical first-order logic. The investigations of structures of cylindric algebras by R. Maddux, H. Andréka, I. Németi, I. Sain, R. Hirsch, and I. Hodkinson have led to deep results on representability, finite axiomatizability, game-theoretic constructions, and more. The close connection between logic and cylindric algebras naturally raises the question of how to algebraize non-classical first-order logics. In this talk, we study cylindric ortholattices and weakening cylindric algebras, with particular emphasis on their construction and representability. We also investigate their connections with polyadic ortholattices and weakening polyadic algebras. This talk is based on joint work with Joseph MacDonald and Peter Jipsen.

The field of intuitionistic modal logic (IML), originating in the 1940s, has evolved into two primary traditions: one (often called "intuitionistic modal logic") focused on meta-logical properties, and another (often called "constructive modal logic") driven by applications in computer science. In this talk we will first briefly survey this developmental landscape and then introduce and investigate a new variant in the IML family called FIK, that is a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We present a sound and complete Hilbert-style axiom system for FIK, then propose a proof-theoretic framework called bi-nested sequent calculus that provides both a decision procedure and a direct counter-model extraction from any failed derivation. With this calculus, we obtain decidability and finite model property of FIK. Furthermore, we demonstrate how to restrict the nesting level of the bi-nested calculus to obtain a "shallow" (1-level nested, single type of nesting), label-free sequent calculus for the logic. The shallow calculus enjoys the cut-elimination property and provides a good complexity bound for the logic's decision problem. Time permitting, we will also discuss how the bi-nested calculus serves as a unified and modular proof-theoretic framework for many other variants of IML. This talk is mainly based on joint work with Philippe Balbiani, Çiğdem Gencer and Nicola Olivetti.

The relationships between various forms of interpolation for propositional logics and amalgamation for classes of algebraic structures have received considerable attention in the literature in the frameworks of model theory, abstract algebraic logic, universal algebra, and residuated structures. A well-known theorem states that a variety with the congruence extension property (CEP) has the amalgamation property (AP) if and only if it has the deductive interpolation property (DIP). This “bridge theorem” provides a powerful technique for establishing the deductive interpolation property via the amalgamation property, and vice versa. However, for varieties that lack the congruence extension property, failure of the amalgamation property does not necessarily imply failure of the deductive interpolation property. For example, the varieties of ℓ-groups and residuated lattices do not have the AP, but since they also lack the CEP, the status of the DIP is open for these cases.

To provide a route to developing a more systematic understanding of deductive interpolation, we will review the different solutions found in the literature to the problem of describing an algebraic property that corresponds directly to the DIP. We will also introduce a property weaker than the congruence extension property that, when combined with the deductive interpolation property, is equivalent to the amalgamation property. Finally, we will present an effective algorithm for deciding whether a congruence-distributive variety, generated by a given finite set of finite algebras, has the DIP.

This is joint work with Wesley Fussner, George Metcalfe and Simon Santschi.

This is a joint work with Wesley Fussner. We show that there are exactly five quasivarieties of Sugihara algebras with the amalgamation property, and that all of these have the relative congruence extension property. As a consequence, we obtain that the amalgamation property and transferable injections property coincide for arbitrary quasivarieties of Sugihara algebras. These results provide a complete description of arbitrary (not necessarily axiomatic) extensions of the logic R-mingle that have the Maehara interpolation property, and further demonstrates that the Robinson property and Maehara interpolation property coincide for arbitrary extensions of R-mingle.

In 1959, Stanley Tennenbaum proved that there are no computable nonstandard models of Peano Arithmetic. In 1964, John Shepherdson showed that there are computable nonstandard models of Peano axioms with the induction schema restricted to quantifier-free formulas. In the 1980s and 90s, much work in the model theory of arithmetic was devoted to the problem of determining the limits Tennenbaum's theorem. In my talk, I will discuss some of these developments and present a general model-theoretic framework for studying the Tennenbaum phenomenon based on applications of the notions recursive saturation and resplendence.

In contemporary developments of first-order relevant logics and (propositional) relevant modal logics, several limitations and challenges have emerged, both from a semantic standpoint (particularly concerning relational models) and from a proof-theoretic one (especially in sequent calculi). The aim of this talk is threefold.
(i) To outline the current state of the debate on first-order relevant logics and relevant modal logics, highlighting, on the one hand, significant proof-theoretic limitations and, on the other, recent semantic advances, particularly the Goldblatt-Mares–Ferenz–Tedder line of work.
(ii) To propose possible approaches to the proof theory of first-order relevant logics, employing labeled sequent calculi to construct systems with admissible Cut that enable a modular treatment of the class of relevant logics under consideration (joint work with N. Ferenz); and to suggest how a similar strategy might be extended to relevant modal logics, which, at the relational level, introduce an additional layer of complexity, being characterized not only by the usual ternary relation for implication but also by one or more binary relations for the modal operators.
(iii) To discuss the (dis)advantages of adopting “external” rather than “internal” calculi, and to explore how, in future developments of this work, one might move — via some suitable translation procedures — toward calculi devoid of “explicit” semantic components within their syntax. This concluding discussion will not be confined to the proof theory of relevant logics but will adopt a broader perspective, informed by both earlier and recent developments in the proof theory of non-classical logics.

Formal Concept Analysis (FCA) is a mathematical framework widely used in Knowledge Representation and Reasoning to study conceptual hierarchies. In FCA, concepts are represented as pairs of objects and features, corresponding to the extension and intension of concepts, and together they form a complete lattice. By Birkhoff's representation theorem, every complete lattice can be represented in this way. Consequently, the logic of formal concepts can be understood as the logic of lattices. This logic, along with its modal extensions and their connection to FCA, has been actively studied in recent years. However, to capture realistic forms of reasoning, it is essential to formalize defeasible reasoning on concepts.

In this talk, I present a generalization of KLM-style defeasible reasoning to the conceptual framework. Specifically, the framework introduces different notions of defeasible inclusion—forms of inclusion that typically hold by default but may be overridden by exceptions in the extension, intension, or both—by generalizing the cumulative reasoning system and the cumulative reasoning system with a loop to the conceptual setting. Furthermore, we extend cumulative models, cumulative ordered models, and preferential models to the conceptual domain and establish soundness and completeness results for these generalized models.

Profinite modal algebras are monadic over Set. This monadicity result suggests that profinite modal algebras could be presented as Lindembaum algebras for propositional theories in infinitary versions of propositional modal calculi. In fact, it is possible to identify such calculi as modal extensions of Maheara-Takeuti’s infinitary extension of the sequent calculus LK. Correspondences between syntactic properties of the calculi and regularity/exactness properties of the opposite category of profinite modal algebras can be established.

Propositional Dynamic Logic (PDL) is a well-known modal logic for reasoning about non-deterministic programs and Game Logic (GL) can be seen as a generalisation from programs to 2-player games. Such logics combine modal reasoning with an algebra of operations on their semantic structures, a perspective which was abstracted into the framework of coalgebraic dynamic logic in [1,2]. State-based structures are modelled as F-coalgebras for some Set-endofunctor F, while modalities are interpreted by natural transformations called predicate liftings. The work [1,2] heavily relies on the assumptions that F is a monad and that operations/tests/modalities are defined in accordance with this monad. However, various (recent) examples of dynamic logics such as Instantial PDL [3] and many-valued variants of PDL [4] do not meet these requirements.

In this talk, we present a broader framework for coalgebraic dynamic logics lifting all the above-mentioned restrictions and, among others, present extensions of the main results of [1] therein. Here, the signature functor F is not required to be a monad, our coalgebraic logic may have countably many types of modalities and furthermore may be fuzzy/many-valued (taking values in an arbitrary FLew-algebra). In particular, this allows us to encompasses the dynamic logics considered in [3,4] into the coalgebraic framework.

First, we describe the general notions of coalgebra operations and tests and identify conditions ensuring them to be safe, i.e., preserving bisimulation/behavioural equivalence. We introduce reducible coalgebra operations and tests, entailing the soundness of certain reduction axioms, and show that reducibility always implies safety. For finitely-valued logics, we proceed to show that if all operations and tests are reducible then one-step completeness of the underlying coalgebraic modal logic implies strong completeness of its dynamic version. This generalises the main results of [1], and with concrete instantiations we obtain, e.g., strong completeness for a many-valued variant of iteration-free game logic and for two-valued iteration-free PDL with weighted accessibility relations.

This talk is based on joint work with Helle Hansen [5].

References:

[1] H.Hansen, C.Kupke, R.Leal: 'Strong Completeness for Iteration-Free Coalgebraic Dynamic Logics', TCS, 2014.
[2] H.Hansen, C.Kupke: 'Weak Completeness of Coalgebraic Dynamic Logics', FICS, 2015.
[3] J.van Benthem, N.Bezhanishvili, S.Enqvist: 'A propositional dynamic logic for instantial neighborhood semantics', Studia Logica, 2019.
[4] I.Sedlár: 'Finitely-valued Propositional Dynamic Logic', AiML, 2020.
[5] H.Hansen, W.Poiger: 'Safety and strong completeness via reducibility for many-valued coalgebraic dynamic logics', to appear in CALCO, 2025.

Mundici's representation of MV-algebras as intervals in Abelian lattice-ordered groups was a landmark result in a number of ways. Besides its key role in the theory of MV-algebras, it sparked the search for further representations of ordered algebras arising in non-classical logic by means of partially ordered groups (po-groups), with the aim of leveraging the extensively studied theory of po-groups to understand these wider (and wilder) classes of algebras. Two notable results in this direction are the representation due to Galatos & Tsinakis of GMV-algebras as so-called nuclear images of certain submonoids of lattice-ordered groups, and the representation due to Dvurečenskij & Vetterlein of so-called pseudo-effect algebras as intervals in po-groups. In this talk, we show that in the project of representing ordered monoidal structures in terms of pogroups, the class of so-called integrally closed po-monoids plays a central role. On the one hand, they are precisely the algebras representable as nuclear images of submonoids of po-groups. This vastly extends the previous representation results in this direction, showing in particular that every integral po-monoid arises from a po-group. On the other hand, they also form the basic building blocks of a different construction, which decomposes a (sufficiently well-behaved) po-monoid into a family of subalgebras associated with its positive idempotent elements.

The idea of associating a non-classical logic with the Hilbert-space model of quantum mechanics goes back to the early days of the development of this physical theory. The success has been modest. Propositions about a quantum physical system correspond to the closed subspaces of a complex Hilbert space and hence their inner structure may be described by an orthomodular lattice. There are calculi that are reasonably called logics of orthomodular lattices. However, a convincing logic doing justice to the canonical model has not been found. Rather, undecidability results have become known.

The situation is different if one replaces the framework of logic by the framework of category theory. More specifically, what we propose is to consider a dagger category whose objects are orthosets and whose morphisms are adjointable maps between them. The notion of an orthoset is entirely built on the notion of orthogonality, which in turn stands for mutual exclusion. As in logic, we deal with the interrelations between objects that are to be interpreted as Hilbert spaces. Orthoclosed subspaces, which model yes-no properties in quantum logic, correspond to dagger monomorphisms. Sasaki projections, which interpret in certain quantum logics the implication connective, correspond in the categorical approach to adjoints of inclusion maps. The conjunction of mutually exclusive propositions in quantum logics might finally be seen as corresponding to the formation of categorical biproducts.

In the talk, we shall present five non-technical assumptions about a dagger category of orthosets that characterise uniquely the standard model of quantum mechanics.

In this talk, I will present a description of finitely generated free algebras in certain finitely generated varieties of commutative BCK-algebras. The construction relies on homomorphisms from free commutative BCK-algebras to free ŁBCK-algebras that extend the insertion of generators, allowing us to draw on existing results. A key step involves analyzing valuations and their equivalence classes, which leads to a precise count of the elements of the free algebras and a full structural characterization. In the final part of the talk, I will outline some ongoing work and open questions concerning the axiomatization of subvarieties of commutative BCK-algebras.

Beginning in the 1970s, Peter Cameron generalized the classical problem of counting the orbits of a finite group action by considering actions on countable sets. These actions naturally give rise to infinite sequences of integers, including many classical sequences. The asymptotic behavior of these sequences was conjectured to be tightly constrained, falling into narrow bands with large gaps. We will indicate the proofs of these conjectures and their fundamental connection to model theory.

The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning. Joint work with Andreas Lööw, Philippa Gardner, et al. (Imperial College London).

A fruitful research programme in the study of residuated lattices has been to take inspiration from results about lattice-ordered groups and extend them to wider classes of residuated lattices. Two important classes for this purpose are the variety of GBL-algebras and its subvariety of GMV-algebras, which significantly extend the variety of lattice-ordered groups while still preserving some group-like behavior. One classical result about ordered groups which has been extended in this way is Hölder's theorem. This theorem is an abstract characterization of the totally ordered groups which embed into the additive ordered group of reals R as precisely the Archimedean ones (i.e. those which lack infinitesimal elements). In their study of the Archimedean property in residuated lattices, Ledda, Paoli and Tsinakis recently extended Hölder's theorem to an abstract characterization of algebras which embed either into the reals R, or into the negative cone of the reals R-, or into the standard MV-chain [0, 1] as precisely the so-called strongly simple GBL-algebras. In the present joint work with Luca Spada, we further extend Hölder's theorem beyond the residuated setting, obtaining an abstract characterization of the dense submonoids of the totally ordered monoids R, R-, and [0, 1].

We investigate the problem of providing relevance properties for first order logics by expanding on recent work concerning relevance as topical in propositional relevant logics. We propose a theory of topic for first order languages, relying on the use of focus markers in an extension of the usual first order language, and suggest how such an enrichment of the language and conceptual apparatus of the logic can provide avenues into the first order relevance problem.

Quantitative extensions of equality characterize the degree of approximation between objects. Fuzzy proximity and similarity relations are notable examples of such extensions. These and similar relations are used to model concepts such as vagueness, uncertainty, imprecision, and imperfection. Various approaches to formalizing quantitative information have led to the development of well-known logical, algebraic, and topological formalisms and structures, such as fuzzy logic, rough logic, metric algebras, quantitative algebras, metric and proximity spaces, etc.

Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are prominent examples that play a crucial role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Our algorithms solve unification and anti-unification problems modulo fuzzy tolerance relations (i.e., reflexive and symmetric but not necessarily transitive), allowing mismatches between symbol names and arities. We will discuss the general principles behind these techniques, provide examples, present some of the algorithms, and characterize their properties.

An ortholattice is a bounded lattice equipped with an order-inverting involutive complementation. A monadic ortholattice is an ortholattice equipped with a closure operator, known as a quantifier, whose closed elements form a sub-ortholattice. Monadic ortholattices generalize monadic Boolean algebras - the algebraic model of the classical predicate calculus in a single variable. Janowitz [3] first considered quantifiers on orthomodular lattices, and Harding [1] studied them, as well as cylindric ortholattices, for their connections to von Neumann algebras, in particular, to subfactors.

We show that the variety of monadic ortholattices is closed under MacNeille and canonical completions. In each case, the completion of A is obtained by forming an associated dual space X that is a monadic orthoframe. This is a set equipped with an orthogonality relation and an additional binary relation satisfying certain conditions. For the MacNeille completion, X is formed from the non-zero elements of A, and for the canonical completion, X is formed from the proper filters of A. In either case, the corresponding completion of A is then obtained as the complete ortholattice of bi-orthogonally closed subsets of X with an additional operation defined through the binary relation on X. With the introduction of a spectral topology on a monadic orthoframe along the lines of McDonald and Yamamoto [4], we obtain a dual equivalence between the category of monadic ortholattices and homomorphisms and the category of monadic upper Vietoris orthospaces and certain continuous frame morphisms. The duality presented here is obtained in ZF independently of the Axiom of Choice. This talk is based on joint work with John Harding and Miguel Peinado [2].

[1] Harding, J.: Quantum monadic algebras. Journal of Physics A: Mathematical and Theoretical. Vol 55 (2023)
[2] Harding, J., McDonald, J., Peinado, M.: Monadic ortholattices: completions and duality. Forthcoming in Algebra Universalis (2025)
[3] Janowitz, M.: Quantifiers and orthomodular lattices. Pacific Journal of Mathematics. Vol 13 (1963)
[4] McDonald, J., Yamamoto, K.: Choice-free duality for orthocomplemented lattices by means of spectral spaces. Algebra Universalis. Vol. 83 (2022)

NP languages coincide by Fagin's theorem to certain classes of structures axiomatisable in a certain fragment of second-order logic. The NP vs. coNP problem may then be expressed as a logical problem, without use of complexity theory's terminology. The problem of closure with respect to complementation may then be studied on a hierarchy of fragments of second-order logic --- this has been, however, resolved only for the first two members of said hierarchy.

In this talk, I will characterize the polyadic algebras arising from algebraic implicative predicate logic, and prove a functional representation theorem. Then I will address the categorical formulation for non-classical polyadic algebras.

We consider two expansions of Gödel logic with two versions of paraconsistent negation. The first one is G_inv — the expansion with an involuitive negation ~_i defined via v(~_iA)=1-v(A). The second one is G^2 --- an expansion with a so-called ‘strong negation’ ¬. This logic utilises two independent valuations on [0,1] — v_1 (positive support) and v_2 (negative support) that are connected via ¬. Two valuations in G^2 can be combined into one valuation v on [0,1]^⟕ — the twisted product of [0,1] with itself — with two components v_1 and v_2. The two logics are closely connected but do not coincide since the set of values of G^2 is not ordered linearly. Our main goal is to study different entailment relations in G_inv and G^2 that are induced by filters on [0,1] and [0,1]^⟕, respectively. In particular, we determine the exact number of such relations in both cases, establish whether any of them coincide with the entailment defined via the order on [0,1] and [0,1]^⟕, and obtain their hierarchy. We also construct reductions of filter-induced entailment relations to the ones defined via the order.

Quantitative models and quantitative analysis in Computer Science are receiving increased attention. The goal of this talk is to investigate quantitative automata and quantitative logics. Weighted automata on finite words have already been investigated in seminal work of Schützenberger (1961). They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory. We investigate weighted automata and their relationship to weighted logics. For this, we present syntax and semantics of a quantitative logic; the semantics counts ‘how often’ a formula is true in a given word. Our main result, extending the classical result of Büchi, shows that if the weights are taken from an arbitrary semiring, then weighted automata and a syntactically defined fragment of our weighted logic are expressively equivalent. A corresponding result holds for infinite words. Moreover, this extends to quantitative automata investigated by Henzinger et al. with (non-semiring) average-type behaviors, or with discounting or limit average objectives for infinite words.

We study the connection between the form of the primitive rules of a proof system and the rules the system admits. We introduce a general and syntactically defined family of sequent-style calculi over the modal language and its fragments as an approximate formalization for "constructively acceptable" systems. We call these calculi constructive and show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules. This means that there exists a polynomial-time algorithm that, given a proof of the premise of a Visser’s rule, provides a proof for its conclusion. As a positive application, we establish the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK, and their extensions by the modal axioms T, B, 4, 5, and the axioms for bounded width and depth, and propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus.

Isabelle is a generic proof assistant that allows axiomatization of arbitrary object logic, the most widely used of which is HOL. The talk will be an introduction in Isabelle/HOL. I will briefly sketch its history and mention my motivation for using it in an ongoing project of formalization of combinatorics on words. The main part of the talk will be a live session illustrating how some design features of Isabelle/HOL are reflected in user's work. Time permitting, these will include the distinction between meta-logic and the object logic, polymorphic simple types, higher order unification, (non-existence of) proof terms, design of proof tactics, and construction of verified algorithms.

It is a well-known fact that Abelian logic has no finitary extensions (which is equivalent to the fact that the quasivariety of Abelian l-groups has no notrivial subquasivariety). In this talk we will try to axiomatize all semilinear (infinitary) extensions of Abelian logic. Alternatively, we will try to provide an axiomatization for all semilinear prevarieties of abelian l-groups. The strategy we will try to use is as follows: For a subdirectly irreducible chain C, we find a generalized quasiequation E such that for any Abelian l-group A we have: E does not hold in A if C is embeddable in A.

We explore the problem of explaining observations from a classically inconsistent theory by adopting a paraconsistent framework. In particular, we consider theories formulated in the languages of the Belnap—Dunn logic and its implicative expansion. The solutions are then given in one of the two further expansions of BD: BD○ that introduces formulas of the form ○ϕ (‘the information on ϕ is reliable’) and BDΔ that augments the language with Δϕ's (‘there is information that ϕ is true’). We show that explanations in BD○ and BDϕ are not reducible to one another. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) depending on the language of the solution and on the language of the theory. In addition, we consider the complexity of abductive reasoning in the Horn fragment of the implicative extension of BD. The talk is based on the joint work with Meghyn Bienvenu and Katsumi Inoue.

In a dynamic vision, in which mathematics is seen as a human product, one moves from a given truth to a careful handling of acquired information. So the foundation is intuitionistic (Law of Excluded Middle is not assumed) to distinguish positive existence, predicative (Power Set Axiom is not assumed) to distinguish sets constructed from below from collections, effective (Axiom of unique Choice is not assumed) to distinguish operations with explicit instructions from functions. Adopting this minimalist foundation in practice brings out some deep underlying structures of topology, such as logical duality between closed and open, symmetry between points and observables, continuity as a commutative square, etc., that were previously hidden by too strong assumptions. Topology in the proper sense is obtained by adding a module of convergence to these basic structures. In this way, richer notions are obtained so that, for example, it can be proved that there is an embedding of the category of concrete spaces, with points, into that of positive topologies, which are pointfree. This brings to solution an issue that has been open for more than half a century, It turns out that topology plays a central role for all mathematics, since it allows one to distinguish real, or computational, aspects from ideal, or infinitary ones. Since points are usually determined by an infinite amount of information, in order to maximize the computational, or real, aspects of mathematics, pointfree topology must be developed as much as possible. Ideal aspects are introduced locally and explicitly as ideal points and spaces over a positive topology. The most important structures in mathematics, such as real numbers, Zariski topology, etc., are obtained as ideal spaces over a positive topology. A lot of future work remains: primarily, to expand the mathematics expressible in this way as much as possible and to develop a proof assistant based on the minimalist foundation.

Epistemic logics formalise reasoning about agents' epistemic attitudes, such as knowledge and belief, towards the occurrence or non-occurrence of events. Similarly, epistemic probability logics formalise reasoning about epistemic attitudes towards the probability of events. One of the most important epistemic probability logics studied in the literature is Fagin and Halpern's PS5 (Fagin and Halpern, 1994), which extends the standard multi-agent epistemic logic S5 with probability operators expressing linear combinations of probabilities of events. In this work-in-progress talk, we outline an alternative approach to combining epistemic logics with probability, based on modal fuzzy logic. Our work aims at extending the results of a recent paper by Baldi, Cintula and Noguera (2020), who showed that there are mutual translations between the propositional fragment of PS5 and the fuzzy logic of probability introduced by Hájek et al. (2000), based on propositional Łukasiewicz logic. Our aim is to determine whether there are similar translations linking richer fragments of PS5, including modal operators, and fuzzy probability logics based on modal Łukasiewicz logic.

We consider the fragment of Second-Order unification, referred to as Second-Order Ground Unification (SOGU), with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert's 10th problem is reducible to a necessary condition for SOGU unifiability if the signature contains a binary function symbol and two constants, thus proving undecidability. This generalizes known undecidability results, as either first-order variable occurrences or multiple second-order variables were required for the reductions. Furthermore, we show that adding the following restriction:(i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has bounded congruence, results in a decidable fragment. The latter fragment is related to bounded second-order unification in the sense that the number of bound variable occurrences is a function of the problem structure. We conclude with a discussion concerning the removal of the bounded congruence restriction. Joint work with Julian Parsert.

Finite model theory's main focus is in the study of logics that have close connections to descriptive complexity. One of the main tools to show e.g. inexpressibility of certain logics are model comparison games, such as the Ehrenfeucht--Fraisse, pebble, and bisimulation games. The main idea behind game comonads comes from the observation that plays in a typical model comparison game can be encoded into a semantics construction which, moreover, admit the structure of a comonad on the category of relational structures. This allows one to treat model comparison games abstractly, in the language of category theory. In this talk, I give an overview of the game comonad programme, its recent development and open problems. Concretely, I will list the most notable game comonads and explain their relationship with various logic fragments. I will also overview the recent model-theoretic results proved in this framework. I shall also explain how the various different model comparison games can be viewed as an instance of a game in arboreal categories, which are used to axiomatise common features of Eilenberg--Moore categories of coalgebras of game comonads.

The literature on residuated lattices (RLs) contains a number of results describing the lattice reducts of some variety V of RLs. Such results frequently state either that every lattice is a subreduct of some RL in V (for example, if V is the variety of commutative RLs or of cancellative RLs) or that the lattice subreducts are precisely the distributive lattices (for example, if V is the variety of l-groups or of Heyting algebras). We improve on existing results of this form in two ways. Firstly, we consider pointed lattice subreducts (subreducts in the signature expanded by the constant 1 for the multiplicative unit), which gives us more fine-grained information about where exactly a sublattice can occur. Typical properties of interest whose statement requires the signature of pointed lattices are conicity and distributivity at 1. Secondly, instead of considering particular varieties of RLs, we treat semi-K and pre-K RLs uniformly, where K ranges all over positive universal classes of pointed lattices contained in a certain variety. For example, we show that every prelinear RL is distributive and that every preconic RL is distributive at 1. The description of the pointed lattice subreducts of RLs and of CRLs is left as an open problem.

In Abelian logic, the reduced models are lattice-ordered Abelian groups. We will focus on three important linear models of Abelian logic: integers, rational numbers and real numbers. These three structures are indistinguishable using finitary rules, but can be separated using infinitary rules. In this talk, we will focus on finding these rules and discuss properties of the corresponding generalized quasivarieties.

The logical underpinnings of quantum mechanics have been the subject of sustained interest since Birkhoff and von Neumann’s pioneering work in the 1930s, but progress has been impeded by the difficulty of several fundamental questions in the area, most notably issues connected to decidability. However, recent years have seen the emergence of a new approach that situates quantum logic within the substructural paradigm, opening the possibility of applying totally new techniques. In this talk, we will discuss these recent trends, report on some important progress arising from this perspective, and identify some open remaining questions.

It is a well-known fact that although the poset of open sets of a topological space is a Heyting algebra, its Heyting implication is not necessarily stable under the inverse image of continuous functions and hence is not a geometric concept. This leaves us wondering if there is any stable family of implications that can be safely called geometric. In this talk, we will first introduce an abstract notion of implication as a binary modality and investigate its basic properties and possible representations. Then, we will use a weaker version of categorical fibrations to define the geometricity of a category of pairs of spaces and implications over a given category of spaces. We will characterize all geometric categories over a given category S, provided that S has some basic closure properties. Specifically, we will show that there is no non-trivial geometric category over the full category of spaces.

In this work-in-progress talk I begin the discussion of relevance properties available in first-order logics. I explore the philosophical motivation for many first-order variants of the Variable Sharing Property, and show of some logics whether or not they satisfy these properties. Future mathematical and philosophical directions are outlined.

We show that while standard first-order inductive logic is not decidable, a large class of inferences in objective Bayesian inductive logic is decidable. Decidability is achieved by reducing the general inference problem to a quantifier-free problem. We show that for any inference if the quantifier-free reduction of the premisses is satisfiable, then the original inference is decidable. We also consider inferences with infinitely many premisses and explore some properties of the logic.

An idempotent semifield is an idempotent semiring such that its multiplicative reduct is a group. In this talk I will present several results about equational theories of idempotent semifields. The results include that no non-trivial class of idempotent semifields has a finitely based equational theory; that there are continuum-many equational theories of idempotent semifields; and that the equational theory of the class of all idempotent semifields is co-NP-complete. This is joint work with George Metcalfe.

Although the prime object of study for structural proof theory is proof calculi (especially analytic ones), it has many applications to important logical properties, such as conservativity, consistency, decidability, complexity, interpolation, etc. In my talk, I will present some recent successes in solving long-time open problems by proof-theoretic means, including the Lyndon interpolation property for Gödel logic (intermediate logic of linear frames) and the decidability of (bimodal) intuitionistic S4.

First Order Modal Logic (FOML) extends First Order Logic (FO) with modal operators. FOML is suitable for many applications including planning, predicate epistemic logics among others. However, FOML is computationally unfriendly. Most of the decidable fragments of FO that are decidable (like the two variable fragment, guarded fragment, restriction to unary predicates) become undecidable when extended with modal operators. Until recently, the only known decidable fragment of FOML was the monodic fragment. In this talk we will discuss some new and interesting decidable fragments of FOML and its variants that we have identified. This talk includes some of the results from the speaker's PhD thesis (supervised by R. Ramanujam) and some results in collaboration with Mo Liu, R. Ramanujam and Yanijing Wang.

"Interpolation" refers to a cluster of fundamental metalogical properties with applications spanning hardware and software verification, databases, and many other areas. In this talk, we survey the state of the art on interpolation in substructural logics, focusing in particular on big-picture features that shed some light on the nature of interpolation generally. We will also discuss some of the most important remaining open questions and on-going efforts to solve them.

In propositional Boolean logic, maximum satisfiability (MaxSAT) problem can be viewed as a generalization of the SAT problem. An input to the SAT problem is a CNF formula (a list of clauses) and the question is whether there is an assignment that satisfies all of them. MaxSAT is an optimization problem, namely to determine the maximum number of satisfied clauses in the list, over all assignments. Our work addresses the MaxSAT problem problem for a list of arbitrary formulas in the language of propositional Łukasiewicz logic, over the semantics provided by the MV-algebra on the real interval [0,1]. First we reduce the MaxSAT problem to the SAT problem in the same semantics. This provides a classification against which other approaches to the problem can be compared. Then we define a tableau-like method that eventually yields one or more systems of linear constraints, similar to the earlier approaches of Hähnle or Olivetti. This is joint work with Felip Manya and Amanda Vidal, presented at Tableaux 2023.

Adding connexive theses to relevant logics has the unsavoury result of allowing one to prove every negated implication. In this talk, I'll diagnose this problem, and consider some avenues by which this result can be avoided.

In this talk, we investigate connections between the family of comparative logics including Abelian logic, and some generalizations of Łukasiewicz logic. We provide axiomatizations for some extensions of pointed Abelian logic including unbound Łukasiewicz logic. We show the importance of the semilinearity property and we present the discrete versions of unboud Łukasiewicz logic. This talk is based on joint work with Marta Bílková, Petr Cintula and Carles Noguera.

The semantic framework for representing questions known as inquisitive semantics is based on a relation of support relating formulas and information states (modeled as sets of possible worlds). In my talk I will discuss two ways of fuzzifying inquisitive semantics. The first one replaces crisp information states with fuzzy information states (modeled as fuzzy sets of possible worlds). The second one replaces the crisp notion of support with a notion of fuzzy support. I will show some properties of the resulting framework. For example, I will show that if we fuzzify inquisitive semantics in these two different directions, we obtain an abstract and very general version of a principle known from the basic inquisitive semantics as Truth-Support Bridge. I will also sketch some open questions related to this approach.

A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a telephone call wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition, given a finite number of agents, is that all agents are experts. We report on research investigating the termination condition that all agents know that all agents are experts. If agents only exchange secrets, there is no knowledge of the time, and no knowledge of the protocol, even stronger termination conditions are unreachable. Furthermore, n-2 + (n choose 2) calls are optimal to reach this epistemic goal. Although it is easy to come up with schedules achieving this, it is remarkably non-trivial to show that they are optimal.

Some references:

1. Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Pierre Régnier: The epistemic gossip problem. Discrete Mathematics 342(3), pp 654-663, 2019.
2. Hans van Ditmarsch, Malvin Gattinger, Rahim Ramezanian: Everyone Knows that Everyone Knows: Gossip Protocols for Super Experts. Studia Logica, to appear, 2023. https://doi.org/10.1007/s11225-022-10032-3
3. Hans van Ditmarsch, Malvin Gattinger: The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable. Proceedings of WoLLIC, pp 237-249, 2022.

One of the major open problems in classical proof complexity is to prove super-polynomial lower bounds on the length of proofs in Frege (aka Hilbert-style) systems, or equivalently, sequent calculus or natural deduction. Interestingly, exponential lower bounds are known for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubeš (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that the presence of disjunction is essential for these lower bounds, but Jeřábek (2017) adapted them to the purely implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon–Boppana). In this talk, I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene’s slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege. One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also older exponential lower bounds on constant-depth proofs), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon–Boppana circuit lower bound.

This talk will be a tutorial of a known technique on computing uniform interpolants by examining finite (or finitely generated) algebras and their extensions. We will focus on intermediate logics, but the method is reasonably general.

The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set L of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from L, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic and we prove some upper and lower bounds for the positive equality-free fragment. The partial results are sufficient, e.g., for all extensions of the latter fragment. This is a joint work with Kristina Asimi and Silvia Butti.

In this talk, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid? Our answer is positive for the Split rule as well as for its newly proposed generalized versions.

Proofs are more than just validations of theorems; they can contain interesting mathematical information like bounds or algorithms. However this information is frequently hidden and proof transformations are required to make it explicit. One such transformation on proofs in sequent calculus is cut-elimination (i.e. the removal of lemmas in formal proofs to obtain proofs made essentially of the syntactic material of the theorem). In his famous paper ``Untersuchungen ueber das logische Schliessen'' Gentzen showed that for cut-free proofs of prenex end-sequents Herbrand's theorem can be realized via the midsequent theorem. In fact Gentzen defined a transformation which, given a cut-free proof p of a prenex sequent S, constructs a cut-free proof p' of a sequent S' (a so-called Herbrand sequent) which is propositionally valid and is obtained by instantiating the quantifiers in S. These instantiations may contain interesting and compact information on the validity of S. Generally, the construction of Herbrand sequents requires cut-elimination in a given proof p (or at least the elimination of quantified cuts). The method CERES (cut-elimination by resolution) provides an algorithmic tool to compute a Herbrand sequent S' from a proof p (with cuts) of S even without constructing a cut-free version of p. A prominent and crucial principle in mathematical proofs is mathematical induction. However, in proofs with mathematical induction Herbrand's theorem typically fails. To overcome this problem we replace induction by recursive definitions and proofs by proof schemata. An extension of CERES to proof schemata (CERESs) allows to compute inductive definitions of Herbrand expansions (so-called Herbrand systems) representing infinite sequences of Herbrand sequents, resulting in a form of Herbrand's theorem for inductive proofs.

Often, for a propositional logic L, some one-variable fragment of L's first order extension corresponds to some modal logic on L. For the relevant logic R, it seems that the one-variable fragment of RQ (the stronger of R's two standard first-order extensions) corresponds to the modal relevant logic RS5 (the S5ish axiomatic extension of R which contains classical S5 in translation). This talk is a work in progress showing this equivalence. One direction of the equivalence is obtained by transforming first-order models into modal models. The other direction is (almost) obtained by evaluating all of RQ in a particular modal model. I also discuss some philosophical upshots/consequences of this result.

Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.

By limiting the range of the predicate variables in a second-order language one may obtain restricted versions of second-order logic such as weak second-order logic or definable subset logic. In this note we provide an infinitary strongly complete axiomatization for several systems of this kind having the range of the predicate variables as a parameter. The completeness argument uses simple techniques from the theory of Boolean algebras. This is joint work with John L. Bell (see https://arxiv.org/abs/2207.02709).