UDC 004.42:510.69 SEQUENT CALCULI OF FIRST-ORDER LOGICS OF PARTIAL PREDICATES WITH EXTENDED RENOMINATIONS AND COMPOSITION OF PREDICATE COMPLEMENT Mykola Nikitchenko[0000-0002-4078-1062], Oksana Shkilniak[0000-0003-4139-2525], Stepan Shkilniak[0000-0001-8624-5778] Taras Shevchenko National University of Kyiv, 01601, Kyiv, Vladimirskaya, 60. Досліджено нові класи програмно-орієнтованих логік – чисті першопорядкові логіки часткових квазіарних предикатів з розширеними реномінаціями та композицією предикатного доповнення. Описано відношення логічного наслідку в таких логіках, для цих відношень побудовано числення секвенційного типу. Наведено базові секвенційні форми цих числень та умови замкненості секвенцій. Для пропонованих числень доведено теореми коректності, теореми про існування контрмоделей та теореми повноти. Ключові слова: логіка, частковий предикат, логічний наслідок, секвенційне числення, коректність, повнота. Исследованы новые классы программно-ориентированных логик – чистые первопорядковые логики частичных квазиарных предикатов с расширенными реноминациями и композицией предикатного дополнения. Описаны отношення логического следствия в таких логиках, для этих отношений построены исчисления секвенциального типа. Приведены базовые секвенциальные формы этих исчислений и условия замкнутости секвенций. Для предложенных исчислений доказаны теоремы корректности, теоремы о существовании контрмоделей и теоремы полноты. Ключевые слова: логика, частичный предикат, логическое следствие, секвенциальное исчисление, корректность, полнота. We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi. Key words: logic, partial predicate, logical consequence, sequent calculus, soundness, completeness. Introduction Many different logic systems have been created (see, for example, [1]), which are used with success in computer science and programming. Usually, the classical logic of predicates [2] and special logics based on it are employed for this purpose. However, classical logic has fundamental limitations, which complicates its use. This brings to the fore the problem of building new, software-oriented logics. Such are the logics of partial quasiary predicates, built on the basis of a compositional-nominative approach common to logic and programming [3]. A number of different classes of quasiary predicate logics are described, in particular, in [3–6]. To solve a number of problems that arise in information and software systems, it is necessary to develop efficient proof searching procedures. Such procedures are provided by Gentzen-style sequent calculi. These calculi formalize the fundamental concept of logical consequence. A number of sequent calculi for different classes of program-oriented logics have been developed (see, e.g., [4–6]). The purpose of this work is to construct sequent calculi for new classes of such logics — pure first-order logics of quasiary predicates with extended renominations and the composition of the predicate complement. A characteristic feature of these logics is the presence of a special non- monotonic operation (composition) of the predicate complement . Operations of this type have been used in extensions of Floyd-Hoare program logics [7, 8] in the case of partial pre- and post-conditions. The logics of partial predicates with the composition of the predicate complement are proposed in [9], they are called LC. Propositional LCs are described in detail in [9], renominative and pure first-order LCs are considered in [10] and [11], various relationships of logical consequence in LC are investigated in [12]. Pure first-order logics of quasiary predicates are called LQ (logics of quantifier level). Their defining feature is the presence of quantification compositions. LQ with extended renominations and predicate-indicators of the presence of value for variables is called LQ, LQ with the composition of the predicate complement is called LQС. A number of sequent calculi in LQ and in LQС are constructed in the paper, and the theorems of soundness and completeness are proved for such calculi. The main emphasis is on the construction of sequential numbers in LQС. Concepts that are not defined in this paper are interpreted in the sense of [6, 9, 12]. To facilitate reading, we provide the necessary definitions for further presentation. 1. Composition systems and languages of pure first-order logics Copyright © 2020 for this paper by its authors. Use permitted under Creative 183 Commons License Attribution 4.0 International (CC BY 4.0). Let VA be a set of all V-A-nominative sets and {T, F} is a set of Boolean values. We define V-A-quasiary predicate as a partial many-valued function Q : VA ® {T, F}. The set of values which many-valued predicate Q yields on argument (data) dVА is denoted Q[d]. Let V be a set of names (variables) and A be a set of values. V-A-nominative set is defined as a partial single- valued function d : V ® A. Nominative sets can be presented in the form [v1a1,...,vnan,...], where vіV, aіA, vі  vj when і  j. For nominative sets we define the parametric operation ||–Z of deleting components with names from Z  V as follows: d ||–Z = {v  ad | vZ}. vn , u1 ,..., um V V ,..., xn ,  ,...,  : А ® A, where vi, xi, uj V, is specified [5] as The parametric operation of extended renomination r vx11,..., ,..., xn ,  ,...,  ( d )  d ||{v1 ,..., vn ,u1 ,..., um }  [v1  d ( x1 ),..., vn  d ( xn )] . In particular, r ( d )  d || x . x r vx11,..., vn , u1 ,..., um We use a special symbol V that denotes the absence of the variable value; d(xі) means that a component with the name vі is absent. v ,u A simpler notation for sequences y1,..., yn will be used: y . Thus, instead of r vx11,..., vn , u1 ,..., um ,..., xn ,  ,...,  , we will write r x ,  . Traditional renomination r vx [2–4] is a special case of extended renomination r vx ,,u . Statement 1. Given d(z), we obtain r vx ,,u,,yz (d )  r vx ,,u,,y (d ) and r vx ,,u,,z (d )  r vx ,,u (d ) . Successive renominations r ux ,, as ,,w,,t та r vy ,,cs ,, z ,,t can be represented [5] by one renomination denoted r ux ,, as ,,w,,t vy,,sc,,z,,t ; we call it the convolution of r ux ,, as ,,w,,t and r vy ,,cs ,, z ,,t . For any dVA we get r ux ,, as ,,w,,t vy,,sc ,,z,,t (d )  r up ,, qs ,,vy,,w,,z,,t (d ) . In this paper we study many-valued predicates of relational type – R-predicates [3, 6], denoted as mappings from V A to the set of Boolean values {T, F}. Each R-predicate Q can be defined by its truth domain T(Q) = {d | TQ[d]} and falsity domain F(Q) = {d | FQ[d]}. We specify the undefinedness domain of R-predicate Q as  (Q)  T (Q)  F (Q) . We call R-predicate Q monotone if d1  d2  Q[d1]  Q[d2]. A name хV is unessential for R-predicate Q, if for any d1, d2 VA we have: d1 ||–х = d2 ||–х  Q[d1] = Q[d2]. Q is a partial single-valued R-predicate (P-predicate), if T(Q)F(Q) = ; Q is a total R-predicate (T-predicate), if T(Q)F(Q) = VA; Q is a total single-valued R-predicate (TS-predicate), if T(Q)F(Q) =  and T(Q)F(Q) = VA. We can define 4 constant R-predicates T, F, К,  as follows: T(F) = F(T) = T (К )  F (К )   ; T(T) = F(F) = T() = F() = VА. Q is a partial constant P-predicate, if F(Q) =  or T(Q) = . We will denote classes of V-A-quasiary R-predicates, P-predicates, T-predicates, and TS-predicates PrV–A, PrPV– A , PrT , and PrTS V–A respectively. The class PrTSV–A is degenerate: all TS-predicates, except constant T and F, are V–A non-monotonic. Basic compositions. Basic compositons of LQ are negation , disjunction , extended renomination R vx ,,u , existential quantifier x, and 0-ary variable assignment predicate Ez. Basic compositons of LQС additionally contain the composition of predicate complement . Logical connectives  are  defined by the truth and falsity domains of the respective predicates: T(P) = F(P); F(P) = T(P); T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q). V A V A v ,u We specify the composition of extended renomination R x ,  : Pr ® Pr as R vx ,,u ( P)[d ]  P [r vx ,,u (d )] . The predicate Ez indicates whether a component zV has a value in a given data: T(Ez) = {d | d(z)}; F(Ez) = {d | d(z)}. Predicates Ez are total, sinle-valued, and non-monotonic. We define the quantifier xP : Pr V  A ® Pr V  A as follows: T(xP) =  {d | d || x  x  a  T ( P )} ; F(xP) =  {d | d || x  x  a  F ( P )} . a A a A Specific non-monotonic 1-ary composition of predicate complement is specified as: T ( P)   ( P)  T ( P)  F ( P)  T ( P)  F ( P) ; F ( P )   . Thus, the sets of basic compositions for LQ and LQС are CQ = {, , R vx ,,u , x, Ex} and CQC = {, , R vx ,,u , x, , Ex} respectively. Statement 2. Compositions , , R vx ,,u , xP preserve totality and monotonicity of predicates. Therefore, classes PrPV–A, PrTV–A, PrTSV–A are closed under compositions CQ. At the same time, we have Statement 3. QPrV–A  Q  PrPV–A; QPrTV–A  Q К. 184 Classes PrTV–A and PrTSV–A are not closed under . Therefore, LC do not make sense for T-predicates and TS- predicates. Due to nonclosedness of PrTSV–A and PrTV–A under , duality [6] of classes PrPV–A and PrTV–A and degeneration of PrTSV–A, we will further consider only logics of R-predicates and P-predicates. We obtain composition systems (VA, PrV–A, CQ), (VA, PrPV–A, CQ), (VA, PrV–A, CQC), (VA, PrPV–A, CQC). They define pure first order composition algebras AQ = (VA, PrV–A, CQ), AQC = (VA, PrV–A, CQC), AQP = (VA, PrPV–A, CQ), AQCP = (VA, PrPV–A, CQC); here AQP and AQCP are subalgebras of algebras AQ and AQC. The main properties of propositional compositions and quantifiers, unrelated to renominations, correspond to those of classical logical connectives and quantifiers (see [3]). Theorem 1. The operation of extended renomination has the following basic properties: R) R(P) = P; RI) R zz ,,vx ,,u ( P)  R vx ,,u ( P) – identical renomination can be eliminated; RU) R zy,,vx,,u ( P)  R vx ,,u ( P) for unessential for predicate Р name zV; R) if d(z) then R vx ,,u,,yz (P)(d )  R vx ,,u,,y (P)(d ) and R vx ,,u,,z (P)(d )  R vx ,,u (P)(d ) ; RR) R vy,,z (R ux ,, t ( P))  R vy ,,z ux ,,t ( P) – convolution of renominations; here R vy ,,z ux ,,t ( P)(d )  P(rxu,,t vy,,z (d )) ; R) R vx ,,u (P)  R vx ,,u ( P) – R-distributivity; R) R vx ,,u ( P  Q)  R vx ,,u ( P)  R vx ,,u (Q) – R- distributivity; R  ) R vx ,,u ( Q)  R vx ,,u (Q) – R  - distributivity. Theorem 2. The properties related to renomination and quantification compositions are the following: Ren) if name z is unessential for P, then yP  zR zy ( P) – renaming of a quantifier name; Rs) yR vx ,,u ( P)  R vx ,,u (yP) if y  {v , x , u } – simple (limited) R- distributivity; R) R vx ,,u (yP)  zR vx ,,u  zy ( P), if name z is unessential for P and z  {v , x , u } – - distributivity; UR) yR zy,,xv ,,u ( P)  R zy,,xv ,,u ( P) if y  {z , x } – unessentiality of upper names in renominations. Statement 4. Properties of renomination of variable assignment predicates: R vx ,,u,,z ( Ez )  F; R vx ,,u,,zy ( Ez )  Ey ; R vx ,,u ( Ez )  Ez, if z  {v , u }. Quantifier elimination is based on the next properties: Theorem 3. T (R uv ,,w,, xy ( P))  T(Ey)  T (R uv ,,w (xP)) and F (R uv ,,w (xP))  T(Ey)  F (R uv ,,w,, xy ( P)) . Languages of LQC. An alphabet of the language of LQС consists of a set of names (variables) V, a set of predicate symbols Ps, and a set of basic compositions’ symbols Cs = {, , Rxv ,,u , , x, Ex}. We define inductively the set of formulas (denoted Fr): – each рPs and each Ex is a formula; formulas of such forms are called atomic; – if , Fr, then Fr, Fr, Rxv ,,u   Fr , xFr,   Fr . We specify a set VT  V of total unessential names (unessential for any рPs) and extend it [3, 6] to formulas:  : Fr2V. If х(), then (see [3, 6]) х is unessential for . Tuple  = (V, VT, Cs, Ps) is called the extended logic signature. We call a formula primitive, if it is atomic or has a form Rxv,,u p, where рPs, there are no identical renominations in Rxv, ,u and {v , u }  ( p)   .  is a СF-formula (constant free), if  does not contain symbols of 0- ary compositions (Ex in the case of the language of LQС). Formulas of the form Rxv , ,u  are called R-formulas. Interpretations. We interpretate the language of the LQC on composition systems CS = (VA, PrV–A, CQC). Symbols in Cs are interpretated as corresponding compositions, symbols Ex – as variable assignment predicates Ex. We specify a total single-valued mapping I : Ps ® PrV–A and extend it to formulas: I : Fr ® PrV–A: I() = (I()), I() = (I(), I()), I ( Rxv,,u )  R vx ,,u ( I ()), I(х) = х(I()), I ( )  ( I ()) . Let the tuple J = (CS, , I) be an interpretation of the language of LQ (further shorten to J = (A, I)). Given interpretation J and formula , we define value of  in J (denoted J) by induction on the structure of . Name xV is unessential for a formula, if it is unessential for J for any interpretation J. Classes of interpretations of the language are called semantics. For LQС we have a general class of R- interpretations – semantics RС. Specifying of subalgebras of P-predicates leads to a subclass of P-interpretations – semantics PС. Copyright © 2020 for this paper by its authors. Use permitted under Creative 185 Commons License Attribution 4.0 International (CC BY 4.0). For LQ we have a general class of R-interpretations – semantics R. For subalgebras of P-predicates, T- predicates, TS-predicates we obtain semantics P, T, TS. Only semantics P will be considered. Let us call constant formulas that are always interpreted as constant predicates. We can distinguish T-formulas, v ,u , z F- formulas, - formulas. For example, Ex  Ex is a T- formula, Rx ,  ,  ( Ez ) is a F- formula, Ez is a - formula. Let formulas that are always interpreted as total predicates (in particular, Ez, T- formulas and F- formulas) be denoted ; formulas with F(J) =  for any J (in particular, all formulas  ) be denoted F; formulas with T(J) =  for any J (in particular, all formulas   ) be denoted T. The language of LQ is defined similarly (omitting everything related to symbols ). Un-formulas. Let Rxx,,yv ,,tu,,w,,z () be R-formula such as {u , w}  () , and  is not a symbol Ez. Let us call Rs- form of an R-formula Rxx,,yv ,,tu,,w,,z () the R-formula obtained from Rxx,,yv ,,tu,,w,,z () by all possible simplifications of external renomination based on properties R, RI, RU. We will call Rs-formulas Rs-forms of R-formulas. Statement 5. If  is a Rs-form of an R-formula , then J = J for all interpretations J. Let Un  V be a set of indefinite names. Each Rs-formula can be presented in the form of Rsr ,,vz,,yx,,u ,,w  , where {r , s , y , u }  Un, {x , v , w}  Un   . Let us call Rvz,,x ,,w  an Un-form of the formula Rsr ,,vz,,yx,,u ,,w  . Primitive Un-formulas have a form of Rvz,,x p, where {x , v } Un   , pPs. Let us call formulas  and  Un-equivalent (denoted  Un ), if for any J = (A, І) and dVA ||–Un we have J (d) = J (d). Statement 6. If  is an Un-form of a formula , then  Un . Un-form Rvz,,x ,,w  can be obtained transforming an Rs-formula Rsr ,,vz,,yx,,u ,,w  according to R. Hence Statement 7. Given zUn, then Rxv,,u ,, zy  Un Rxv,,u ,,y  and Rxv ,,u ,,z  Un Rxv,,u  . 2. Logical consequence relation A number of various logical consequence relations can be defined on the sets of formulas of the languages of LQ and LQC. Among them are the relations defined in the languages of LQ [12, 6]: P|=IR, P|=T, P|=F, P|=TF, R|=TF. For the simplicity sake, we will omit symbol  in the names of relations. Firstly, let us specify a logical consequence relation for two sets of formulas in interpretation J. Let , ,   Fr and J be an interpretation. We denote:      T ( J ) as T (J),  F ( J ) as F (J),  T ( J ) as T (J),  F ( J ) as F (J).      is an IR-consequence of  in interpretation J (denoted  J|=IR ), if T(J)  F(J) = .  is a T-consequence of  in interpretation J (denoted  J|=T ), if T(J)  T(J).  is an F-consequence of  in interpretation J (denoted  J|=F ), if F(J)  F(J).  is TF-consequence of  in interpretation J (denoted  J|=TF ), if  J|=T  and  J|=F . The corresponding logical -consequence relations in semantics  are defined as follows:  |= , if  J|=  for arbitrary J. Here  denotes one of the semantics: R, P, RС, PС. There are 8 logical consequence relations in each of LQ and LQC: P |=IR, P|=T, P|=F, P|=TF; R|=IR, R|=T, R|=F, R|=TF ; Pс |=IR, Pс|=T, Pс|=F, Pс|=TF; Rс|=IR, Rс|=T, Rс|=F, Rс|=TF . Some of them are degenerate, some of the relations coincide (see [12]). For instance: Statement 8. If  and  consist of CF-formulas that do not contain , then  R|IR  and  Rс|IR . At the same time, Ez, Ez J|=IR  та  J|=IR Ez, Ez for each J. Therefore, Rс|=IR and R|=IR are degenerate. Example 1. For any Fr and JRС we have F (  J )  , T (  J )  , T(J)  T (  J ) = (J), F(J)  F (  J ) = (J). Hence  Rc|=F  and   Rс|=T ; however,  Rс|T  and   Rс|F . There are 5 distinct non-degenerate relations in LQ: P|=IR, P|=T, P|=F, P|=TF, R|=TF . In LQС, we obtain 7 distinct non-degenerate relations: Pс|=IR, Pс|=T, Pс|=F, Pс|=TF, Rс|=T, Rс|=F, Rс|=TF . The Hasse diagrams for those relations are shown below (we use an arrow  instead of symbol ): P Rc Pc |=T |=T  |=T R |=TF  P|=TF P |=IR Rc |=TF  Pc|=TF Pс |=IR P Rс Pс |=F |=F  |=F 186 At the same time, for the relation Pс|=IR it is impossible to make a decomposition  ([12]). Such a decomposition requires to specify explicitly an undefinedness domain, which leads to the more general irrefutability logical consequence relation under the conditions of undefinedness |=IR ([9]). For the latter relation, sequent calculi of propositional, renominative and first order levels are constructed [9–11]. In [12], there are introduced logical consequence relations under the conditions of undefinedness Pс|=T, Pс|=F, Rс |=T , |=F; the theorem of elimination of the conditions of undefinedness is proved which allows to express them by  Rс relations Pc|=T, Pc|=F, Rc|=T, Rc|=F. Logical consequence relations on pairs of formulas induce respective logical equivalence relations. We define a -equivalence relation in interpretation J as follows:  J , if  J|=  and  J|= . A logical -equivalence relation in semantics  is defined as follows:   , if  |=  and  |= . Note the importance of the relation J TF:  JTF   T(J) = T(J) and F(J) = F(J)  J = J . Equivalent transformations in LQ та LQС are based on the equivalence and substitution of equivalent theorems. Theorem 4. Let ' be obtained from formula  by substitution of 1, ..., n instead of 1, ..., n. If 1  1, ..., n  n, then   ' (here  denotes one of the following: RTF, PTF, PIR, RсTF, PсTF, PсIR).  Theorem 5. Let  TF , then we have: ,  |=   ,  |= ;  |= ,    |=, . Let TF denote one of the relations of the TF type, and |= denote an arbitrary logical consequence relation. Let us consider properties of logical consequence relations. M) If   ,    and  |= , then  |=  – monotonicity. Theorem 6. The following basic properties of formula decomposition hold: L) ,  |=   ,  |= ; R)  |= ,    |= , ; L) ,  |=   ,  |=  and ,  |= ; R)  |= ,    |= , , ; L) (),  |=   , ,  |= ; R)  |= , ()   |= ,  and  |= , . For the relations of the IR type, additionally hold (and do not hold for the relations of the types T, F, TF): L) ,  |=IR    |=IR , . R)  |=IR ,   ,  |=IR . Let с#|=T denote Pс|=T or Rc|=T; с#|=F denote Pc|=F, Rc|=T, Rc|=F; с#|=TF denote Pс|=TF or Rc|=TF. Theorem 7. The following properties of decomposition for  formulas hold: ,  с#|=T    с#|=T , , ; RT)  |=T ,   ,  |=T  and ,  |=T ; с# с# с# LT) с#  RF)  |=F ,    , ,  |=F ; с#  LF)  ,  |=F    |=T ,  and  |=T , . с# с# с# Theorem 8. The following properties of elimination for  formulas hold:  El)  с#|=T ,     с#|=T ; El) ,  с#|=F    с#|=F . Statement 9. The properties that guarantee the specified logical consequence relation: C )  c # | F ,  ; C ) ,   c # |T  . Composition has different properties on truth and falsity domains of predicates inducing different properties of decomposition for  formulas for the relations of the types T and F and making impossible to formulate a joint property for the relations of the TF type. Therefore, for relations с#|=TF decomposition for  is possible for с#|=T and с# |=F only separately. Thus, sequent calculi for relations с#|=TF aggregate calculi for relations с#|=T and с#|=F. We will concentrate on the relations P|=IR, P|=T, P|=F, P|=TF, R|=TF in LQ and Pс|=T, Pс|=F, Rс|=T, Rс|=F in LQС. Let us consider properties R, RI, RU, RR, R, R, R  for predicates. Each of the properties R induces 4 corresponding properties RL, RR, RL, RR for a logical consequence relation, depending on the position of a formula or its negation (either in the left or in the right side of the relation). R induces the following 8 properties: R1) Rxv,,u ,, zy (),  |= , Ez  Rxv,,u ,,y (),  |= , Ez;  |= , Rxv,,u ,, zy (), Ez   |= , Rxv ,,u ,,y (), Ez; R1) Rvx,,u,,yz (),  |= , Ez  R vx,,u,,y (),  |= , Ez;  |= , Rvx,,u,,yz (), Ez   |= , Rxv ,,u ,,z (), Ez; R2) Rxv,,u ,,z (),  |= , Ez  Rxv,,u (),  |= , Ez;  |= , Rxv,,u ,,z (), Ez   |= , Rxv,,u (), Ez; R2) Rxv ,,u ,,z (),  |= , Ez  Rxv ,,u (),  |= , Ez;  |= , Rxv,,u ,,z (), Ez   |= , Rxv,,u (), Ez; Properties of  elimination in Ez and in R vw,,u ( Ez ) and renomination properties of variable assignment predicates are the following: E) Ez,  |=    |= , Ez;  |= , Ez  Ez,  |= ; ¬ R  E ) Rwv ,,u ( Ez ),  |    | Rwv ,,u ( Ez ),  ;  | Rwv ,,u ( Ez ),   Rwv ,,u ( Ez ),  |  ; R  E ) Rxv ,,u ( Ez ),  |   Ez,  | , де z  {v , u };  | , Rxv ,,u ( Ez )   | , Ez, де z  {v , u } ; R  Ev ) Rxv,,u ,, zy ( Ez ),  |   Ey,  | ;  | , Rxv ,,u ,, zy ( Ez )   | , Ey . Let us specify properties of quantifier elimination, E-distribution and primary definition: Copyright © 2020 for this paper by its authors. Use permitted under Creative 187 Commons License Attribution 4.0 International (CC BY 4.0). L) х,  |=   Rzx (), Ez ,  |=  given zfu(, , х)); RL) Rwv ,,u (x),  |=   Rwv ,,u ,, xz (), Ez,  |=  given z  fu (, , Rwv ,,u (x)) ; R)  |= х,   , Ez |=  Rzx (),  given zfu(, , х)); RR)  |=  Rwv ,,u (x),   , Ez |=  Rwv ,,u ,, xz (),  given z  fu (, , Rwv ,,u (x)) ; vR) , Ey |= х,   , Ey |= х, Ryx (),  ; RvR) , Ey |= , Rwv ,,u (x)  , Ey |= ; vL) х, Ey,  |=   x, Ryx (), Ey,  |= ; RvL) Rwv ,,u (x), Ey,  |=   Rwv ,,u (x), Rwv ,,u ,, xy (), Ey,  |= ; Ed)  |=    |= , Ey and Ey,  |= ; Ev)  |=   Ez,  |= , де zfu(, ). Let us describe the properties that guarantee the specified logical consequence relation: С) ,  |= ,  – holds for all introduced logical consequence relations. The following properties additionally guarantee the specified logical consequence relation: СL) , ,  P|=T ; , ,  Pс|=T ; СR)  P|=F , , ;  Pс|=F , , ; СLR) , ,  P|=TF , , . Various properties which guarantee the specified logical consequence relation can be obtained from properties of constant and partial constant predicates: properties C , C and CF) Rxv ,,u ,,z ( Ez ),  |*  – holds for all introduced logical consequence relations. Finally, we can specify the conditions that guarantee a certain logical consequence relation: С) there exists formula  such that:  and  –  |=*  for every introduced relation; СL) there exists formula  such that:  and  – guarantees  P|=T  and  Pс|=T ; СR) there exists formula  such that:  and  – guarantees  P|=F  and  Pс|=F ; СLR) there exist formulas ,  such that: ,  and ,  – guarantees  P|=TF ; СF) there exists formula Rxv ,,u ,,z ( Ez )   – guarantees  |=*  for every introduced relation; C )    – guarantees  Pс|=F  and  Rс|=F ; C )     – guarantees  Pс|=T  and  Rс|=T . 3. First order sequent calculi Sequent calculi formalize logical consequence relations between sets of formulas. We construct calculi in the style of semantic tableau, so, we will treat sequents as finite sets of formulas signed (marked, indexed) by symbols |– and –| . Sequents are denoted |– –|, in abbreviated form . Formulas from  (they are signed by |–) are called T- formulas, formulas from  (they are signed by –|) are called F-formulas. Sequent calculus is constructed in such a way that a sequent |––| is derivable   |= . For a set of signed formulas  = |––|, let us introduce sets of defined and undefined names (val-variables and unv-variables): val(|––|) = {xV | Ex}; unv(|––|) = {xV | Ex}. Also we specify a set of undistributed names for : ud() = nm() \ (val()  unv()). The derivation in sequent calculi has the form of a tree, the vertices of which are sequents; such trees are called sequent trees. A sequent  is derivable if there is a closed sequent tree with the root . A sequent tree is closed if every its leaf is a closed sequent. Sequent calculus is defined by basic sequent forms and closure conditions for sequents. Closed sequents are axioms of the sequent calculus. A closedness |––| must guarantee  |= . Rules of sequent calculus are called sequent forms. They are syntactical analogues of the semantic properties of    the corresponding logical consequence relations and have a form of or .   For the relations P|=IR, P|=T, P|=F, P|=TF, R|=TF in LQ we have calculi СQIR, СQT, СQF, СQTF, СQTFR. For the relations Pс|=T, Pс|=F, Rс|=T, Rс|=F in LQС we obtain calculi СQСT, СQСF, СQCTR, СQСFR. Closure conditions for sequents. Closure conditions for a sequent |––| correspond to conditions that guarantee a certain logical consequence relation: – calculus СQIR: condition C  CF (guarantees  P|=IR ); – calculus СQT: condition C  CF  CL (guarantees  P|=T ); – calculus СQF: condition C  CF  CR (guarantees  P|=F ); – calculus СQTF: condition C  CF  CLR (guarantees  P|=TF ); – calculus СQTFR: condition C  CF (guarantees  R|=TF ); 188 – calculus СQCT: condition C  CF  CL  C (guarantees  Pc|=T ); – calculus СQCF: condition C  CF  CR  C (guarantees  Pc|=F ); – calculus СQCTR: condition C  CF  C (guarantees  Rc|=T ); – calculus СQCFR: condition C  CF  C (guarantees  Rc|=F ). The conditions C, CF, CL, CR, CLR, C , C were specified earlier. Basic sequent forms for the calculi СQT, СQF, СQTF, СQTFR. Properties of logical consequence relations induce the corresponding sequent forms. Let us specify basic forms for the calculi СQT, СQF, СQTF, СQTFR. Their basic forms are the same, the difference is in closure conditions for sequents. Simplification forms (condition for the forms of type RU: у()): | ,  |  ,  |  ,  | ,  |–R ; –|R ; |–R ; –|R ; | R ( ),  | R ( ),  | R ( ),  | R ( ),  | Rxv,,u (),  | Rxv,,u (),  | Rxv ,,u (),  | Rxv ,,u (),  |–RI ; –|RI ; |–RI –|RI ; | Rzz,,xv,,u (),  | Rzz,,xv,,u (),  | Rzz,,xv ,,u (),  | Rzz,,xv ,,u (),  | Rxv,,u (),  | Rxv,,u (),  | Rxv,,u (),  | Rxv,,u (),  |–RU ; –|RU ; |–RU ; –|RU ; | Rzy,,xv,,u (),  | Rzy,,xv,,u (),  | Rzy,,xv,,u ( ),  | Rzy,,xv,,u ( ),  | Rxv,,u ,,y ( p), | Ez ,  | Rxv,,u ,,y ( p), | Ez ,  |–R1 , where pPs; –|R1 , where pPs; | Rxv,,u ,, zy ( p), | Ez ,  | Rxv,,u ,, zy ( p), | Ez ,  | Rxv,,u ,,y ( p),| Ez,  | Rxv,,u ,,y ( p), | Ez,  |–R1 , where pPs; –|R1 , where pPs; | Rxv ,,u ,, zy ( p),| Ez,  | Rxv ,,u ,, zy ( p), | Ez,  | Rxv ,,u ( p), | Ez,  | Rxv ,,u ( p), | Ez,  |–R2 , where pPs; –|R2 , where pPs; | Rxv,,u ,,z ( p), | Ez ,  | Rxv,,u ,,z ( p), | Ez ,  | Rxv ,,u ( p), | Ez,  | Rxv ,,u ( p), | Ez,  |–R2 , where pPs; –|R2 , where pP. | Rxv,,u ,,z ( p), | Ez,  | Rxv,,u ,,z ( p), | Ez,  Forms of equivalent transformations: | Ry ,   x ,  ( ),  Ryv ,,z ux ,,t (),  v ,z u ,t | |–RR ; –|RR ; | Ry ,  (Rx ,  ( )),  Rxv ( Ryw ()),  v ,z u ,t | | Ryv ,,z ux ,,t ( ),  | Ryv ,,z ux ,,t ( ),  |–RR ; –|RR ; | Ryv ,,z (Rxu,,t ( )),  | Ryv ,,z (Rxu,,t ( )),  | Rxv ,,u (),  | Rxv ,,u (),  |–R ; –|R ; | Rxv ,,u (),  | Rxv ,,u (),  | Rxv ,,u (),  | Rxv ,,u (),  |–R ; –|R ; | Rxv,,u (),  | Rxv,,u (),  | Rxv,,u ()  Rxv,,u ( ),  | Rxv,,u ()  Rxv,,u ( ),  |–R ; –|R ; | Rxv,,u (   ),  | Rxv,,u (   ),  | ( Rxv,,u ()  Rxv ,,u ( )),  | ( Rxv,,u ()  Rxv ,,u ( )),  |–R ; –|R . | Rxv,,u (   ),  | Rxv,,u (   ),  Forms of  elimination in formulas Ey and Rxv,,u ( Ez ) : | Ez,  | Ez,  | Rxv ,,u ( Ez ),  | Rxv ,,u ( Ez ),  |–E ; –|E ; |–RE ; –|RE . | Ez,  | Ez,  | Rxv,,u ( Ez ),  | Rxv,,u ( Ez ),  Renomination simplification for variable assignment predicates (condition for |–RE та –|RE: z  {v , u } ): | Ez,  | Ez,  | Ey,  | Ey,  |–RE ; –|RE ; |–REv ; –|REv . | R v ,u x , ( Ez ),  | R v ,u x , ( Ez ),  | R v ,u , z x ,, y ( Ez ),  | R v ,u , z x ,, y ( Ez ),  Decomposition forms: |  ,  | ,  | ; |  ; | ,  | ,  Copyright © 2020 for this paper by its authors. Use permitted under Creative 189 Commons License Attribution 4.0 International (CC BY 4.0). | ,  | ,  | ,  |  ,  | ; | ; |   ,  |   ,  | , | ,  | ,  | ,  | ; | ; | (   ),  | (   ),  Forms of quantifier elimination: |  Rz ( ), | Ez ,  Rzx (), | Ez,  x | | ; | ; |  x,  | x,  | Rwv ,,u,, xz (), | Ez,  | Rwv ,,u,, xz ( ), | Ez ,  |–R ; –|R ; | Rwv ,,u (x),  | Rwv ,,u (x ),  | x, | Ey, | Ryx (),  | x, | Ey, | Ryx (),  |v ; |v ; | x, | Ey,  | x, | Ey,  | Rwv ,,u (x), | Rwv ,,u ,, xy (), | Ey,  | Rwv ,,u (x), | Rwv ,,u ,, xy (), | Ey,  |–Rv ; –|Rv . | Rwv ,,u (x), | Ey,  | Rwv ,,u (x), | Ey,  Let us call forms |–R, –|R, |–, –| – T-forms; forms –|v, |–v, –|Rv, |–Rv – F-forms. Conditions for |–, –|: zfu(, x); conditions for |–R, –|R: z  fu (, Rw, (x)) ; condition for F-form: Ey does not belong v ,u to . Auxiliary forms of E-distribution Ed and primary definition of Ev: |  Ex,  | Ex,  |  Ez ,  Ed ; Ev given zfu().   Basic sequent forms for the calculus СQIR. Forms |–R, –|R, |–RI, –|RI, |–RU, –|RU, |–R1, –|R1, |–R2, –|R2, |–RR, –|RR, |–R, –|R, |–R,–|R, |–RE, –|RE, |–REv, –|REv, |, |, |, |–R, |v, –|Rv, Ed, Ev with addition of: | ,  |  ,  | ; |  . | ,  | ,  Basic sequent forms for the calculi СQCT and СQCTR. Their basic forms are the same, the difference is in closure conditions for sequents. To the specified above sequent forms we add forms of the type R  and forms of decomposition of | T and | T : | R v ,u x , (),  | Rxv ,,u (),  |–R ; –|R ; | R v ,u x , ( ),  | Rxv ,,u ( ),  |  Rxv ,,u (),  |  Rxv ,,u (),  |–R ; –|R ; | Rxv ,,u (  ),  | Rxv ,,u (  ),  | , | ,  | ,  | ,  ; . | T | ,  | T | ,  Basic sequent forms for the calculi СQCF and СQCFR. Their basic forms are the same, the difference is in closure conditions for sequents. We take the sequent forms for calculi СQCT and СQCTR replacing forms | T and | T by |  F and |  F : | ,  | ,  | , | ,  |  ; |  . F |  ,  F |  ,  Forms of types R, RІ, RU, R are auxiliary, they are used every time the specified situation arises. Forms Ed and Ev are also specific; all the other basic sequents are main forms. The main property of sequent forms. Let |= be one of the introduced logical consequence relations.  | Theorem 9. 1. Let | be a basic sequent form. Then: a)  |=    |= ; b)  |    | . |   |   | |   |  2. Let | be a basic sequent form. Then: a)  |=  and  |=    |= ; b)  |  or  |    | . |   |  Procedure of construction of a sequent tree. The main action during the process of derivation (construction of a sequent tree) is decomposition or simplification of a formula choosen from the sequent. We treat sequents as sets of 190 signed formulas, so we will not add there another copy of a formula that may happen to be obtained at some stage of derivation. Let us describe all stages of the procedure for a given finite sequent . We start from the root. On the initial stage primary distribution of names is performed: we obtain all the possible distributions of names from ud() to defined and undefined by applying Ed-form. This leads to a tree of a height h = |ud()| with root  and m = 2h descendants. If val() = , we use Ev-form to perform primary definition for a descendant sequent 0 with val(0) = : 0 is enriched with formula |–Ez such that zfu(), so sequent 0, |–Ez is obtained. As a result, the set of defined names is not empty for all descendants of  which guarantees applicability of F-forms. Let us describe derivation of an unclosed sequent leaf ; this implies building a finite subtree with node . We activate all non-primitive formulas in the sequent . A corresponding main form is applied to each active formula. During the process, every time the situation arise, appropriate auxiliary forms R, RI, RU, R are used for simplifications. Forms R are applied to primitive formulas and their negations. After that, all primitive formulas in the sequent and their negations become Un-formulas, where Un is a set of all unv-variables of formulas in sequents in the path from root to the current sequent. Resulting formula(s) become(s) passive after application of a main form and implicated simplifications: at this stage main forms can not be used on them. Let us take a look at main forms’ application. At first, we use all the forms except F-forms. With each application of T, a new (absent in the path from root to the current sequent) zVT is taken. F-forms are applied after T- forms. F-form should be used repeatedly for each defined у of formulas in the path from  to the current sequent. When no active formulas are left on the current stage, we need to check every sequent leaf  on closedness. If all the leaves are closed sequents, we obtained a finite closed tree: the procedure ended positively. If a sequent leaf  is unclosed, it has to be checked whether  is a final sequent. Unclosed sequent node  is called final, if there is no applicable form to it or no new (differing from formulas on the path from  to ) formula can be obtained using applicable forms. It signals that the sequent tree has an unclosed path (from root to the current final sequent, all its nodes are unclosed sequents): the derivation process ended negatively. Thus, during construction of a sequent tree the following cases are possible: 1) construction procedure is completed positively; we obtained a finite closed tree; 2) construction procedure is completed negatively; we obtained a finite unclosed tree. Such tree has at least one unclosed path, all nodes of which are unclosed sequents. 3) construction procedure is not completed; we obtained an infinite unclosed tree. König's lemma [2] states that such tree has at least one infinite path. All its nodes should be unclosed sequents, otherwise this path would finish. Hence, there is an infinite unclosed path in the tree. Let us see the differences in the construction of a sequent tree for a given countable sequent . The process also has its stages and starts from the root . There is a finite set of available on the current stage formulas (see [4, 6]); forms can be applied only to these formulas. In the beginning a pair of first formulas from the lists of T-formulas and F-formulas of the sequent  is available (and one of the lists can be empty). Every stage starts with an access step for all unclosed sequents: another pair from the lists of T-formulas and F- formulas of a sequent is added to the set of available formulas. Let  be a sequent obtained in the beginning of a stage after adding a pair of new available formulas. Stage distribution of names is performed next: we obtain all the possible distributions of names from ud() to defined and undefined by applying Ed-form. This leads to a subtree of a height |ud()| with root  and k = 2|ud()| descendants. If val() = , we use Ev-form to perform primary definition for a descendant sequent 0 with val(0) =  and obtain a sequent 0, |–Ez. Forms’ application is not different from the finite sequent case. When no active formulas are left on the current stage, every sequent leaf  is checked on closedness. If all the leaves are closed sequents, we obtained a finite closed tree: the procedure ended positively. Otherwise begin the next stage. For a sequent tree for a countable sequent the notion of a final node does not make sense, thus only two outcomes are possible: 1) procedure is completed positively; we obtained a finite closed tree; 2) procedure is not completed; we obtained an infinite unclosed tree with an infinite unclosed path: every formula of the sequent  will appear in this path and become available. The soundness theorem. It has the same formulation for all introduced calculi. Let the logical consequence relations P|=IR, P|=T, P|=F, P|=TF, R|=TF, Pс|=T, Pс|=F, Rс|=T, Rс|=F correspond to the calculi СQIR, СQT, СQF, СQTF, СQTFR, СQСT, СQСF, СQCTR, СQСFR respectively. We obtain Theorem 10 (soundness). Let sequent |––| is derivable in CQ#. Then  |= . If |––| is derivable in a calculus CQ#, then a finite closed tree was constructed for |––|. For any node of this tree |––| we have  |= . For leaves it is implied from the notion of a closed sequent. By Theorem 9, sequent forms preserve logical consequence relation. Hence, for the root |––| we also have that  |=  holds. Copyright © 2020 for this paper by its authors. Use permitted under Creative 191 Commons License Attribution 4.0 International (CC BY 4.0). 4. The counter-model existence theorems. The completeness theorem The completeness of sequent calculi is traditionally proved on the basis of theorems of the existence of a counter-model for the set of formulas of an unclosed path in the sequent tree. In this case a method of Hintikka (model) sets is used ([4]). Let us apply this method for the calculi CQCTR and CQCFR. Theorem 11. Let  be an unclosed path in the derivation tree constructed in CQCTR for a sequent |––|; let Н be the set of all specified formulas of this path. Then there exist an interpretation A = (S, I) and data VS such that: НT) |–Н  T(A) and –|Н  T(A). Theorem 12. Let  be an unclosed path in the derivation tree constructed in CQCFR for a sequent |––|; let Н be the set of all specified formulas of this path. Then there exist an interpretation B = (S, I) and data VA such that: НF) |–Н  F(B) and –|Н  F(B). Let (A, ) be called T-counter-model and let (B, ) be called F-counter-model for a sequent |––|. Let us define a set Un = {ynm(Н) | –|EyН} and call it a set of undefined names of the set Н. Let us specify W = nm(Н) \ Un. The primary definition gives the condition W = {ynm(Н) | |–EyН}. Theorems 11 and 12 are proved in the same style. We continuously apply forms to sequents of the path  while we can: in the end, every non-primitive formula of the path (or its negation) will be decomposed or simplified. All the sequents of the path  are unclosed, therefore the closure condition does not hold: C  CF  C for СQCTR and C  CF  C for СQCFR. Thus, for the set Н the following correctness conditions hold: НС) there is no formula  such that |–Н and –|Н; НCF) there is no formula Rxv,,u ,,z ( Ez ) such that | Rxv ,,u ,,z ( Ez )  H ; HC ) there is no formula  such that |    H – for the set Н from theorem 11; HC ) there is no formula  such that |   H – for the set Н from theorem 12. We can move from lower to higher node of the path  after applying a certain sequent form, therefore the corresponding conditions for transition for Н should hold. In particular: НR1) –|EzН and | Rxv ,,u ,, zy ( p)  H  | Rxv ,,u ,,y ( p)  H ; –|EzН and | Rxv ,,u ,, zy ( p)  H  | Rxv ,,u ,,y ( p)  H ; НR1) –|EzН and | Rxv ,,u ,, zy ( p)  H  | Rxv ,,u ,,y ( p)  H ; –|EzН and | Rx ,  , z ( p )  H  | Rxv ,,u ,,y ( p)  H ; v ,u , y НR2) –|EzН and | Rxv,,u ,,z ( p)  H  | Rxv,,u ( p)  H ; –|EzН and | Rxv,,u ,,z ( p)  H  | Rxv,,u ( p)  H ; НR2) –|EzН and | Rxv ,,u ,,z ( p)  H  | Rxv ,,u ( p)  H ; –|EzН and | Rxv ,,u ,,z ( p)  H  | Rxv ,,u ( p)  H ; НE ) |–EzН  –|EzН; –|EzН  |–EzН; НRE ) | Rxv ,,u ( Ez )  H  | Rxv ,,u ( Ez )  H ; | Rxv ,,u ( Ez )  H  | Rxv ,,u ( Ez )  H ; НRE ) given z  {v , u } we have: | Rxv,,u ( Ez )  H  | Ez  H ; | Rxv,,u ( Ez )  H  | Ez  H ; НREv ) | Rxv ,,u ,, zy ( Ez )  H  | Ey  H ; | Rxv ,,u ,, zy ( Ez )  H  | Ey  H ; Let us call the set of signed formulas Н for which the conditions of correctness НС, НCF, HC , the specified above conditions of transition and the condition Н T apply, an RTС-model set. Let us call the set of signed formulas Н for which the conditions of correctness НС, НCF, HC , the specified above conditions of transition and the condition Н F apply, an RFС-model set. Conditions Н T and Н F are defined as follows: Н T) |   H  –|Н and –|Н; |   H  |–Н or |–Н; Н F) |    H  –|Н or –|Н; |    H  |–Н and |–Н. Let us obtain a counter-model using the RTС-model set Н. Let S be a set such that |S| = |W|. We need to take an injective VS with its domain W; such  is a bijection W ® S. |–Ex  Н gives xW, then ExА () = T, therefore T(ExА); –|Ex  Н gives xW, then (x), therefore T(ExА). Let us specify basic values of predicates: we define values of atomic formulas, primitive Un-formulas and their negations on  in interpretation A as follows: – |– рН  T(рA); –| рН  T(рA); |–рН T(pA); –|pН  T(pA); – | Rxv,,u ( p)  H    T ( Rxv,,u ( p) A ); | Rxv,,u ( p)  H    T ( Rxv,,u ( p) A ); – | Rxv,,u ( p)  H    T (Rxv,,u ( p) A ); | Rxv ,,u ( p)  H    T (Rxv ,,u ( p) A ). 192 In the same way we can obtain a counter-model using the RFС-model set Н. S and  are defined similarly. |–Ex  Н gives xW, then ExА () = T, therefore F(Ex B); –|Ex  Н gives xW, then (x), therefore F(Ex B). We specify basic values of predicates, defining values of atomic formulas, primitive Un-formulas and their negations on  in interpretation B as follows: – |– рН  F(рB); –| рН  F(рB); |–рН  F(pB); –|pН  F(pB); – | Rxv ,,u ( p)  H    F ( Rxv ,,u ( p) B ); | Rxv ,,u ( p)  H    F ( Rxv ,,u ( p) B ); – | Rxv ,,u ( p)  H    F (Rxv ,,u ( p) B ); | Rxv,,u ( p)  H    F (Rxv ,,u ( p) B ). For atomic formulas, primitive Un-formulas and their negations, statements of theorem 11 and theorem 12 hold basing on the definitions above. We will prove the condition НR1 for both interpretations A and B. Let –|EzН and | R vx,,u,,yz ( p)  H . Condition –|EzН gives zW, then (z), therefore r vx ,,u,,y ()  r vx ,,u,,yz (). By НR1 we have | Rvx,,u,,y ( p)  H . Whence   T ( Rvx,,u,,y ( p) A ) ,   T ( Rvx,,u,,yz ( p) A ) and   F ( Rvx,,u,,y ( p) B ),   F ( Rvx,,u,,yz ( p) B ) . Let –|EzН and | R vx,,u,,yz ( p)  H . Condition –|EzН gives zW, then (z), therefore r vx ,,u,,y ()  r vx ,,u,,yz (). By НR1 we have | Rvx,,u,,y ( p)  H . Whence   T ( Rvx,,u,,y ( p) A ) ,   T ( Rvx,,u,,yz ( p) A ) and   F ( Rvx,,u,,y ( p) B ),   F ( Rvx,,u,,yz ( p) B ) . The proof will be similar for the conditions НR1, НR2, НR2 and НE, НRE . The rest can be proved by the usual way by induction on the formula structure. We will illustrate it for Н T (theorem 11) and Н F (theorem 12). Let |   H . By Н T we have –|Н and –|Н. By induction hypothesis we have T(A) and T(A) = F(A), whence (A). However (A) = T (  A ) , therefore  T (  A ) . Let |   H . Be Н T we have |–Н or |–Н. By induction hypothesis we have T(A) or T(A) = F(A), whence (A). However (A) = T (  A ) , therefore  T (  A ) . Let |    H . By Н F we have –|Н or –|Н. By induction hypothesis we have F(B) or F(B) = T(B), whence (B). However (B) = T (  B )  F (  B ), therefore  F (  B ) . Let |    H . By Н F we have |–Н and |–Н. By induction hypothesis we have F(B) and F(B) = T(B), whence (B). However (B) = T (  B )  F (  B ) , therefore  F (  B ) . The counter-model existence theorems for the calculi CQСT and CQСF can be formulated and proved similarly. As calculi CQСT and CQСF formalize relations Pс|=T and Pс|=F, all the predicates A and B need to be single-valued. Additional correctness conditions should be specified for the set Н: НСL) there is no formula  such that |–, |–Н (case of derivation in CQСT); НСR) there is no formula  such that –|, –|Н (case of derivation in CQСF). The counter-model existence theorems for the calculi CQT and CQF can be formulated and proved similarly to theorems 11 and 12: conditions HR  , HR  , Н T, Н F and HC , HC , should be omitted, conditions НСL and НСR added instead. Let us specify the counter-model existence theorems for the calculi CQTFR, CQTF and CQIR. Theorem 13. Let  be an unclosed path in the derivation tree constructed in CQTFR for a sequent |––|; let Н be the set of all specified formulas of this path. Then there exist interpretations A = (S, IA), B = (S, IB) and data VS such that conditions НT and НF hold. We will call such (A, ) and (B, ) T-counter-model and F-counter-model for |––|. Theorem 14. Let  be an unclosed path in the derivation tree constructed in CQTF for a sequent |––|; let Н be the set of all specified formulas of this path. Then there exist interpretations A = (S, IA), B = (S, IB) and data VS such that conditions НT and НF hold. We will call such (A, ) and (B, ) TP-counter-model and FP-counter-model for |––|. In the proofs of theorems 13 and 14 the conditions HR  , HR  , Н T, Н F and HC , HC , are omitted; the following correctness condition НСLR is added for theorem 14: НСLR) there are no formulas  and  such that |–, |–Н and –|, –|Н. Obviously, НСLR  НСL  НСR. One should make clear the choice of a counter-model in this situation. For TP- counter-model , violation of the condition НСL (there is a formula  such that |–Н and |–Н) gives A() = T and A() = T, therefore A() = F, and ambiguity for A . For FP-counter-model  violation of the condition НСR, Copyright © 2020 for this paper by its authors. Use permitted under Creative 193 Commons License Attribution 4.0 International (CC BY 4.0). (there is a formulda  such that –|Н and –|Н) gives B() = F and B() = F, therefore B()= T, and ambiguity for B . Thus, should we have the condition НСLR, in the case of violation of НСL we choose the FP-counter-model, and in the case of violation of НСR we choose the TP-counter-model; we can choose any of the two counter-models if both conditions НСL and НСR hold. Theorem 15. Let  be an unclosed path in the derivation tree constructed in CQIR for a sequent |––|; let Н be the set of all specified formulas of this path. Then there exist interpretation A = (S, I) and data VS such that: НС) |–Н  A() = T and –|Н  A() = F. We will call such (A, ) IR-counter-model for |––|. Theorems of the existence of a counter-model for the considered sequent calculi allow us to prove the completeness theorem. It has the same formulation for all these calculi. Let the logical consequence relations P|=IR, P|=T, P |=F, P|=TF, R|=TF, Pс|=T, Pс|=F, Rс|=T, Rс|=F correspond to the calculi СQIR, СQT, СQF, СQTF, СQTFR, СQСT, СQСF, СQCTR, СQСFR respectively. We obtain Theorem 16 (completeness). Let  |= . Then sequent |––| is derivable in CQ#. Let us prove for relation Rc|=T and calculus CQCTR (for more similar proofs see [4, 11]). Assume that  Rс|=T , but sequent |––| is not derivable. In this case a sequent tree for |––| is not closed. Thus, an unclosed path  exists in this tree. Let H be the set of all signed formulas of this path. By Theorem 11, there is a T- counter-model (A, ): |–Н  T(A) and –|Н  T(A). By |––|  Н for all  we have T(A), for all Ψ we have T(ΨA). Whence T(A) and T(A), therefore T(A)  T(A) does not hold. This contradicts to  A|=T , so it contradicts to  Rс|=T . Conclusion We have studied new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. Such operations are used in various versions of the Floyd-Hoare program logic with partial pre- and post-conditions. We have considered composition systems and languages of these logics, specified various logical consequence relations and described properties of formulas decomposition and quantifier elimination. Properties of logical consequence relations form a semantic base for construction of corresponding calculi of sequent type. We have defined basic sequent forms for the specified calculi and closeness conditions, and illustrated the process of derivation (building a sequent tree). The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi. References 1. ABRAMSKY, S., GABBAY, D. and MAIBAUM, T. (editors). (1993–2000). Handbook of Logic in Computer Science. Oxford University Press. 2. KLEENE, S. (1967) Mathematical Logic. New York. 3. NIKITCHENKO, M. and SHKILNIAK, S. (2013). Applied logic. Кyiv: VPC Кyivskyi Universytet (in ukr). 4. SHKILNIAK, S. (2013). Spectrum of sequent calculi of first-order composition-nominative logics. Problems in Progamming. No 3. P. 22–37 (in ukr). 5. NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2014). First-order composition-nominative logics with generalized renominations. Problems in Progamming. № 2–3. P. 17–28 (in ukr). 6. NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2016). Pure first-order logics of quasiary predicates. Problems in Progamming. No 2–3. P. 73–86 (in ukr). 7. HOARE, C. (1969). An axiomatic basis for computer programming, Comm. ACM 12(10). P. 576–580. 8. APT, K. (1981). Ten years of Hoare’s logic: a survey – part I, ACM Trans. Program. Lang. Syst. 3(4). P. 431–483 9. NIKITCHENKO, M., SHKILNIAK, O., SHKILNIAK, S. and MAMEDOV, T. (2019). Propositional logics of partial predicates with composition of predicate complement. Problems in Progamming. No 1. P. 3–13 (in ukr). 10. NIKITCHENKO, M., SHKILNIAK, O. and SHKILNIAK, S. (2019). Program Logics of Renominative Level with the Composition of Predicate Complement. Proceedings of the 15th International Conference on ICT. CEUR Workshop, Kherson, Ukraine. Vol. 2393. P. 603–616. 11. NIKITCHENKO, M., SHKILNIAK, O., SHKILNIAK, S. and MAMEDOV, T. (2019). Completeness of the First-Order Logic of Partial Quasiary Predicates with the Complement Composition. Computer Science Journal of Moldova, vol. 27, No 2 (80). P.162–187. 12. SHKILNIAK, O. (2019). Relations of logical consequence of logics of partial predicates with composition of predicate complement. Problems in Progamming. No 3. P. 11–27 (in ukr). Про авторів: Нікітченко Микола Степанович, доктор фізико-математичних наук, професор, завідувач кафедри теорії та технології програмування. Кількість наукових публікацій в українських виданнях – понад 220, в т.ч. кількість наукових публікацій у фахових виданнях – понад 120. Кількість наукових публікацій в зарубіжних виданнях – понад 50. Scopus Author ID: 6602842336; h-індекс (Google Scholar): 15 (13 з 2015). http://orcid.org/0000-0002-4078-1062, 194 Шкільняк Оксана Степанівна, кандидат фізико-математичних наук, доцент, доцент кафедри інтелектуальних програмних систем. Кількість наукових публікацій в українських виданнях – понад 80, в т.ч. кількість наукових публікацій у фахових виданнях – понад 40. Кількість наукових публікацій в зарубіжних виданнях – 17. Scopus Author ID: 57190873266; h-індекс (Google Scholar): 5 (3 з 2015). http://orcid.org/0000-0003-4139-2525, Шкільняк Степан Степанович, доктор фізико-математичних наук, професор, професор кафедри теорії та технології програмування. Кількість наукових публікацій в українських виданнях – понад 200, в т.ч. кількість наукових публікацій у фахових виданнях –понад 110. Кількість наукових публікацій в зарубіжних виданнях – 35. Scopus Author ID: 36646762300; h-індекс (Google Scholar): 8 (6 з 2015). http://orcid.org/0000-0001-8624-5778. Місце роботи авторів: Київський національний університет імені Тараса Шевченка, 01601, Київ, вул. Володимирська, 60. Тел.: (044) 5213345. E-mail: me.oksana@gmail.com, nikitchenko@unicyb.kiev.ua, sssh@unicyb.kiev.ua. Copyright © 2020 for this paper by its authors. Use permitted under Creative 195 Commons License Attribution 4.0 International (CC BY 4.0).