First-order transitional modal logics of quasiary predicates with equality

In this paper we study new classes of program-oriented logical formalisms of the modal type – first-order transitional modal logics (TML) of quasiary predicates with equality. Modal logics are successfully used for describing and modeling various subject areas. Epistemic logics are used to describe artificial intelligence, information, and expert systems. Temporal logics are used for modeling complex dynamic systems, program specification and verification. Traditional modal logics are based on classical predicate logic. However, such logic insufficiently accounts for the incompleteness, partiality and structuredness of information about the subject area. These limitations necessitate the development of new, program-oriented modal logical formalisms; this underscores the relevance of the proposed paper. We consider pure first-order TML of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Two types of such logics can be distinguished: TMLQ≡ with strong equality predicates ≡х, and TMLQ= with weak equality predicates =ху. A feature of these logics is the use of the extended renomination composition. For quantifier elimination in TMLQ≡, special total indicator predicates Ez are used, while in TMLQ= the partial indicator predicates are =zz. Transitional modal systems (TMS) form the semantic basis of TML. For TMLQ≡ and TMLQ= important varieties of such systems are specified: general (GMSQ≡ and GMSQ=), temporal (TmMSQ≡ and TmMSQ=), and multimodal (MMSQ≡ and MMSQ=). We describe semantic models and languages of these TMS and examine the properties related to equality predicates. Four types of consequence relations in TMS and logical consequence relations on sets of formulas specified with states are considered: irrefutability (IR), truth (T), falsity (F), and strong (TF). The properties of replacement of equals in TMLQ≡ and TMLQ= are described. The properties of logical consequence relations on sets of formulas specified with states are the semantic basis for the further construction of the corresponding sequent type calculi.