Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules

TL;DR

This paper explores linear temporal logic based on intransitive time, focusing on representing knowledge, and addresses decidability and admissibility of inference rules in such frameworks.

Contribution

It introduces methods to determine decidability and rule admissibility in intransitive linear temporal logic, a novel approach in temporal logic research.

Findings

Decidability established for non-uniform intransitive temporal logic

Admissibility of inference rules solved for uniform intransitive temporal logic

Open problems for future research are identified

Abstract

Our manuscript studies linear temporal (with UNTIL and NEXT) logic based at a conception of intransitive time. non-transitive time. In particular, we demonstrate how the notion of knowledge might be represented in such a framework (here we consider logical operation NN and the operation UNTIL (actually, the time overall) to be directed to past). The basic mathematical problems we study are the fundamental ones for any logical system - decidability and decidability w.r.t. admissible rules. First, we consider the logic with non-uniform non-transitivity, and describe how to solve the decidability problem for this logic. Then we consider a modification of this logic - linear temporal logic with uniform intransitivity and solve the problem of admissibility for inference rules. A series of open problems is enumerated in the concluding part of the paper.