Pozvánka na seminář
Pozvánka na přednášku: TBA
@04.11.2026 16:00
Pozvánka na přednášku: Relevance and interpolation via binary nested sequents
@21.10.2026 16:00
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.
Pozvánka na přednášku: Interpolation without equality
@14.10.2026 16:00
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.
Pozvánka na přednášku: Potential infinity in alternative set theory
@07.10.2026 16:00
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.
Pozvánka na přednášku: Sequent Calculi for Semiring Semantics (in person talk)
@08.07.2026 16:00
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.
Pozvánka na přednášku: Displaying First-Order Relevant Logics
@01.07.2026 16:00
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.
Pozvánka na přednášku: Algebraic Semantics for Real-Valued Pointed Modal Logic
@24.06.2026 16:00
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.
Pozvánka na přednášku: Amalgamation for lower-involutive idempotent semilinear residuated lattices
@17.06.2026 16:00
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.
Pozvánka na přednášku: Representing dynamics in logic: from models to proof
@11.06.2026 16:00
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.
Pozvánka na přednášku: From implicit to explicit definability in algebra and logic
@10.06.2026 16:00
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
Pozvánka na přednášku: Model-theoretic properties up to Vopěnka's Principle and beyond
@03.06.2026 16:00
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.
Pozvánka na přednášku: On connexivity in modal and conditional contexts (online)
@27.05.2026 16:00
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)
Pozvánka na přednášku: MacNeille Completion, Canonical Completion, and Duality for Cylindric Orthocomplemented Lattices
@13.05.2026 16:00
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.
Pozvánka na přednášku: Decidability of PDL, but at what cost?
@29.04.2026 16:00
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 based 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.
Pozvánka na přednášku: Conditionals: where do we stand?
@15.04.2026 16:00
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.)
Pozvánka na přednášku: Finite embeddability via nuclear and conuclear images
@25.03.2026 16:00
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.
Pozvánka na přednášku: Fine grained analysis of conservative Maltsev CSP
@18.03.2026 16:00
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.
Pozvánka na přednášku: Formalizing fragments of ZFfin in Isabelle/HOL
@11.03.2026 16:00
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.
Pozvánka na přednášku: Parametric canonical extensions
@25.02.2026 16:00
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.
Pozvánka na přednášku: On Regular Lawvere Theory
@28.01.2026 16:00
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.
Pozvánka na přednášku: On the logics of finite Gödel Kripke models
@14.01.2026 16:00
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.
Pozvánka na přednášku: Complexity of Unbounded Łukasiewicz logic
@07.01.2026 16:00
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.