Czech Society for Cybernetics and Informatics

Seminar Announcement

Talk by Wolfgang Poiger: Coalgebraic dynamic logic (re-)visited

@ Seminar on Applied Mathematical Logic28.05.2025 16:00

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.

Talk by Thomas Vetterlein: Quantum logic, dagger categories, and the basic model of quantum physics

@ Seminar on Applied Mathematical Logic30.05.2025 16:00

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.

Talk by Václav Cenker: Free Algebras in Finitely Generated Varieties of Commutative BCK-Algebras

@ Seminar on Applied Mathematical Logic23.04.2025 16:00

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.

Talk by Sam Braunfeld: Orbit-counting for groups acting on countable sets

@ Seminar on Applied Mathematical Logic16.04.2025 16:00

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.

Talk by Nicholas Ferenz: Topics, Focus, and Relevance Properties in First-Order Relevant Logic

@ Seminar on Applied Mathematical Logic05.03.2025 16:00

Talk by Temur Kutsia: Symbolic Constraints and Quantitative Extensions of Equality

@ Seminar on Applied Mathematical Logic26.02.2025 16:00

Talk by Joseph McDonald: MacNeille completion, canonical completion, and duality for monadic ortholattices

@ Seminar on Applied Mathematical Logic12.02.2025 16:00

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

Talk by Martin Q. Putzer: Monadic NP Sets

@ Seminar on Applied Mathematical Logic08.01.2025 16:00

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.