The Research On Temporal Logic With "Now" Operator

The technical analysis of the “now” logic originated from Hans Kamp.He proposed the two dimensional semantics to explain the "now" operator in the note sent to Arthur Prior,and opened up a study of multi-dimensional operators.Kamp and Prior conducted frequent communications within a month,then Prior proposed a hybrid temporal logic of “now” by adding the nominal “?’’ into the hybrid temporal language to indicate “now”.Kamp continues to use two dimensional semantics to study the redundancy of “now” operator and the construction of axiomatic system in temporal propositional logic and temporal predicate logic.Patrick Blackburn reconstructs the tableau system and axiomatic system of hybrid temporal logic of “now”,which based on Prior’s work by replacing the global operator with satisfying operator.By adding “Kamp Rule” to the logic,logical and contextual validity have been linked,and the completeness of the systems was respectively proved by using two-dimensional semantics and pointed semantics.This paper sorts out the research of "now" logic and prove that the "now" operator is redundant in the temporal propositional logic.Introduction: Introduce the research background and research status.Chapter 1: Briefly Introducing Temporal Logic and hybrid temporal logicChapter 2: A Brief Account of Prior’s analysis of "now",and his work on hybrid temporal logicChapter 3: A brief description of Blackburn’s work on the connection between logic and contextual validity in hybrid temporal logic of "now".Chapter 4: Explain the redundancy of "now" operator in temporal propositional and predicate logic,proves that the "now" operator is redundant in the temporal propositional logic.Conclusion...