• counterpart semantics
• linear temporal logic
• logic
• proof system
• quantified temporal logic
• semantics

First-Order Linear Temporal Logic (FOLTL) is the extension of the well-known propositional Linear Temporal Logic with first-order quantification. Its interpretation is classically over Kripke-frames, that is, a set of time-points or worlds and an accessibility relation, the properties of which determine the axioms of the logic. However, such interpretation suffers limitations, since it requires restrictions on the accessibility relation between worlds. We introduce a novel semantics for FOLTL based on counterpart relations, i.e. families of partial homomorphisms between algebras. This approach overcomes most limitations, completely removing the trans-world identity problem and thus streamlining the modeling of dynamic creation, deletion and merging of entities. We also provide the logic with a Hilbert-style deductive system, and we conclude with consideration about completeness, decidability and possible extensions.