Non-primitive recursive decidability of products of modal logics with expanding domains

Citations of this article
Mendeley users who have this article in their library.


We show that-unlike products of 'transitive' modal logics which are usually undecidable-their 'expanding domain' relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component-call it the 'flow of time'-is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding over time. (It is known that none of these logics is decidable when interpreted in structures where the second component does not change over time.) The decidability proof is based on Kruskal's tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable (in non-primitive recursive time) if the number of function iterations is assumed to be finite. © 2006 Elsevier B.V. All rights reserved.




Gabelaia, D., Kurucz, A., Wolter, F., & Zakharyaschev, M. (2006). Non-primitive recursive decidability of products of modal logics with expanding domains. Annals of Pure and Applied Logic, 142(1–3), 245–268.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free