Unless stated otherwise, all talks will take place in Seminar Room 228 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.
Schedule
Date  Time  Speaker  Title 

20.02.2020  11.00  12.00  Johannes Marti  University of Amsterdam  Unification in coalgebraic modal logics 
27.02.2020  10.15  10.45  Nathanael Glauser  University of Bern  Amalgamation in varieties of semilinear commutative idempotent residuated lattices 
11.00  12.00  Lídia del Rio  ETH Zürich  Inadequacy of Modal Logic in Quantum Settings  
05.03.2020  11.00  12.00  Aloïs Rosset  EPFL, Lausanne  BlackersMassey Theorem from the perspective of homotopy type theory 

11.00  12.00  David Lehnherr  University of Bern  How to prevent chaos  An introduction to model verification 
23.04.2020  11.00  12.00  George Metcalfe  University of Bern  From lgroups to lmonoids and back again 
29.04.2020  16.00  17.00  Igor Sedlar  Czech Academy of Sciences  Finitelyvalued Propositional Dynamic Logic 
07.05.2020  11.00  12.00  Nenad Savic  University of Bern  Nonclassical Reasoning with Justifications 
13.05.2020  16.00  17.00  Petr Cintula  Czech Academy of Sciences  How much Propositional Logic Suffices for Rosser’s Essential Undecidability Theorem? 
20.05.2020  16.00  17.00  Olim Tuyt  University of Bern  A realvalued modal abelian logic 
27.05.2020  16.00  17.00  Vit Puncochar  FLU CAS and ICS CAS, Prague  Inquisitive Heyting algebras 
Abstracts
Unification in coalgebraic modal logics
Johannes Marti
In this talk I present a characterization of the unification problem in coalgebraic modal logics in terms of the existence of a morphism between onestep coalgebras.
The unification problem is the following decision problem: Given two terms in the free algebra of some variety, is there a substitution under which they are equal? In the work presented in this talk we consider the unification problem for varieties whose free algebras are the syntactic algebras of coalgebraic modal logics. We apply ideas from Ghilardi's characterization of the substitution in the theory of normal forms to reformulate the unification problem on the level of the onestep coalgebras that are dual to the onestep algebras approximating the free algebra. The advantage of this approach is that in many interesting cases the points of onestep coalgebras are finite treelike objects and the unification problem becomes a combinatorial problem about these trees.
We consider three instances of this characterization:
 We obtain a new proof of the decidability of unification for the modal logic (Alt1), which was originally established by Balbiani and Tinchev. (Alt1) is the modal logic of the class of frames in which every world has at most one successor. With our characterization the decidability of unification in this logic follows from a simple pumping argument.
 As a variation on the previous example we consider the logic over frames in which every world has exactly one successor that is labeled with either 0 or 1. In this case the unification problem can be reformulated as the question whether there exists a graph homomorphism from some de Bruijn graph into a graph given in the input. So far, we have not been able to establish whether this problem is decidable or not.
 An important motivation for developing our characterization is that the modal logic K can be presented as a coalgebraic modal logic. Despite considerable efforts the decidability of unification in K is an open question.
