=Paper=
{{Paper
|id=Vol-2866/ceur_182-197_nikitchenko18
|storemode=property
|title=Sequent Calculi of First-order Logics of Partial Predicates with Extended Renominations and Composition of Predicate Complement
|pdfUrl=https://ceur-ws.org/Vol-2866/ceur_182-197_nikitchenko18.pdf
|volume=Vol-2866
|authors=Mykola Nikitchenko,Oksana Shkilniak,Stepan Shkilniak
|dblpUrl=https://dblp.org/rec/conf/ukrprog/NikitchenkoSS20
}}
==Sequent Calculi of First-order Logics of Partial Predicates with Extended Renominations and Composition of Predicate Complement==
https://ceur-ws.org/Vol-2866/ceur_182-197_nikitchenko18.pdf
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 LQ, LQ with the composition of the predicate complement is called LQС. A number of
sequent calculi in LQ and in LQС 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 LQС.
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) dVА 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 [v1a1,...,vnan,...], 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 ad | vZ}.
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 dVA 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 | TQ[d]} and
falsity domain F(Q) = {d | FQ[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 LQ are negation , disjunction , extended renomination R vx ,,u ,
existential quantifier x, and 0-ary variable assignment predicate Ez. Basic compositons of LQС 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(PQ) = T(P)T(Q); F(PQ) = 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 zV 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 LQ and LQС are CQ = {, , R vx ,,u , x, Ex} and CQC = {, , 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 CQ. At the same time, we have
Statement 3. QPrV–A Q PrPV–A; QPrTV–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, CQ), (VA, PrPV–A, CQ), (VA, PrV–A, CQC), (VA, PrPV–A, CQC). They
define pure first order composition algebras AQ = (VA, PrV–A, CQ), AQC = (VA, PrV–A, CQC), AQP = (VA, PrPV–A, CQ),
AQCP = (VA, PrPV–A, CQC); here AQP and AQCP are subalgebras of algebras AQ and AQC.
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;
RI) R zz ,,vx ,,u ( P) R vx ,,u ( P) – identical renomination can be eliminated;
RU) R zy,,vx,,u ( P) R vx ,,u ( P) for unessential for predicate Р name zV;
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 ) ;
RR) 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;
Rs) 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 LQC. An alphabet of the language of LQС 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 , xFr, Fr .
We specify a set VT V of total unessential names (unessential for any рPs) and extend it [3, 6] to formulas:
: Fr2V.
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 LQС). Formulas of the form Rxv ,
,u
are called R-formulas.
Interpretations. We interpretate the language of the LQC on composition systems CS = (VA, PrV–A, CQC).
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 LQ (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 xV 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 LQС 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 LQ 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 LQ 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, RI, RU. 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 , pPs.
Let us call formulas and Un-equivalent (denoted Un ), if for any J = (A, І) and dVA ||–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 zUn, 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
LQ and LQC. 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 LQ
and LQC:
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 JRС 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 LQ: P|=IR, P|=T, P|=F, P|=TF, R|=TF .
In LQС, 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: JTF T(J) = T(J) and F(J) = F(J) J = J .
Equivalent transformations in LQ та LQС 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: RTF, PTF, PIR, 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 LQ and Pс|=T, Pс|=F, Rс|=T, Rс|=F in LQС.
Let us consider properties R, RI, RU, RR, R, R, R for predicates. Each of the properties R
induces 4 corresponding properties RL, RR, RL, RR 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:
R1) Rxv,,u ,, zy (), |= , Ez Rxv,,u ,,y (), |= , Ez; |= , Rxv,,u ,, zy (), Ez |= , Rxv ,,u ,,y (), Ez;
R1) Rvx,,u,,yz (), |= , Ez R vx,,u,,y (), |= , Ez; |= , Rvx,,u,,yz (), Ez |= , Rxv ,,u ,,z (), Ez;
R2) Rxv,,u ,,z (), |= , Ez Rxv,,u (), |= , Ez; |= , Rxv,,u ,,z (), Ez |= , Rxv,,u (), Ez;
R2) 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 zfu(, , х));
RL) Rwv ,,u (x), |= Rwv ,,u ,, xz (), Ez, |= given z fu (, , Rwv ,,u (x)) ;
R) |= х, , Ez |= Rzx (), given zfu(, , х));
RR) |= Rwv ,,u (x), , Ez |= Rwv ,,u ,, xz (), given z fu (, , Rwv ,,u (x)) ;
vR) , Ey |= х, , Ey |= х, Ryx (), ;
RvR) , Ey |= , Rwv ,,u (x) , Ey |= ;
vL) х, Ey, |= x, Ryx (), Ey, |= ;
RvL) Rwv ,,u (x), Ey, |= Rwv ,,u (x), Rwv ,,u ,, xy (), Ey, |= ;
Ed) |= |= , Ey and Ey, |= ; Ev) |= Ez, |= , де zfu(, ).
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(|––|) = {xV | Ex}; unv(|––|) = {xV | 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 LQ we have calculi СQIR, СQT, СQF, СQTF, СQTFR.
For the relations Pс|=T, Pс|=F, Rс|=T, Rс|=F in LQС 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 RU: у()):
| , | , | , | ,
|–R ; –|R ; |–R ; –|R ;
| R ( ), | R ( ), | R ( ), | R ( ),
| Rxv,,u (), | Rxv,,u (), | Rxv ,,u (), | Rxv ,,u (),
|–RI ; –|RI ; |–RI –|RI ;
| Rzz,,xv,,u (), | Rzz,,xv,,u (), | Rzz,,xv ,,u (), | Rzz,,xv ,,u (),
| Rxv,,u (), | Rxv,,u (), | Rxv,,u (), | Rxv,,u (),
|–RU ; –|RU ; |–RU ; –|RU ;
| Rzy,,xv,,u (), | Rzy,,xv,,u (), | Rzy,,xv,,u ( ), | Rzy,,xv,,u ( ),
| Rxv,,u ,,y ( p), | Ez , | Rxv,,u ,,y ( p), | Ez ,
|–R1 , where pPs; –|R1 , where pPs;
| Rxv,,u ,, zy ( p), | Ez , | Rxv,,u ,, zy ( p), | Ez ,
| Rxv,,u ,,y ( p),| Ez, | Rxv,,u ,,y ( p), | Ez,
|–R1 , where pPs; –|R1 , where pPs;
| Rxv ,,u ,, zy ( p),| Ez, | Rxv ,,u ,, zy ( p), | Ez,
| Rxv ,,u ( p), | Ez, | Rxv ,,u ( p), | Ez,
|–R2 , where pPs; –|R2 , where pPs;
| Rxv,,u ,,z ( p), | Ez , | Rxv,,u ,,z ( p), | Ez ,
| Rxv ,,u ( p), | Ez, | Rxv ,,u ( p), | Ez,
|–R2 , where pPs; –|R2 , where pP.
| Rxv,,u ,,z ( p), | Ez, | Rxv,,u ,,z ( p), | Ez,
Forms of equivalent transformations:
| Ry , x , ( ), Ryv ,,z ux ,,t (),
v ,z u ,t
|
|–RR ; –|RR ;
| Ry , (Rx , ( )), Rxv ( Ryw ()),
v ,z u ,t
|
| Ryv ,,z ux ,,t ( ), | Ryv ,,z ux ,,t ( ),
|–RR ; –|RR ;
| 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 ; |–RE ; –|RE .
| Ez, | Ez, | Rxv,,u ( Ez ), | Rxv,,u ( Ez ),
Renomination simplification for variable assignment predicates (condition for |–RE та –|RE: z {v , u } ):
| Ez, | Ez, | Ey, | Ey,
|–RE ; –|RE ; |–REv ; –|REv .
| 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,
|–Rv ; –|Rv .
| Rwv ,,u (x), | Ey, | Rwv ,,u (x), | Ey,
Let us call forms |–R, –|R, |–, –| – T-forms; forms –|v, |–v, –|Rv, |–Rv – F-forms. Conditions for
|–, –|: zfu(, 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 zfu().
Basic sequent forms for the calculus СQIR. Forms |–R, –|R, |–RI, –|RI, |–RU, –|RU, |–R1, –|R1, |–R2, –|R2,
|–RR, –|RR, |–R, –|R, |–R,–|R, |–RE, –|RE, |–REv, –|REv, |, |, |, |–R, |v, –|Rv, 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 zfu(), 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, RI, RU, 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) zVT 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 CQ#. Then |= .
If |––| is derivable in a calculus CQ#, 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 CQCTR and CQCFR.
Theorem 11. Let be an unclosed path in the derivation tree constructed in CQCTR 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 CQCFR 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 = {ynm(Н) | –|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 = {ynm(Н) | |–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:
НR1) –|EzН and | Rxv ,,u ,, zy ( p) H | Rxv ,,u ,,y ( p) H ; –|EzН and | Rxv ,,u ,, zy ( p) H | Rxv ,,u ,,y ( p) H ;
НR1) –|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
НR2) –|EzН and | Rxv,,u ,,z ( p) H | Rxv,,u ( p) H ;
–|EzН and | Rxv,,u ,,z ( p) H | Rxv,,u ( p) H ;
НR2) –|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Н;
НRE ) | Rxv ,,u ( Ez ) H | Rxv ,,u ( Ez ) H ; | Rxv ,,u ( Ez ) H | Rxv ,,u ( Ez ) H ;
НRE ) given z {v , u } we have: | Rxv,,u ( Ez ) H | Ez H ; | Rxv,,u ( Ez ) H | Ez H ;
НREv ) | 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 xW, then ExА () = T, therefore T(ExА); –|Ex Н gives xW, 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 xW, then ExА () = T, therefore F(Ex B); –|Ex Н gives xW, 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 НR1 for both interpretations A and B.
Let –|EzН and | R vx,,u,,yz ( p) H . Condition –|EzН gives zW, then (z), therefore r vx ,,u,,y () r vx ,,u,,yz ().
By НR1 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 zW, then (z), therefore r vx ,,u,,y () r vx ,,u,,yz ().
By НR1 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 НR1, НR2, НR2 and НE, НRE .
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 CQСT and CQСF can be formulated and proved similarly.
As calculi CQСT and CQС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 CQСT);
НСR) there is no formula such that –|, –|Н (case of derivation in CQСF).
The counter-model existence theorems for the calculi CQT and CQF can be formulated and proved similarly to
theorems 11 and 12: conditions HR , HR , Н 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 CQTFR, CQTF and CQIR.
Theorem 13. Let be an unclosed path in the derivation tree constructed in CQTFR 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 CQTF 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 , HR , Н 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 CQIR 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 CQ#.
Let us prove for relation Rc|=T and calculus CQCTR (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).