I am open to supervise projects on modal logic and duality theory, including bachelor and master projects. Broadly speaking, I am interested in non-classical logic (where either the modalities or the propositional base logic is non-classical, or both), duality theory, bisimulations, and more. Below is a non-exhaustive list of possible projects.
If you're interested in learning more about a particular topic in modal logic, we can pick a textbook to follow. TBC
Non-distributive positive logic is a logic with propositions letters, true, false, and binary connectives meet and join. In the literature one can find various types of frame semantics for this logic:
Polarities. Non-distributive positive logic can be interpreted in polarities, which are a two-sorted analogue of Kripke frames. This means that a frame consists of two sets and a binary relation between them. In this type of semantics, formulas are interpreted in so-called Galois-stable sets, which are certain special subsets of the frame. More information can be found, for example, in this paper.
Semilattice semantics. Another type of semantics is given by meet-semilattices with a top element. Formulas are interpreted as filters. This gives rise to a non-standard interpretation of joins, which ensures non-distributivity. Details of this type of semantics can be found in Section 3.2 of this paper.
Doubly ordered sets. Lastly, we can also interpret the logic in doubly ordered sets. These are sets equipped with two partial orders. While not explicitly formulate, this idea arises from a representation of lattices using doubly ordered sets.
The goal of this project is to compare these various semantics. Explicitly:
Learn how "non-distributive positive logic" can be defined.
Understand how formulas are interpreted in the various types of semantics.
Compare the semantics: can we turn one type of frame into another type? For example, given a polarity, can we find a semilattice frame that (dis)satisfies the same formulas?
Ockham algebras are distributive lattices D with a weak negation operator ~ : D → D that satisfies
~(x ∧ y) = ~x ∨ ~y
~(x ∨ y) = ~x ∧ ~y
~0 = 1
~1 = 0
The idea of the project is to investigate positive logic with an additional operator ~ that satisfies the same property. The weak negation can be viewed as a modal operator, so we can (try to) use tools and techniques from classical modal logic. A duality already exists. It is expected that we can give it frame semantics by means of a poset with an order-reversing function. A state x in (a model based on) such a frame (X, ≤, g) satisfies the formula ~φ if and only if g(x) does not satisfy φ. In this setting, we can try to define and prove analogues of the following theorems:
Sahlqvist correspondence and Sahlqvist canonicity.
Bisimulation, saturated frames, and a Hennessy-Milner theorem.
An analogue of the Van Benthem characterisation theorem.
This project is suitable for those who already know or who would like to learn about the theorems mentioned above (in the context of classical modal logic) and then want to try to adapt them to a different setting.
Modal meet-implication logic is the extension of the meet-implication fragment of intuitionistic logic with modal operators. It can be interpreted in semilattice semantics, see for example this paper. We can define a straightforward notion of Kripke bisimulations between its models. However, it is not cleat whether or not this is the "right" notion of bisimulation. In particular, we can ask if we can obtain:
A Hennessy-Milner style theorem.
An analogue of the Van Benthem characterisation theorem.
If this is not the case, then we may need to adapt the definition of bisimulations for this logic and its semantics, possibly taking inspiration from bisimulations for non-distributive positive logic.
To do
The extension of intuitionistic logic with a conditional operator was recently studied by Weiss, Ciardelli and Liu, and Dufty (link forthcoming). They consider a binary conditional operator that behaves like a normal box in its second argument. But they do not consider a diamond-like implication operator.
The goal of this project is to investigate intuitionistic conditional logic with two types of implication: the box-like implication and the diamond-like implication. We will do so along the lines of Constructive Modal Logic, see for example this paper. This is interesting, because it results in a diamond-like operator that does not preserve joins in its second argument, but is merely monotone. Concrete questions to begin with are:
How do we axiomatise the logic?
Can we provide a sound and complete semantics for this logic?
Is there a philosophical interpretation for the new diamond-like implication?