Уақыт логикасы және оның қолданылуы

System for representing and reasoning about time
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something"). It is sometimes also used to refer to tense logic, a modal logic based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians. Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. Such a statement can conveniently be expressed in a temporal logic.

Consider the statement "I am hungry". Though its meaning is constant in time, the statement's truth value can vary in time. Sometimes it is true, and sometimes false, but never simultaneously true and false. In a temporal logic, a statement can have a truth value that varies in time—in contrast with an atemporal logic, which applies only to statements whose truth values are constant in time. This treatment of truth value over time differentiates temporal logic from computational verb logic. Temporal logic always has the ability to reason about a timeline. So called "linear time" logics are restricted to this type of reasoning. Branching time logics, however, can reason about multiple timelines. This permits in particular treatment of environments that may act unpredictably. To continue the example, in a branching time logic we may state that "there is a possibility that I will stay hungry forever", and that "there is a possibility that eventually I am no longer hungry". If we do not know whether or not I will ever be fed, these statements can both be true.

Łoś’s logic was published as his 1947 master’s thesis Podstawy Analizy Metodologicznej Kanonów Milla (The Foundations of a Methodological Analysis of Mill’s Methods). His philosophical and formal concepts could be seen as continuations of those of the Lviv–Warsaw School of Logic, as his supervisor was Jerzy Słupecki, disciple of Jan Łukasiewicz. The paper was not translated into English until 1977, although Henryk Hiż presented in 1951 a brief, but informative, review in the Journal of Symbolic Logic. This review contained core concepts of Łoś’s work and was enough to popularize his results among the logical community. The main aim of this work was to present Mill's canons in the framework of formal logic. To achieve this goal the author researched the importance of temporal functions in the structure of Mill's concept. Having that, he provided his axiomatic system of logic that would fit as a framework for Mill's canons along with their temporal aspects.

Burgess gives a Meredith translation from statements in TL into statements in first order logic with one free variable 0 (representing the present moment). This translation is defined recursively as follows:

where is the sentence with all variable indices incremented by 1 and is a one place predicate defined by .