The logic of time is a subfield of logic that is of interest to philosophers, computer scientists and mathematicians alike. It played an important role in the development of modal logic, and it continues to be used in theoretical computer science and in many applications.
Tense logic
The logical study of time was initiated by Arthur Prior, who called it tense logic to reflect the different tenses of natural language. Tense logic is a normal modal logic with four modal operators:
- Pφ means that φ is the case in the past
- Hφ means that φ has always been the case
- Fφ means that φ will be the case in the future
- Gφ means that φ is always going to be the case
The project
We investigate what happens if we weaken the conditions on the modal operators. Technically, we assume that they are monotone, but not normal. (You will learn what all means in the project.) We can approach this from three directions:
- Philosophical: what does it mean if the modal operators are monotone? How can we think about this?
- Proof theoretic: how does the move from normal to monotone modal operators affect the proof theory of the logic?
- Semantic: what are suitable models to interpret the logic?
Prerequisites
This project is all about (modal) logic, so it will be useful if you have done the Logic Course (COMP2620) and possibly the Overview of Logic and Computation (COMP4630). You will need a strong background in maths.
Background material
During the project we will use (some of) the following books and articles. You can have a look at them to see if it looks interesting to you.
- Müller, Tense or Temporal Logic
- Blackburn, de Rijke & Venema, Modal Logic
- Pacuit, Neighborhood Semantics for Modal Logic
- Hansen, Monotone Modal Logics
Contact
Jim de Groot: jim.degroot@anu.edu.au
Ian Shillito: ian.shillito@anu.edu.au