The paper considers new classes of software-oriented logical formalisms - pure first-order logics of partial quasiary predicates with extended renominations and predicates of strong equality and of weak equality, denoted respectively L⊥Q≡ and L⊥Q=. The characteristic features of the studied logics are using of composition of extended renomination, and special 0-ary predicate compositions that detect if the subject variables or predicates of equality have assigned values. We specify two kinds of equality predicates: the predicate of weak (up to definedness) equality =xy, and the predicate of strong equality ≡ xy. For the considered logics, main properties of their compositions are given, their languages are described, and various variants of logical consequence relations are defined. For the language L⊥Q= we obtain only one correct relation P|=IR, at the same time for L⊥Q≡ we have relations P≡|=IR, P≡|=T, P≡|=F, P≡|=TF, R≡|=TF . We describe properties of the introduced relations, paying special attention to those connected with equality predicates. As sequent calculi formalise logical consequence relations for sets of formulas, properties of the latter become the semantic basis for construction of the respective calculi. Thus, for P=|=IR we get calculus С⊥Q=IR; relations R≡|=TF, P≡|=TF, P≡|=T, P≡|=F, and P≡|=IR induce calculi С⊥Q≡TFR, С⊥Q≡TF, С⊥Q≡T, С⊥Q≡F, and С⊥Q≡IR respectively. We specify basic sequent forms (rules) for the presented calculi, and conditions for sequent closedness. Description of the derivation procedure via sequent tree is given, using of rules concerning equality predicates explained. The counter-model existence theorems are considered; on the example of calculus С⊥Q≡TFR we illustrate a counter-model construction by an unclosed path in the sequent tree. For the introduced calculi, the soundness and completeness theorems are proved; the proof of the completeness theorems is based on construction of the respective counter-models.
Methods of mathematical logic have proved to be effective in various applications in computer
science and programming. Many different logic systems have been created (see, for example, [
Pure first-order logics of quasiary predicates (PCNL) are called LQ (logics of quantifier level).
PCNL with extended renominations are called ⊥PCNL, and also L⊥Q; PCNL with predicates of strong
equality and weak equality are called LQ≡ and LQ= respectively; ⊥PCNL with predicates of strong
equality and weak equality are called L⊥Q≡ and L⊥Q= respectively. PCNL and their calculi are described
in [
The purpose of this work is to investigate logical consequence relations in L⊥Q= and L⊥Q≡, and to
construct their sequent calculi. These calculi generalize sequent calculi both for ⊥PCNL [
To facilitate reading, we provide the necessary definitions for further presentation. Concepts that
are not defined in this paper are interpreted in the sense of [
Let VA be a set of all V-A-nominative sets and {T, F} is a set of Boolean values. We define V-Aquasiary predicate as a partial many-valued function Q : VA Æ {T, F}.
Let V be a set of names (variables) and A be a set of values. V-A-nominative set is defined [
For nominative sets we define set theory operations ∩ and \, and parametric operations || Z and ||–
Z [
d || Z = {v a a ∈ d | v ∈ Z}; d ||–Z = {v a a ∈ d | v ∉ Z}.
The parametric operation of extended renomination r[v1a x1,...,vn a xn,u1a ⊥,...,um a ⊥] : VА Æ VA, where vi, xi, uj ∈V, is specified as rvx11,,......,,vxnn,,u⊥1,,......,,⊥um (d ) = d ||−{v1,...,vn,u1,...,um} ∪ [v1 a d(x1),..., vn a d(xn )]. In particular, r[ua ⊥](d) = d ||−u .
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.
A simpler notation for sequences y1,..., yn will be used: y . Thus, instead of r[v1a x1,...,vn a xn ,u1a ⊥,...,um a ⊥] , we will write rvx,,u⊥ .
Given d(z)#, we obtain rvx,,u⊥,,yz (d) = rvx,,u⊥,,y⊥ (d) and rvx,,u⊥,,z⊥ (d) = rvx,,u⊥ (d) .
Successive renominations rux,,as,,w⊥,,t⊥ and rvy,,cs,,⊥z,,t⊥ can be represented [
In this work we construct sequent calculi for logics of many-valued (non-deterministic) predicates of relational type (R-predicates): R-predicates are interpreted as mappings (relations) from VA to {T, F}. Each R-predicate Q is unequivocally defined by two sets: its truth domain T(Q) = {d | T∈Q(d)} and falsity domain F(Q) = {d | F∈Q(d)}, where Q(d) denotes the set of values which Q assumes on argument d∈VА.
A name х∈V is unessential for R-predicate Q, if for any d1, d2 ∈VA we have: d1 ||–х = d2 ||–х ⇒ Q(d1) = Q(d2).
V-A-quasiary R-predicate Q is: – partial single-valued, or P-predicate, if T(Q)∩F(Q) = ∅; – total, or T- предикат, if T(Q)∪F(Q) = VA; – total single-valued, or TS- predicate, if T(Q)∩F(Q) = ∅ and T(Q)∪F(Q) = VA; – irrefutable, or partially true, if F(Q) = ∅; all irrefutable predicates are P-predicates; – totally true (denoted T), if F(Q) = ∅ and T(Q) = VА; – totally false (denoted F), if T(Q) = ∅ and F(Q) = VА; – totally undefined (denoted ), if T(Q) = F(Q) = ∅; – totally ambivalent (denoted ϒ), if T(P) = F(P) = VА; – monotonic, if d1 ⊆ d2 ⇒ Q(d1) ⊆ Q(d2); antitonic, if d1 ⊆ d2 ⇒ Q(d1) ⊇ Q(d2).
We will denote classes of V-A-quasiary R-predicates, P-predicates, T-predicates and TS-predicates PrV–A, PrPV–A, PrTV–A and PrTS V–A respectively. The class PrTSV–A is degenerate: all TS-predicates, except constant T and F, are non-monotonic.
Considering the duality of classes PrPV–A and PrTV–A, and the degeneracy of PrTSV–A [
– L⊥Q≡ and L⊥Q≡P – ⊥PCNL of R-predicates with strong equality and ⊥PCNL of P-predicates with strong equality.
A tuple (VA, PrV–A, CB), where CB is a set of basic compositions, is called a composition predicate system; it forms a semantic basis for CNL. Each such system defines a data algebra (VA, PrV–A) and a composition predicate algebra (PrV–A, CB).
Sets of basic compositions for different classes of ⊥PCNL are introduced as follows: C⊥Q = {¬ , ∨, Rvx,,u⊥ , ∃ x, Ex} for L⊥Q and L⊥QP, C⊥Q= = C⊥Q ∪ {={x,y}} for L⊥Q= and L⊥Q=P, C⊥Q≡ = C⊥Q ∪ {≡ {x,y}} for L⊥Q≡ and L⊥Q≡P. Let us specify the basic compositions.
Logical connectives ¬ and ∨ 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).
We specify the composition of extended renomination Rvx,,u⊥ : PrV −A Æ PrV −A as follows:
Rvx,,u⊥ (P)(d) = P (rvx,,u⊥ (d)) .
A convolution of the renomination compositions is defined by a convolution of the corresponding renomination operations:
Rvy,,z⊥ oux,,t⊥ (P)(d) = (Rvy,,z⊥ (Rux,,⊥t (P)))(d) = P(rxu,,⊥t gvy,,z⊥ (d)).
We define the quantifier (composition of quantification) ∃ xP : PrV −A Æ PrV −A as follows: T(∃ xP) = U {d | d ||−x ∪ x a a ∈T (P)} ; F(∃ xP) = I {d | d ||−x ∪ x a a ∈ F (P)}.
a∈A a∈A
A 0-ary predicate Ez indicates whether a component z∈V has a value on a given data [
T(Ez) = {d | d(z)$}; F(Ez) = {d | d(z)#}.
Predicates Ez are total, sinle-valued, and non-monotonic. Each x∈V such that x ≠ z, is unessential for Ez.
Predicates of weak equality (up to definedness) ={x,y} are specified as follows [
T(={x,y}) = {d | d(x)$, d(y)$ and d(x) = d(y)};
F(={x,y}) = {d | d(x)$, d(y)$ and d(x) ≠ d(y)}.
Predicates of strong equality ≡ {x,y} are defined as follows [
T(≡ {x,y}) = {d | d(x)$, d(y)$ and d(x) = d(y)} ∪ {d | d(x)# and d(y)#};
F(≡ {x,y}) = {d | d(x)$, d(y)$ and d(x) ≠ d(y)} ∪ {d | d(x)$, d(y)# or d(x)#, d(y)$}.
We will further denote the predicates ={x,y} and ≡ {x,y} as =xy and ≡ xy respectively; note that such predicates are traditionally denoted as x = y and x ≡ y.
Predicates ≡ xy are total single-valued, non-monotonic and non-antitonic. Every name z∈V \{x, y} is unessential for ≡ {x,y}.
Predicates =xy are partial single-valued and monotonic (equitone). Every name z∈V \{x, y} is unessential for ={x,y}.
The special case for ={x,y} and ≡ {x,y} is the situation, when x and y represent the same name; the corresponding predicates ={x} and ≡ {x} will be denoted as =xх and ≡ xх (in traditional form x = x and x ≡ x). Every name z∈V \{x} is unessential for =xх and ≡ xх.
For predicate ≡ xx we have T(≡ xx) = VА and F(≡ xx) = ∅, whence ≡ xx = T. For predicate =xx we have F(=xx) = ∅, whence =xx is irrefutable.
Thus, the following predicate composition algebras of ⊥PCNL can be specified: – A⊥Q = (VA, PrV–A, C⊥Q) and A⊥QP = (VA, PrPV–A, C⊥Q), wherein A QP is a subalgebra of A⊥Q; ⊥ – A⊥Q= = (VA, PrV–A, C⊥Q=) and A Q=P = (VA, PrPV–A, C⊥Q=), wherein A Q=P is a subalgebra of A⊥Q=; ⊥ ⊥ – A⊥Q≡ = (VA, PrV–A, C⊥Q=) and A⊥Q≡P = (VA, PrPV–A, C⊥Q≡), wherein A⊥Q≡P is a subalgebra of A⊥Q≡.
The main properties of the ⊥PCNL compositions. Properties of propositional compositions and
quantifiers, unrelated to renominations, correspond to those of classical logical connectives and
quantifiers [
Let us specify basic simplification properties for the composition of extended renomination: R⊥I) R zz,,vx,,u⊥ (P) = Rvx,,u⊥ (P) – identical renomination can be eliminated; R⊥U) z∈V is unessential for predicate Р ⇒ R zy,,vx,,u⊥ (P) = Rvx,,u⊥ (P); R#) given d(z)# we have Rvx,,u⊥,,yz (P)(d) = Rvx,,u⊥,,y⊥ (P)(d) and Rvx,,u⊥,,z⊥ (P)(d ) = Rvx,,u⊥ (P)(d ) ; R⊥E) Rvx,,u⊥,,zy (Ez) = Ey ; given z ∉{v ,u} we have Rvx,,u⊥ (Ez) = Ez.
Properties related to renomination R, R⊥R, R⊥¬, R⊥∨ and quantification compositions are given in
[
Let us consider properties of equality predicates. Note that the symmetric property of equality lies within notation, as pairs ≡ xy and ≡ yx, =xy and =yx are essentially the same predicates.
We define the reflexivity properties as follows:
Rf=) each predicate =xx is irrefutable; moreover, =xx can be denoted as =xx = Ex ∨ ; Rf≡) each predicate ≡ xx is totally true, i.e. ≡ xx = T.
The transitivity properties are specified as follows:
Tr=) for all d∈VA we have: =xy(d) = T and =yz(d) = T ⇒ =xz(d) = T; whence =xy & =yz → =xz is irrefutable.
Tr≡) for all d∈VA we have: ≡ xy(d) = T and ≡ yz(d) = T ⇒ ≡ xz(d) = T; whence ≡ xy & ≡ yz → ≡ xz = T.
Let us consider properties of renominations for weak equality predicates (properties of the type R⊥=):
R⊥=xx) Rvw,,u⊥,,xz ( =xx) = =zz; R⊥=1) given y ∉{u,v}, x ≠ y we have Rvw,,u⊥,,xz ( =xy) = =zy;
R⊥=2) Rvw,,u⊥,,xz,,ys ( =xy) = =zs;
R⊥=0) given x, y ∉{u, v} we have Rvw,,u⊥ ( =xy) = =xy; in particular, given x ∉{u, v} we have Rvw,,u⊥ ( =xx) = =xx;
R⊥=⊥) Rvw,,u⊥,,⊥x ( =xy) = ; in particular, Rvw,,u⊥,,⊥x ( =xx) = .
For weak equality predicates we have properties of substitution of equals and elimination of pair of equals in renominations:
=R⊥r) for all P∈PrPV–A and d∈VA we have: =xy(d) = T ⇒ Rvw,,u⊥,,zx (P)(d) = Rvw,,u⊥,,zy (P)(d) – substitution of equals;
=elR⊥) for all P∈PrPV–A and d∈VA we have: =xy(d) = T ⇒ Rvw,,u⊥,,xy (P)(d) = Rvw,,u⊥ (P)(d) . Properties of renominations for strong equality predicates (properties of the type R⊥≡ ): R⊥≡xx) Rvw,,u⊥,,xz (≡xx ) = ≡zz ; R⊥≡2E) Rvw,,u⊥,,xz,,y⊥ (≡xy ) = ¬Ez; R⊥≡1) for all y ∉{u,v}, x ≠ y we have Rvw,,u⊥,,xz (≡xy ) = ≡zy ; R⊥≡1E) for all y ∉{u,v}, x ≠ y we have Rvw,,u⊥,,x⊥ (≡xy ) = ¬Ey;
R⊥≡2) Rvw,,u⊥,,xz,,ys (≡xy ) = ≡zs ;
R⊥≡0) for all x, y ∉{u, v} we have Rvw,,u⊥ (≡xy ) = ≡xy ; in particular, Rvw,,u⊥ (≡xx ) = ≡xx given x ∉{u,v};
R⊥≡⊥) Rvw,,u⊥,,x⊥,,y⊥ (≡xy ) = T; in particular, Rvw,,u⊥,,⊥x (≡xx ) = T.
Properties of substitution of equals and elimination of pair of equals in renominations for strong equality predicates:
≡R⊥r) for all P∈PrPV–A and d∈VA we have: ≡xy(d) = T ⇒ Rvw,,u⊥,,zx (P)(d) = Rvw,,u⊥,,zy (P)(d) – substitution of equals;
≡elR⊥) for all P∈PrPV–A and d∈VA we have: ≡xy(d) = T ⇒ Rvw,,u⊥,,xy (P)(d) = Rvw,,u⊥ (P)(d) . 3. Logical consequence relations for L⊥Q= and L⊥Q≡
Let us describe languages of ⊥PCNL. We will concentrate on the language of L⊥Q≡, languages of L⊥Q= and L⊥Q are defined in the similar manner.
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, each Ex, and each ≡ху is a formula; such formulas are called atomic; – let Φ, Ψ∈Fr; then ¬Φ∈Fr, ∨ΦΨ∈Fr, Rxv,,⊥uΦ ∈ Fr, ∃xΦ∈Fr.
We specify a set VT ⊆ V of totally unessential names (unessential for any р∈Ps) and extend it
[
If х∈ν(Φ), then х is unessential for Φ [
We call a formula primitive, if it is atomic or has a form Rxv,,⊥u p, where р∈Ps, {v ,u}∩ ν( p) = ∅ and there are no identical pair of names in Rxv,,⊥u . Formulas of the form Rxv,,⊥uΦ are called R-formulas.
The set of names x∈V that occur in Φ is denoted nm(Φ).
For any Γ ⊆ Fr we denote: nm(Γ) = U nm(Φ); ν(Γ) = I ν(Φ); fu(Γ) = VT \ nm(Γ).
Φ∈Γ Φ∈Γ We interpretate the language of L⊥Q≡ on composition systems CS = (VA, PrV–A, C⊥Q≡).
Symbols in Cs are interpretated as corresponding compositions; symbols Ex – as variable assignment predicates Ex; symbols ≡ху – as corresponding predicates of strong equality ≡ху.
We specify a total single-valued mapping I : Ps Æ PrV–A, and extend it to formulas as an interpretation mapping I : Fr Æ PrV–A:
I(¬Φ) = ¬ (I(Φ)), I(∨ΦΨ) = ∨ (I(Φ), I(Ψ)), I (Rxv,,⊥uΦ) = Rvx,,u⊥ (I (Φ)), I(∃хΦ) = ∃ х(I(Φ)).
Let the tuple J = (CS, Σ, I), where Σ = (V, VT, Cs≡, Ps) is an extended signature of the language, be an interpretation of the language of L⊥Q≡ (further shortened to J = (A, I)).
Predicate I(Φ) is a value of a formula in the interpretation J (further denoted ΦJ).
Name x∈V is unessential for a formula Φ, if x is unessential for ΦJ for any interpretation J. The language for L⊥Q= is specified in the same manner (changing ≡ху to =ху).
For the language for L⊥Q we omit everything connected with ≡ху .
Classes of interpretations of a language are also called semantics. Specifying of subalgebras of Ppredicates in algebras A⊥Q, A⊥Q=, A⊥Q≡ leads to the following respective semantics: ⊥R and ⊥P, ⊥R= and ⊥P=, ⊥R≡ and ⊥P≡.
Formula Φ is irrefutable in the interpretation J (denoted J |= Φ), if ΦJ is a irrefutable predicate. Formula Φ is irrefutable in the semantics α (denoted α|= Φ), if J |= Φ for any interpretation J∈α . Formula Φ totally true in the interpretation J (denoted J |=id Φ), if ΦJ is a totally true predicate. Formula Φ totally true in the semantics α (denoted α|=id Φ), if J |=id Φ for any interpretation J∈α . Let us call constant formulas that are always interpreted as constant predicates T, F, . For example, Ex ∨ ¬Ex, ≡ xx, ∃xEx, R⊥x,,⊥z (≡xz ) are T-formulas; Rxv,,⊥u,,⊥z (Ez) is an F-formula, Rvx,,u⊥,,z⊥ (=zy ) is a ⊥formula.
Un-equivalent formulas. Let Rxx,,yv,,tu,,⊥w,,⊥z (Φ) be an R-formula, such that {u, w} ⊆ ν(Φ). Let us call an Rs-form of an R-formula Ryv,,⊥z (Φ) the R-formula obtained from Ryv,,⊥z (Φ) by all possible simplifications of external renomination based on properties R, R⊥I, R⊥U, and properties of the type R⊥≡ .
We will call Rs-formulas Rs-forms of R-formulas. If ϑ is an Rs-form of an R-formula Ψ, then ϑJ = ΨJ for all J.
Let Un ⊆ V be a set of indefinite names.
Let us call formulas Ψ and ϑ Un-equivalent (denoted Ψ ∼Un ϑ), if for all J = (A, І) and d∈VA ||–Un we have ΨJ (d) = ϑJ (d).
Statement 1 (implied from R#). Let z∈Un, then Rxv,,⊥u,,zyΦ : Un Rxv,,⊥u,,⊥y Φ and Rxv,,⊥u,,⊥zΦ : Un Rxv,,⊥uΦ.
Rs-formula can be presented in the form
Rvz,,yx,,sr,,⊥u,,⊥wΦ , where {y, r , s ,u} ⊆ Un, {v, x, w}∩Un = ∅.
Un-form Rvz,,⊥x,,⊥wΦ (also called Un-formula) can be obtained transforming an Rs-formula Rvz,,yx,,sr,,⊥u,,⊥wΦ in such a manner.
Statement 2. If Ψ is an Un-form of a formula Φ, then Φ ∼Un Ψ.
Logical consequence relations. Let us extend logical consequence relations P|=IR, P|=T, P|=F, P|=TF,
R|=TF defined on formulas of the language LQ [
Firstly, let us specify the following logical consequence relations for two sets of formulas in the interpretation J: – IR-consequence, or irrefutable J|=IR : Φ J|=IR Ψ ⇔ T(ΦJ)∩F(ΨJ) = ∅; – T-consequence (on truth) J|=T : Φ J|=T Ψ ⇔ T(ΦJ) ⊆ T(ΨJ); – F-consequence (on falsity) J|=F : Φ J|=F Ψ ⇔ F(ΨJ) ⊆ F(ΦJ); – TF-consequence, or strong J|=TF : Φ J|=TF Ψ ⇔ Φ J|=T Ψ and Φ J|=F Ψ.
The corresponding logical τ-consequence relations in the semantics α are defined as follows: Φ α|=τ Ψ, if Φ J|=τ Ψ for every interpretation J∈α .
We define a logical τ-equivalence relation in the interpretation J as follows:
Φ J∼τ Ψ, if Φ J|=τ Ψ and Ψ J|=τ Φ.
A logical τ-equivalence relation in the semantics α are defined as folllows:
Φ α∼τ Ψ, if Φ α|=τ Ψ and Ψ α|=τ Φ.
Note the importance of the relation J ∼TF : Φ J∼TF Ψ ⇔ T(ΦJ) = T(ΨJ) and F(ΦJ) = F(ΨJ) ⇔ ΦJ = ΨJ.
Consequence and logical consequence relations for a pair of formulas can be extended on pairs of sets of formulas.
Let Σ, Γ, Δ ⊆ Fr be sets of formulas, J be an interpretation. We will further denote: I T (θJ ) as T∩(ΣJ), U T (θJ ) as T∪(ΣJ), I F(θJ ) as F∩(ΣJ), U F(θJ ) as F∪(ΣJ).
θ∈Σ θ∈Σ θ∈Σ θ∈Σ Δ is an IR-consequence of Γ in the interpretation J (denoted Γ J|=IR Δ), if T∩(ΓJ) ∩ F∩(ΔJ) = ∅. Δ is T-consequence of Γ in the interpretation J (denoted Γ J|=T Δ), if T∩(ΓJ) ⊆ T∪(ΔJ). Δ is F-consequence of Γ in the interpretation J (denoted Γ J|=F Δ), if F∩(ΔJ) ⊆ F∪(ΓJ). Δ is TF-consequence of Γ in the interpretation J (denoted Γ J|=TF Δ), if Γ J|=T Δ and Γ J|=F Δ. The corresponding logical τ-consequence relations in the semantics α are defined as follows: Γ α|=τ Δ, if Γ J|=τ Δ for every interpretation J∈α.
Here α denotes one of the semantics: ⊥R, ⊥P, ⊥R=, ⊥P=, ⊥R≡, ⊥P≡. Thus, there is a total of 24 logical concequence relations.
Some of them coincide, some are degenerate, and the relations P=|=T, P=|=F, P=|=TF, R=|=TF are
incorrect [
P|=IR, P|=T, P|=F, P|=TF, R|=TF ; P=|=IR; P≡|=IR, P≡|=T, P≡|=F, P≡|=TF, R≡|=TF .
We will use P# to denote one of the P, P=, P≡; R# to denote one of the R, R=, R≡; ∼TF to denote one of the R#∼TF, P#∼TF; and |=∗ to denote one of the P#|=IR, P#|=T, P#|=F, P#|=TF, R#|=TF. Also the meaning of the notations =|=∗ and ≡|=∗ should be obvious.
Properties of logical consequence relations. As sequent calculi formalise logical consequence
relations, properties of the latter become the semantic basis for construction of the respective calculi.
Such properties are described in [
Traditional properties of formulas decomposition are specified in detail in [
For Ez and their renominations we have properties of carrying ¬ to the other side of a relation: ¬EL) ¬Ez, Γ |=∗ Δ ⇔ Γ |=∗ Δ, Ez; ¬ER) Γ |=∗ Δ, ¬Ez ⇔ Ez, Γ |=∗ Δ; ¬REL) ¬Rwv,,u⊥ (Ez), Γ |=∗ Δ ⇔ Γ |=∗ Rwv,,⊥u (Ez), Δ; ¬RER) Γ |=∗ ¬Rwv,,u⊥ (Ez), Δ ⇔ Rwv,,u⊥ (Ez), Γ |=∗ Δ.
Properties of equivalent transformations connected with extended renominations hold for P#|=IR,
P#|=T, P#|=F, P#|=TF, R#|=TF , they are based on the predicates properties R, R⊥I, R⊥U, R#, R⊥¬, R⊥∨, R⊥R
and R⊥E. Each of R, R⊥I, R⊥U, R⊥¬, R⊥∨, R R induces 4 corresponding properties 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 two foursomes of properties: R#1L) Rxv,,⊥u,,zy (Φ), Γ |=∗ Δ, Ez ⇔ Rxv,,⊥u,,⊥y (Φ),Γ |=∗ Δ, Ez; R#1R) Γ |=∗ Δ, Rxv,,⊥u,,zy (Φ), Ez ⇔ Γ |=∗ Δ, Rxv,,⊥u,,⊥y (Φ), Ez; R#2L) Rxv,,⊥u,,⊥z (Φ), Γ|=∗ Δ, Ez ⇔ Rxv,,⊥u (Φ),Γ |=∗ Δ, Ez;
R#2R) Γ |=∗ Δ, Rxv,,⊥u,,⊥z (Φ), Ez ⇔ Γ |=∗ Δ, Rxv,,⊥u (Φ), Ez; To them will be added similar properties ¬R#1L, ¬R#1R, ¬R#2L, ¬R#2R.
R⊥E induces the next 4 properties of simplification of external renomination of predicatesindicators:
R⊥EvL ) Rxv,,⊥u,,zy (Ez), Γ |=∗ Δ ⇔ Ey, Γ |=∗ Δ;
R⊥EvR ) Γ |=∗ Δ, Rxv,,⊥u,,zy (Ez) ⇔ Γ |=∗ Δ, Ey; R⊥EL ) Rxv,,⊥u (Ez), Γ |=∗ Δ ⇔ Ez, Γ |=∗ Δ, where z ∉{v ,u};
R⊥ER ) Γ |=∗ Δ, Rxv,,⊥u (Ez) ⇔ Γ |=∗ Δ, Ez, where z ∉{v, u}.
Properties of quantifier elimination, E-distribution and primary definition are defined in [
Let us describe properties which guarantee the specified logical consequence relation. There is a general for all considered relations property С and property СF, connected with constant F-formulas (see R⊥EF): С) Φ, Γ |=∗ Δ, Φ;
CF) Rxv,,⊥u,,⊥z (Ez), Γ |=∗ Δ.
СL) Φ, ¬Φ, Γ P#|=T Δ; СR) Γ P#|=F Δ, Φ, ¬Φ; СLR) Φ, ¬Φ, Γ P#|=TF Δ, Ψ, ¬Ψ.
Basing on these properties, we can define conditions which guarantee a certain logical consequence relation Γ |=*Δ.
С) there exists Φ: Φ∈Γ and Φ∈Δ; СF) there exists Rxv,,⊥u,,⊥z (Ez) ∈ Γ ; СL) there exists Φ: Φ∈Γ and ¬Φ∈Γ; СR) there exists Φ: Φ∈Δ and ¬Φ∈Δ; СLR) there exist Φ, Ψ: Φ, ¬Φ∈Γ and Ψ, ¬Ψ∈Δ.
С and СF guarantee every Γ |=*Δ; СL guarantees Γ P#|=T Δ; СR guarantees Γ P#|=F Δ; СLR guarantees Γ P#|=TF Δ.
Let us consider properties, connected with =xy. Transitivity of the weak equality relation does not
hold for P=|=F and P=|=T [
Transitive property for =xy:
Tr=) =xy, =yz, Γ P=|=IR Δ ⇔ =xy, =yz, =xz Γ P=|=IR Δ.
Properties, based on R⊥=xx, R⊥=2, R⊥=1, R⊥=0:
R⊥=xxL) Rwv,,u⊥,,xz (=xx ), Γ P=|=IR Δ ⇔ =zz, Γ P=|=IR Δ; R⊥=2L) Rwv,,u⊥,,xz,,sy(=xy),Γ P=|=IR Δ ⇔ =zs, Γ P=|=IR Δ; R⊥=2R) Γ P=|=IR Δ, Rwv,,u⊥,,xz,,sy(=xy) ⇔ Γ P=|=IR Δ, =zs; R⊥=1L) Rwv,,u⊥,,xz(=xy),ΓP=|=IR Δ ⇔ =zy, Γ P=|=IR Δ given y∉{u,v}, x ≠ y; R⊥=1R) Γ P=|=IR Δ, Rwv,,⊥u,,xz(=xy) ⇔ Γ P=|=IR Δ, =zy given y∉{u,v}, x ≠ y; R⊥=0L) Rwv,,⊥u(=xy),ΓP=|=IR Δ ⇔ =xy, Γ P=|=IR Δ given x, y∉{u,v};
R⊥=0R) Γ P=|=IR Δ, Rwv,,u⊥(=xy) ⇔ Γ P=|=IR Δ, =xy given x, y∉{u,v}. =R⊥r induces properties of substitution of equals for P|=IR : =R⊥rL) =xy,Rwv,,u⊥,,zx(Φ),Γ P=|=IR Δ ⇔ =xy,Rwv,,u⊥,,zx(Φ),Rwv,,u⊥,,zy(Φ),ΓP=|=IR Δ; =R⊥rR) =xy,Γ P=|=IR Rwv,,u⊥,,zx(Φ),Δ ⇔ =xy,Γ P=|=IR Rwv,,u⊥,,zx(Φ),Rwv,,u⊥,,zy(Φ),Δ .
Properties of elimination of pair of equals in renominations are based =elR⊥: =elR⊥L) =xy,Rwv,,u⊥,,yx(Φ),Γ P=|=IR Δ ⇔ =xy,Rwv,,u⊥(Φ),ΓP=|=IR Δ; =elR⊥R) =xy,Γ P=|=IR Rwv,,u⊥,,xy(Φ),Δ ⇔ =xy,Γ P=|=IR Rwv,,u⊥(Φ),Δ.
Rf= and R⊥=⊥ induce properties that guarantee the relation P=|=IR : СRf=) Γ P=|=IR =xx, Δ. С⊥L) Rwv,,u⊥,,⊥x(=xy),ΓP=|=IR Δ and Rwv,,u⊥,,⊥x(=xx),ΓP=|=IR Δ; С⊥R) Γ P=|=IR Δ, Rwv,,u⊥,,⊥x(=xy) and Γ P=|=IR Δ, Rwv,,u⊥,,⊥x(=xx).
Therefore, we can define conditions which guarantee Γ P=|=IR Δ :
СE=L) =xy, Γ P=|=IR Ex, Δ; in particular, =xx, Γ P=|=IR Ex, Δ; СE=R) Γ P=|=IR =xy, Ex, Δ. We have T(=xy)∩F(Ex) = ∅ and F(=xy)∩F(Ex) = ∅, whence properties which guarantee P=|=IR : СRf=) =xx∈Δ; С⊥L) Rwv,,u⊥,,⊥x(=xy)∈Γ; in particular, Rwv,,u⊥,,⊥x(=xx)∈Γ; С⊥R) Rwv,,u⊥,,⊥x(=xy)∈Δ; in particular, Rwv,,u⊥,,⊥x(=xx)∈Δ; СE=L) =xy∈Γ and Ex∈Δ; in particular, =xx∈Γ and Ex∈Δ; СE=R) =xy∈Δ and Ex∈Δ.
Let us consider properties, connected with ≡xy. Transitivity for ≡xy:
Tr≡) ≡xy, ≡yz, Γ ≡|=∗ Δ ⇔ ≡xy, ≡yz, ≡xz, Γ ≡|=∗ Δ.
For ≡xy and their renominations we have properties of ¬ elimination after carrying to the other side of a relation: ¬≡L) ¬≡xy, Γ |=∗ Δ ⇔ Γ |=∗ Δ, ≡xy; ¬R≡L) ¬Rwv,,u⊥(≡xy),Γ |=∗ Δ ⇔ Γ |=∗ Rwv,,u⊥(≡xy),Δ; ¬R≡R) Γ |=∗ ¬Rwv,,u⊥(≡xy),Δ ⇔ Rwv,,u⊥(≡xy),Γ|=∗ Δ.
¬≡R) Γ |=∗ Δ, ¬≡xy ⇔ ≡xy, Γ |=∗ Δ; Simplification properties based on R⊥≡xx, R⊥≡2, R⊥≡1, R⊥≡0:
R⊥≡xxL) Rwv,,u⊥,,xz(≡xx),Γ≡|=∗ Δ ⇔ ≡zz, Γ ≡|=∗ Δ; R⊥≡xxR) Γ ≡|=∗ Δ, Rwv,,⊥u,,xz(≡xx) ⇔ Γ ≡|=∗ Δ, ≡zz ; R⊥≡2L) Rwv,,u⊥,,xz,,sy(≡xy),Γ ≡|=∗ Δ ⇔ ≡zs, Γ ≡|=∗ Δ; R⊥≡2R) Γ ≡|=∗ Δ, Rwv,,u⊥,,xz,,sy(≡xy) ⇔ Γ ≡|=∗ Δ, ≡zs ; R⊥≡2EL) Rwv,,u⊥,,xz,,⊥y(≡xy),Γ≡|=∗ Δ ⇔ ¬Ez, Γ ≡|=∗ Δ; R⊥≡2ER) Γ ≡|=∗ Δ, Rwv,,⊥u,,xz,,⊥y(≡xy) ⇔ Γ ≡|=∗ Δ, ¬Ez; R⊥≡1L) Rwv,,u⊥,,xz(≡xy),Γ≡|=∗ Δ ⇔ ≡zy, Γ ≡|=∗ Δ; R⊥≡1R) Γ ≡|=∗ Δ, Rwv,,⊥u,,xz(≡xy) ⇔ Γ ≡|=∗ Δ, ≡zy; R⊥≡1EL) Rwv,,u⊥,,x⊥(≡xy),Γ≡|=∗ Δ ⇔ ¬Ey, Γ ≡|=∗ Δ; R⊥≡1ER) Γ ≡|=∗ Δ, Rwv,,u⊥,,x⊥(≡xy) ⇔ Γ ≡|=∗ Δ, ¬Ey.
R⊥≡0L) Rwv,,⊥u(≡xy),Γ≡|=∗ Δ ⇔ ≡xy, Γ ≡|=∗ Δ;
R⊥≡0R) Γ ≡|=∗ Δ, Rwv,,u⊥(≡xy)|=∗ Δ ⇔ Γ ≡|=∗ Δ, ≡xy.
Condition for R⊥≡1L, R⊥≡1R, R⊥≡1EL, R⊥≡1ER: y ∉{u,v}, x ≠ y . x, y ∉{u, v}.
Properties of elimination of pair of equals in renominations based on ≡elR⊥: СRf≡) Γ ≡|=∗ Δ, ≡xx; СRf≡) ≡xx∈Δ; ≡ elR⊥L) ≡xy , Rwv,,u⊥,,yx (Φ), Γ ≡|=∗ Δ ⇔ ≡xy , Rwv,,u⊥ (Φ), Γ ≡|=∗ Δ; ≡ elR⊥R) ≡xy , Γ ≡|=∗ Rwv,,u⊥,,xy (Φ), Δ ⇔ ≡xy , Γ ≡|=∗ Rwv,,u⊥ (Φ), Δ; . ≡ el¬R⊥L) ≡xy , ¬Rwv,,⊥u,,xy (Φ), Γ |=∗ Δ ⇔ ≡xy , ¬Rwv,,u⊥ (Φ), Γ |=∗ Δ; ≡ el¬R⊥R) ≡xy , Γ ≡|=∗ ¬Rwv,,u⊥,,yx (Φ), Δ ⇔ ≡xy , Γ ≡|=∗ ¬Rwv,,u⊥ (Φ), Δ .
Properties of substitution of equals induced by ≡R⊥r: ≡ R⊥rL) ≡xy , Rwv,,u⊥,,zx (Φ), Γ ≡|=∗ Δ ⇔ ≡xy , Rwv,,u⊥,,zx (Φ), Rwv,,u⊥,,zy (Φ), Γ ≡|=∗ Δ; ≡ R⊥rR) ≡xy , Γ ≡|=∗ Rwv,,u⊥,,zx (Φ), Δ ⇔ ≡xy , Γ ≡|=∗ Rwv,,u⊥,,zx (Φ), Rwv,,u⊥,,zy (Φ), Δ . ≡ ¬R⊥rL) ≡xy , ¬Rwv,,⊥u,,zx (Φ), Γ|=∗ Δ ⇔ ≡xy , ¬Rwv,,u⊥,,zx (Φ), ¬Rwv,,u⊥,,zy (Φ), Γ |=∗ Δ; ≡ ¬R⊥rR) ≡xy , Γ ≡|=∗ ¬Rwv,,u⊥,,zx (Φ), Δ ⇔ ≡xy , Γ ≡|=∗ ¬Rwv,,⊥u,,zx (Φ), ¬Rwv,,⊥u,,zy (Φ), Δ .
Properties of ≡xy which guarantee the relation ≡|=*:
CE≡L) ≡xy, Ex, Γ ≡|=∗ Ey, Δ; CE≡R) Γ ≡|=∗ ≡xy, Ex, Ey, Δ.
Finally, we can obtain conditions which guarantee Γ ≡|=* Δ :
CR≡) Γ ≡|=∗ Δ, Rxv,,⊥u,,⊥x,,z⊥ (≡xz ); in particular, Γ ≡|=∗ Δ, Rxv,,⊥u,,⊥x (≡xx ); СR≡) Rxv,,⊥u,,⊥x,,z⊥ (≡xz ) ∈ Δ; in particular, Rwv,,u⊥,,⊥x (≡xx ) ∈ Δ; СE≡L) ≡xy∈Γ, Ex∈Γ and Ey∈Δ;
СE≡R) ≡xy∈Δ, Ex∈Δ and Ey∈Δ. 4. Sequent calculi for L⊥Q= and L⊥Q≡
Let us construct calculi of sequent type which formalize logical consequence relations for sets of
formulas for L⊥Q= and L⊥Q≡. We will obtain the calculus С⊥Q=IR for the relation P=|=IR in L⊥Q=, and calculi
С⊥Q≡TFR, С⊥Q≡TF, С⊥Q≡T, С⊥Q≡F, С⊥Q≡IR for the relations R≡|=TF, P≡|=TF, P≡|=T, P≡|=F, P≡|=IR. These caluculi extend
the calculi for P|=IR, P|=T, P|=F, P|=TF, R|=TF in L⊥Q [
Sequent calculus is defined by basic sequent forms and closure conditions for sequents.
Closed sequents are axioms of the sequent calculus. The closedness of |–Γ–|Δ must guarantee Γ |= Δ.
Rules of sequent calculus are called sequent forms. They are syntactical analogues of the semantic properties of the corresponding logical consequence relations. 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 tree is closed if every its leaf is a closed sequent. A sequent Σ is derivable if there exists a closed sequent tree with the root Σ, called a derivation of the sequent Σ.
For a set of signed formulas Σ = |–Γ–|Δ let us introduce sets of defined and undefined names (valvariables and unv-variables): val(|–Γ–|Δ) = {x∈V | Ex∈Γ}; unv(|–Γ–|Δ) = {x∈V | Ex∈Δ}.
Also we specify a set of undistributed names for Σ: ud(Σ) = nm(Σ) \ (val(Σ) ∪ unv(Σ)).
Closure conditions for a sequent |–Γ–|Δ correspond to conditions that guarantee a certain logical consequence relation. Thus,we get the following closure conditions for a sequent |–Γ–|Δ.
For the calculus С Q=IR: condition C ∨ CF ∨ СRf= ∨ С⊥L ∨ , С⊥R ∨ СE=L ∨ СE=R .
⊥ For the calculus С⊥Q≡IR: condition C ∨ CF ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R .
For the calculus С⊥Q≡T: condition C ∨ CF ∨ CL ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R .
For the calculus С⊥Q≡F: condition C ∨ CF ∨ CR ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R .
For the calculus С⊥Q≡TF: condition C ∨ CF ∨ CLR ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R .
For the calculus С⊥Q≡TFR: condition C ∨ CF ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R .
Basic sequent forms. Basic sequent forms for the calculi С⊥Q≡TFR, С⊥Q≡TF, С⊥Q≡T, С⊥Q≡F are the same,
the difference lies in closure conditions. The rules consist of basic forms for the calculus С⊥QTFR [
Basic sequent forms for the calculi С⊥Q≡IR and С Q=IR consist of basic forms for the calculus
С⊥QIR [
For the calculi С⊥Q≡TFR, С⊥Q≡TF, С⊥Q≡T, С⊥Q≡F, their basic sequent forms can be split into the following groups.
Auxiliary simplification forms, inherited from the calculi for L⊥Q: |–R |–R⊥I |− Rxv,,⊥u (Φ),Σ |− Rzz,,xv,,⊥u (Φ),Σ ; –|R⊥I −| Rxv,,⊥u (Φ),Σ
−| Rzz,,xv,,⊥u (Φ),Σ |–R⊥U |− Rxv,,⊥u (Φ),Σ ; –|R⊥U −| Rxv,,⊥u (Φ),Σ ; ; −| Rzy,,xv,,⊥u (Φ),Σ |− Rzy,,xv,,⊥u (Φ),Σ |–R#1 |− Rxv,,⊥u,,⊥y ( p), −| Ez,Σ
|− Rxv,,⊥u,,zy ( p), −| Ez,Σ |–¬R#1 |− ¬Rxv,,⊥u,,⊥y ( p), −| Ez,Σ
|− ¬Rxv,,⊥u,,zy ( p), −| Ez,Σ |–R#2 |− Rxv,,⊥u ( p), −| Ez,Σ
|− Rxv,,⊥u,,⊥z ( p), −| Ez,Σ |–¬R#2 |− ¬Rxv,,⊥u ( p), −| Ez,Σ |− ¬Rxv,,⊥u,,⊥z ( p), −| Ez,Σ ; ; ; ; |–¬R
|− ¬Φ,Σ |− ¬R(Φ),Σ ; –|¬R
−| ¬Φ,Σ −| ¬R(Φ),Σ
; |–¬R⊥I |− ¬Rxv,,⊥u (Φ),Σ |− ¬Rzz,,xv,,⊥u (Φ),Σ –|¬R⊥I −|¬Rxv,,⊥u (Φ),Σ
−|¬Rzz,,xv,,⊥u (Φ),Σ |–¬R⊥U |− ¬Rxv,,⊥u (Φ),Σ ; –|¬R⊥U −|¬Rxv,,⊥u (Φ),Σ ; ; −|¬Rzy,,xv,,⊥u (Φ),Σ |− ¬Rzy,,xv,,⊥u (Φ),Σ –|R#1 −| Rxv,,⊥u,,⊥y ( p), −| Ez,Σ
−| Rxv,,⊥u,,zy ( p), −| Ez,Σ –|¬R#1 −|¬Rxv,,⊥u,,⊥y ( p), −| Ez,Σ
; −|¬Rxv,,⊥u,,zy ( p), −| Ez,Σ –|R#2 −| Rxv,,⊥u ( p), −| Ez,Σ
−| Rxv,,⊥u,,⊥z ( p), −| Ez,Σ –|¬R#2 −|¬Rxv,,⊥u ( p), −| Ez,Σ
. −|¬Rxv,,⊥u,,⊥z ( p), −| Ez,Σ ; ;
Condition for the forms of the type R⊥U: у∈ν(Φ); condition for the forms of the types R#1 and R#2: p∈Ps.
Forms of elimination of ¬ and renomination of predicates-indicators, inherited from the calculus С QTFR: ⊥ |–¬E |–R⊥E |–R⊥EV −| Ez,Σ |− ¬Ez,Σ
; |− Ez,Σ |− Rxv,,⊥u (Ez),Σ
|− Ey,Σ |− Rxv,,⊥u,,zy (Ez), Σ ; –|¬E , z ∉{v ,u}; |− Ez,Σ −| ¬Ez,Σ
; |–R⊥R |− Ryv,,⊥z oux,,t⊥ (Φ),Σ |− Ryv,,⊥z (Rxu,,⊥t (Φ)),Σ
; |–¬R⊥R |− ¬Ryv,,⊥z oux,,t⊥ (Φ),Σ |− ¬Ryv,,⊥z (Rxu,,⊥t (Φ)),Σ
; |–R⊥¬ |− ¬Rxv,,⊥u (Φ),Σ |− Rxv,,⊥u (¬Φ),Σ
; |–¬R⊥¬
|− Rxv,,⊥u (Φ),Σ |− ¬Rxv,,⊥u (¬Φ),Σ
; |–R⊥∨ |− Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ),Σ
; |− Rxv,,⊥u (Φ ∨ Ψ),Σ Forms of equivalent transformations, inherited from the calculi for L⊥Q:
–|R⊥E –|R⊥EV
−| Ey,Σ −| Rxv,,⊥u,,zy (Ez), Σ
. |− ¬Rxv,,⊥u (Ez),Σ −| Ez,Σ −| Rxv,,⊥u (Ez),Σ
, z ∉{v ,u}; |–¬RE −| Rxv,,⊥u (Ez),Σ ; –|¬RE |− Rxv,,⊥u (Ez),Σ
; −| ¬Rxv,,⊥u (Ez),Σ –|R⊥R −| Ryv,,⊥z oux,,t⊥ (Φ),Σ
; −| Rxv (Ryw (Φ)),Σ –|¬R⊥R −|¬Ryv,,⊥z oux,,t⊥ (Φ),Σ −|¬Ryv,,⊥z (Rxu,,⊥t (Φ)),Σ
; –|R⊥¬ −|¬Rxv,,⊥u (Φ),Σ
; −| Rxv,,⊥u (¬Φ),Σ –|¬R⊥¬
−| Rxv,,⊥u (Φ),Σ −|¬Rxv,,⊥u (¬Φ),Σ
; –|R⊥∨ −| Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ),Σ
; −| Rxv,,⊥u (Φ ∨ Ψ),Σ |–¬R⊥∨ |− ¬(Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ)),Σ
; |− ¬Rxv,,⊥u (Φ ∨ Ψ), Σ –|¬R⊥∨ −| ¬(Rxv,,⊥u (Φ) ∨ Rxv,,⊥u (Ψ)),Σ
Decomposition forms, inherited from the calculi for L⊥Q: |−¬¬
Forms of quantifier elimination, E-distribution and primary definition, inherited from the calculi for L⊥Q:
Simplification forms – renominations of equality:
|− ¬Rwv,,⊥u (∃xΦ), |− Ey,Σ |–¬∃R⊥v |− ¬Rwv,,u⊥ (∃xΦ), |− ¬Rwv,,⊥u,,xy (Φ), |− Ey,Σ ; –|∃R⊥v −| Rwv,,u⊥ (∃xΦ), −| Rwv,,⊥u,,xy (Φ), |− Ey,Σ ; Ed |− Ex,Σ −|Ex,Σ Σ ;
Ev |− Ez, Σ Σ 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 (Σ, Rwv,,u⊥ (∃xΦ)); condition for ∃F-form: Ey does not belong to Σ.
–|¬≡ |− ≡xy , Σ −| ¬ ≡xy , Σ
; Specific form of transitivity of ≡xy for the calculi L⊥Q≡: Tr≡ |− ≡xy , |− ≡yz , |− ≡xz , Σ .
Forms of ¬ elimination for equality and renomination of equality: |− ≡xy , |− ≡yz , Σ |–¬R≡ −| Rwv,,⊥u (≡xy ), Σ |− ¬Rwv,,u⊥ (≡xy ), Σ ; –|¬R≡ Auxiliary simplification forms – elimination of a pair of equals in renominations: |−∃ |− Rzx (Φ), |− Ez, Σ
; |− ∃xΦ, Σ |–∃R⊥ |− Rwv,,u⊥,,xz (Φ), |− Ez,Σ
; |− Rwv,,⊥u (∃xΦ), Σ |−¬∃v |− ¬∃xΦ, |− Ey, |− ¬Ryx (Φ), Σ
; |− ¬∃xΦ, |− Ey, Σ |–¬≡
−| ≡xy , Σ |− ¬ ≡xy , Σ
; |− Rwv,,⊥u (≡xy ), Σ −| ¬Rwv,,u⊥ (≡xy ), Σ
.. |–≡elR |− ≡xy , |− Rwv,,⊥u (Φ), Σ |− ≡xy , |− Rwv,,⊥u,,xy (Φ), Σ
; |–≡el¬R |− ≡xy , |− ¬Rwv,,⊥u (Φ), Σ
; |− ≡xy , |− ¬Rwv,,⊥u,,xy (Φ), Σ |–R⊥≡xx |–R⊥≡0 |–R⊥≡2 |–R⊥≡2E
|− ≡xz , Σ |− Rwv,,u⊥,,xz (≡xx ), Σ
|− ≡xy , Σ |− Rwv,,u⊥ (≡xy ), Σ
; |− ≡zs , Σ |− Rwv,,u⊥,,xz,,sy (≡xy ), Σ ; ; |− ¬Ez, Σ |− Rwv,,u⊥,,xz,,⊥y (≡xy ), Σ ; −|¬∃ −| ¬Rzx (Φ), |− Ez, Σ
; −| ¬∃xΦ, Σ –|¬∃R⊥ −|∃v −| ¬Rwv,,u⊥,,xz (Φ), |− Ez,Σ
−| ¬Rwv,,u⊥ (∃xΦ),Σ −| ∃xΦ, |− Ey, −| Ryx (Φ), Σ −| ∃xΦ, |− Ey, Σ ;
; −| Rwv,,u⊥ (∃xΦ), |− Ey,Σ given z∈fu(Σ). –|≡elR |− ≡xy , −| Rwv,,⊥u (Φ), Σ |− ≡xy , −| Rwv,,⊥u,,xy (Φ), Σ
; –|≡el¬R |− ≡xy , −| ¬Rwv,,⊥u (Φ), Σ
.
|− ≡xy , −| ¬Rwv,,⊥u,,xy (Φ), Σ –|R⊥≡xx –|R⊥≡0 –|R⊥≡2 –|R⊥≡2E
−| ≡xz , Σ −| Rwv,,u⊥,,xz (≡xx ), Σ
−| ≡xy , Σ −| Rwv,,u⊥ (≡xy ), Σ
; −| ≡zs , Σ −| Rwv,,u⊥,,xz,,sy (≡xy ), Σ ; ; −| ¬Ez, Σ −| Rwv,,u⊥,,xz,,⊥y (≡xy ), Σ ; |–R⊥≡1 |–R⊥≡1E
|− ≡zy , Σ |− Rwv,,u⊥,,xz (≡xy ), Σ
|− ¬Ey, Σ |− Rwv,,u⊥,,x⊥ (≡xy ), Σ ; ; –|R⊥≡1 –|R⊥≡1E
−| ≡zy , Σ −| Rwv,,u⊥,,xz (≡xy ), Σ
−| ¬Ey, Σ −| Rwv,,u⊥,,x⊥ (≡xy ), Σ ; ; Conditions for |–R⊥≡1, –|R⊥≡1, |–R⊥≡1E, –|R⊥≡1E: y ∉{u,v} and x ≠ y.
Conditions for |–R⊥≡0, –|R⊥≡0: x, y ∉{u,v}.
Special forms of substitution of equals (condition: p∈Ps): |–≡R⊥r |− ≡xy , |− Rwv,,⊥u,,zx ( p), |− Rwv,,u⊥,,zy ( p), Σ ; −|≡R⊥r |− ≡xy , −| Rwv,,⊥u,,zx ( p), −| Rwv,,⊥u,,zy ( p), Σ ; |− ≡xy , |− Rwv,,⊥u,,zx ( p), Σ
|− ≡xy , −| Rwv,,⊥u,,zx ( p), Σ |–≡¬R⊥r |− ≡xy , |− ¬Rwv,,⊥u,,zx ( p), |− ¬Rwv,,⊥u,,zy ( p), Σ ; −|≡¬R⊥r |− ≡xy , −| ¬Rwv,,u⊥,,zx ( p), −| ¬Rwv,,u⊥,,zy ( p),Σ . |− ≡xy , |− ¬Rwv,,⊥u,,zx ( p), Σ |− ≡xy , −| ¬Rwv,,u⊥,,zx ( p),Σ
Note that forms of the type R, RІ, RU, R#, ≡elR are auxiliary: they should be used every time the corresponding situation occurs.
Basic sequent forms for the calculus С⊥Q≡IR consist of the specified above forms except the forms with negation of external renomination and the forms of the types ¬E, ¬RE, ¬≡, ¬R≡, and with addition of the following rules: |−¬
Basic sequent forms for the calculus С⊥Q=IR consist of the basic forms for the calculus С QIR (i.e. ⊥ forms |–R, –|R, |–R⊥I, –|R⊥I, |–R⊥U, –|R⊥U, |–R#1, –|R#1, |–R#2, –|R#2, |–R⊥E, –|R⊥E, |–R⊥EV, –|R⊥EV, |–R⊥R, –|R⊥R, |–R⊥¬, –|R⊥¬, |–R⊥∨, –|R⊥∨, |–¬, –|¬, |−∨, −|∨, |−∃, |–∃R⊥, −|∃v, –|∃R⊥v, Ed, Ev), with addition of the forms connected with predicates =xy .
Specific form of transitivity of =xy for the calculus С⊥Q=IR: Tr= |− =xy , |− =yz , |− =xz , Σ . |− =xy , |− =yz , Σ Simplification forms – renominations of the weak equality: |–R⊥=x |–R⊥=0 |–R⊥=2 |–R⊥=1
|− =xz , Σ |− Rwv,,u⊥,,xz (=xx ), Σ
|− =xy , Σ |− Rwv,,u⊥ (=xy ), Σ
; |− =zs , Σ |− Rwv,,u⊥,,xz,,sy (=xy ), Σ
|− =zy , Σ |− Rwv,,u⊥,,xz (=xy ), Σ ; ;
; |–=elR |− =xy , |− Rwv,,⊥u (Φ), Σ |− =xy , |− Rwv,,⊥u,,xy (Φ), Σ ; –|R⊥=xx –|R⊥=0 –|R⊥=2 –|R⊥=1
−| =xz , Σ −| Rwv,,u⊥,,xz (=xx ), Σ
−| =xy , Σ −| Rwv,,u⊥ (=xy ), Σ
; −| =zs , Σ −| Rwv,,u⊥,,xz,,sy (=xy ), Σ
−| =zy , Σ −| Rwv,,⊥u,,xz (=xy ), Σ –|=elR |− =xy , −| Rwv,,⊥u (Φ), Σ |− =xy , −| Rwv,,⊥u,,xy (Φ), Σ .
Condition for |–R⊥=1, –|R⊥=1: y ∉{u,v} and x ≠ y; condition for |–R⊥=0, –|R⊥=0: x, y ∉{u,v}.
Auxiliary simplification forms – elimination of a pair of equals in renominations: Special forms of substitution of equals (condition: p∈Ps): |–=R⊥r |− =xy , |− Rwv,,⊥u,,zx ( p), |− Rwv,,u⊥,,zy ( p), Σ
; |− =xy , |− Rwv,,⊥u,,zx ( p), Σ −|=R⊥r |− =xy , −| Rwv,,u⊥,,zx ( p), −| Rwv,,u⊥,,zy ( p), Σ
. |− =xy , −| Rwv,,u⊥,,zx ( p), Σ
For each of the specified sequent calculi, properties of the corresponding logical consequence relations for sets of formulas induce the main property of basic sequent forms:
Theorem 1.
be a basic sequent form. Then: a) Λ |=∗ Κ ⇔ Γ |=∗ Δ; b) Γ |≠∗ Δ ⇔ Λ |≠∗ Κ. 2. Let |− Λ−|Κ |−Χ−|Ζ |− Γ−|Δ
be a basic sequent form. Then: a) Λ |=∗ Κ та Χ |=∗ Ζ ⇔ Γ |=∗ Δ; b) Λ |≠∗ Κ or Χ |≠∗ Ζ ⇔ Γ |≠∗ Δ.
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.
Let us describe all stages of the procedure for a given finite sequent Σ, for the calculus С⊥Q≡TFR. For the other calculi the process is similar.
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
Edform (more details in [
Let us describe derivation of an unclosed sequent leaf η; this implies building a finite subtree with the 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 of the types R, R⊥I, R⊥U, R#, ≡ elR are used for simplifications.
Forms of the type 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 unvvariables of formulas in sequents in the path from root to the current sequent.
Forms of the type ≡ R⊥r (substitution of equals) are applied every time the following pair of formulas appears: one of the type |–x ≡ y, another – of the type either |− Rwv,,⊥u,,zx ( p), −| Rwv,,u⊥,,zx ( p), |−¬Rwv,,u⊥,,zx ( p), or −|¬Rwv,,⊥u,,zx ( p), note that at least one the pair should be new for the sequent. Forms of the type Tr≡ are applied every time the pair of formulas |–≡xy and |–≡yz appears, and at least one of them is new for the sequent.
During each stage, ∃T-forms are applied before ∃F-forms. With each application of ∃T, a new (absent in the path from root to the current sequent) z∈VT is taken. Each ∃F-form should be used repeatedly for each defined у of formulas in the path from Σ 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. The obtained sequent should be checked for closedness after applying a form. 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 for a finite sequent, the following cases are possible: 1) the construction procedure is completed positively; we obtained a finite closed tree; 2) the 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) the construction procedure is not completed; we obtained an infinite unclosed tree. König's
lemma [
During 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; forms
can be applied only to these formulas. More on the procedure can be found in [
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) the construction procedure is completed positively; we obtained a finite closed tree; 2) the construction 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.
For all the introduced calculi the soundness theorem holds, with the same formulation and style of proof. The calculi С⊥Q≡TFR, С⊥Q≡TF, С⊥Q≡T, С⊥Q≡F, С⊥Q≡IR, С Q=IR correspond to the respective logical ⊥ consequence relations R≡|=TF, P≡|=TF, P≡|=T, P≡|=F, P≡|=IR, P=|=IR.
Theorem 2 (soundness). Let the sequent |–Γ–|Δ be derivable in the calculus C#, then Γ |=∗ Δ.
If |–Γ–|Δ is derivable in the calculus C#, then a finite closed tree was constructed for this sequent. For any node of the tree |–Λ–|Κ we have Λ |=∗ Κ. For leaves it is implied from the notion of a closed sequent; by Theorem 1, sequent forms preserve logical consequence relation bottom up. Hence, for the root |–Γ–|Δ we also have Γ |=∗ Δ.
The counter-model existence theorems. The completeness of sequent calculi is 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 the method of Hintikka (model) sets is used. The proof of the
countermodel theorems below is similar to the proof of the corresponding theorems for PCNL [
Theorem 3. Let ℘ be an unclosed path in the derivation tree constructed for |–Γ–|Δ, 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: НT) |–Φ∈Н ⇒ δ∈T(ΦA) and –|Φ∈Н ⇒ δ∉T(ΦA); НF) |–Φ∈Н ⇒ δ∉F(ΦB) and –|Φ∈Н ⇒ δ∈F(ΦB).
We will call (A, δ) and (B, δ) T≡-counter-model and F≡-counter-model for |–Γ–|Δ respectively.
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∈Н}; we will consider W as the set of defined names of the set Н.
We continuously apply forms to sequents of the path ℘ while we can: eventually, every nonprimitive formula of the path ℘ (or its negation) will be decomposed or simplified.
All the sequents of the path ℘ are unclosed, therefore the closure condition C ∨ CF ∨ СRf≡ ∨ СR≡ ∨ СE≡L ∨ СE≡R does not hold. Therefore, 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; НСRf≡ ) there is no name x∈V such that –| ≡ xx ∈ Н; НCR≡) there is no formula Rxv,,⊥u,,⊥x,,z⊥ (≡xz ) such that −| Rxv,,⊥u,,⊥x,,z⊥ (≡xz ) ∈ H; НCE≡L) there are no formulas ≡ xy, Ex, Ey such that |– ≡ xy ∈ Н, |–Ex ∈ Н, –|Ey ∈ Н; НСE≡R) there are no formulas ≡ xy, Ex, Ey such that |– ≡ xy ∈ Н, –|Ex ∈ Н, –|Ey ∈ Н.
We can move bottom up from a lower to a higher node of the path ℘ after applying a certain sequent form, therefore the corresponding conditions for transition for Н should hold, in particular: НTr≡ ) |– ≡xy ∈Н and |– ≡yz ∈Н ⇒ |– ≡xz ∈Н; Н≡ R⊥r) |− ≡xy∈ H, |− Rwv,,u⊥,,zx ( p) ∈ H ⇒ |− ≡xy∈ H, |− Rwv,,u⊥,,zx ( p) ∈ H, |− Rwv,,u⊥,,zy ( p) ∈ H;
|− ≡xy∈ H, −| Rwv,,u⊥,,zx ( p) ∈ H ⇒ |− ≡xy∈ H, −| Rwv,,u⊥,,zx ( p) ∈ H, −| Rwv,,u⊥,,zy ( p) ∈ H; Н¬≡ R⊥r) |− ≡xy∈ H, |− ¬Rwv,,u⊥,,zx ( p) ∈ H ⇒ |− ≡xy∈ H , |− ¬Rwv,,u⊥,,zx ( p) ∈ H , |− ¬Rwv,,u⊥,,zy ( p) ∈ H; |− ≡xy∈ H, −| ¬Rwv,,⊥u,,zx ( p) ∈ H ⇒ |− ≡xy∈ H , −| ¬Rwv,,u⊥,,zx ( p) ∈ H , −| ¬Rwv,,u⊥,,zy ( p) ∈ H.
Let us call a set of signed formulas Н for which the conditions above apply, an RTF≡-model set. Let us obtain a counter-model using the RTF≡-model set Н.
Equality predicates induce on the set W an equivalence relation: x ∼ y ⇔ |– ≡ xy ∈Н.
Let S = W ~ be a quotient set on the set W corresponding to ~. We denote an equivalence class with the representive v as 〈v〉. Let us δ = [v!〈v〉 | v∈W ]; such δ is a surjection W Æ S.
For predicates-indicators and equalities in the interpretations A and B we have: – |–Ex ∈ Н gives x∈W, hence Ex А (δ) = T and Ex B (δ) = T ⇒ δ∈T(Ex А) and δ∉F(Ex B); – –|Ex ∈ Н gives x∉W, hence δ(x)#, therefore Ex А (δ) = Ex B (δ) = F ⇒ δ∉T(Ex А) and δ∈F(Ex B); – if |– ≡ xy ∈Н, then x ∼ y, hence by construction δ ≡ xy А (δ) = T and ≡ xy B (δ) = T ⇒ δ∈T(≡ xy А) and δ∉F(≡ xy B);
– if –| ≡ xy ∈Н, then x ∼ y is incorrect, hence by construction δ ≡ xy А (δ) = F and ≡ xy B (δ) = T ⇒ δ∈F(≡ xy A) and δ∉T(≡ xy B).
Let us specify values of the predicates represented by predicate symbols and their negations and by primitive Un-formulas and their negations on δ in the interpretations A and B as follows: – |– р∈Н ⇒ δ∈T(рA) and δ∉F(рB); –| р∈Н ⇒ δ∉T(рA) and δ∈F(рB); – |–¬р∈Н ⇒δ∈T(¬pA) and δ∉F(¬pB); –|¬p∈Н ⇒ δ∉T(¬pA) and δ∈F(¬pB); – |− Rxv,,⊥u ( p) ∈ H ⇒ rvx,,u⊥ (δ) ∈T ( pA ) and rvx,,u⊥ (δ) ∉ F( pB ), namely δ ∈T (Rxv,,⊥u ( p)A ) and δ ∉ F(Rxv,,⊥u ( p)B ); – |− Rxv,,⊥u ( p) ∈ H ⇒ rvx,,u⊥ (δ) ∉T ( pA ) and rvx,,u⊥ (δ) ∈ F( pB ), namely δ ∉T (Rxv,,⊥u ( p)A ) and δ ∈ F(Rxv,,⊥u ( p)B ); – |−¬Rxv,,⊥u ( p) ∈ H ⇒ rvx,,u⊥ (δ) ∈T (¬pA ) and rvx,,u⊥ (δ) ∉ F(¬pB ), namely δ ∈T (¬Rxv,,⊥u ( p)A ) and δ ∉ F(¬Rxv,,⊥u ( p)B ); – |−¬Rxv,,⊥u ( p) ∈ H ⇒ rvx,,u⊥ (δ) ∉T (¬pA ) and rvx,,u⊥ (δ) ∈ F(¬pB ), namely δ ∉T (¬Rxv,,⊥u ( p)A ) and δ ∈ F(¬Rxv,,⊥u ( p)B ).
For atomic formulas, primitive Un-formulas and their negations, the statements of the theorem hold basing on the defined above values of the corresponding predicates. For clauses, induced by forms Tr≡ and forms of the type ≡ R⊥r, the statements of the theorem hold basing on the definitions of values of equality predicates and values of basic predicates and their negations. Other clauses connected with Ez and equality predicates are proved likewise.
The rest of clauses can be proved by induction on the formula structure according to the definition of Н.
The counter-model existence theorems for the calculi C⊥Q≡T, C⊥Q≡F, С⊥Q≡TF, C⊥Q≡IR, C⊥Q≡IR can be formulated and proved in the same manner. Below, we will provide the theorems for the calculi С⊥Q≡TF and C⊥Q≡IR.
Theorem 4. Let ℘ be an unclosed path in the sequent tree constructed in С⊥Q≡TF for |–Γ–|Δ, let Н be the set of all specified formulas of the path ℘. Then there exist interpretations A = (S, IA), B = (S, IB) and data δ∈VS such that: НTS) |–Φ∈Н ⇒ ΦA(δ) = T and –|Φ∈Н ⇒ ΦA(δ) ≠ T; НFS) |–Φ∈Н ⇒ ΦB(δ) ≠ F and –|Φ∈Н ⇒ ΦB(δ) = F.
The pairs (A, δ) and (B, δ) are called T P≡-counter-model and F P≡-counter-model for |–Γ–|Δ respectively.
In the formulations of the counter-model theorems, for the calculus C⊥Q≡T only the interpretation A = (S, IA) and clause НTS remain, while for the calculus C⊥Q≡T only the interpretation B = (S, IB) and clause НFS remain.
Theorem 5. Let ℘be an unclosed path in the sequent tree constructed in C⊥Q≡IR for |–Γ–|Δ, let Н be the set of all specified formulas of the path ℘. Then there exist an interpretation A = (S, I) and data δ∈VS such that:
НС) |–Φ∈Н ⇒ ΦA(δ) = T and –|Φ∈Н ⇒ ΦA(δ) = F.
The pair (A, δ) is called IR≡ -counter-model for the sequent |–Γ–|Δ .
For the calculus C⊥Q=IR, the formulation of the counter-model existence theorem matches with the Theorem 5.
The completeness theorem. The theorems of the existence of a counter-model allow us to obtain the corresponding completeness theorems with the same formulation for all of the introduced here calculi.
Theorem 6 (completeness). Let Γ |=∗ Δ, then the sequent |–Γ–|Δ is derivable in the calculus C#.
Let us show the proof for the relation R≡|=TF and calculus C⊥Q≡TFR (for more similar proofs see
[
Assume that Γ R≡|=TF Δ, but the sequent |–Γ–|Δ is not derivable. In this case the sequent tree for |–Γ– |Δ is not closed, thus, an unclosed path ℘ exists in this tree. Let Н be the set of all signed formulas of this path. By the Theorem 3, there exist a T≡-counter-model (A, δ) and an F≡-counter-model (B, δ) such that:
|–Φ∈Н ⇒ δ∈T(ΦA) and –|Φ∈Н ⇒ δ∉T(ΦA); |–Φ∈Н ⇒ δ∉F(ΦB) and –|Φ∈Н ⇒ δ∈F(ΦB).
For T≡-counter-model, 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≡|=TF Δ.
For F≡-counter-model, by |–Γ–|Δ ⊆ Н for all Φ∈Γ we have δ∉F(ΦB), for all Ψ∈Δ we have δ∈F(ΨB). Whence δ∉F(ΓB) and δ∈F(ΔB), therefore F(ΔB) ⊆ F(ΓB) does not hold. This contradicts to Γ B|=F Δ, so it contradicts to Γ R≡|=TF Δ.
We study new classes of software-oriented logical formalisms – pure first-order logics of partial quasiary predicates with extended renominations and predicates of strong equality and of weak equality, denoted respectively L⊥Q≡ and L⊥Q=. For the considered logics, main properties of their compositions are given, and their languages are described. We define various variants of logical consequence relations and describe their properties, paying special attention to those connected with equality predicates. For the introduced logical consequence relations we construct calculi of sequent type. We specify basic sequent forms for the presented calculi and conditions for sequent closedness, and describe the derivation procedure via a sequent tree. The counter-model existence theorems are considered; an example illustrating a counter-model construction by an unclosed path in the sequent tree is provided. For the studied calculi, the soundness and completeness theorems are proved; the proof of the completeness theorems is based on a construction of the respective counter-models. In the future we plan to investigate extending the logic L⊥Q≡ with the composition of predicate complement.