Monotone tense logic

17 Nov 2023

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:

• means that φ is the case in the past
• means that φ has always been the case
• means that φ will be the case in the future
• 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:

1. Philosophical: what does it mean if the modal operators are monotone? How can we think about this?
2. Proof theoretic: how does the move from normal to monotone modal operators affect the proof theory of the logic?
3. 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.

Contact

Jim de Groot: jim.degroot@anu.edu.au

Ian Shillito: ian.shillito@anu.edu.au

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.