(Japan Advanced Institute of Science and Technology)

We will show that the logics based on well-ordered and dually well-ordered linear Kripke frames with constant domains of length up to \omega^\omega can already be separated by the fragments of one monadic predicate symbol.These investigations started from a very simple question:

How much can we express with one monadic predicate symbol over linear order.

More specifically, considering logics over linear Kripke frames with constant domains, we asked ourselves how many separate fragments of one monadic predicate symbol exist. Very early guesses were as low as 4 (`What can we express more than infima and suprema and their order?'). It soon turned out that this was a over-simplification, but although we have now a much better view of the expressive power of monadic predicate symbols over linear oders, we are still far from a full understanding.

Separation is achieved by expressing infima/suprema of arbitrary finite degree, and their orders. While this method is currently restricted to the two cases of well-ordered and dually well-ordered, we expect that by using ordinal notations and extending the classical Cantor-Bendixon rank we can extended the current results to a broader class of Kripke frames.

Robert Recorde Room

Department of Computer Science