Relevant Seminars

RSS

Seminar Talk Announcement

  • Wolfgang Poiger (Institute of Computer Science, Prague):

    Coalgebraic dynamic logic (re-)visited

    28.05.2025 16:00Room 318 (zoom) @ Institute of Computer Science
    Pod Vodárenskou věží 2
    Praha, 182 00
    Applied Mathematical Logic Seminar

    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.

  • Thomas Vetterlein (Johannes Kepler University Linz):

    Quantum logic, dagger categories, and the basic model of quantum physics

    30.05.2025 16:00Room 318 (zoom) @ Institute of Computer Science
    Pod Vodárenskou věží 2
    Praha, 182 00
    Applied Mathematical Logic Seminar

    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.

Past Talks