The paper explores new classes of program-oriented logical formalisms of the modal type -pure first-order modal logics of partial quasiary predicates with the monotonicity condition removed and enriched with equality predicates. The apparatus of modal logics is used for the description and modeling of various subject areas, artificial intelligence systems, and information and software systems. The limitations of classical predicate logic, on which traditional modal logics are based, underscore the relevance of developing new program-oriented logical formalisms. Such are transitional modal logics of quasiary predicates (TML), which reflect the aspect of change and development in subject areas. They synthesize the capabilities of traditional modal logics and the logics of partial quasiary predicates. Pure first-order TML are called TMLQ. We propose two types of TMLQ with equality: with strong equality predicates ≡xy, called TMLQ≡, and with weak equality predicates =xy, called TMLQ=. The characteristic features of these logics include the use of extended renomination compositions and special indicator predicates that denote the presence of a component with the corresponding subject name in the input data, which are necessary for the quantifier elimination in non-monotonic predicate logics. The work describes the semantic models and languages of TMLQ≡ and TMLQ=. Attention is focused on properties related to equality predicates, and the features of substitution of equals in these logics are described. A number of logical consequence relations for sets of formulas specified with states is defined, and their main properties are described. Based on this semantic foundation, calculi of sequent type are proposed for the investigated logics. Various types of such calculi for different logical consequence relations are described, basic sequent forms for these calculi are presented, and the closedness conditions for sequents are provided. The construction of derivations in the proposed calculi is described, and the soundness and completeness theorems for them are proven.
Modal logics are used with great success to describe a dynamic world that changes and evolves. The
exceptional flexibility of modal logics allows them to be applied to analyze and model a wide variety
of human activities. The apparatus of modal logics is utilized for the description and modeling of
artificial intelligence systems, information and software systems (see, for example [
The aim of this work is to study new classes of program-oriented modal logics – pure first-order TML of partial quasiary predicates with the monotonicity condition (equitonicity) removed and enriched with equality predicates. Two types of such predicates have been distinguished [10]: weak equality =ху and strong equality ≡ху. Pure first-order TML without the monotonicity restriction will be called TMLQ; TMLQ with strong equality predicates will be called TMLQ≡, while TMLQ with weak equality predicates will be called TMLQ=. TMLQ without equality predicates have been studied in [11, 12]. TMLQ≡ and TMLQ= are considered in this paper. The semantic models and languages of these logics are described, along with the features of the substitution of equals in TMLQ≡ and TMLQ=. We define a number of logical consequence relations for sets of formulas specified with states of the language, and properties of these relations are provided.
One of the most important applications of mathematical logic is the automation of proof search. Efficient proof search is essential for successfully solving a number of problems that arise in computer science and programming. A powerful tool for constructing proofs is Gentzen-type calculi, also known as sequent calculi. These calculi formalize the fundamental notion of logical consequence. In this work, we propose such calculi for TMLQ with equality predicates. The semantic basis for constructing sequent calculi for TML is the properties of logical consequence relations for sets of formulas specified with states. Varieties of these calculi for different logical consequence relations are described, and basic sequent forms and conditions for the closedness of sequents are provided for them. The soundness and completeness theorems for the proposed calculi are proved.
Concepts not defined here are interpreted in the sense of works [8, 10, 11, 13].
At the core of the CNML concept lies the notion of a compositional nominative modal system (CNMS). Such systems serve as models for the possible worlds in modal logics.
CNMS is the object M = (Cms, Ds, Iт), where: – Cms is a composition modal system which defines semantic aspects of the world; – Ds is a descriptive system which defines standard descriptions: usually a set Fт of formulas of the CNML language;
– Dns is a denotation system which determines values of standard descriptions on semantic models: usually an interpretation mapping Iт of formulas on states of the world.
Composition modal system is the object 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 St; – C is a set of compositions on Pr.
Thus, CMS are relational-type semantic models.
In expanded form, we will further define CNMS as follows: M = ((St, R, Pr, C), Fт, Iт).
For the first-order CNMS, the set St is specified as a set of algebraic systems (structures) α = (Aα, Prα), where Aα is a set of basic data of the state α, Prα is a set of quasiary predicates VAα → {T, F}.
The predicates Prα are called predicates of the state α.
The predicates VA →{T, F}, where A = U Aα , will be called global.
α∈S
Transitional modal logics (TML), an important class of CNML, reflect the aspect of change and development in subject areas, describing transitions from one state of the world to another. Central to TML is the concept of a transitional modal system (TMS), which can be considered the most important class of CNMS.
We specify TMS as CNMS in which the set R consists of relations of the form R ⊆ St × St. These relations are treated as state transition relations, hence the name.
Traditional varieties of TMS include general transitional, temporal, and multimodal systems (see [11, 12]).
TMS, in which R consists of a single binary relation >, and the basic modal composition is £ ("necessary"), are called general (GMS).
TMS, in which R consists of a single binary relation >, and the basic modal compositions are £ ↑ ("it will always be the case") і £ ↓ ("it has always been the case"), are called temporal (TmMS).
TMS with the set of relations R = { > i | i∈I}, and basic modal compositions Mi, i∈I, in which each > i ∈R is matched with the corresponding modal composition Mi, are called multimodal (MМS). In MМS, each Mi acts as £ , but only with respect to its own relation > i , i∈I. In this sense, GMS is a special case of MMS.
For GMS, the derivative composition ¸ ("possibly") is traditionally defined as: ¸ Р means ¬ £ ¬ Р.
For TmMS, we specify the derivative compositions ¸ ↑ ("it will sometimes be the case") and ¸ ↓ ("it was sometime the case"): ¸ ↑Р means ¬ £ ↑¬Р, while ¸ ↓Р means ¬ £ ↓¬ Р.
Pure first-order TMS will be called TMSQ. The corresponding notation GMSQ, TmMSQ, MMSQ will be used for pure first-order GMS, TmMS, MMS respectively.
Basic logical compositions of for TMSQ are logical connectives ¬ and ∨ , renomination Rvx,,u⊥ and existential quantification ∃ x. For TMSQ with equality we add special 0-ary compositions – equality predicates. TMSQ with strong equality predicates ≡xy will be called TMSQ≡, and TMSQ with weak equality predicates =xy will be called TMSQ=.
V-A-quasiary predicate [8] is a partial function Q: VA → {T, F}, where VA is a set of all V-Anominative sets, {T, F} is the set of truth values; V and A are interpreted as sets of subject names (variables) and subject values respectively.
V-A-nominative set (V-A-NS) is defined [
For V-A-NS, we introduce the operations of projection ||Z and ||–Z, where Z ⊆ V, overlay ∇, and (extended) renomination rvx,,u⊥ (see [8, 13, 14]).
Note that in this work, we use extended renomination operations rvx,,u⊥ and the corresponding extended renomination compositions
Rvx,,u⊥ . Traditional renomination operations rvx and renomination compositions Rvx are their particular cases which were used, for example, in [8, 11, 12].
Each V-A-quasiary predicate Q is determined by two sets: its truth domain T(Q) = {d | Q(d) = T} and its falsity domain F(Q) = {d | Q(d) = F}.
Predicate Q is single-valued, or P-predicate, if T(Q)∩F(Q) = ∅.
In this work, only single-valued V-A-quasiary predicates will be considered.
Predicate Q is irrefutable, if F(Q) = ∅; Predicate Q is satisfiable, if T(Q) ≠ ∅.
In the class of P-predicates, we have 3 constant predicates: – Q is identically true (denoted by T), if F(Q) = ∅ and T(Q) = VА; – Q is identically false (denoted by F), if T(Q) = ∅ and F(Q) = VА; – Q is totally undefined (denoted by ⊥ ), if T(Q) = F(Q) = ∅.
P-predicate Q is equitone, if (Q(d)$ and d ⊆ d') ⇒ Q(d')$ = Q(d).
Subject name х∈V is unessential for the predicate Q, if d1 ||–х = d2 ||–х ⇒ Q(d1) = Q(d2). The basic logical compositions ¬ , ∨ , ∃ x, Rvx,,u⊥ for quasiary predicates are specified in [13].
Equality predicates are treated as special 0-ary compositions, considering their general logical status. Two varieties of these predicates are distinguished [10]: weak (up to definability) equality predicates ={x,y} and strong (strict) equality predicates ≡ {x,y}. They are defined as follows: T(={x,y}) = {d | d(x)$, d(y)$ and d(x) = d(y)}, F(={x,y}) = {d | d(x)$, d(y)$ and d(x) ≠ d(y)}; 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)$}.
Specific cases of ={x,y} and ≡ {x,y}, when x and y coincide, are ={x} and ≡ {x}.
The predicates ={x,y}, ={x} and ≡ {x,y}, ≡ {x} will be more conventionally denoted as =xy, =xx and ≡ xy, ≡ xx.
Thus, =xy and =yx represent the same predicate, as do ≡ xy and ≡ yx, respectively.
The predicates ≡ xy and ≡ xx are total and non-monotonic; the predicates =xy and =xx are partial and equitone.
For quantifier elimination in the logics of non-monotonic predicates, special 0-ary compositions –predicates-indicators which detect whether a component with a corresponding name has a value in the input data – are needed. The use of such indicator predicates is a characteristic feature of TMLQ. Total predicates-indicators determine the presence or absence of a component with a given name, while partial predicates-indicators only detect the presence of such a component.
Total predicates-indicators Ez are non-monotonic; they are defined as follows (see [8]): T(Ez) = {d | d(z)$};
F(Ez) = {d | d(z)#}.
Total indicator predicates Ez were used, in particular, in [8, 10, 11, 13].
Partial predicates-indicators are already present in TMSQ= as the equitone predicates =zz. Indeed, we have T(=zz) = {d | d(z)$} = T(Ez) and F(=zz) = {d | d(z)$ and d(z) ≠ d(z)} = ∅.
Note that the predicates Ez can be expressed as ∃ y ≡ xy, but it is more appropriate to explicitly define them as special 0-ary compositions, which is done in TMLQ≡. At the same time, partial indicator predicates, such as the predicates =xx, are explicitly present in TMLQ=.
Therefore, we have the following varieties of TMSQ with equality: GMSQ≡, TmMS Q≡, MМS Q≡ for TMSQ≡, and GMSQ=, TmMS Q=, MМS Q= for TMSQ=.
Let us describe a language of GMSQ≡. The alphabet: a set V of subject names (variables); a set Ps of predicate symbols; the set {¬,∨, Rxv,,⊥u ,∃x, ≡xy , Ex} of basic logical compositions’ symbols; the set Ms = {£} of basic modal compositions’ symbols.
The set Fr of formulas of the language is determined as follows:
Fa) Ps ⊆ Fr; F≡) {Ex | x∈V} ⊆ Fr and {≡ху | x, у∈V} ⊆ Fr; Fp) Φ, Ψ∈Fr ⇒ ¬Φ∈Fr and ∨ΦΨ∈Fr; FR) Φ∈Fr ⇒ Rxv,,⊥uΦ∈ Fr; F∃) Φ∈Fr ⇒ ∃xΦ∈Fr;
F¨) Φ∈Fr ⇒ £Φ∈Fr.
Formulas of the form р∈Ps, Ex, ≡ху will be called atomic.
Atomic formulas and formulas of the form Rxv,,⊥u ( p), where р∈Ps, will be called primitive.
To write formulas, we will traditionally use the prefix notation and the symbols for derived compositions →, &, ∀x, ¸. Thus, the formulas ∨¬ΦΨ, ¬∨¬Φ¬Ψ, ¬∃x¬Φ, and ¬£¬Φ will be abbreviated Φ→Ψ, Φ&Ψ, ∀xΦ, and ¸Φ, respectively.
Sets of guaranteed to be unessential names for formulas are specified by a function ν : Fr → 2V (see [8]). At the same time, we define ν(£Φ) = ν(Φ).
The type of GMSQ≡ is determined by the extended signature σ = (Ps, ν) and properties of the relation > .
Let us define an interpretation mapping Im of formulas on states of the world. First, we specify Im : Рs × St → Pr, with condition Iт(p, α) ∈ Prα (basic predicates are predicates of states). Compositions’ symbols are interpreted as corresponding compositions (in particular, the symbols Ex and ≡xy are interpreted as the corresponding predicates-indicators and equality predicates). The mapping Im is continued to Fт × St → Pr in the following fashion:
Ip) Iт(¬, α) = ¬(Iт(Φ, α)); Iт(∨ΦΨ, α) = ∨(Iт(Φ, α), Iт(Ψ, α)); IR) Im(Rxv,,⊥u (Φ),α) = Rvx,,u⊥ (Im(Φ,α));
⎧T , if exists a ∈ A : Im(Φ, α)(d∇x a a) = T , I∃) Iт(∃xΦ, α)(d) = ⎨⎪ F, if Im(Φ, α)(dα∇x a a) = F for all a ∈ Aα , ⎩⎪ else undefined.
⎧⎪T , if Im(Φ, δ)(d ) = T for all δ ∈ S : α > δ, I¨) Iт(£Φ, α)(d) = ⎨F, if exists δ ∈ S : α > δ and Im(Φ, δ)(d ) = F,
⎩⎪ else undefined.
Given for α∈St there is no β such that α > β , then we define Iт(£Φ, α)(d)↑ for all d∈VA. For abbreviations of formulas of the form ∀xΦ and ¸Φ, the mapping Iт is specified as follows: ⎧T , if Im(Φ,α)(d∇x a a) = T for all a ∈ Aα , ⎪ I∃) Iт(∀xΦ, α)(d) = ⎨F, if exists a ∈ A : Im(Φ,α)(d∇x a a) = F,
α ⎪⎩ else undefined. ⎧T , if exists δ ∈ St such that α > δ and Im(Φ, δ)(d ) = T , ⎪ I¸ ) Iт(¸Φ, α)(d) = ⎨ F, if Im(Φ, δ)(d ) = F for all δ ∈ St such that α > δ,
⎩⎪ else undefined.
Given for α∈St there is no β such that α > β , then we define Iт(¸Φ, α)(d)↑ for all d∈VA. Predicates that are values of modalized formulas, belong to global predicates.
We specify TMS as M = (St, R, A, Im).
The following definitions are given identically for all the described variants of TMSQ. Predicate Iт(Φ, α), which is a value of the formula Φ on state α, is denoted by Φα. Formula Φ is irrefutable on state α (denoted by α |= Φ), if Φα is a irrefutable predicate. Formula Φ is irrefutable in TMS M (denoted by M |= Φ), if for all α∈St, Φα is irrufutable. Let be a TMS class of a given type.
Formula Φ is -irrefutable (denoted by |= Φ), if M |= Φ for all TMS M∈ .
Depending on conditions imposed on the relation >, different classes of GMSQ≡ can be specified. Traditionally, we can consider cases of reflexive, symmetric or transitive > , or their combinations: then we add the corresponding symbol R/T/S to the GMSQ≡ name. Thus, the following classes are obtained: R-GMSQ≡, T-GMSQ≡, S-GMSQ≡, RT-GMSQ≡, RS-GMSQ≡, TS-GMSQ≡, RTS-GMSQ≡.
The language of GMSQ= is defined similarly to the language of GMSQ≡ with the following differences. The set of symbols of basic logical compositions is {¬,∨, Rxv,,⊥u ,∃x, =xy}. In the definition of the set of formulas, instead of the item F≡ we have {=ху | x, у∈V} ⊆ Fr; the interpretation mapping is defined accordingly.
Let us describe the TmMSQ≡ language. The alphabet is identical to the alphabet of GMSQ≡ with the set of basic modal compositions’ symbols specified as Ms = {£↑, £↓}. The set Fт of formulas of the language is determined according to the items Fa, F≡, Fp, FR, F∃ for the language of GMSQ≡, but instead of F¨ we have:
F¨↑↓) Φ∈Fr ⇒ £↑Φ∈Fr and £↓Φ∈Fr.
When we define the mapping Iт, instead of I¨ we have the following item I¨↑↓ (see [11, 12]): ⎧T , if Im(Φ,δ)(d ) = T for all δ ∈ St such that α > δ, ⎪ I¨↑↓) Iт(£↑Φ, α)(d) = ⎨F, if there exists δ ∈ St such that α > δ and Im(Φ,δ)(d ) = F, ⎪⎩ else undefined; ⎧T , if Im(Φ, δ)(d ) = T for all δ ∈ St such that δ > α, ⎪ Iт(£↓Φ, α)(d) = ⎨F, if there exists δ ∈ St such that δ > α and Im(Φ,δ)(d ) = F,
⎩⎪ else undefined.
Given for α∈St there is no β such that α > β , then we define Iт(£↑Φ, α)(d)↑ for all d∈VA. Given for α∈St there is no β such that β > α , then we define Iт(£↓Φ, α)(d)↑ for all d∈VA. For the abbreviated formulas ¸↑Φ and ¸↓Φ, we have the following interpretation mapping Iт: ⎧T , if there exists δ ∈ S, such that α > δ and Im(Φ,δ)(d ) = T , ⎪ I¸ ↑↓) Iт(¸↑Φ, α)(d) = ⎨F, if Im(Φ,δ)(d ) = F for all δ ∈ S, such that α > δ,
⎩⎪ else undefined; ⎧T , if there exists δ ∈ S, such that δ > α and Im(Φ,δ)(d ) = T , ⎪ Iт(¸↓Φ, α)(d) = ⎨F, if Im(Φ,δ)(d ) = F for all δ ∈ S, such that δ > α,
⎩⎪ else undefined.
Given for α∈St there is no β such that α > β , then we define Iт(¸↑Φ, α)(d)↑ for all d∈VA. Given for α∈St there is no β such that β > α , then we define Iт(¸↓Φ, α)(d)↑ for all d∈VA.
The language of TmMSQ= is defined similarly to the language of TmMSQ≡, with the differences corresponding to those between the languages of GMSQ= and GMSQ≡.
Depending on the conditions imposed on >, we define different classes of GMSQ=, TmMSQ≡, and TmMSQ= as done for GMSQ≡.
Similarly, we define the languages of MMSQ≡ and MMSQ=.
Depending on how the value Φδ(d) is set in case d∉VAδ, two types of TMS are distinguished ([12]): with strong condition of undefinedness on states and with general condition of undefinedness on states. The strong condition is specified as follows: under the condition d∉VAδ we have Φδ(d)↑. Hence: (£Φ)α(d) = T ⇒ d∈VAδ for all δ such that α▹ δ. This implies that basic objects cannot disappear when transitioning to a successor state, which imposes too strong a restriction on semantic models. The strong condition also does not preserve [12] equitonicity of predicates with modalities.
The general condition of undefinedness on states does not have these drawbacks; it is defined as follows: for all d∈VA and δ∈St, we have Φδ(d) = Φδ(dδ).
Here dδ denotes the name set [ v a a ∈ d | a∈Aδ].
Given d∉VAδ, we have Φδ(d) = Φδ(dδ), meaning that predicates on states δ “perceive” only components v a a with basic data a∈Aδ.
The interaction of modal compositions with renominations and quantifiers has been studied in [12]. Let us briefly describe it for GMSQ.
Theorem 1. For all Φ∈Fr, d∈VA we have Rxv,,⊥u (®Φ)α (d) = ®(Rxv,,⊥u (Φ))α (d) .
Therefore, symbols of Ms can be carried through renomination symbols.
Theorem 2. Formulas ∃x£Φ → £∃xΦ, £∀xΦ →∀x£Φ, ¸∀xΦ → ∀x¸Φ, ∃x¸Φ → ¸∃xΦ are irrefutable in GMSQ of equitone predicates.
Theorem 3. Formulas ∃x£Φ → £∃xΦ, £∀xΦ →∀x£Φ are refuted in GMSQ.
Corrolary 1. Formulas ¸∀xΦ → ∀x¸Φ, ∃x¸Φ → ¸∃xΦ are refuted in GMSQ.
Theorem 4. Formulas £∃xΦ → ∃x£Φ, ∀x£Φ → £∀xΦ are refuted in GMSQ of equitone predicates.
Corollary 2. Formulas ∀x¸Φ → ¸∀xΦ, ¸∃xΦ → ∃x¸Φ are refuted in GMSQ of equitone predicates.
Examples of GMSQ, in which the formulas specified in Theorems 3 and 4 are refuted, are given in the work [12].
Let's consider the specific properties of GMSQ, related to equality predicates. For TmMSQ and MMSQ, these properties are formulated similarly.
Assertion 1. 1) for every GMSQ≡ M we have M |= ≡хх and M |= £≡хх; 2) for every GMSQ= M we have M |= =хх and M |= £=хх.
Indeed, F(≡ хх) = ∅ and F(=хх) = ∅.
Example 1. Let us consider GMSQ≡ with St = {α, β} and R = { α > β }. Since there is no state η such that β > η, then (£≡ хх)β(d)# for each d.
Therefore, £≡ хх is not always interpreted as the constant predicate Т.
Theorem 5. Formulas =ху → £=ху and £=ху → =ху are irrefutable in GMSQ=.
In particular, =хх → £=хх and £=хх → =хх are irrefutable in GMSQ=. At the same time, we have Example 2. Formulas ≡ ху → £≡ ху and £≡ ху → ≡ ху are refuted in the following GMSQ≡. Let St = {α, β}, R = { α > β}, Aα = {a}, Aβ = {b}.
Let d = [x a b, z a a] ⇒ dα = [z a a], dβ = [x a b]. 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 = [x a a, z a b] ⇒ hα = [x a a], hβ = [z a b]. 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.
Thus, (£≡ ху → ≡ ху)α(h) = F ⇒ α |≠ £≡ ху → ≡ ху.
Example 3. Formulas Ex → £Ex and £Ex → Ex are refuted in GMSQ≡.
Let us consider the GMSQ≡ from Example 2.
Let us take h = [x a a, z a b] ⇒ hα = [x a a], hβ = [z a b]. From this, Exα(h) = Т, Exβ(h) = F, which gives £Exα(h) = F. Therefore, (Ex → £Ex)α(h) = F, whence α |≠ Ex → £Ex.
Let us take d = [x a b, z a a] ⇒ dα = [z a a], dβ = [x a b]. From this, Exα(d) = F, Exβ(d) = T, which gives £Exα(d) = T. Therefore, (£Ex → Ex)α(h) = F, whence α |≠ £Ex → Ex.
Theorem 5 and Example 2 demonstrate significant differences between GMSQ≡ and GMSQ=. Another confirmation of this is provided below by Theorem 6 and Example 4.
Theorem 6. Formula =ху & £=хz → £=уz is irrefutable in GMSQ=.
Example 4. Formula ≡ ху & £≡ хz → £≡ уz is refuted in the following GMSQ≡.
Let St = {α, β}, R = { α > β}, Aα = {a}, Aβ = {b, с}.
Let us take d = [x a c, y a b, z a c, s a a] ⇒ dα = [s a a], dβ = [x a c, y a b, z a c]. Hence dα(x)#, dα(y)#; dβ(x) = c, dβ(y) = b, dβ(z) = c.
From this, (≡ ху)α(d) = (≡ ху)α(dα) = Т; (≡ хz)β(d) = (≡ хz)β(dβ) = T, (≡ yz)β(d) = (≡ yz)β(dβ) = F. We obtain (≡ хz)β(d) = T and α▹β ⇒ (£≡ хz)α(d) = T; (≡ yz)β(d) = F and α▹β ⇒ (£≡ yz)α(d) = F.
Therefore, (≡ ху & £≡ хz → £≡ уz)α(d) = F. 4. Logical consequence relations for sets of formulas specified with states
We will define logical consequence relations in TMS on a set of formulas specified with names of states, or simply, specified with states.
Formula specified with a name of the state has the form Φα, where Φ is a formula of the language, α∈S – its specification, S – a set of names of states of the world.
Let us call a set of formulas specified with states Σ with a specifications’ set S consistent with TMS M = (St, R, A, Im), provided that an injection of S into St is defined.
On sets of formulas specified with states, we introduce the relations of irrefutability (IRconsequence), truth (T-consequence), falsity (F-consequence), and strong (TF-consequence) logical consequence. These relations correspond to the similarly named relations in logics of quasiary predicates (see [8, 10, 13]).
Let Δ and Γ be sets of formulas specified with states. Further on, the notation Γ M|=* Δ by default assumes that Γ and Δ are consistent with TMS M.
Δ is a IR-consequence of Γ in a consistent with them TMS M (denoted Γ M|=IR Δ), if for all d∈VA we have: Φα(d) = T for all Φα∈Γ ⇒ Ψβ(d) ≠ F for some Ψβ∈Δ.
Δ is a logical IR-consequence of Γ with respect to a TMS of a type Γ M|=IR Δ for all M∈ .
Δ is a T-consequence of Γ in a consistent with them TMS M (denoted Γ M|=T Δ), if for all d∈VA we have: Φα(d) = T for all Φα∈Γ ⇒ Ψβ(d) = T for some Ψβ∈Δ.
Δ is a logical T-consequence of Γ with respect to a TMS of a type (denoted Γ |=T Δ), if Γ M|=T Δ for all M∈ .
Δ is an F-consequence of Γ in a consistent with them TMS M (denoted Γ M|=F Δ), if for all d∈VA we have: Ψβ(d) = F for all Ψβ∈Δ ⇒ Φα(d) = F for some Φα∈Γ.
Δ is a logical F-consequence of Γ with respect to a TMS of a type (denoted Γ |=F Δ), if Γ M|=F Δ for all M∈ .
Δ is a TF-consequence of Γ in a consistent with them TMS M (denoted Γ M|=TF Δ), if Γ M|=T Δ and Γ M|=F Δ.
Δ is a logical TF-consequence of Γ with respect to a TMS of a type (denoted Γ |=TF Δ), if Γ M|=TF Δ for all M∈ .
Therefore, we have: Γ |=TF Δ ⇔ Γ |=T Δ and Γ |=F Δ.
In logics with weak equality predicates, the relations of types T, F and TF are incorrect (see [10]), so in GMSQ= we consider only relations of the IR type. In GMSQ≡, all the above-defined relations can be considered.
The non-modal properties of the relations for sets of formulas specified with states repeat the corresponding properties of the same-named relations for sets of formulas of the traditional logic of quasiary predicates described in [8, 10, 13, 14]. These are such properties.
1) Properties of formulas decomposition ¬¬L, ¬¬R, ∨L, ∨R, ¬∨L, ¬∨R, and also properties ¬L,and ¬R for |=IR (see [8]).
2) Properties of simplification and equivalent transformations related to renominations, induced by the predicates properties R, R⊥I, R⊥U, R⊥R, R⊥¬, R⊥∨, R# (see [13, 14]).
3) Properties of simplification related to renomination of the Ez predicates, induced by the predicates properties R⊥E and R⊥Ev, and the property ElRE of elimination of the F-formula Rxv,,⊥u,,⊥z (Ez)(see [13]).
4) Auxiliary properties in GMSQ≡: elimination of ¬ when carrying a formula from the left side of the consequence relation to the right and vice versa for the symbols Ez, ≡ху, and their renominations.
5) Properties related to the quantifier elimination; in GMSQ≡, they repeat the properties ∃R⊥L, ¬∃R⊥R, ∃R⊥vR, ¬∃R⊥vL (see [8]), in GMSQ=, we have the analogous properties ∃R⊥L=, ¬∃R⊥R=, ∃R⊥vR=, ¬∃R⊥vL=, where instead of Ez, we use =zz; moreover, we add the properties of E-distribution Ed and of primary definition Ev in GMSQ≡ (see [14]), and similarly, the properties $=d and $=v with =zz instead of Ez in GMSQ=.
6) Properties in GMSQ≡ related to the ≡ху predicates; these are simplification properties induced by the predicates properties R⊥≡xx, R⊥≡0, R⊥≡1, R⊥≡ 2, R⊥≡1E, R⊥≡2E; properties of elimination of the Tformulas ≡xx and Rwv,,⊥u,,⊥x,,y⊥ (≡xy ), elimination of the pair of equals in a renomination ≡elR, transitivity Tr≡ (see [13]). For example, let us consider the transitivity property (here and further on the symbol * denotes one of the IR, T, F, TF):
Tr≡ ) ≡xyα, ≡yzα, Γ M|=∗ Δ ⇔ ≡xyα, ≡yzα, ≡xzα, Γ M|=∗ Δ.
We add to them the properties of substitution of equals in GMSQ≡ described below.
CF ) Rxv,,⊥u,,⊥z (Ez), Γ |=∗ Δ .
Additionally, the corresponding consequence relation is guaranteed by one of the following properties: СL) Φα, ¬Φα, Γ M|=T Δ; СR) Γ M|=F Δ, Φα, ¬Φα; СLR) Φα, ¬Φα, Γ M|=TF Δ, Ψα, ¬Ψα.
Based on the properties of equality, we have the properties of the presence of each of the relations: СRf≡) Γ M|=∗ Δ, ≡xxα; CE≡L) ≡xyα, Exα, Γ |=∗ Eyα, Δ; CE≡R) Γ |=∗ ≡xyα, Exα, Eyα, Δ;
CT≡) Γ M|=∗ Δ, Rxv,,⊥u,,⊥x,,z⊥ (≡xz )α .
Based on the properties of guaranteed presence of one of the relations Γ M|=IR Δ, Γ M|=T Δ, Γ M|=IF Δ, Γ M|=TF Δ, we have the corresponding conditions that guarantee this relation.
С) there exists a formula Φ: Φα∈Γ and Φα∈Δ – for all relations; СF) there exists a formula Rxv,,⊥u,,⊥z (Ez)α ∈Γ – for all relations; СL) there exists a formula Φα: Φα∈Γ and ¬Φα∈Γ – for the relation M|=T; СR) there exists a formula Φα: Φα∈Δ and ¬Φα∈Δ – for the relation M|=F; ; СLR) there exist formulas Φ and Ψ: Φα, ¬Φα∈Γ and Ψα, ¬Ψα∈Δ – for the relation M|=TF; СRf≡) there exists a formula ≡xxα∈Δ – for all relations; CE≡L) there exist formulas ≡xy, Ex and Ey: ≡xyα, Exα∈Γ and Eyα∈Δ – for all relations; CE≡R) there exist formulas ≡xy, Ex and Ey: ≡xyα, Exα, Eyα∈Δ – for all relations;
CT≡) there exists a formula Rvx,,u⊥,,x⊥,,z⊥ (≡xz ) : Rvx,,u⊥,,x⊥,,z⊥ (≡xz )α ∈ Δ – for all relations.
This provides the complete conditions that guarantee each of the corresponding relations Γ M|=∗ Δ in GMSQ≡.
The relation M|=IR : С ∨ CF ∨ СRf≡ ∨ CE≡L ∨ CE≡R ∨ CT≡.
The relation M|=T : С ∨ СL ∨ CF ∨ СRf≡ ∨ CE≡L ∨ CE≡R ∨ CT≡.
The relation M|=F : С ∨ СR ∨ CF ∨ СRf≡ ∨ CE≡L ∨ CE≡R ∨ CT≡.
The relation M|=TF : С ∨ СLR ∨ CF ∨ СRf≡ ∨ CE≡L ∨ CE≡R ∨ CT≡.
Let us describe the properties of guaranteed presence of the relation Γ M|=IR Δ in GMSQ=. These are the basic property С and the following ones: СRf=) Γ M|=IR Δ, =xxα; C⊥L) Rwv,,u⊥,,⊥x (=xy )α , Γ M|=IR Δ; C⊥R) Γ M|=IR Δ, Rwv,,u⊥,,⊥x (=xy )α . С⊥L) there exists a formula Rwv,,u⊥,,⊥x (=xy )α ∈ Γ; С⊥R) there exists a formula Rwv,,u⊥,,⊥x (=xy )α ∈ Δ.
С ∨ СRf= ∨ C⊥L ∨ C⊥R.
Hence, the same-named conditions that guarantee the relation Γ M|=IR Δ in GMSQ=.
СRf=) there exists a formula =xxα∈Δ; Thus, we obtain the complete condition of guaranteed presence of the relation Γ M|=IR Δ in GMSQ=: To conclude the description of the non-modal properties of consequence relations for sets of formulas specified with states in GMSQ≡, we will examine properties related to the substitution of equals.
Example 5. The property ≡ хуα, £≡ хzα M|=IR £≡ уzα is refuted in the following GMSQ≡.
In the GMS M from Example 4 for d = [x a c, y a b, z a c, s a a] we have (≡ ху)α(d) = Т, (£≡ хz)α(d) = T, (£≡ yz)α(d) = F; hence ≡ хуα, £≡ хzα M|≠IR £≡ уzα.
Thus, ≡ хуα, £≡ хzα M|≠* £≡ уzα, where the symbol * denotes one of the IR, T, F, TF.
At the same time, we have ≡ хуα, £≡ хzα, £≡ уzα |=*£≡ уzα by the property С of guaranteed presence of each of the logical consequence relations.
Assertion 2. The following statements are not equivalent:
≡xyα , Rwv,,u⊥,,vx (Φ)α ,Γ M |=∗ Δ and ≡xyα , Rwv,,u⊥,,vx (Φ)α, Rwv,,u⊥,,vy (Φ)α, Γ M |=∗ Δ .
We have Rxv (£≡vz )α = £≡xzα and Ryv (£≡vz )α = £≡yzα , by Example 5 ≡ хуα, £≡ хzα M|≠* £≡ уzα, hence ≡xyα , Rxv (£≡vz )α M |≠* Ryv (£≡vz )α.
However, ≡xyα , Rxv (£≡vz )α , Ryv (£≡vz )α |=* Ryv (£≡vz )α , therefore the statements
≡xyα , Rxv (Φ)α ,Γ M |=* Δ and ≡xyα , Rxv (Φ)α , Ryv (Φ)α Γ M |=* Δ equivalent; in thegeneral case, the statements ≡xyα , Rwv,,u⊥,,vx (Φ)α , Rwv,,u⊥,,vy (Φ)α ,Γ M |=∗ Δ are not equivalent.
Thus, the condition validity for ≡ хуα is insufficient for the substitution of equals.
Assertion 3. We have ≡ хуα, Exα, Eyα, £≡ хzα, |=*£≡ уzα.
Let us prove this by contradiction for the case of |=IR, similarly, it is proven for |=T, |=F, and |=TF.
Let us assume the opposite: suppose for some GMS M = (St, R, A, Im) and α∈St, d∈VA we have (≡ ху)α(d) = Т, Exα(d) = T, Eyα(d) = T, (£≡ хz)α(d) = T and (£≡ yz)α(d) = F; from this dα(x)$ = dα(y)$ = a∈Aα for some a∈A ⇒ d(x) = d(y) = a. According to (£≡ yz)α(d) = F we have (≡ yz)β(d) = F for some β such that α > β . According to (£≡ хz)α(d) = T we have (≡ хz)β(d) = T, which gives us two possible cases: 1) dβ(x)# and dβ(z)#; hence d(x)∉dβ, and since d(x) = d(y) = a we have dβ(y)#, so (≡ yz)β(d) = T, which contradicts (≡ yz)β(d) = F.
2) dβ(x)$ = dβ(z)$; since d(x) = d(y) = a then dβ(z) = dβ(x) = dβ(y) = a, which contradicts (≡ yz)β(d) = F. In both cases, we obtained a contradiction.
Assertion 4. We have ≡ хуα, Exα, Eyα |=*£≡ xyα, where the symbol * denotes either IR or F.
It is sufficient to prove for the case |=F. Let us assume the opposite: suppose for some GMS M = (St, R, A, Im) and α∈St, d∈VA we have (£≡ xy)α(d) = F, (≡ ху)α(d) ≠ F, Exα(d) ≠ F, Eyα(d) ≠ F. Since the predicates Ex and ≡ xy are total, we have (≡ ху)α(d) = T, Exα(d) = T, Eyα(d) = T. Hence dα(x)$, dα(y)$, and since (≡ ху)α(d) = T, therefore dα(x) = dα(y) = a for some a∈Aα ⊆ A, so d(x) = d(y) = a. Given (£≡ xy)α(d) = F, we have (≡ xy)β(d) = F for some β such that α > β. We obtain three possible cases: 1) dβ(x)$, dβ(y)$ and dβ(x) ≠ dβ(y); since Aβ ⊆ A then d(x)$, d(y)$ and d(x) ≠ d (y); at the same time we have d(x) = d(y) = a, which gives us a contradiction;
2) dβ(x)$ and dβ(y)#; since Aβ ⊆ A then dβ(x) = d(x) = d(y) = a, so a∈Aβ, hence dβ(y) = a, which contradicts dβ(y)#; 3) the case dβ(x)# and dβ(y)$ is treated similarly to 2).
Assertion 5. In the general case we have ≡ хуα, Exα, Eyα |≠T £≡ xyα. Indeed, for GMS M = (St, R, A, Im), where no β exists such that α > β , we have (£≡ xy)α(d)# for all d∈VA. However, for d = [x a a, y a a] with a∈Aα we have (≡ ху)α(d) = T, Exα(d) = T, Eyα(d) = T.
At the same time, by adding £≡ xx to the left side, |=F and |=IR are preserved, and |=T is guaranteed even in the absence of β such that α > β . Indeed, then (£≡ xy)α(d)# and (£≡ xx)α(d)# for all d∈VA. Hence, we get:
Assertion 6. We have ≡ хуα, Exα, Eyα, £≡ xxα |=*£≡ xyα, where * denotes one of the IR, F, T, TF. Note that the reflexivity of the relation > guarantees |=T and |=TF in Assertion 6. ≡xyα , Rwv,,u⊥,,vx (Φ)α ,Γ M |=∗ Δ are not and
Adding the validity conditions Exα та Eyα to the validity condition ≡ хуα allows for the substitution of equals. Finally, we have the following properties of substitution of equals in GMSQ≡: ≡ rpL) ≡xyα , Exα , Eyα , Rwv,,u⊥,,zx (Φ)α ,Γ M |=∗ Δ ⇔
≡xyα , Exα , Eyα , Rwv,,u⊥,,zx (Φ)α, Rwv,,u⊥,,zy (Φ)α, Γ M |=∗ Δ; ≡ rpR) ≡xyα , Exα , Eyα ,Γ M |=∗ Rwv,,u⊥,,zx (Φ)α , Δ ⇔ ≡xyα , Exα , Eyα ,Γ M |=∗ Rwv,,u⊥,,zx (Φ)α , Rwv,,u⊥,,zy (Φ)α, Δ; ≡ ¬rpL) ≡xyα , Exα , Eyα ,¬Rwv,,u⊥,,zx (Φ)α ,Γ M |=∗ Δ ⇔ ≡xyα, Exα, Eyα,¬Rwv,,u⊥,,zx (Φ)α,¬Rwv,,u⊥,,zy (Φ)α,Γ M |=∗ Δ; ≡ ¬rpR) ≡xyα , Exα , Eyα ,Γ M |=∗ ¬Rwv,,u⊥,,zx (Φ)α , Δ ⇔ ≡xyα, Exα, Eyα,Γ M |=∗ ¬Rwv,,u⊥,,zx (Φ)α,¬Rwv,,u⊥,,zy (Φ)α, Δ.
Let us describe the properties related to modal compositions. In TMS of non-monotonic predicates with equality, these properties are generally analogous to the corresponding properties of TMS without equality predicates (see, for example, [12]). These are properties of carrying modalities over renominations, which belong to the properties of equivalent transformations, and properties of modality elimination. We will present the properties of carrying £ over renomination in GMS.
R*L) Γ, Rxv,,⊥u (£Φ)α M |=* Δ ⇔ Γ, £Rxv,,⊥u (Φ)α M |=∗ Δ ; ¬R*L) Γ,¬Rxv,,⊥u (£Φ)α M |=* Δ ⇔ Γ, ¬£Rxv,,⊥u (Φ)α M |=∗ Δ; R*R) Γ M |=* Δ, Rxv,,⊥u (£Φ)α
⇔ Γ M |=∗ Δ, £Rxv,,⊥u (Φ)α ; ¬R*R) Γ M |=* Δ,¬Rxv,,⊥u (£Φ)α
⇔ Γ M |=∗ Δ, ¬£Rxv,,⊥u (Φ)α .
For the relation M|=IR, it is sufficient to have the properties R*L and R*R.
The properties of elimination of the modal composition £ in TMS are as follows: £L) £Φα, Γ M|=* Δ ⇔ {Φβ | α > β}∪Γ M|=* Δ; ¬£R) Γ M|=* Δ, ¬£Φα ⇔ Γ M|=* Δ∪{¬Φβ | α > β}; £R) Γ M|=* Δ, £Φα ⇔ Γ M|=* Δ, Φβ for all states β∈S such that α > β ; ¬£L) ¬£Φα, Γ M|=* Δ ⇔ ¬Φβ, Γ M|=* Δ for all states β∈S such that α > β.
For the relation M|=IR, it is sufficient to have the properties £L and £R.
Similar properties related to modal compositions are formulated for TmMS тa MMS.
For the properties of the relation M|=*, the corresponding dual properties of the relation M|≠* can be specified (see [11]), using which the sequent forms of the calculus that formalizes M|=* can be directly formulated. In particular, the properties of modality elimination for M|≠* in GMS have the form: n£L) £Φα, Γ M|≠* Δ ⇔ {Φβ | α > β }∪Γ M|≠* Δ; n¬£R) Γ M|≠* Δ, ¬£Φα ⇔ Γ M|≠* Δ∪{¬Φβ | α > β }; n£R) Γ M|≠* Δ, £Φα ⇔ Γ M|≠* Δ, Φβ for some β∈S such that α > β; n¬£L) ¬£Φα, Γ M|≠* Δ ⇔ ¬Φβ, Γ M|≠* Δ for some β∈S such that α > β .
With additional conditions imposed on the relation > , the properties of modality elimination are correspondingly modified. For the cases where the relation can be either transitive, reflexive, symmetric, or their combinations, these properties are described, in particular, in [11].
Properties of logical consequence relations on sets of formulas specified with states are the semantic foundation for construction of the sequent type calculi for TML. Specifications take the form of α|– or α–|, where α is the name of the state. Sequents are treated as sets of such formulas. By singling out |–-formulas and –|-formulas, we denote sequents by |–Γ–|Δ.
Sequents are enriched with sets of relations on states obtained at the time of derivation. Let M be such a reachability relation constructed for the names of states i.e. world model schema. The enriched sequents are denoted by Σ // M.
The sets of defined, undefined, and undistributed names of a state α of the sequent Σ are defined as: val(Σα) = {u | α|–Eu∈Σ}; unv(Σα) = {u | α–|Eu∈Σ}; ud(Σα) = nm(Σα) \ (val(Σα) ∪ unv(Σα)).
We propose sequent calculi that formalize the relation M=|=IR in GMSQ= and the relations M|=IR, M|=T, M|=F, M|=TF in GMSQ≡. The calculus for the relation M=|=IR in GMSQ= will be called СGQ=IR, and the calculi for M|=IR, M|=T, M|=F, M|=TF in GMSQ≡ will be called СGQ≡IR, СGQ≡T, СGQ≡F, СGQ≡TF.
In this paper, we will restrict ourselves to describing the calculi СGQ≡IR, СGQ≡T, СGQ≡F, СGQ≡TF. The calculus СGQ=IR is generally similar to СGQ≡IR, but with =xx serving as predicates-indicators.
Sequent calculus is defined by basic sequent forms and closedness conditions for sequents.
The derivation in sequent calculi has the form of a tree, the vertices of which are sequents; such trees are called sequent trees. Inference rules in sequent calculi are called sequent forms; they are induced by properties of logical consequence relations for sets of formulas specified with states. Closed sequents are axioms of the sequent calculus. The closedness of |–Γ–|Δ must guarantee Γ |= Δ. The sequent tree is closed if every its leaf is a closed sequent. The sequent Σ is derivable if there exists a closed sequent tree with the root Σ, called a derivation of the sequent Σ.
The closedness conditions for |–Γ–|Δ are defined by the specified above conditions that guarantee the corresponding logical consequence relation Γ M|=* Δ.
Although the calculi СGQ≡T, СGQ≡F, СGQ≡TF have the same basic sequent forms, their closedness conditions for sequents are different.
We have the following closedness conditions for a sequent Σ: С) there exists a formula Φ: α|–Φ∈Σ and α–|Φ∈Σ; СF) there exists a formula α|− Rxv,,⊥u,,⊥z (Ez) ∈ Σ ; СL) there exists a formula Φ: α|–Φ∈Σ and α|–¬Φ∈Σ; СR) there exists a formula Φ: α–|Φ∈Σ and α–|¬Φα∈Σ; СLR) there exist formulas Φ and Ψ: α|–Φ∈Σ, α|–¬Φ∈Σ and α–|Ψ∈Σ, α–|¬Ψ∈Σ; СRf≡) there exists a formula α–| ≡xxα∈Σ; CE≡L) there exist formulas ≡xy, Ex and Ey: α|– ≡xy∈Σ, α|– Ex∈Σ, α–|Ey∈Σ; CE≡R) there exist formulas ≡xy, Ex and Ey: α–| ≡xy∈Σ, α–|Ex∈Σ, α–|Ey∈Σ;
CT≡) there exists a formula Rvx,,u⊥,,x⊥,,z⊥ (≡xz ) : α−| Rvx,,u⊥,,x⊥,,z⊥ (≡xz ) ∈Σ .
Thus, we get the following closedness conditions for a sequent Σ in a certain calculus: – for the calculus MCQ≡T: the condition С ∨ CF ∨ CL ∨ СRf≡ ∨ CE≡L ∨CE≡R ∨CT≡; – for the calculus MCQ≡F: the condition С ∨ CF ∨ CR ∨ СRf≡ ∨ CE≡L ∨CE≡R ∨CT≡; – for the calculus MCQ≡TF: the condition С ∨ CF ∨ CLR ∨ СRf≡ ∨ CE≡L ∨CE≡R ∨CT≡ .
The closedness condition for the calculus MСQ≡IR: С ∨ CF ∨ СRf≡ ∨ CE≡L ∨CE≡R ∨CT≡. Let us present basic sequent forms for the calculi MCQ≡T, MCQ≡F, MCQ≡TF.
Simplification forms (types R, RІ, RU, R#1, R#2, and ≡elR):
α|− Φ, Σ // M α−| Φ, Σ // M |–RU |–¬RU α|− Rxv,,⊥u (Φ), Σ // M α|− Rzy,,xv,,⊥u (Φ), Σ // M α|− ¬Rxv,,⊥u (Φ), Σ // M α|− ¬Rzy,,xv,,⊥u (Φ), Σ // M , у∈ν(Φ); , у∈ν(Φ); –|RU –|¬RU α−| Rxv,,⊥u (Φ), Σ // M α−| Rzy,,xv,,⊥u (Φ), Σ // M α−| ¬Rxv,,⊥u (Φ), Σ // M α−| ¬Rzy,,xv,,⊥u (Φ), Σ // M , у∈ν(Φ); , у∈ν(Φ); α|− R(Φ), Σ // M
α|− ¬Φ, Σ // M α|− ¬R(Φ), Σ // M ;
; |–R |–¬R |–RI α|− Rxv,,⊥u (Φ), Σ // M α|− Rzz,,xv,,⊥u (Φ), Σ // M
; |–¬RI α|− ¬Rxv,,⊥u (Φ), Σ // M α|− ¬Rzz,,xv,,⊥u (Φ), Σ // M ; α−| R(Φ), Σ // M
α−| ¬Φ, Σ // M α−| ¬R(Φ), Σ // M ;
; –|R –|¬R –|RI α−| Rxv,,⊥u (Φ), Σ // M α−| Rzz,,xv,,⊥u (Φ), Σ // M
; –|¬RI α−| ¬Rxv,,⊥u (Φ), Σ // M α−| ¬Rzz,,xv,,⊥u (Φ), Σ // M
; , p ∈ Ps; , p ∈ Ps; , p ∈ Ps; –|¬R#1
–|R#2 –|¬R#2 –|≡elR –|≡el¬R Forms of equivalemt transformations – renomination of predicates-indicators: Forms of equivalemt transformations – renomination of equality predicates: , z ∉{v , u}; , z ∉{v , u}; |–R#1 |–¬R#1 |–R#2 |–¬R#2 α|− α|− R v ,u , y x ,⊥,⊥ v ,u , y x ,⊥,z ( p), ( p), v ,u , y α|− ¬Rx ,⊥,⊥
v ,u , y α|− ¬Rx ,⊥, z α|− α|−
R v ,u x ,⊥ R v ,u ,z x ,⊥,⊥ ( p), ( p), v ,u α|− ¬Rx ,⊥
v ,u ,z α|− ¬Rx ,⊥,⊥ α−| α−| ( p), ( p), α−| α−| ( p), ( p),
Ez, Σ // M Ez, Σ // M α−| α−|
Ez, Σ // M
Ez, Σ // M Ez, Σ // M Ez, Σ // M α−| α−|
Ez, Σ // M
Ez, Σ // M |–≡elR |–≡el¬R α|− ≡ xy , α|− R v ,u w,⊥ (Φ), Σ // M α|− ≡ xy , α|− R v ,u ,x w,⊥, y (Φ), Σ // M
; v ,u α|− ≡ xy , α|− ¬Rw,⊥ (Φ), Σ // M
v ,u ,x α|− ≡ xy , α|− ¬Rw,⊥, y (Φ), Σ // M
; , p ∈ Ps; –|R#1 α−| α−|
Rv ,u , y α−| x ,⊥,⊥
Rv ,u , y α−| x ,⊥,z ¬R ¬R v ,u , y x ,⊥,⊥ v ,u , y x ,⊥,z ( p), ( p), ( p), ( p), α−| α−| α−| α−|
Ez, Σ // M Ez, Σ // M Ez, Σ // M
Ez, Σ // M α−| Rxv,,⊥u
Rv ,u ,z α−| x ,⊥,⊥ ( p), ( p), α−| α−|
Ez, Σ // M
Ez, Σ // M α−| α−| ¬R v ,u x ,⊥ ¬R v ,u ,z x ,⊥,⊥ ( p), ( p), α−| α−|
Ez, Σ // M
Ez, Σ // M α|− ≡ xy , α−| Rwv,,u⊥ (Φ), Σ // M α|− ≡ xy , α−| Rwv,,u⊥,,xy (Φ), Σ // M
; v ,u α|− ≡ xy , α−| ¬Rw,⊥ (Φ), Σ // M
v ,u ,x α|− ≡ xy , α−| ¬Rw,⊥, y (Φ), Σ // M .
Condition for the forms |–R≡0 and –|R≡0: x, y ∉{u , v}, x ≠ y.
Condition for the forms |–R≡1, –|R≡1, |–R≡1E and –|R≡1E: y ∉{u , v}, x ≠ y.
α|− α|−
Ryv,,⊥z oux ,,t⊥ (Φ), Σ // M R v , z y ,⊥ (R u ,t x ,⊥ (Φ)), Σ // M v ,z u ,t α|− ¬Ry ,⊥ ox ,⊥ (Φ), Σ // M
v ,z α|− ¬Ry ,⊥ (R u ,t x ,⊥ (Φ)), Σ // M
; Forms of equivalemt transformations – renomination of compositions: −|RR α−| Ryv ,,⊥z oux ,,t⊥ (Φ), Σ // M α−| Ryv,, ⊥z (R u ,t x ,⊥ (Φ)), Σ // M ; , p ∈ Ps;
, p ∈ Ps; . ; . , p ∈ Ps; |–R⊥E |–R⊥Ev |–R≡xx |–R≡0 |–R≡1 |–R≡1E |–R≡2 |–R≡2E |−RR |−¬RR |−R¬ ; ; ; ; ; ; ; ; α|− α|− R v ,u x ,⊥ α|−
Ez, Σ // M (Ez), Σ // M
Ey, Σ // M α|−
R v ,u ,z x ,⊥, y (Ez), Σ // M α|− ≡xx , Σ // M α|−
R v ,u w,⊥ (≡xx ), Σ // M α|− ≡ xy , Σ // M α|−
R α|−
R v ,u x ,⊥ (¬Φ), Σ // M
; α|− ≡ zy , Σ // M α|−
Rwv,,u⊥,,xz (≡xy ), Σ // M α−|
Ey, Σ // M α|−
R v ,u ,x w,⊥,⊥ (≡xy ), Σ // M α|− ≡zs , Σ // M α|−
R v ,u ,x, y w,⊥,z,s (≡xy ), Σ // M α−|
Ez, Σ // M α|−
R v ,u ,x, y w,⊥,z,⊥ (≡xy ), Σ // M α−|
Ez, Σ // M α−| Rxv,,⊥u (Ez), Σ // M α−|
Ey, Σ // M α−| Rxv,,⊥u,,zy (Ez), Σ // M
α−| ≡xx , Σ // M α−| Rwv,,u⊥ (≡xx ), Σ // M
α−| ≡xy , Σ // M α−| Rwv,,u⊥ (≡xy ), Σ // M . .
; α−| ≡ zy , Σ // M α−| Rwv,,u⊥,,xz (≡xy ), Σ // M
; α|−
Ey, Σ // M α−| Rwv,,u⊥,,x⊥ (≡xy ), Σ // M
α−| ≡zs , Σ // M α−| Rwv,,u⊥,,xz,,sy (≡xy ), Σ // M α|−
Ez, Σ // M α−| Rwv,,u⊥,,xz,, ⊥y (≡xy ), Σ // M –|R⊥E –|R⊥Ev –|R≡xx –|R≡0 –|R≡1 –|R≡1E –|R≡2 –|R≡2E −|¬RR −|R¬ α−| α−| ¬Ryv,,⊥z oux ,,t⊥ (Φ), Σ // M ¬R v ,z y ,⊥ (R u ,t x ,⊥ (Φ)), Σ // M
; α−| ¬R α−| Rxv,,⊥u (¬Φ), Σ // M ; α|−
Rxv,,⊥u (Φ), Σ // M
v ,u α|− ¬Rx ,⊥ (¬Φ), Σ // M
; α|−
Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ), Σ // M α|−
Rxv,,⊥u (Φ ∨ Ψ), Σ // M
; α|− ¬(Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ)), Σ // M
v ,u α|− ¬Rx ,⊥ (Φ ∨ Ψ), Σ // M
; v ,u α|− Rx ,⊥ (Φ), Σ // M α|−
Rxv,,⊥u (Φ), Σ // M
; v ,u α|− ¬Rx ,⊥ (Φ), Σ // M
v ,u α|− ¬Rx ,⊥ (Φ), Σ // M ; −|¬R¬ −|R∨ −|¬R∨ −|R£ −|¬R£ α−| ¬R
; α−| Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ), Σ // M α−| Rxv,,⊥u (Φ ∨ Ψ), Σ // M
; α−| ¬(Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ)), Σ // M α−| ¬R v ,u x ,⊥ (Φ ∨ Ψ), Σ // M
; α−| α−| R . |−¬R¬ |−R∨ |−¬R∨ |−R£ |−¬R£ |–¬E≡ |–¬RE |–¬≡ |–¬R≡ |–¬¬ |−∨ |−¬∨ |–∃ |–∃R –|∃v –|∃Rv Forms of elimination for the constant T-formula:
ElRE
Σ // M α|−
Rxv,,⊥u,,⊥z (Ez), Σ // M ;
El≡
Σ // M α|− ≡ xx , Σ // M ;
ElR≡
Σ // M α|−
Rwv,,u⊥,,x⊥,,y⊥ (≡ xy ), Σ // M .
Forms of elimination of ¬ in formulas related to TS-predicates: α−| Ez, Σ // M α|− ¬Ez, Σ // M α−| Rwv,,u⊥ (Ez), Σ // M
v ,u α|− ¬Rw,⊥ (Ez), Σ // M Forms of quantifier elimination:
x α|− Rz (Φ),
α|− Ez, Σ // M α|− ∃xΦ, Σ // M
; α|−
Rwv,,u⊥,,xz (Φ), α|− Ez, Σ // M α|−
Rwv,,u⊥ (∃xΦ), Σ // M
; x α−| ∃xΦ, α−| Ry (Φ),
α|− Ey, Σ // M α−| ∃xΦ, α|− Ey, Σ // M
; α−| Rwv,,u⊥ (∃xΦ), α−|
Rwv,,⊥u,,xy (Φ),
α|− Ey, Σ // M α−| Rwv,,u⊥ (∃xΦ), α|− Ey, Σ // M –|¬∃ –|¬∃R |–¬∃v ;
x α−| ¬Rz (Φ),
α|− Ez, Σ // M α−| ¬∃xΦ, Σ // M
; α−| ¬Rwv,,u⊥,,xz (Φ), α|− Ez, Σ // M α−| ¬R v ,u w,⊥ (∃xΦ), Σ // M
; α|− ¬∃xΦ, α|− ¬Ryx (Φ),
α|− Ey, Σ // M α|− ¬∃xΦ, α|− Ey, Σ // M ; |–¬∃Rv α|− ¬Rwv,,u⊥ (∃xΦ), α|− ¬Rwv,,u⊥,,xy (Φ), α|− Ey,Σ // M Condition for |–∃ and –|¬∃: z∈fu(Σ, ∃xΦ); condition for |–∃R and –|¬∃R: z ∈ fu(Rwv,,⊥u (∃xΦ)).
The forms |–∃, –|¬∃, |–∃R and –|¬∃R will be called ∃T-forms; the forms –|∃v, |–¬∃v, –|∃Rv and |–¬∃Rv will be called ∃F-forms.
Forms of E-distribution and primary definition:
Ed α|− Ex, Σ // M α−|Ex, Σ // M
, where α|–Ex, α–|Ex ∉Σ.
Σ
Tr≡ α−| ≡xy , α|− ≡yz , α|− ≡xz ,Σ // M
; α|− ≡xy , α|− ≡yz ,Σ // M |–≡rp α|− ≡xy , α|− Ex, α|− Ey, α|− Rwv,,⊥u,,zx (Φ), α|− Rwv,,⊥u,,zy (Φ),Σ // M
α|− ≡xy , α|− Ex, α|− Ey, α|− Rwv,,⊥u,,zx (Φ),Σ // M –|≡rp α|− ≡xy , α|− Ex, α|− Ey, α−| Rwv,,⊥u,,zx (Φ), α−| Rwv,,⊥u,,zy (Φ),Σ // M α|− ≡xy , α|− Ex, α|− Ey, α−| Rwv,,⊥u,,zx (Φ),Σ // M ; ; |–¬≡rp α|− ≡xy , α|− Ex, α|− Ey, α|− ¬Rwv,,u⊥,,zx (Φ), α|−¬Rwv,,⊥u,,zy (Φ),Σ // M
α|− ≡xy , α|− Ex, α|− Ey, α|− ¬Rwv,,u⊥,,zx (Φ),Σ // M –|¬≡rp α|− ≡xy , α|− Ex, α|− Ey, α−|¬Rwv,,u⊥,,zx (Φ), α−|¬Rwv,,u⊥,,zy (Φ),Σ // M α|− ≡xy , α|− Ex, α|− Ey, α−|¬Rwv,,u⊥,,zx (Φ),Σ // M ; .
The forms of modal operator elimination depend on the properties of the relation > . We will describe these forms in the general case where no additional conditions are imposed on the relation.
The names of the calculi MCQ≡T, MCQ≡F and MCQ≡TF correspond to this case.
If at the moment of applying the form to α|−£Φ or α−|¬£Φ we have states β1,…, βn such that α > β1,...,α > βn , then we apply the corresponding form to α|−£Φ or α|−¬£Φ:
α|− Φ,Σ // M α−|¬Φ,Σ // M If there are no such γ such that α > γ , then we apply the form to α|−£Φ or α−|¬£Φ: |−£ α|− Φ, β1|− Φ,..., βn|−Φ, Σ // M ; −|¬£ α−|¬Φ, β1−| ¬Φ,..., βn −|¬Φ, Σ // M . |−£f α|− Φ, β|− Φ,Σ // M ∪{α > β}
α|− Φ, Σ // M −|¬£f α−| ¬Φ, β−| ¬Φ,Σ // M ∪{α > β} α−|¬Φ, Σ // M , β is a new state;
, β is a new state.
The elimination form applied to α−|£Φ or α|−¬£Φ is: −|£ β−|Φα,Σ−|//ΦM, Σ∪/{/αM> β} , β is a new state; |−¬£ β|− ¬Φα|−,¬Σ//ΦM, Σ∪/{/αM> β} , β is a new state.
Let us describe basic sequent forms for the sequent calculus MСQ≡IR. There is no need to list the sequent forms for external negation on renomination, which results in the following basic forms.
Simplification forms |–R, –|R, |–RI, –|RI, |–RU, –|RU, –R#1, –|R#1, |–R#2, –|R#2, |–≡elR, –|≡elR.
Forms of equivalemt transformations: |−RR, −|RR, |−R¬, −|R¬, |−R∨, −|R∨, |−R£, −|R£; |–R⊥E, –|R⊥E, |–R⊥Ev, –|R⊥Ev; |–R≡xx, –|R≡xx, |–R≡0, –|R≡0, |–R≡1, –|R≡1, |–R≡2,–|R≡2, |–R≡1E, –|R≡1E, |–R≡2E, –|R≡2E.
Forms of elimination for the constant T-formula ElRE, El≡, ElR≡.
Forms of decomposition of the formulas |−∨ and −|∨, to which the forms |–¬ and −|¬ are added: |– ¬
Forms of quantifier elimination |–∃, |–∃R, –|∃v, –|∃Rv; E-distribution Ed, and primary definition Ev. Forms of transitivity and substitution of equals Tr≡, |–≡rp, –|≡rp.
Forms of modal operator elimination |−£, |−£f, −|£ (in the absence of additional conditions on > ). We have the following groups of basic forms for the calculi MCQ≡T, MCQ≡F, MCQ≡TF, MСQ≡IR: – auxiliary simplification forms: types R, RІ, RU, R#1, R#2, and ≡elR; – forms of E-distribution and primary definition: Ed та Ev; – main forms: all other basic sequent forms.
The main property of the listed basic sequent forms of TML is described by Theorem 7. Let |− Λ−|Κ // M and |− Λ−|Κ // M |− Γ−|Δ // M |− Γ−|Δ // M |−Χ−|Ζ // M be sequent forms. Then: 1) Λ |=* Κ ⇔ Γ |=* Δ; Λ |=* Κ and Χ |=* Ζ ⇔ Γ |=*’ Δ; 2) Γ |≠* Δ ⇔ Λ |≠* Κ; Γ |≠* Δ ⇔ Λ |≠* Κ and Χ |≠* Ζ.
Let us briefly describe the construction of derivations in sequent calculi for TML. The step-bystep construction of a sequent tree for countable sequents in TML calculi is similar to that for calculi of quasiary predicate logics (see [9, 13]). The process is carried out in parallel with the formation of the world model schema. This schema is updated with each application of the appropriate forms of modality elimination, which add new states.
The construction of the tree begins from its root – the initial sequent Σ. Each application of a sequent form is performed on a finite set of formulas available at the moment.
At the start of each stage, an access step is performed: one formula from each of the lists of |−formulas and −|-formulas is added to the list of available formulas. At the beginning of the construction, a pair of the first formulas from these lists is available (either a single |−-formula or −|formula, if one of the lists is empty).
After applying each sequent form, we check the resulting sequent Ω for closedness. If a closed sequent is obtained, no further forms can be applied to it, and the construction of the tree on this path terminates. If all leaves of the constructed tree are closed, then we have a closed sequent tree, and the proof construction is completed successfully.
If the construction is not completed, for each non-closed leaf ξ, we proceed with the next access step and then extend a finite subtree with root ξ as follows. We activate all available (except primitive) formulas of ξ. Next, we apply the corresponding sequent forms to each active formula. Whenever appropriate, we perform simplifications using the necessary auxiliary forms of the types R, RI, RU, R#1, R#2, and ≡elR; forms of the types R#1 and R#2 are applied to primitive formulas and their negations, yielding primitive Un-forms (see [13]) with the set Un = {x | α–|Ex∈Θ}, where Θ is the set of formulas on the path from the root Σ to the given sequent. After applying the main form and performing simplifications, the formulas generated on this stage become passive; at this stage, the main sequent forms cannot be applied to such formulas.
In the application of the main sequent forms, the process proceeds as follows. First, all nonmodalized forms are executed. The application of ∃T-forms precedes the application of ∃F-forms. When applying an ∃T-form, we always select a new totally non-essential z that does not appear on the path from the root to the sequent where the ∃T-form is applied. Each ∃F-form is applied multiple times for each assigned component у from formulas on the path from Σ to the given sequent η. Let Ξ be the set of available sequent formulas on the path from Σ to η. For each α, we define Udα = ud(Ξα). If, when transitioning to the application of an ∃F-form, Udα ≠ ∅, then there are undistributed names of the state α, so using Еd, we perform all possible distributions of names from Udα into assigned and unassigned ones. This results in constructing a subtree of height |Udα| with the subroot η, which produces m = 2|Udα| successors of η – sequents η1,…,ηm with sets Vnαk ⊆ Udα of new assigned names. If val(Ξα) = ∅, then for ηj, where Vnαj = ∅, we perform the initial assignment – adding α|–Ez for a new totally unessential z, which results in Vnαj = {z}. In each of these ηk, we apply the ∃F-form for each у∈Vnαk.
The forms Tr≡ are applied every time a pair of formulas of the form α|–≡xy and α|–≡yz appears, where at least one of them is new to the sequent. The forms of the type ≡ rp (substitution of equals) are applied each time a pair of formulas appears, one of which is of the form α|– ≡xy, and the other is one of the forms α|− Rwv,,u⊥,,zx ( p), α−| Rwv,,u⊥,,zx ( p), α|− ¬Rwv,,u⊥,,zx ( p), α−|¬Rwv,,u⊥,,zx ( p), where at least one of them is new to the sequent.
Next, we apply –|£-forms, and finally, at the end of the stage, we apply – |−£-forms. If the construction of the sequent tree is completed successfully, then we obtain a closed tree.
If the construction does not complete, then we have an infinite, unclosed tree. In such a tree, there is an unclosed path ℘ (by König's lemma, see [15]), all of whose vertices are unclosed sequents. Each of the formulas from the initial sequent Σ will appear on ℘ and become accessible.
For the proposed sequent calculi for TML, the soundness and completeness theorems hold. For these calculi, the theorems are formulated in a similar manner, with the relations |=IR, |=T, |=F, |=TF corresponding to the calculi MCQ≡IR, MCQ≡T, MCQ≡F, MCQ≡TF.
Theorem 8 (soundness). Let the sequent |–Γ–|Δ be derivable in the calculus С; then Γ |=*Δ.
Let |–Γ–|Δ be derivable in the calculus С. Then, a closed sequent tree has been constructed for it. All its leaves are closed sequents, so for each such leaf |–Χ–|Ζ, we have Χ |=* Ζ. The movement from the leaves of the tree to its root is accomplished using sequent forms. By Theorem 7, the relation |=* is preserved when moving from the premises of the forms to the conclusions. Therefore, Λ|=* Κ for each vertex |–Λ–|Κ of the sequent tree. In particular, for the root |–Γ–|Δ we also have Γ |=* Δ.
The proof of completeness for the sequent calculi of TML relies on the theorem about constructing a counter-model using an unclosed path in the sequent tree built in the corresponding calculus. The proof of the counter-model theorems is based on the method of model (Hintikka) sets (see [11]).
Theorem 9 (on counter-models for the calculus MСQ≡TF). Let ℘ be an unclosed path in a sequent tree constructed for the sequent |–Γ–|Δ in the calculus MСQ≡TF, and let S be the set of names of states of the world in the specified formulas along the path ℘. Then there exist GMS MT = (St, R, А, IтT), MF = (St, R, A, IтF), and δ∈VA such that for all α∈S: α|–Φ∈Нα ⇒ ΦTα(δ) = Т; α–|Φ∈Нα ⇒ ΦTα(δ) ≠ T.
α|–Φ∈Нα ⇒ ΦFα(δ) ≠ F; α–|Φ∈Нα ⇒ ΦFα(δ) = F.
Here, ΦTα and ΦFα denote IтT(Φ, α) and IтF(Φ, α), respectively.
Such GMS MT and MF are called T-conter-model and F-counter-model for |–Γ–|Δ.
Let M be the union of all world model schemes of the sequents on the path ℘, then S is the set of state names from M. Let Нα be the set of all specified formulas of the state α on the path ℘ Wα = nm(Нα)\unv(Нα), W = U Wα , НM = ({Нα | α∈S}, M).
α∈S Such НM is called a model system (i.e. a set of model sets).
Equality predicates induce equivalence relations on the sets Wα: x ∼α y ⇔ α|– ≡xy, α|–Ex, α|–Ey ∈ Н .
α Let us denote 〈v〉α = {u | v ∼α u}. Now, we define 〈v〉 = {u | v ∼α u for some α∈S}.
This definition is correct. It is based on the interpretation of the equality of basic data as an identity: for the same data d, it is impossible for d(x)↓ = d(y)↓ on one state and d(x)↓ ≠ d(y)↓ on another state.
We denote Aα = {〈v〉 | v∈Wα]. Then A = U Aα = {〈v〉 | v∈W}.
α∈S Let us specify δ = [v"〈v〉 | v∈W] and δα = [v"〈v〉 | v∈Wα].
For predicates-indicators and equality predicates in GMS MT and MF, we have: – α|–Ex ∈ Нα implies x∈W, so ExTα(δ) = T and ExFα(δ) = T, therefore ExFα(δ) ≠ F; – α–|Ex ∈ Нα implies x∉W, so ExTα(δ) = F, therefore ExTα(δ) ≠ T, and ExFα(δ) = F; – α|–≡xy ∈Нα ⇒ (≡xy) α(δ) = T and (≡xy)Fα(δ) = T, therefore (≡xy)Fα(δ) ≠ F; – α–|≡xy ∈Нα ⇒ (≡xy)Tα(δ) = F, therefore (≡xy)Tα(δ) ≠ T, and (≡xy)Fα(δ) = F. – α|− Rxv,,⊥u ( p) ∈ Hα ⇒ pTα (rvx,,u⊥ (δ)) = T and pFα (rvx,,u⊥ (δ)) ≠ F; – α−| Rxv,,⊥u ( p) ∈ Hα
⇒ pTα (rvx,,u⊥ (δ)) ≠ T and pFα (rvx,,u⊥ (δ)) = F; – α|− ¬Rxv,,⊥u ( p) ∈ Hα ⇒ ¬pTα (rvx,,u⊥ (δ)) = T and ¬pFα (rvx,,u⊥ (δ)) ≠ F; – α−|¬Rxv,,⊥u ( p) ∈ Hα ⇒ ¬pTα (rvx,,u⊥ (δ)) ≠ T and ¬pFα (rvx,,u⊥ (δ)) = F.
Next, we prove by induction on the formula structure.
Similarly, the theorems on counter-models for the calculi MСQ≡T and MСQ≡F can be formulated.
Theorem 10 (on a counter-model for the calculus MСQ≡T). Let ℘ be an unclosed path in a sequent tree constructed for the sequent |–Γ–|Δ in the calculus MСQ≡T, and let S be the set of names of states of the world in the specified formulas along the path ℘. Then there exist GMS M = (St, R, А, Iт) and δ∈VA such that for all α∈S:
α|–Φ∈Нα ⇒ Φα(δ) = Т; α–|Φ∈Нα ⇒ Φα(δ) ≠ T.
Such GMS M will be called a T-counter-model for |–Γ–|Δ.
Theorem 11 (on a counter-model for the calculus MСQ≡F). Let ℘ be an unclosed path in a sequent tree constructed for the sequent |–Γ–|Δ in the calculus MСQ≡F, and let S be the set of names of states of the world in the specified formulas along the path ℘. Then there exist GMS M = (St, R, А, Iт) and δ∈VA such that for all α∈S:
α|–Φ∈Нα ⇒ Φα(δ) ≠ F; α–|Φ∈Нα ⇒ Φα(δ) = F.
Such GMS M will be called an F-counter-model for |–Γ–|Δ.
Let us examine in detail the theorem on the counter-model for the calculus MСQ≡IR.
Theorem 12 (on a counter-model for the calculus MСQ≡IR). Let ℘ be an unclosed path in a sequent tree constructed for the sequent |–Γ–|Δ in the calculus MCQ≡IR, and let S be the set of names of states of the world in the specified formulas along the path ℘. Then there exist GMS M = (St, R, А, Iт) and δ∈VA such that for all α∈S:
α|–Φ∈Нα ⇒ Φα(δ) = Т; α–|Φ∈Нα ⇒ Φα(δ) = F.
Such GMS M will be called an IR-conter-model for |–Γ–|Δ.
We specify δ = [v"〈v〉 | v∈W] and δα = [v"〈v〉 | v∈Wα] as described in Theorem 9. For predicates-indicators and equality predicates in GMS M, we have: – α|–Ex ∈ Нα implies x∈W, therefore Exα(δ) = T; – α–|Ex ∈ Нα implies x∉W, therefore Exα(δ) = F; – α|–≡xy ∈Нα ⇒ (≡xy)α(δ) = T; – α–|≡xy ∈Нα ⇒ (≡xy)α(δ) = F.
Let us specify the values of the predicates represented by predicate symbols and primitive Unformulas on δ in GMS M: – α|–р∈Нα ⇒ рα(δ) = Т; – α–|р∈Нα ⇒ рα(δ) = F; – α|− Rxv,,⊥u ( p) ∈ Hα ⇒ pα (rvx,,u⊥ (δ)) = T; – α−| Rxv,,⊥u ( p) ∈ Hα ⇒ pα (rvx,,u⊥ (δ)) = F.
Next, we prove by induction on the formula structure.
From the theorems on constructing counter-models, we obtain the completeness theorems.
Theorem 13 (completeness of MСQ≡IR). Let Γ |=IR Δ; then the sequent |–Γ–|Δ is derivable in the calculus MСQ≡IR.
Let us assume the opposite: suppose Γ |=IR Δ, i.e. Γ M|=IR Δ holds for every consistent GMS M, but the sequent Σ = |–Γ–|Δ is not derivable. Then there exists an unclosed path in the tree for Σ. By Theorem 12, there exist GMS M = (S, R, А, Jт) and δ∈VA: α|–Φ∈Нα ⇒ Φα(δ) = Т and α–|Φ∈Нα ⇒ Φα(δ) = F. In particular, this holds for the formulas of the sequent |–Γ–|Δ. Therefore, Φα(δ) = Т for all Φα∈Γ and Ψβ(δ) = F for all Ψβ∈Δ. This contradicts Γ M|=IR Δ, hence Γ |≠IR Δ. We have reached a contradiction. Thus, the assumption that |–Γ–|Δ is not derivable is incorrect, which proves the theorem.
Theorem 14 (completeness of MСQ≡TF). Let Γ |=TF Δ; then the sequent |–Γ–|Δ is derivable in the calculus MСQ≡TF.
Let us assume the opposite: suppose Γ |=TF Δ, i.e. Γ M|=TF Δ holds for every consistent GMS M, but the sequent Σ = |–Γ–|Δ is not derivable. Then there exists an unclosed path in the tree for Σ. By Theorem 9, there exist MT = (St, R, А, IтT), MF = (St, R, A, IтF), and δ∈VA such that: α|–Φ∈Нα ⇒ ΦTα(δ) = Т; α–|Φ∈Нα ⇒ ΦTα(δ) ≠ T; α|–Φ∈Нα ⇒ ΦFα(δ) ≠ F; α–|Φ∈Нα ⇒ ΦFα(δ) = F.
For a T-counter-model, according to |–Γ–|Δ ⊆ Н, for all Φα∈Γ we have ΦTα(δ) = Т, and for all Ψβ∈Δ we have ΨTβ(δ) ≠ T. This contradicts Γ M|=T Δ, therefore, Γ |≠TF Δ.
For an F-counter-model, according to |–Γ–|Δ ⊆ Н, for all Φα∈Γ we have ΦTα(δ) ≠ F, and for all Ψβ∈Δ we have ΨTβ(δ) = F. This contradicts Γ M|=F Δ, therefore, Γ |≠TF Δ.
Thus, the assumption that |–Γ–|Δ is not derivable is incorrect, which proves the theorem.
The completeness theorem for the calculi MСQ≡T and MСQ≡F can be proved in the similar manner.
The work investigates program-oriented logical formalisms of the modal type – pure first-order modal logics of partial non-monotonic quasiary predicates. Variants of such logics with strong equality predicates and weak equality predicates are proposed. The semantic models and languages of these logics are described, with a focus on properties related to equality predicates, specifically the characteristics of the substitution of equals. A number of logical consequence relations for sets of formulas specified with states are defined, and their main properties are outlined. Based on this semantic foundation, the corresponding sequent type calculi for the studied logics are proposed. The varieties of these calculi for different logical consequence relations are described, along with the basic sequent forms and the conditions for the closedness of sequents. The construction of derivations (sequent trees) in the proposed calculi is explained, and the soundness and completeness theorems for the calculi are proved. [8] M. Nikitchenko, O. Shkilniak, and S. Shkilniak, Pure First-Order Logics of Quasiary Predicates,
No 2–3 of Problems in Programming, Kyiv, 2016, pp. 73–86 (in Ukrainian). [9] M. Fitting, R.L. Mendelsohn, First-Order Modal Logic, 2nd edition, Springer, 2023. [10] S. Shkilniak, First-Order Composition Nominative Logics with Predicates of Weak Equality and of Strong Equality, No 3 of Problems in Programming, Kyiv, 2019, pp. 28–44 (in Ukrainian). [11] O. Shkilniak, Transitional Modal Logics of Non-monotone Partial Predicates, Bulletin of Taras Shevchenko National University of Kyiv, Series: Physics & Mathematics. 3, 2015, pp. 141–147 (in Ukrainian). [12] O. Shkilniak, Transitional Modal Logics of Non-monotone Quasiary Predicates, Computer
Mathematics, Issue 2, 2014, pp. 99–110 (in Ukrainian). [13] O. Shkilniak, S. Shkilniak, First-Order Sequent Calculi of Logics of Quasiary Predicates with Extended Renominations and Equality, UkrPROG’2022, CEUR Workshop Proceedings (CEURWS.org), 2023, pp. 3–18. [14] Mykola Nikitchenko, Oksana Shkilniak, Stepan Shkilniak. Sequent Calculi of First-order Logics of Partial Predicates with Extended Renominations and Composition of Predicate Complement, UkrPROG’2020, CEUR Workshop Proceedings (CEUR-WS.org), 2020, pp.182–197. [15] S. C. Kleene, Mathematical Logic, Dower Publications, 2013.