A strongly complete axiomatization of intuitionistic temporal logic

摘要

In this paper, we consider the logic ITLe, a variant of intuitionistic linear temporal logic that is interpreted over the class of dynamic Kripke frames. These are bi-relational structures of the form W, less than or similar to, f where less than or similar to is a partial order on W and f : W - W is a less than or similar to-monotone function. Our main result answers a question recently raised by Boudou et al. (2017, A decidable intuitionistic temporal logic. In Computer Science Logic 2017, pp. 14:1-14:17. Vol. 82 of LIPIcs) about axiomatizing this logic. We provide an axiomatization of ITLe and prove its strong completeness with respect to the class of all dynamic Kripke frames. The proposed axiomatization is infinitary; it has two derivation rules with countably many premises and one conclusion. It should be mentioned that ITLe is semantically non-compact, so no finitary proof system for this logic could be strongly complete.