The purpose of this paper is to study new classes of program-oriented logical formalisms of the modal type. We propose transitional modal logics (TML) of partial quasiary predicates without monotonicity condition and enriched with equality predicates. The work describes semantic models and languages of pure first-order TML with strong equality predicates, the properties of the equality predicates are given. A feature of these logics is the use of the extended renomination composition. The semantic basis of TML is transitional modal systems (TMS). Important varieties of such systems are specified - general TMS (GMS), temporal TMS (TmMS), multimodal TMS (MMS). The languages of GMS, TmMS and MMS are described, interpretation mappings of formulas on semantic models are defined. The properties of transitional modal systems are considered, the interaction of modal compositions with renominations and quantifiers is investigated. A number of logical consequence relations are determined on sets of formulas specified with states (irrefutability, truth, falsity and strong logical consequence relations). The properties of these relations, in particular, properties related to equality predicates, are described. On the basis of these properties, a construction of sequent type calculi is planned for the proposed logics.
The apparatus of modal logics is used with great success to describe and model various subject
areas and aspects of human activity (see, e.g., [
In this paper we study new classes of program-oriented logical formalisms of modal type – pure first-order transitional modal logics of partial non-monotonic quasiary predicates with equality. Such logics use the extended renomination composition and 0-ary compositions xy (strong equality predicates). Transitional modal systems of these logics (TMS) and their important varieties – general (GMS), temporal (TmMS) and multimodal (MMS) TMS – are described. We specify languages of the introduced systems and present their properties. Special attention is paid to properties related to the strong equality predicates and interaction of quantifiers with modal compositions. For formalization of logical consequence in TML for sets of formulas specified with states, we define irrefutability, truth, falsity and strong logical consequence relations and provide their main properties, in particular, ones related to the equality predicates and elimination of modalities.
To facilitate reading, we will provide the definitions necessary for the further presentation.
Concepts that are not defined here are interpreted in the sense of works [
In this paper, we will follow the notation used in [
Quasiary predicates. Data in the logics of quasiary predicates have a structure of nominative sets. Functions and predicates defined on nominative sets are called quasiary.
A nominative set is a set of named values, i.e. set of pairs (name, value). Formally, a V-Anominative set (V-A-NS) is defined as a single-valued function of the form d :V ® A . We interpret V and A as sets of subject names (variables) and subject values respectively. Next, V-A-NS is presented in the form [v1a1,...,vnan,...]; here vіV, aіA, vі vj when і j. We denote the set of all V-Anominative sets by VA.
– f(d), if the value of f(d) is undefined.
For single-valued functions, we will further write: – f(d), if the value of f(d) is defined, For V-A-NS we introduce operations || Z and ||–Z, where Z V: d || Z {v a d | v Z}; d || Z {v a d | v Z}.
Operation rvx11,,......,,vxnn,,u1,,......,,um :VА ® VA of the extended renomination, where all vi, xi, uj V, and the symbol V means no value, is specified as follows: rvx11,,......,,vxnn,,u1,,......,,um (d) d ||{v1,...,vn ,u1,...,um} [v1 d(x1),..., vn d(xn )].
We introduce an abbreviated notation y for y1,..., yn: instead of rvx11,,......,,vxnn,,u1,,......,,um , we will write rvx,,u. Thus, given d(z), we obtain rvx,,u,,yz (d) rvx,,u,,y (d) and rvx,,u,,z (d) rvx,,u (d).
can be interpreted as one renomination operation called their convolution and denoted by rvy,,z ux,,t. Hence rux,,t (rvy,,z (d )) rvy,,z ux,,t (d).
A partial function of the form Q : VA ® {T , F} is called a V-A-quasiary predicate. Here {T, F} is the set of truth values. In this paper, we will consider modal logics of single-valued quasiary predicates, or P-predicates.
We will denote by PrPV–A the class of V-A-quasiary predicates. Each P-predicate S is determined by two sets: – the truth domain T(S) = {d | S(d) = T}; – the falsity domain F(S) = {d | S(d) = F}.
The single-valuedness of the predicate S means that T(S)F(S) = .
The name хV is unessential for the predicate S, if for all d1, d2 VA we have:
d1 ||–х = d2 ||–х Q(d1) = Q(d2).
The unessentiality of x means that the predicate S is “insensitive” to the data component named x. V-A-quasiary P-predicate S is: – irrefutable (partially true), if F(S) = ; – constantly true (denoted T), if F(S) = and T(S) = VА; – constantly false (denoted F), if T(S) = and F(S) = VА; – totally undefined (denoted Ê ), if T(S) = F(S) = .
P-predicate S is equitone if the conditions S(d) and d d' imply S(d') = S(d).
Therefore, we have three constant P-predicates: T, F, and Ê .
For single-valued predicates, the concept of monotonicity is specified as equitonicity – preservation of the already accepted value after data expansion.
Variable assignment predicates Ez which indicate whether a component with a corresponding name
zV has a value in the input data are used for quantifier elimination in logics of non-monotonic
predicates [
T(z) = {d | d(z)}; F(z) = {d | d(z)}.
Predicates z are total, single-valued, non-monotonic.
Every xV such that x z, is unessential for z.
Equality predicates. In logics of quasiary predicates, two types of equality predicates can be considered: weak (up to definability) equality and strong equality. Weak equality predicates are inherent for logics of monotonic (equitone) predicates, while strong equality predicates are inherent for logics of non-monotonic predicates.
In this work, we consider modal logics of P-predicates without monotonicity restrictions with
strong equality predicates {x,y}. We specify these predicates as follows (see [
T({x,y}) = {d | d(x), d(y) and d(x) = d(y)} {d | d(x) and d(y)},
F({x,y}) = {d | d(x), d(y), d(x) d(y)} {d | d(x), d(y) or d(x), d(y)}.
Further on the predicates {x,y} will be denoted as xy. We will also use the traditional notation x y. Note that xy and yx denote the same predicate!
Predicates {x} – a special case of {x,y} when x and y are the same name – will be denoted by xх (or x x in the traditional form).
Every zV \{x, y} is unessential for xy; every zV \{x} is unessential for xх.
Predicates xy are total single-valued and non-monotonic.
For xх we have T(xx) = VА and F(xx) = , therefore xх is a constant predicate T.
Basic logical compositions. Basic logical compositions of pure first-order modal logics of
quasiary predicates are logical connectives
and , renomination
quantification x. Let us briefly recall their definitions (see [
Renomination composition is specified using a corresponding operation:
Rvx,,u (Q)(d ) Q(rvx,,u (d)) for all dVА.
We define compositions , , x through the truth and falsity domains of the corresponding predicates: T(PQ) = T(P)T(Q); aA
F(P) = T(P); F(PQ) = F(P)F(Q); aA T(xP) = {d | Q(d ||x x a) T};
F(xP) = {d | Q(d ||x x a) F}.
Properties of propositional compositions and quantifiers not related to renominations are similar to the properties of classical logical connectives and quantifiers. Properties associated with renominations are specified as follows:
R) R(Q) = Q; RI) R zz,,vx,,u (Q) Rvx,,u (Q) – convolution of an identical pair of names in renomination; RU) zV is unessential for the predicate Q R zy,,vx,,u (Q) Rvx,,u (Q) ;
R ) given d(z) , then Rvx,,u,,yz (Q)(d) Rvx,,u,,y (Q)(d) and Rvx,,u,,z (Q)(d) Rvx,,u (Q)(d) ; R) Rvx,,u (Q) Rvx,,u (Q); R) Rvx,,u (P Q) Rvx,,u (P) Rvx,,u (Q); RR) Rvy,,z (Rux,,t (Q)) Rvy,,z ux,,t (Q); Ren) given z is unessential for Q then yQ zR y (Q);
z Rs) given y {v , x,u} then yRvx,,u (Q) Rvx,,u (yQ);
R) given z is unessential for Q and z {v , x, u} then Rvx,,u (yP) zRvx,,u yz (P). The quantifier elimination is based on the following properties:
Tv) T (Ruv,,w,,xy (Q)) T ( y ) T (Ruv,,w(xQ)); Fv) F(Ruv,,w(xQ)) T ( y ) F(Ruv,,w,,xy (Q)).
Let the predicate z be denoted by z . Then we have z z = T.
Let us consider properties of equality predicates. Note that the symmetry of equality is virtually technical as xy and yx is the same predicate.
The reflexivity of equality predicates follows from the fact that T(xx) = VА and F(xx) = :
Rf) xx = T, i.e. each xx is a constant predicate T.
The transitivity of equality predicates:
Tr) xy & yz xz = T.
Renomination properties of equality predicates (properties of the R type):
Rxx) Rvw,,u,,xz (xx ) zz ; R0) given x, y {u , v} , then Rvw,,u (xy ) xy ; in particular, given x {u , v}, then Rvw,,u (xx ) xx ; R1) given y {u , v} and x y, then Rvw,,u,,xz (xy ) zy ; R2) Rvw,,u,,xz,,ys (xy ) zs ;
R 1) given y {u , v} and x y, then Rvw,,u,,x (xy ) y ;
R 2) Rvw,,u,,xz,,y (xy ) z ; rp) xy(d) = T Rvw,,u,,zx (Q)(d ) Rvw,,u,,zy (Q)(d ).
elR) xy(d) = T Rvw,,u,,xy (Q)(d ) Rvw,,u (Q)(d).
The substitution of equals in renomination: for all QPrPV–A and dVA we have Derivative property of the elimination of a pair of equals: for all QPrPV–A and dVA we have
The concept of composition nominative modal system [
Composition nominative modal system (CNMS) is an object of the form M = (Cms, Ds, Dns), where: – Cms is a composition modal system (CMS); it defines semantic aspects of the world; – Ds is a descriptive system; it defines a set of standard descriptions Fm – formulas of the CNML language;
– Dns is a denotation system; it determines values of standard descriptions (language formulas) on semantic models; an interpretation mapping Iт of formulas on states of the world is usually used for this.
CMS are relational semantic models. They have the form Cms = (St, R, Pr, C), where: – St is a set of states of the world; – R is a set of relations on St of the form R St Stn; – Pr is a set of predicates on states of the world; – C is a set of compositions on Pr.
Therefore, CNMS can be interpreted as objects M = ((St, R, Pr, C), Fт, Iт).
For the first-order CNMS, a set of states of the world St is specified as a set of algebraic structures = (A, Pr), where A is a set of basic data of the state , Pr is a set of quasiary predicates VA {T, F}, called predicates of the state .
Let us call global the predicates of the form VA {T, F}, where A S
A set of compositions in CNMS is determined by basic logical compositions of the corresponding level and basic modal compositions.
We consider logical connectives and , compositions of extended renomination Rvx,,u , quantification compositions x and special 0-ary compositions – strong equality predicates xy – to be basic logical compositions of pure first-order KNMS with equality.
Transitional modal systems. An important class of CNML, transitional modal logics (TML)
reflect the aspect of change and evolution of subject areas, describing transitions from one state of the
world to another. At the heart of TML lies the concept of transitional modal system [
Transitional modal system (TMS) are CNMS in which the set R consists of relations of the form R St St. We interpret them as state transition relations.
Special cases of TMS are general transitional, temporal and multimodal systems.
TMS in which R consists of a single binary relation and with a basic modal composition ("necessary") are called general (GMS).
TMS in which R consists of a single binary relation and with basic modal compositions ("it will always be the case") and ("it has always been the case") are called temporal (TmMS).
TMS with a set of relations R = {i | iI} and basic modal compositions Mi, iI, in which each i R is matched with a corresponding modal composition Mi, are called multimodal (MMS).
GMS is a special case of MMS, with R consisting of a single relation and a single basic modal composition M identical to .
For GMS, the derivative composition ("possible") is traditionally specified as:
Р means Р.
For MMS, each Mi is identical to with respect to its relation i, iI.
For TmMS, the derivative compositions ("it will sometimes be the case") and ("it was sometime the case") are defined as:
Р means Р; Р means Р.
Further on TMS will be abbreviated denoted M = (St, R, A, Im), where A S GMS languages. Let us describe a language of a first-order GMS with equality. The alphabet: – a set V of subject names (variables); – a set Ps of predicate symbols (language signature); A .
– a set of basic logical compositions’ symbols {, , Rxv,,u , x, xy}; – a set of basic modal compositions’ symbols (modal signature), which consists of one symbol: Ms = {}.
The set Fт of language formulas is determined inductively:
FA) every pPs and every symbol ху is a formula; such formulas are atomic; FP) let and be formulas; then and are formulas;
F) let be a formula, then is a formula.
We will use the derived modal composition , and thus write instead of .
For each pPs, a set of its unessential names is specified using a total mapping : Ps2V. Let us limit ourselves to the set VT V of names unessential for all рPs – called a set of totally unessential names, therefore (р) VT for each рPs. To define sets of guaranteed to be unessential names for formulas, we continue to the mapping : Fт2V as follows: – (ху) = V \{x, y}; – () = (Ф); – () = ()(); – (x) = (){x}; – () = ().
– (Rxv11,,......,,xvnn ,,u1,,......,,um ) ((){v1,...,vn, u1...,um}) \ {xi | vi(), i{1,…, n}}; The pair = (Ps, ) is an extended GMS signature.
A GMS type is determined by an extended signature and properties of the relation . Let us define an interpretation mapping of formulas on states of the world.
First, we specify an interpretation mapping of atomic formulas Im : Рs St Pr, where a condition Iт(p, ) Pr should hold (basic predicates are predicates of states). Compositions’ symbols (in particular, xy symbols) are interpreted as corresponding compositions (in particular, corresponding equality predicates xy). The mapping Im is continued to an interpretation mapping of formulas on states Iт : Fт St Pr as follows:
IP) Iт(, ) = (Iт(, )); Iт(, ) = (Iт(, ), Iт(, )); IR) Im(Rxv,,u (), ) Rvx,,u (Im(, )); T , if Im(, )(d ||x x I) Iт(x, )(d) = F, if Im(, )(d ||x x
else undefined. I ) for each St we set a) T for some a A , a) F for any a A , T , if Im(, )(d ) T for any St : , Iт(, )(d) F , if exists St : and Im(, )(d ) F ,
else undefined.
Given for St there is no such that , then for each dVA we define Iт(, )(d). Note that for abbreviations of formulas of the form , we define the mapping Iт as follows: Iт(, )(d) TF, ,ififeIxmis(ts,)(Sdt):F foraanndyIm(S,t:)(d ) ,T ,
else undefined.
Given for St there is no such that , then for each dVA we define Iт(, )(d). Predicates which are values of formulas that do not use modalities belong to predicates of states. A predicate Iт(, ), which is a value of the formula in the state , is denoted by . A formula is valid on state (denoted |= ), if is a valid (irrefutable) predicate. A formula is valid in GMS M (denoted M |= ), if for each St the predicate is valid.
Let ℳ be a GMS class of a given type. The formula is called ℳ-valid (denoted ℳ |= ), if M |= for all GMS Mℳ.
Depending on conditions imposed on the relation , different classes of GMS can be specified. Traditionally, cases where can be reflexive, symmetric or transitive are considered. In case is reflexive/transitive/symmetric, then we will write the corresponding symbol R/T/S in the GMS name. Thus we get the following GMS classes:
R-GMS, T-GMS, S-GMS, RT-GMS, RS-GMS, TS-GMS, RTS-GMS.
Note that R-GMS, RS-GMS, RT-GMS, RTS-GMS are similar to classical T-model, B-model, S4model and S5-model structures.
TmMS languages. Let us describe a language of a first-order TmMS with equality. The alphabet is identical to the alphabet of a first-order GMS language with equality, with a set Ms specified as follows: Ms = {, }.
The set Fm of language formulas is determined according to the described above items FA, FP, FR, F, but instead of F we have:
F) let be a formula, then and are formulas.
We will use the derived modal compositions and to write formulas of the form та .
When we define a mapping Im, instead of I for formulas and we have: I ) for each St we specify:
T , if Im(, )(d ) T for any St : , Iт(, )(d) F , if exists St : and Im(, )(d ) F , else undefined.
T , if Im(, )(d ) T for any St : , Iт(, )(d) F , if exists St : and Im(, )(d ) F ,
else undefined.
Given for St there is no such that , then for each dVA we define Iт(, )(d). Given for St there is no such that , then for each dVA we define Iт(, )(d).
Depending on conditions imposed on , different classes of TmMS can be defined. Considering the cases when can be reflexive, symmetric or transitive, we obtain the following classes: R-TmMS, T-TmMS, S-TmMS, RT-TmMS, RS-TmMS, TS-TmMS, RTS-TmMS.
MMS languages. Let us describe a language of a first-order MMS language with equality. The alphabet is identical to the alphabet of a first-order GMS language with equality, with a set Ms is specified as follows: Ms = {Mi | iI}.
The set Fт of language formulas is determined according to the described above items FA, FP, FR, F, but instead of F we have:
FM) let be a formula, Mi Ms; then Mi is a formula.
When we define a mapping Im, instead of I for formulas of the form Mi we have:
T , if Im(, )(d ) T for any St : i , Iт(Mi , )(d) F, if exists St : i and Im(, )(d ) F,
else undefined.
Given for St there is no such that i , then for each dVA we define Iт(Mi , )(d).
Depending on properties of relations i, different classes of MMCs can be defined. We consider cases where i can be reflexive, symmetric or transitive, and all i are of the same type. Thus we obtain the following MMS pure types:
R-MMS, T-MMS, S-MMS, RT-MMS, RS-MMS, TS-MMS, RTS-MMS.
At the same time, much more complex, mixed types are possible here. For example, the relation 1 is transitive and reflexive, 2 is symmetric, 3 is transitive, etc.
We will call MMS with finite sets of same-type relations i epistemic MMS (EpMS). Therefore, GMS can be interpreted as a special case of EpMS.
Traditional systems of epistemic logic of knowledge can be naturally considered within EpMS. In particular, R-EpMS, RT-EpMS, RTS-EpMS are generalizations of epistemic Т(n), S4(n), S5(n)-systems respectively.
Let dVA. The question arises: how to set the value of (d)?
Let given dVA we have (d), hence (d) dVA. Such a property is called a strong condition of undefinedness on states. In this case, from ()(d) = T follows that dVA for all such that . This means that basic objects (basic data) cannot disappear when transitioning to a successor state, which imposes strong restrictions on semantic models. In addition, equitonicity of predicates is violated under a modal composition. Therefore, the strong undefinedness on states condition is too restrictive.
The general condition of undefinedness on states seems more organic:
given dVA, we specify (d) = (d).
Here d denotes NS [vad | aA].
Informally, this means that a predicate on states "perceives" only such components va that aA. Hence for TMS with a general condition of undefinedness on states, we have (d) = (d) for all dVA.
It is not difficult to show that in GMS, TmMS, MMS with a general condition of undefinedness on states, basic modal compositions preserve the predicates’ equitonicity.
Thus, further on we will consider TMS with a general condition of undefinedness on states.
Predicates that are values of non-modalized formulas, belong to predicates of state; they are defined as follows: for each dVA we have (d) = (d).
Predicates which are values of modalized formulas, belong to global predicates.
Interaction of modal compositions with renominations and quantifiers. Symbols of TMS modal compositions can be carried through renominations:
Theorem 1. Rvx,,u ( ())(d) (Rvx,,u ())(d) for arbitrary Ms, Fm, dVA. The statement of Theorem 1 is specified for the cases of GMS, TmMS, MMS.
Here we consider:
Ms= { } for the GMS case,
, } for the TmMS case, Ms= {
Ms= {Mi | iI} for the MMS case.
(Rvx,,u ()), where Ms, are irrefutable.
The interaction of modal compositions and quantifiers in TMS is more interesting. We will consider the interaction of and with x and x in GMS, cases of TmMS and MMS are similar.
Theorem 2. Let M be a GMS of equitone predicates, then for each Fm we have: 1) M |= x x; 2) M |= x x.
Consequence 2. Let M be a GMS of equitone predicates, then for each Fm we have: 1) M |= x x; 2) M |= x x. Txhus, ixna , GxMS ofxequiatroenierrefpurteadbilceat(evsa,lidf)o.rmulas x x, x x,
In contrast to the statement of Theorem 2, in a GMS without monotonicity restrictions, formulas
x x та x x are refutable (see also [
Example 1. Formula xx is refuted in a GMS without monotonicity restrictions. Let St = {, }, R = {}, A = {a, b}, A = {b}. We have [xa, yb] = [yb]. Let us take рPs from (р) = V \{x}. Let us set р([yb]) = T, р([xb, yb]) = F.
Given A = {b} and р([xb, yb]) = F, we have (x р)([yb]) = F (x р)([yb]) = F. We obtain р([xa, yb]) = р([yb]) = T (р)([xa, yb]) = T (xр)([yb]) = T. So, (xрx р)([yb]) = F, therefore | xрx р.
Example 2. Formula x x is refuted in a GMS without monotonicity restrictions. Let St = {, }, R = {}, A = {a}, A = {b}. Let us take рPs from (р) = V \{x}. Let us set р() = F, р() = F, р([xb]) = T.
We have р[xb] = T (x р)() = T (x р)() = F.
We obtain [xax]р=xрр)([(x) a=]F) =р( |) =F ( р)([xa]) = F (xр)() = F. Therefore, ( x рxр.
Note that in the examples 1 and 2, the predicate р is non-equitone.
Consequence 3. Formulas xx and xx are refutable.
Example 3. Formulas xx and xx are refuted in a GMS of equitone predicates.
Let St = {, }, R = {}, A = {a}, A = {a, b}.
Let us take р, qPs from (р) = (q) = V \{x}.
Let us set р([xa]) = F, р([xa]) = F, р([xb]) = T.
Given A = {a}, we have р[xa] = F (р)[xa] = F (xр)([xa]) = F . However, given р([xb]) = T, we obtain (x р)([xa]) = T (x р)([xa]) = T. Therefore, (x рxр)([xa]) = F | x рxр.
Let us set q([xa]) = T, q([xa]) = T, q([xb]) = F.
We have q[xb] = F (x q)([xa]) = F (x q)[xa] = F.
Given q([xa]) = T, we have (q)([xa]) = T (xq)([xa]) = T.
Therefore, (xqx q)[xa]) = F, whence |xqx q.
Consequence 4. Formulas xx and xx are refutable in a GMS of equitone predicates.
Characteristic features of equality predicates in TML. In the classical logic of predicates, formulas of the form x = y are refutable under 2-element interpretations, but they are irrefutable under 1-element interpretations. However, this is not the case for formulas ху of logic of quasiary predicates, they are also refutable under 1-element interpretations. Indeed, let us take an 1-element interpretation A = ({a}, I) and d = [xa]. Then d(x) = a and d(y), therefore ху([xa]) = F.
For TML, this gives the following result.
Statement 1. Formulas ху and ху can be refuted on GMS with 1-element states. At the same time, formulas xx are always interpreted as a constant predicate T. Hence Statement 2. M |= хх and M |= хх for each GMS M.
Note that хх is not always interpreted as a constant predicate T!
Example 4. Let us consider GMS with St = {, } and R = {}. Since there is no state such that , then (хх)(d) for each d.
Example 5. Formulas ху ху and ху ху are refuted in the specified above GMS. Let St = {, }, R = {}, A = {a}, A = {b}.
Let us take d = [xb, za] d = [za], d = [xb]. Hence d(x), d(y), d(x) = b, d(y). We have (ху)(d) = (ху)(d) = Т.
At the same time, (ху)(d) = (ху)(d) = F (ху)(d) = (ху)(d) = F.
Therefore, (ху ху)(d) = F | ху ху.
Let us take h = [xa, zb] h = [xa], h = [zb]. Hence h(x) = a, h(y), h(x), h(y). We have (ху)(h) = (ху)(h) = F.
At the same time, (ху)(h) = (ху)(h) = T ( ху)(h) = ( ху)(h) = T.
Therefore, (ху ху)(h) = F | ху ху.
We will define logical consequence relations in TML on a set of formulas specified with names of states (or simply, specified with states).
Let us denote a formula specified with a state by , where is a formula of the language, and S is its specification (S is a set of names of states of the world). Hence, the specification indicates the state of the world on which the formula is considered.
To eliminate quantifiers in the logics of non-monotonic predicates, variable assignment predicates z will be used. Therefore, further on we will consider extended sets of formulas specified with states, in which special formulas of the form z can appear: although the set of language formulas is expanded with predicate symbols z, formulas z are not used for construction of more complex formulas. In fact it is possible to consider z as full-fledged atomic formulas, using them for construction of complex formulas, however this does not actually change semantic properties of the language.
Let be a set of formulas specified with states with a specifications’ set S. We will call a set consistent with a TMS M = (St, R, A, Im), provided that an injection of S into St is defined.
On sets of formulas specified with states, we will introduce the relations of irrefutability, truth,
falsity and strong (denoted by IR, T, F and TF respectively) logical consequence. Such relations are
specified similarly to the corresponding relations in the traditional logics of quasiary predicates
(see [
Let and be sets of formulas specified with states.
Further on, when writing M|=* , we will assume by default that and are consistent with the TMS M.
is an IR-consequence of in a consistent with them TMS M (denoted M|=IR ), if for all dVA: (d) = T for all Ψ(d) F for some Ψ. is a logical IR-consequence of with respect to a TMS of a type ℳ if M|=IR for all TMS Mℳ. We will denote this by ℳ|=IR , or |=IR , if ℳ is implied.
Therefore, |IR a TMS M consistent with and and dVA exist such that: (d) = T for all and Ψ(d) = F for all Ψ.
(d) = T for all Ψ(d) = T for some Ψ. is a T-consequence of in a consistent with them TMS M (denoted M|=T ), if for all dVA: is a logical T-consequence of with respect to a TMS of a type ℳ if M|=T for all TMS Mℳ. ℳ|=T , or |=T , if ℳ is implied.
Therefore, |T a TMS M consistent with and and dVA exist such that:
for all we have (d) = T and for all Ψ we have Ψ(d) T. is a F-consequence of in a consistent with them TMS M (denoted M|=F ), if for all dVA: Ψ(d) = F for all Ψ (d) = F for some .
is a logical F-consequence of with respect to a TMS of a type ℳ if M|=F for all TMS Mℳ. We will denote this by ℳ|=F , or |=F , if ℳ is implied.
Therefore, |F a TMS M consistent with and and dVA exist such that:
for all Ψ we have Ψ(d) = F and for all we have (d) F. is a TF-consequence of in a consistent with them TMS M (denoted M|=TF ), if: M|=T and M|=F .
Therefore, M|TF M|T or M|F .
is a logical TF-consequence of with respect to a TMS of a type ℳ if M|=TF for all TMS Mℳ. This will be denoted by ℳ|=TF , or |=TF , if ℳ is implied.
It is obvious that |=TF |=T and |=F .
Therefore, |TF a TMS M consistent with and exists such that:
M|T or M|F .
The non-modal properties of the specified relations repeat the corresponding properties of the same-named relations for sets of formulas of the traditional logic of quasiary predicates.
These properties are: – decompositions of formulas L, R, L, R, L, R, and also L, R; – properties that guarantee the corresponding consequence relation; – simplifications and equivalent transformations induced by properties of predicates R, RI, RU, R, R, RR, R. Each such property R (except R) produces 4 corresponding properties RL, RR, RL, RR for the logical consequence relation when the selected formula or its negation is on the left or right side of this relation, and R produces 8 properties; – properties related to the quantifier elimination; – properties related to equality predicates.
As an example, let us give the properties produced by R:
R1L) Rvx,,u,,yz (), M|=* , z
Rvx,,u,,y (), M|=* , z; R1L) Rvx,,u,,yz () , M|=* , z
Rvx,,u,,y (), M|=* , z; R1R) M|=* , Rvx,,u,,yz (), z
M|=* , Rvx,,u,,y (), z ; R1R) M|=* , Rvx,,u,,yz (), z
M|=* , Rvx,,u,,y (), z ; R2L) Rvx,,u,,y (), M|=*, y
Rvx,,u (), M|=*, y; R2L) Rvx,,u,,y (), M|=*, y Rvx,,u () , M|=*, y; R 2R) M|=* , Rvx,,u,,y () , y M|=* , Rvx,,u () , y .
Equality properties. Let us consider properties related to equality predicates.
Predicates xy are total single-valued, so can be removed similarly to L and R: L) xy, M|= M|= xy, ; R) M|= xy, xy, M|= ;
RL) Rwv,,u (xy ) , M |
M | Rwv,,u (xy ), ; RR) M | Rwv,,u (xy ) ,
Rwv,,u (xy ), M | .
Tr) xy, yz, M|= xy, yz, xz, M|= .
Basing on Rxx, R0, R1, R2, R 1, R 2, we obtain the corresponding simplification properties; let us give an example of the properties induced by R 1 and R 2:
R 1L) given y {u , v} and x y then Rvw,,u,,x (xy ) , M | M | , y ; R1R) given y {u , v}, x y then M | , Rv ,u ,x (xy ) w,, y , M | ; Basing on Rxx and R, we obtain the elimination properties for the constant T-formula: R2L) Rvw,,u,,xz,,y (xy ) , M |
R 2R) M | , Rvw,,u,,xz,,y (xy ) , M | , z ; z , M | .
Elxx) xx, M|= M|= ;
ElRxx) Rvw,,u,, x (xx ) , M |
M | ; ElR) Rvw,,u,,x,,y (xy ) , M |
M | .
Property rp induces the following properties of substitution of equals: rpL) xy , x , y , Rwv,,u,,zx (), M | xy , x , y , Rwv,,u,,zx (), Rwv,,u,,zy (), M | ;
rpR) xy , x , y , M | Rwv,,u,,zx (),
xy, x , y , M | Rwv,,u,,zx (), Rwv,,u,,zy (), ; rpL) xy , x , y , Rwv,,u,,zx () , M |
xy , x , y , Rwv,,u,,zx () , Rwv,,u,,zy () , M | ; rpR) xy , x , y , M | Rwv,,u,,zx () ,
xy , x , y , M | Rwv,,u,,zx () , Rwv,,u,,zy () , .
Basing on Rf, Rxx and RT, we obtain the properties which guarantee each of the consequence relations: СRf) M|= , xx;
СRxx) M|= , Rwv,,u (xx ) ;
CR) M|= , Rxv,,u,,x,,z (xz ) .
The property related to z and xy which guarantees each of the consequence relations: C ) xy, x, M|= y, .
Properties related to modal compositions. For TMS of non-monotonic predicates with equality,
such properties are generally analogous to the corresponding properties of TMS without equality
predicates (see, e.g., [
The properties of carrying modalities over renominations belong to the properties of equivalent transformations based on Theorem 1. In a general case, there are 4 such properties. We present these properties for the composition in GMS, for TmMS and MMS they are formulated similarly: RL) , Rxv,,u ( ) M |* , Rxv,,u () M | ; RL) , Rxv,,u ( ) M |* ,
Rxv,,u () M | ; RR) M |* , Rxv,,u ( ) M | ,
Rxv,,u (); RR) M |* , Rxv,,u ( ) M | ,
Rxv,,u ().
El_R) M|=* , The elimination properties for the composition in GMS have the following form:
El_L) , M|=* { | } M|=* ;
M|=* { | }; El_R) M|=* ,
M|=* , for all states S such that ;
El_L) , M|=* , M|=* for all states S such that .
The properties of El_L and El_R are sufficient for the relation M|=IR.
The elimination properties for modalities can be similarly formulated for TmMS and MMS.
In the case of additional conditions imposed on the transition relation, the elimination properties for modalities will be modified accordingly.
For example, for the relation M|=IR in GMS, let us consider the cases when can be transitive, reflexive or symmetric. reflexive. We have
, therefore, for
symmetric. We have S El_L) S El_R) M|=IR , , M|=IR { | 4. transitive. We have El_R and
TEl_L) , M|=IR { | Here { |
El_L an additional condition {| }. , therefore El_L and El_R are specified as follows: or
} M|=IR . }{ |
} M|=IR .
M|=IR , for all states S such that reflexive and symmetric. We have SEl_R and since we obtain RSEl_L) or } M|=IR and { | and
. or }.
} is necessary due to the transitivity of the relation 5. transitive and reflexive. We have El_R and TEl_L, and since condition { | }. .
for T El_L we obtain the
transitive and symmetrical. We have S El_R and TS El_L)
, M|=IR { | or } { | or 7. transitive, reflexive and symmetric. We have SEl_R and TSEl_L, and since we obtain the condition { | or }. } M|=IR .
for TS El_L
The above properties of relations M|=* for sets of formulas in a given TMS M induce analogous properties of the corresponding logical consequence relations |=*.
Properties of logical consequence relations for sets of formulas specified with states are the semantic basis for constructing the corresponding sequent calculi.
In this paper we propose new classes of program-oriented logical formalisms – transitional modal logics of partial non-monotonic quasiary predicates with equality and extended renomination. We describe the semantic models and languages of pure first-order TMLs with strong equality predicates, the properties of equality predicates are given. The following classes of transitional modal systems are specified: general TMS, temporal TMS, multimodal TMS. The languages of such systems are described, the semantic properties, in particular, properties related to equality predicates, are considered. The interaction of modal compositions with renominations and quantifiers is investigated. We define relations of irrefutability, truth, falsity and strong logical consequence on sets of formulas specified with states, and present their properties. These properties are the semantic basis for further constructing the sequent type calculi for the proposed logics.