Amalgamation in varieties of semilinear commutative idempotent residuated lattices
Nathanael Glauser
In this talk we will investigate the amalgamation property for subvarieties of the variety of semilinear commutative idempotent residuated lattices (SemCIdRL). For this we will introduce a structure theorem and several lemmas. We will also describe all finitely generated subvarieties of SemCIdRL with the amalgamation property.
Inadequacy of Modal Logic in Quantum Settings
Lídia del Rio
In Proceedings QPL 2018, arXiv:1901.09476
We test the principles of classical modal logic in fully quantum settings. Modal logic models our reasoning in multiagent problems, and allows us to solve puzzles like the muddy children paradox. The FrauchigerRenner thought experiment highlighted fundamental problems in applying classical reasoning when quantum agents are involved; we take it as a guiding example to test the axioms of classical modal logic.
In doing so, we find a problem in the original formulation of the FrauchigerRenner theorem: a missing assumption about unitarity of evolution is necessary to derive a contradiction and prove the theorem. Adding this assumption clarifies how different interpretations of quantum theory fit in, i.e., which properties they violate.
Finally, we show how most of the axioms of classical modal logic break down in quantum settings, and attempt to generalize them. Namely, we introduce constructions of trust and context, which highlight the importance of an exact structure of trust relations between agents. We propose a challenge to the community: to find conditions for the validity of trust relations, strong enough to exorcise the paradox and weak enough to still recover classical logic.
In this talk, we will in addition include an introduction to quantum measurements, aimed at logicians, mathematicians and philosophers of science unfamiliar with the quantum formalism.
BlackersMassey Theorem from the perspective of homotopy type theory
Aloïs Rosset
The BlakersMassey Theorem is an important result of homotopy theory, expressing the high connectivity of a specific map going into the pullback of a pushout. Homotopy type theory is a field which combines type theory and homotopy theory, proposing a refreshing point of view about constructing and studying mathematics. The presentation will be about getting an overview of this theory and the tools needed to understand the theorem.
How to prevent chaos  An introduction to model verification
David Lehnherr
Could you image a world where nothing works as intended?
In this talk, we will motivate the usage of model verification
for designing cyberphysical systems. Once we are convinced
that modelchecking is needed, we will transfer our problem
to a logical framework.
The main result of this talk is, that we can indeed decide whether
something works as intended. In order to establish this result,
we will make use of infinite automata and linear temporal
time logic (LTL).
From lgroups to lmonoids and back again
George Metcalfe
(joint work with Almudena Colacito and Nikolaos Galatos)
Removing the inverse operation from any latticeordered group (lgroup), such as the ordered additive group of integers, produces a distributive latticeordered monoid (lmonoid), but clearly not every distributive lmonoid admits an lgroup structure. In particular, every lgroup embeds into an lgroup of automorphisms of some chain and is either trivial or infinite, whereas every distributive lmonoid embeds into a possibly finite lmonoid of endomorphisms of some chain.
In this talk, we will see that inversefree abelian lgroups generate only a proper (infinitely based) subvariety of the variety of commutative distributive lmonoids, but inversefree lgroups generate the whole variety of distributive lmonoids. We will also see that the validity of an lgroup equation can be reduced to the validity of a (constructible) finite set of distributive lmonoid equations, yielding  since the variety of distributive lmonoids has the finite model property — an alternative proof of the decidability of the equational theory of lgroups.
Finitelyvalued Propositional Dynamic Logic
Igor Sedlar
We study a manyvalued generalization of Propositional Dynamic Logic where both formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite residuated lattice. One natural interpretation of this framework is related to reasoning about costs of performing structured actions. We prove that PDL over any finite residuated lattice is decidable. We also establish a general completeness proof for a class of PDLs based on commutative integral residuated lattices.
Nonclassical Reasoning with Justifications
Nenad Savic
In the talk, one line of research during my PhD in Bern will be presented, namely the results of the following three papers:
 Z. Ognjanovic, N. Savic, and T. Studer. Justification logic with approximate conditional probabilities. LORI 2017, Sapporo, Japan, September 1114, 2017, Proceedings, pages 681686, 2017.
 D. Doder, Z. Ognjanovic, N. Savic, and T. Studer. Incomplete Information and Justifications, Submitted to: TbiLLC 2019, 1620 September, 2019, Batumi, Georgia, Conference proceedings
 N. Savic and T. Studer. Relevant justification logic. Journal of Applied Logics  IfCoLoG Journal of Logics and their Applications, 6(2):395410, 2019.
How much Propositional Logic Suffices for Rosser’s Essential Undecidability Theorem?
Petr Cintula
In this talk we explore the following question: how weak can a logic be for Rosser’s essential undecidability result to be provable for a weak arithmetical theory? It it well known for intuitionistic logic and Robinson’s Q, and Petr Hájek proved it in fuzzy logic BL for Grzegorczyk’s variant of Q which interprets the arithmetic operations as nontotal nonfunctional relations.
We present a proof of essential undecidability in a much weaker substructural logic and for much weaker arithmetic theory, a version of Robinson’s R (with arithmetic operations also interpreted as mere relations). Our result is based on structural version of the undecidability argument introduced by Kleene and we show that it goes well beyond the scope of the Boolean, intuitionistic, or fuzzy logic.
A realvalued modal abelian logic
Olim Tuyt
In this talk we study a manyvalued modal logic, with connectives interpreted in the additive group of the real numbers and an S5modality. This logic can be viewed as the modal counterpart of the onevariable fragment of a (monadic) firstorder realvalued logic. A class of monadic abelian lgroups, in the same spirit as monadic Heyting algebras and monadic MValgebras, is introduced. We then prove a functional representation theorem for this class of algebras, using amalgamation in the class of linearly ordered abelian lgroups. From this, we deduce a completeness theorem for the manyvalued modal logic.
Inquisitive Heyting algebras
Vit Puncochar
In my talk I will explore a class of inquisitive Heytingv algebras as algebraic structures that are isomorphic to algebras of finite antichains of bounded implicative meet semilattices. I will show that these structures are suitable for algebraic semantics of inquisitive superintuitionistic logics, i.e. logics of questions based on intuitionistic logic and its extensions. I will explain how questions are represented in these structures (prime elements represent declarative propositions, nonprime elements represent questions, join is a questionforming operation) and provide several alternative characterizations of these algebras. For instance, it will be shown that a Heyting algebra is inquisitive if and only if its prime filters and filters generated by sets of prime elements coincide and prime elements are closed under relative pseudocomplement. We prove that the weakest inquisitive superintuitionistic logic is sound with respect to a Heyting algebra iff the algebra is what we call a homomorphic pimage of some inquisitive Heyting algebra. It is also shown that a logic is inquisitive iff its LindenbaumTarski algebra is an inquisitive Heyting algebra.