| Temporal logics are an important branch of modal logics.With the emergence and development of artificial intelligence,software engineering and model checking,temporal logics are becoming more and more important in computer science.The study subject of this paper is the minimal non-normal temporal logic C2 t,which is obtained by temporizing the minimal non-normal modal logic C2 proposed by E.J.Lemmon.On the minimal non-normal temporal logic C2 t,this paper explores the following five aspects from the perspectives of proof theory,model theory and algebra:1.The Hilbert style axiomatic system HC2 t is established.First,we give the language and semantics for C2 t.The language of C2 t and the language of the minimal normal temporal logic Kt are identical,but we interpret it in regular models.The regular models are models of non-normal modal logics,and the characteristics of regular models are that it can contain some non-normal worlds.Second,we inductively define the notion of a formula being satisfied in a regular model at some point.Different from the classical modal logic is that the true value of a modal formula at a world depends not only on the information of worlds which can be reached from the current world,but also on whether or not the current world is a normal world.Last,we give the axioms and inference rules of HC2 t,and construct its canonical model,and prove the completeness of HC2 t by using the method of canonical model.2.The labelled sequent calculus GC2 t is established.Labelled sequent calculus systems are a new kind of proof systems which occur in recent years.It is characterized by changing the semantics of modal operators into natural deduction rules.First,the concept of sequent is defined,and the axioms and inference rules of GC2 t are given.The inference rules of GC2 t include propositional connectives rules,temporal operators rules and relational rules.Second,it is proved that some structural rules are admissible in GC2 t,such as weakening rules,contraction rules and cut rule,and the most important rule is cut rule.Then,we define the labelled extensions of regular models and prove that GC2t(with respect to the labelled extensions of regular models)is sound and complete.Last,we prove the Decidability of derivations in GC2 t.3.The characterization theorem for the definability of a class of regular models in temporal language is given.Definability is the core problem in model theory and it isthe problem that whether or not a class of models or a property can be defined or expressed in a logical language.First,some relations on regular models are defined,such as the temporal equivalence relation,homomorphism,strong homomorphism and bounded morphism.It is proved that the satisfaction relation is invariant under strong homomorphism and bounded morphism.We prove that the satisfaction relation is invariant under strong homomorphism and bounded morphism.We define the concept of C2t-image finite,and prove that if two regular models are C2t-iamge finite,then the temporal equivalence relation and the C2t-bisimilation on the regular models are equal.Then we define the concept of disjoint unions,generated submodels etc,and prove that if a class of regular models is temporal definable,then it is closed under taking surjective C2t-bisimulations,disjoint unions,and generated submodels.We define the concept of temporal saturation,and prove that the temporal equivalence implies C2t-bisimulation on a class of saturated regular models.We also define the concept of C2t-ultrafilter extensions,and prove that the C2t-ultrafilter extension of any regular model is a saturated regular model,and a definable class of regular models is closed under the C2t-utrafilter extensions.Finally,we prove that a class of regular models is temporally definable if and only if it is closed under taking disjoint unions and surjective C2t-bisimulations and C2t-ultrafilter extensions,while its complement is closed under C2t-ultrafilter extensions.This characterization theorem explains the expressive power of temporal language over regular models.4.The correspondence theory between C2 t language and first order language,and the finite model property of C2 t language is proved.First,we define the C2t's standard translation,and prove that for any temporal formula and its corresponding first order formula under the standard translation are equivalent.At the same time,we use the C2t's standard translation to prove the compactness of the C2 t language.Second,for any regular model we define its filtration through a set of formulas,and prove that for any regular model and any set of formulas with certain properties,we can always find a filtration of the regular model through the set of formulas.Finally,the method of filtration is used to prove that the C2 t language has the finite model property.5.The algebraic semantics for C2 t is established.First,we define the regular temporal algebra,and some basic properties of regular temporal algebras are proved.The complex algebra of the regular frame is defined and the complex algebra of any regular frame is proved to be a regular temporal algebra.This suggests that a regulartemporal algebra can be constructed from a regular frame.We also give the concept of an equation being true in a regular temporal algebra.It is proved that an equation is true in the complex algebra of a regular frame if and only if its corresponding temporal formula is valid in the regular frame.Then,we define the Lindenbaum-Tarski algebra of C2 t,and prove that it is a regular temporal algebra.In a sense,it is a “canonical” regular temporal algebra.We also prove that the equations corresponding to C2t's theorems are true in the Lindenbaum-Tarski Algebra of C2 t and conversely,the temporal formulas corresponding to the equations which are true in the Lindenbaum-Tarski Algebra are C2t's Theorems.Using the above results,we can prove the algebraic completeness of C2t(with respect to regular temporal algebras).Finally,we give a representation theorem for temporal regular algebras.Specifically,we define the ultrafilter frame of a regular temporal algebra,and prove that for any regular temporal algebra it can be embedded into the complex algebra of its ultrafilter frame.At the same time,we also prove that the canonical frame underlying the canonical model of C2 t and the ultrafilter frame of C2t's Lindenbaum-Tarski Algebra are isomorphic.The work of this paper theoretically enriches the existing temporal logic systems,and establishes some important conclusions for C2 t.These conclusions have certain guiding significance in the field of software specification,automatic theorem proving and model checking.Therefore,this study not only has theoretical significance,but also practical value. |
PDF Full Text Request