tenslogik

Tense logic, or tenslogik, is a branch of modal logic that studies temporal relations by using operators that refer to the past and the future. The basic language extends propositional logic with temporal operators such as P for the past and F for the future. Some formulations also include H (historically) and G (globally) to quantify over all past or future moments.

Semantics: A model for tense logic consists of a set of time points with a linear order, together with a valuation of propositional variables at each point. A formula Pφ is true at a time t if there exists a time t' < t with φ true at t'. Fφ is true at t if there exists t' > t with φ true at t'. Hφ is true at t if φ is true at all times t' < t, and Gφ is true at t if φ is true at all times t' > t. The operators are dual in the sense that Fφ is equivalent to not P not φ, and Gφ is equivalent to not H not φ.

Variants: Linear-time temporal logic (LTL) uses a single timeline and often includes additional operators such as X (neXt) and U (until) to express properties over sequences. Branching-time temporal logic (CTL and related logics) allows multiple possible futures from a given moment, enabling reasoning about different potential courses of time.

History and usage: Tense logic originated with the work of Arthur N. Prior in the mid-20th century and has influenced both philosophical and linguistic analyses of time as well as practical applications in computer science. It provides a formal framework for specifying and verifying temporal properties in systems, programs, and protocols, and it remains a foundational concept in the study of temporal semantics.