Spring Semester 2020

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

Schedule

Abstracts

In this talk I present a characterization of the unification problem in coalgebraic modal logics in terms of the existence of a morphism between one-step 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 one-step coalgebras that are dual to the one-step algebras approximating the free algebra. The advantage of this approach is that in many interesting cases the points of one-step coalgebras are finite tree-like objects and the unification problem becomes a combinatorial problem about these trees.

We consider three instances of this characterization:

1. 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.
2. 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.
3. 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.

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.

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 multi-agent problems, and allows us to solve puzzles like the muddy children paradox. The Frauchiger-Renner 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 Frauchiger-Renner 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.

The Blakers-Massey 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.

Could you image a world where nothing works as intended? In this talk, we will motivate the usage of model verification for designing cyber-physical systems. Once we are convinced that model-checking 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).

(joint work with Almudena Colacito and Nikolaos Galatos)

Removing the inverse operation from any lattice-ordered group (l-group), such as the ordered additive group of integers, produces a distributive lattice-ordered monoid (l-monoid), but clearly not every distributive l-monoid admits an l-group structure. In particular, every l-group embeds into an l-group of automorphisms of some chain and is either trivial or infinite, whereas every distributive l-monoid embeds into a possibly finite l-monoid of endomorphisms of some chain.

In this talk, we will see that inverse-free abelian l-groups generate only a proper (infinitely based) subvariety of the variety of commutative distributive l-monoids, but inverse-free l-groups generate the whole variety of distributive l-monoids. We will also see that the validity of an l-group equation can be reduced to the validity of a (constructible) finite set of distributive l-monoid equations, yielding --- since the variety of distributive l-monoids has the finite model property — an alternative proof of the decidability of the equational theory of l-groups.

We study a many-valued 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.

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 11-14, 2017, Proceedings, pages 681-686, 2017.
• D. Doder, Z. Ognjanovic, N. Savic, and T. Studer. Incomplete Information and Justifications, Submitted to: TbiLLC 2019, 16-20 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):395-410, 2019.

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 non-total non-functional 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.

In this talk we study a many-valued modal logic, with connectives interpreted in the additive group of the real numbers and an S5-modality. This logic can be viewed as the modal counterpart of the one-variable fragment of a (monadic) first-order real-valued logic. A class of monadic abelian l-groups, in the same spirit as monadic Heyting algebras and monadic MV-algebras, is introduced. We then prove a functional representation theorem for this class of algebras, using amalgamation in the class of linearly ordered abelian l-groups. From this, we deduce a completeness theorem for the many-valued modal logic.

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, non-prime elements represent questions, join is a question-forming 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 p-image of some inquisitive Heyting algebra. It is also shown that a logic is inquisitive iff its Lindenbaum-Tarski algebra is an inquisitive Heyting algebra.