Program-Oriented Logics of Renominative Level with Extended Renomination and Equality

Abstract

The formalism of program logics is the main instrument for software verification. Such logics are based on formal program models and reflect main program properties. Among various program logics, Floyd-Hoare logic and its variants take a special place because of its naturalness and simplicity. But such logics are oriented on total pre- and post-conditions, and in the case of partial conditions they become unsound. Different methods to overcome this problem were proposed in our previous works. One of the methods involves extension of program algebras with the composition of predicate complement. This permits to modify rules of the logic making them sound. Such modification requires introduction of undefinedness conditions into logic rules. To work with such conditions, an underlying predicate logic should become more expressive. In this paper we continue our research of such logics. We investigate a special program-oriented predicate logic called logic of renominative (quantifier-free) level with the composition of predicate complement, extended renomination, and equality predicate. This logic is a constituent part of the program logic. We introduce a special consequence relation for this logic, construct a sequent calculus, and prove its soundness and completeness.

1 Introduction

The formalism of program logics is the main instrument for software verification [1]. To be effective, such logics should reflect main program properties. Therefore, adequate formal program models should be constructed which will form a base for a program logic. Among such logics we should point to Floyd-Hoare logic and its variants as quite natural and simple [2,3,4]. But such logics are oriented on total pre- and post-conditions, and in the case of partial conditions (predicates) they become unsound.

In our previous works [5,6,7] we considered several methods to extend Floyd-Hoare logic for partial predicates, in particular, we proposed such methods: (1) introduction of special rule constraints; (2) restriction of the class of program assertions (of Hoare triples), and (3) extending program logics with the composition of predicate complement. All methods make a logic sound but the first two are difficult for practical usage or are rather restrictive. Here we concentrate on the third method. Introduction of the complement composition permits to modify rules of Floyd-Hoare logic in such a way that they become sound, but a negative side of this proposal is that logic becomes more complicated because undefinedness conditions for predicates should be taken into account. To work with such conditions, an underlying predicate logic should become more expressive. We add to this logic equality predicates and extended renominations that permit processing of undefined variables.

In this paper we continue our research of program-oriented logics of partial quasiary predicates [8,9,10,11,12]. We focus on a logic L $^{R \equiv }$ of renominative (quantifier-free) level with the predicate complement, extended renomination, and equality predicate. We construct a special predicate algebra and study its properties. Then we define a consequence relation with undefinedness conditions and investigate its properties. At last, we construct a sequent calculus for this logic and prove its soundness and completeness.

2 Program Algebras with Predicate Complement, Extended Renomination, and Equality

According to the principles of composition-nominative approach [8, 13] we construct program logics based on program algebras. Such algebras are defined in the following way [9, 14]:

• (1) a set D of data processed by programs is defined;

• (2) the classes of partial predicates $Pr = D\mathop \to \limits^{p} Bool$ and partial functions $Fn = D\mathop \to \limits^{p} D$ are defined;

• (3) operations (compositions) over Pr and Fn are specified.

This scheme leads to two-sorted program algebras. In our previous works we considered program algebras with traditional compositions. Here we concentrate on a program algebra extended with the composition of predicate complement. This unary predicate composition is defined in the following way $\left( {p \in Pr,\;d \in D} \right)$:

$$ ({}^{ \sim }p)(d) = \left\{ {\begin{array}{*{20}c} {T,\;{\text{if}}\;p(d)\;{\text{is}}\;{\text{undefined}},} \\ {{\text{undefined,}}\;{\text{if }}\;p(d)\;{\text{is}}\;{\text{defined}} .} \\ \end{array} } \right. $$

Specifying D as the class $D_{CC} (V,A)$ of hierarchical nominative data [15, 16] with complex names and values built over the set of basic names V and the set of basic values A, we can define a complemented program algebra as a two-sorted algebra

$$ \begin{aligned} & CPAND_{CC} (V,A) = (Pr_{CC} (V,A),Fn_{CC} (V,A); \\ & AS^{u} ,id,IF,WH,S_{F}^{{\bar{u}}} ,S_{P}^{{\bar{u}}} , \Rightarrow v,v \Rightarrow_{a} , \vee ,\neg ,\exists x,{}^{ \sim }) \\ \end{aligned} $$

where $Pr_{CC} (V,A)$ and $Fn_{CC} (V,A)$ are classes of partial predicates and partial function over $D_{CC} (V,A)$ respectively; $AS^{u} ,\;id,\;IF,\;WH,\;S_{P}^{{\bar{u}}} ,\;S_{F}^{{\bar{u}}}$ are compositions of assignment, identity, conditional, cycle, superposition into predicate, superposition into function respectively; $\Rightarrow v$ and $v \Rightarrow_{a}$ are naming and denaming functions; $\vee ,\;\;\neg ,\;\;\;\exists x,\;{}^{ \sim }$ are composition of disjunction, negation, existential quantification, and predicate complement; $v,\;u,\;x \in V^{ + }$ are complex names, $\bar{u} \in \bar{U}$ is a sequence of complex names. This algebra is quite expressive to present formal semantics of rather complex programs.

A special program logic of Floyd-Hoare type based on such algebras is presented in [15]. Its distinctive feature is introduction of new rules which are sound for partial predicates and which use preconditions constructed with the help of the composition of predicate complement.

Obtained program logic can be an important instrument of program verification. So, its thorough investigation is required. This is a rather complicated challenge; therefore, we start with more simple logics. First, we identify a special predicate logic as a constituent part of the program logic. Such predicate logic can be considered as a logic defining constraints (program annotations). Second, we will consider here only logic $L^{ \, R \equiv }$ of renominative level which can be characterized as quantifier-free predicate logic of partial quasiary predicates with the composition of predicate complement, extended renomination, and equality. For simplicity, we call this logic extended logic of partial quasiary predicates of renominative level. The case of first-order logic with quantifiers and functions is planned to study in the forthcoming papers.

3 Extended Logic of Partial Quasiary Predicates of Renominative Level

To define a logic $L^{ \, R \equiv }$ we should define [9, 14]

• its class of algebras;

• its language (based on logic signature);

• its class of interpretations;

• its consequence relation;

• its inference relation based on some calculus.

Formal definitions will be given in the next subsections. We will use the following notations:

• $S\mathop \to \limits^{p} S^{{\prime }} \,(S\mathop \to \limits^{t} S^{{\prime }} )$ is the class of partial (total) mappings from $S$ to $S'$;

• $p(d){\downarrow} (p(d){\uparrow})$ means that p is defined (undefined) on d;

• $p(d){\downarrow} = T\,(p(d){\downarrow} = F)$ means that p is defined on d with value T (F). For this case we also use simpler notation p(d) = T (p(d) = F);

• p(d) = q(d) means that both p(d) and q(d) are simultaneously undefined or defined, and in this case their values are equal.

The terms and notations, not defined here, are treated in the sense of [11].

3.1 Extended Algebras of Partial Quasiary Predicates of Renominative Level

Let V be a set of names (variables) and A be a set of values. The class ^VA of nominative sets (partial assignments, partial data) is defined as the class of all partial mappings from V to A, thus, ${}^{V}A = V\mathop \to \limits^{p} A$.

Nominative sets represent states of program variables.

We use a special symbol ⊥∉V that denotes the absence of the variable value.

The main operation for nominative sets is parametric operation of extended renomination ${\text{r}}_{{ \, x_{1} , \ldots ,x_{n} , \bot , \ldots , \bot }}^{{v_{1} , \ldots v_{n} ,u_{1} , \ldots ,u_{m} }} :{}^{V}A{ \to }{}^{V}A$, where $v_{1} , \ldots ,v_{n} ,x_{1} , \ldots ,x_{n} ,u_{1} , \ldots ,u_{m}$ are names, and $v_{1} , \ldots ,v_{n} ,u_{1} , \ldots ,u_{m}$ are distinct, is defined by the following formula $(d \in {}^{V}A)$:

$$ {\text{r}}_{{ \, x_{1} , \ldots ,x_{n} , \bot , \ldots , \bot }}^{{v_{1} , \ldots ,v_{n} ,u_{1} , \ldots ,u_{m} }} (d) = d||_{{ - \{ v_{1} , \ldots ,v_{n} ,u_{1} , \ldots ,u_{m} \} }} \cup \;[v_{1} \mapsto d(x_{1} ), \ldots ,v_{n} \mapsto d(x_{n} )]. $$

Intuitively, given nominative set d this operation yields a new nominative set changing the values of $v_{1} , \ldots ,v_{n}$ to the values of $x_{1} , \ldots ,x_{n}$ respectively and making the variables $u_{1} , \ldots ,u_{m}$ to be undefined. We also use simpler notation for this renomination: ${\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}}$. We write $x \in \bar{v}$ to denote that x is a variable from $\bar{v}$; we write $\bar{v} \cup \bar{x}$ to denote the set of variables that occur in the sequences $\bar{v}$ and $\bar{x}$; names from V (maybe with indexes) are denoted x, y, z, v, u, t.

The order of names is not important, therefore ${\text{r}}_{ \, x,z, \bot }^{v,y,u} ,{\text{r}}_{ \, x, \bot ,z}^{v,u,y} ,{\text{r}}_{ \, \bot ,z,x}^{u,y.v}$ denote the same operation.

Traditional renomination ${\text{r}}_{{ \, \bar{x}}}^{{\bar{v}}}$ [9, 11] is a special case of extended renomination ${\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}}$.

Lemma 1.

The operation of extended renomination has the following properties (d, d₁, d₂ ∈ ^VA):

• it is monotone: $d_{1} \subseteq d_{2} \Rightarrow {\text{r}}_{{ \, \bar{y}, \bot }}^{{\bar{v},\bar{z}}} (d_{1} ) \subseteq {\text{r}}_{{ \, \bar{y}, \bot }}^{{\bar{v},\bar{z}}} (d_{2} )$;

• identical renomination can be eliminated: ${\text{r}}_{{ \, \bar{z},\bar{x}, \bot }}^{{\bar{z},\bar{v},\bar{u}}} (d) = {\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (d)$;

• if d(z)$\uparrow$ then ${\text{r}}_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (d) = {\text{r}}_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (d)$;

• successive renominations ${\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}}$ and ${\text{r}}_{{ \, \bar{y}, \bot }}^{{\bar{z},\bar{t}}}$ can be represented by one renomination denoted ${\text{r}}_{{ \, \bar{y}, \bot }}^{{\bar{z},\bar{t}}} \, \circ \,_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}}$ [9].

Proof

follows directly from definitions.

Let $Pr_{A}^{V} = \;^{V} A\mathop \to \limits^{p} Bool$ be the set of all partial predicates over ^VA. Such predicates are called partial quasiary predicates. For a predicate $p \in Pr_{A}^{V}$ its truth, falsity, and undefinedness domains are denoted T(p), F(p), and $\bot (p)$ respectively. Please note that these domains do not intersect pairwise and their union is equal to ^VA; thus, predicate p is defined by T(p) and F(p) only, because $\bot (p) = \;^{V} A\backslash (T(p) \cup F(p))$.

A predicate p is

• irrefutable (partially valid) if F(p) = ∅;

• satisfiable if T(p) ≠ ∅.

A name (variable) z is unessential for p if for any $d \in {}^{V}A$ the value of p does not depend on the value of z in d [9, 11].

Operations over $Pr_{A}^{V}$ are called compositions. Basic compositions of renominative level over quasiary predicates are disjunction ∨, negation ¬, predicate complement ${}^{ \sim }$, and extended renomination $R_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}}$.

These compositions are defined by the following formulas ($p,q \in Pr_{A}^{V}$):

• $T(p \vee q) = T(p) \cup T(q);F(p \vee q) = F(p) \cap F(q);$

• $T(\neg p) = F(p);F(\neg p) = T(p);$

• $T({}^{ \sim }p) \, = { \bot }(p) ; F({}^{ \sim }p) = \varnothing;$

• $T (R_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p)) = \{ d \in {}^{V}A\left| {{\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (d) \in T\left( p \right)\} ;F (R_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p))\{ d \in {}^{V}A} \right|{\text{r}}_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (d) \in F(p)\} .$

Please note that definitions of disjunction and negation are similar to strong Kleene’s connectives [17]. Properties of such compositions are described in [18].

Traditional renomination $R_{{\bar{x}}}^{{\bar{v}}}$ is a special case of extended renomination $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}}$.

To enrich expressivity of the logic we also add parametric variable assignment predicate Ex and parametric equality ≡_xy.

Variable assignment predicate Ex checks whether a variable x has a value in nominative data. It is defined by the following formulas:

$$ T(Ez) = \{ d|d(z){\downarrow} \} ;F(Ez) = \{ d|d(z){\uparrow}\} . $$

At last, we introduce parametric equality predicate ≡_xy by the following formulas:

$$ T({ \equiv }_{{\left\{ {x,y} \right\}}} ) = \{ d\left| {d\left( x \right){\downarrow} ,d\left( y \right){\downarrow} } \right.\,,\,d\left( x \right) = d\left( y \right)\} \cup \{ d\left| {d\left( x \right){\uparrow} } \right.\,{\text{and}}\,d\left( y \right){\uparrow} \} , $$

$$ F( \equiv_{{\left\{ {x,y} \right\}}} ) = \{ d|d\left( x \right){\downarrow} ,d\left( y \right){\downarrow} ,d\left( x \right) \ne d\left( y \right)\} \cup \{ d|d\left( x \right){\downarrow} ,d\left( y \right){\uparrow} \,\text{or}\,d\left( x \right){\uparrow} ,d\left( y \right){\downarrow} \} . $$

Please note that ≡_xy is strong equality.

A tuple

$$ {\mathcal{A}}^{R \equiv } \left( {V,A} \right) = < Pr_{A}^{V} ; \vee ,\neg ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ,{}^{ \sim },Ex, \equiv_{xy} > $$

is called an extended algebra of partial quasiary predicates of renominative level.

A class of such algebras (with different A) forms a semantic base for logic L $^{R \equiv }$.

Now we describe the main properties of ${\mathcal{A}}^{R \equiv } \left( {V,A} \right)$. We do not formulate traditional properties of propositional compositions of disjunction and negation [9, 11], but concentrate on properties of compositions of extended renomination and equality.

Lemma 2.

Extended renomination, variable assignment predicates, and equality have the following properties $(p,q \in Pr_{A}^{V},\,d \in^{V} A):$

• ${\text{R}})\;R(p) \, = p;$

• ${\text{R}}_{ \bot } {\text{I}})\;R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (p) = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p);$

• ${\text{R}}_{ \bot } {\text{U}})\;R_{{y,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (p) = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p)$ if z ∈ V is unessential for p;

• ${\text{R}}_{ \bot } \uparrow )R_{{\bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (p )(d) = R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (p )(d)$ if d(z)↑;

• ${\text{R}}_{{ \bot }} \neg )R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg p) = \neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p);$

• $R_{ \bot } \vee )\;R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p \vee q) = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (q);$

• ${\text{R}}_{ \bot } {\text{R}})R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (p)) = R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (p);$

• ${\text{R}}_{ \bot } {}^{ \sim })\;R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ({}^{ \sim }p) = {}^{ \sim }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (p);$

• ${\text{R}}_{ \bot } {\text{Ev}})\;R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez) = Ey;$

• ${\text{R}}_{ \bot } {\text{E}})\;R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) = Ez$ if $z \notin \bar{v} \cup \bar{u};$

• ${\text{R}} \equiv_{xx} )\;R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) =_{{}} \equiv_{xx} ;$

• $R_{ \bot } \equiv_{2} )R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) = \equiv_{zs} ;$

• $R_{ \bot } \equiv_{{2{\text{E}}}} )R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u}, \, x,y}} ( \equiv_{xy} ) = \neg Ez;$

• ${\text{R}}_{ \bot } \equiv_{1} )R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ) = \equiv_{zy} {\text{if}}\,y \notin \bar{u} \cup \bar{v}, \, x \ne y;$

• ${\text{R}}_{ \bot } \equiv_{{1{\text{E}}}} )R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u}, \, x}} ( \equiv_{xy} ) = \neg Ey\,{\text{if}}\,y \notin \bar{u} \cup \bar{v}, \, x \ne y;$

• ${\text{R}}_{ \bot } \equiv_{0} )R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ) = \equiv_{xy} \,{\text{if}}\,y \notin \bar{u} \cup \bar{v}, \, x \ne y;$

• $\equiv {\text{R}}_{ \bot } {\text{r}})R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (p)(d) = R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (p)(d)\,{\text{if}}\, \equiv_{xy} (d) = T.$

Proof

is trivial.

3.2 Language (Signature and Formulas) of L $^{R \equiv }$

Let Ps be a set of predicate symbols, V be an infinite set of names (variables). Usually, within V a subset V_U of unessential variables is identified [11]. A tuple

$$ \Sigma ^{R \equiv } = (V,V_{U} ; \vee ,\neg ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ,{}^{ \sim },Ex, \equiv_{xy} ;Ps) $$

is called the language signature.

For simplicity, we use the same notation for symbols of compositions and compositions themselves.

Given $\Sigma ^{R \equiv }$, we define inductively the language of $L^{ \, R \equiv }$ – the set of formulas denoted Fr $(\Sigma ^{R \equiv } )$ or simply Fr:

• if $P \in Ps$ then P ∈ Fr. Formulas of such forms are called atomic;

• if Φ, Ψ ∈ Fr then $\Phi \vee\Psi ,\neg\Phi ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}}\Phi ,$ ${}^{ \sim }\Phi ,\;Ex,\; \equiv_{xy} \in Fr$.

Formulas of the form $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (P)$ are called primitive $(P \in Ps)$.

3.3 L $^{R \equiv }$-Interpretations

Let ${\mathcal{A}}^{R \equiv } \left( {V,A} \right)\, = \, < Pr_{A}^{V} ; \vee ,\neg ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ,{}^{ \sim },Ex, \equiv_{xy} >$ be an extended algebra of a signature $\Sigma ^{R \equiv } = (V,V_{U} ; \vee ,\neg ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ,^{ \sim } ,Ex, \equiv_{xy} ;Ps)$; $I_{Q}^{Ps} = Ps\mathop \to \limits^{t} Pr_{A}^{V}$ be an interpretation mapping of predicate symbols. Then a tuple $J(\Sigma ^{R \equiv } ) = ({\mathcal{A}}^{R \equiv } \left( {V,A} \right),I_{Q}^{Ps} )$ is called an $L^{ \, R \equiv }$-interpretation.

We simplify notation for $L^{ \, R \equiv }$-interpretation $J(\Sigma ^{R \equiv } )$ omitting $L^{ \, R \equiv }$ and $\Sigma ^{R \equiv }$.

In interpretation J, algebra ${\mathcal{A}}^{R \equiv } \left( {V,A} \right)$ defines interpretations of composition symbols while $I_{Q}^{Ps}$ defines interpretations of predicate symbols.

For given interpretation J and formula Φ, we can define by induction on the structure of Φ its value in J. Obtained predicate is denoted Φ_J.

Formula Φ is irrefutable in J (denoted J |= Φ) if predicate Φ_J is irrefutable. Formula Φ is irrefutable (denoted |=Φ) if J |= Φ for any interpretation J. Irrefutability may be treated as partial validity.

Formula Φ is satisfiable in J (denoted J |∼Φ) if predicate Φ_J is satisfiable. Formula Φ is satisfiable (denoted |∼Φ) if J |∼Φ for some interpretation J.

Variable x is unessential for Φ if for any J variable x is unessential for Φ_J. Variable x is unessential for Γ ⊆ Fr if for any J variable x is unessential for any formula Φ ∈ Γ. The set of all variables (names) that occur in Φ is denoted nm(Φ).

The set fu(Φ) = V_U \ nm(Φ) is called the set of fresh unessential variables for Φ.

For any Γ ⊆ Fr we define $nm(\Gamma ) = \cup_{{\Phi \in\Gamma }} nm(\Phi )$ and $fu(\Phi ) = \cap_{{\Phi \in\Gamma }} fu(\Phi )$.

We generalize notation fu(Γ) on sequences of formulas and sets of formulas.

Lemma 3.

Let x ∈ V, Φ ∈ Fr, Γ ⊆ Fr. Then

• (1) x is unessential for Φ if x ∈ fu(Φ);

• (2) x is unessential for Γ if x ∈ fu(Γ).

Proof.

Induction on the structure of Φ.

3.4 Logical Consequence Relation Under Conditions of Undefinedness

Introduction of composition ${}^{ \sim }$ requires more complicated consequence relation because undefinedness domains should be taken into consideration. Here we use new consequence relation between sets of formulas denoted ${{\models}_{IR}}^{ \bot}$ [7] which generalizes irrefutability relation ${{\models}_{IR}}$ [9, 11].

Let Σ ⊆ Fr and J be an interpretation. We denote:

$$ \Sigma _{J} \,{\text{as}}\,\{\Phi _{J} |\;\Phi \in\Sigma \} ,\bigcap\limits_{{\Phi \in\Sigma }} {T(\Phi _{J} )} \,{\text{as}}\,T^{ \cap } (\Sigma _{J} ),\bigcap\limits_{{\Phi \in\Sigma }} {F(\Phi _{J} )} \,{\text{as}}\,F^{ \cap } (\Sigma _{J} ),\bigcap\limits_{{\Phi \in\Sigma }} { \bot (\Phi _{J} )} \,{\text{as}}\, \bot^{ \cap } (\Sigma _{J} ). $$

Set Σ can be empty. In this case

$$ T^{ \cap } (\Sigma ) = T^{ \cap } (\varnothing ) = F^{ \cap } (\Sigma ) = F^{ \cap } (\varnothing ) = \bot^{ \cap } (\Sigma ) = \bot^{ \cap } (\varnothing ) = {}^{V}A. $$

Let Γ, U, Δ ⊆ Fr. Then Δ is irrefutable consequence of Γ under undefinedness conditions U in interpretation J (denoted U/Γ _J ${{\models}_{IR}}^{ \bot}$ Δ ) if

$$ T^{ \cap } (\Gamma _{J} ) \cap \bot^{ \cap } ({\text{U}}_{J} ) \cap F^{ \cap } (\Delta_{J} ) = \varnothing . $$

In particular, for U = ∅ we obtain irrefutability consequence relation Γ _J${{\models}_{IR}}$ Δ.

Δ is logical irrefutable consequence of Γ under undefinedness conditions U (denoted U/Γ ${{\models}_{IR}}^{ \bot}$ Δ) if U/Γ _J ${{\models}_{IR}}^{ \bot}$ Δ for any interpretation J.

In particular, for U = ∅, we get traditional logical irrefutability relation Γ |=_IR Δ.

Let us now describe the main properties of the consequence relation ${{\models}_{IR}}^{ \bot}$ for propositional level.

By definition of ${{\models}_{IR}}^{ \bot}$, we obtain monotonicity:

M) Let Γ ⊆ Λ, U ⊆ W, and Δ ⊆ Σ; then U/Γ ${{\models}_{IR}}^{ \bot}$ Δ ⇒ W/Λ ${{\models}_{IR}}^{ \bot}$ Σ.

Let us introduce on Fr the binary relation ≃ of logical strong equality. Namely, Φ ≃ Ψ if Φ_J = Ψ_J for any interpretation J.

Theorem 1.

Let Φ ≃ Ψ. Then:

• ${\text{U/}}\Phi ,\Gamma {{\models}_{IR}}^{ \bot} \Delta \Leftrightarrow {\text{U}}/\,\Psi ,\Gamma \,{{\models}_{IR}}^{ \bot} \Delta ;$

• ${\text{U/}} \Gamma {{\models}_{IR}}^{ \bot} \Delta ,\Phi \Leftrightarrow {\text{U}}/\Gamma {{\models}_{IR}}^{ \bot} \Delta ,\Psi ;$

• ${\text{U,}}\Phi /\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U,}}\Psi /\Gamma {{\models}_{IR}}^{\bot} \Delta .$

Proof.

Proof is based on set-theoretical transformation of definitions of ${{\models}_{IR}}^{\bot}$ and ≃.

For ${{\models}_{IR}}^{\bot}$ the following properties of formula decomposition hold.

Theorem 2.

For any ${\text{U}},\Gamma ,\Delta \subseteq Fr,\Phi ,\Psi ,\upvartheta \in Fr:$

• $\vee_{\text{L}} ){\text{U/}}\Phi \vee\Psi ,\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U}}/\Phi ,\Gamma {{\models}_{IR}}^{\bot} \Delta \,{\text{and}}\,{\text{U}}/\Psi ,\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $\vee_{\text{R}} ) {\text{U/}}\Gamma {{\models}_{IR}}^{\bot} \Delta ,\Phi \vee\Psi \Leftrightarrow {\text{U/}}\Gamma {{\models}_{IR}}^{\bot} \Delta ,\Phi ,\Psi ;$

• $\begin{aligned} \vee_{\text{U}}) \quad {\text{U}},\Phi \vee\upvartheta/\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow & {\text{U}},\Phi ,\upvartheta /\Gamma {{\models}_{IR}}^{\bot} \Delta \quad {\text{and}}\quad {\text{U}},\Phi /\Gamma {{\models}_{IR}}^{\bot}\upvartheta,\Delta \quad {\text{and}}\, \\ & {\text{U}},\upvartheta/\Gamma {{\models}_{IR}}^{\bot}\Phi ,\Delta ; \\ \end{aligned}$

• $\neg_{\text{L}}{\text{)U/}}\neg\Phi ,\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U/}}\Gamma {{\models}_{IR}} \Delta ,\Phi ;$

• $\neg_{\text{R}} ){\text{U/}}\Gamma {{\models}_{IR}}^{\bot} \Delta ,\neg\Phi ,\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $\neg_{\text{U}}{\text{)U}},\neg\upvartheta/\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U}},\upvartheta/\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $\sim_{\text{U}} ){\text{U,}}^{ \sim }\Phi /\varGamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U/}}\Phi ,\Gamma {{\models}_{IR}}^{\bot} \Delta \,{\text{and}}\,{\text{U/}}\Gamma {{\models}_{IR}}^{\bot} \Delta ,\Phi ;$

• $\sim_{\text{L}} ){\text{U}}/^{ \sim }\Phi ,\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U}},\Phi /\Gamma {{\models}_{IR}}^{\bot} \Delta .$

Proof.

Property ∨_U holds because

$$ \bot (\Phi _{J} \vee\Psi _{J} ) = ( \bot (\Phi _{J} ) \cap \bot (\Psi _{J} )) \cup ( \bot (\Phi _{J} ) \cap F(\Psi _{J} )) \cup (F(\Phi _{J} ) \cap \bot (\Psi _{J} )). $$

Property ¬_U holds because ⊥(¬Φ_J) = ⊥(Φ_J).

Property $^{ \sim }$_U holds because ⊥$(^{ \sim }\Phi _{J} ) = T(\Phi _{J} ) \cup F(\Phi _{J} )$.

Properties ¬_L, ¬_R, ∨_L, ∨_R are similar to properties of |=_IR [9, 11, 12]. Properties ¬_U, ∨_U, ${}^{ \sim }$_L, ${}^{ \sim }$_U are special for $L^{ \, R \equiv }$.

Let us consider properties of relation $\left| { =_{{IR}^{ \bot}} } \right.$ of a renominative level. Each of the properties ${\text{R}},{\text{R}}_{ \bot } {\text{I}},{\text{R}}_{ \bot } {\text{U}},{\text{R}}_{ \bot } {\text{R}},{\text{R}}_{ \bot } \vee ,R_{ \bot } \neg$, ${\text{R}}_{ \bot }^{ \sim }$ of Lemma 2 induces three corresponding properties for $\left| { =_{{IR}^{ \bot }} } \right.$, depending on the position of a formula (in the left side of $\left| {=_{{IR}^{ \bot }} } \right.$, in the right side of $\left| {=_{{IR}^{ \bot }} } \right.$, in the undefinedness conditions of $\left| { =_{{IR}^{ \bot }} } \right.$). Such properties are formulated in a similar way, for example, the following properties ${\text{R}}_{ \bot } \vee_{\text{L}} ,{\text{R}}_{ \bot } \vee_{\text{R}} ,{\text{R}}_{ \bot } \vee_{\text{U}}$ and ${\text{R}}_{ \bot } \sim_{\text{L}}$, ${\text{R}}_{ \bot } \sim_{\text{R}}$, ${\text{R}}_{ \bot } \sim_{\text{U}}$ and are induced by R_⊥∨ and ${\text{R}}_{ \bot }^{ \sim }$:

• ${\text{R}}_{ \bot } \vee_{\text{L}} ){\text{U}}/R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ),\Gamma {{\models}_{IR}}^{\bot} \Delta \, \Leftrightarrow \,{\text{U}}/R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ),{\text{G}}{{\models}_{IR}}^{\bot} \Delta ;$

• ${\text{R}}_{ \bot } \vee_{\text{R}} ){\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \Leftrightarrow {\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi );$

• ${\text{R}}_{ \bot } \vee_{\text{U}} ){\text{U}},R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi )/\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U}},R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\varPhi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\varPsi )/\varGamma {{\models}_{IR}}^{\bot}\Delta ;$

• ${\text{R}}_{ \bot } \sim_{\text{L}} ) {\text{U/}}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ({}^{ \sim }\Phi ),\Gamma {{\models}_{IR}}^{\bot} \Delta \Leftrightarrow {\text{U}}/{}^{ \sim }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• ${\text{R}}_{ \bot } \sim_{\text{R}} ){\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (^{ \sim }\Phi ) \Leftrightarrow {\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,{}^{ \sim }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi );$

• ${\text{R}}_{ \bot } \sim_{\text{U}} ){\text{U,}}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ({}^{ \sim }\Phi )/\Gamma {{\models}_{IR}}^{\bot} \Delta { \Leftrightarrow }{\text{U}},{}^{ \sim }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi )/\Gamma {{\models}_{IR}}^{\bot} \Delta .$

Property R_⊥↑ induces the following properties of ${{\models}_{IR}}^{\bot}$:

• R_⊥↑_L) U/$R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),$ Γ ${{\models}_{IR}}^{\bot}$ Δ, Ez ⇔ U/$R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ) ,$Γ ${{\models}_{IR}}^{\bot}$ Δ, Ez;

• R_⊥↑_R) U/Γ ${{\models}_{IR}}^{\bot}$ Δ, $R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),Ez$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, $R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),Ez;$

• R_⊥↑_U) U, $R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi )$/Γ ${{\models}_{IR}}^{\bot}$ Δ, Ez ⇔ U, $R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )$/Γ ${{\models}_{IR}}^{\bot}$ Δ, Ez.

Based on renomination properties of variable assignment predicates (Lemma 2) we obtain:

• R_⊥EL) U/$R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez),$ Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/Ez, Γ ${{\models}_{IR}}^{\bot}$ Δ if $z \notin \bar{v} \cup \bar{u}$;

• R_⊥ER) U/Γ ${{\models}_{IR}}^{\bot}$ Δ, $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez)$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, Ez if $z \notin \bar{v} \cup \bar{u}$;

• R_⊥EU) ${\text{U}},R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez)/$ Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, Ez/Γ ${{\models}_{IR}}^{\bot}$ Δ if $z \notin \bar{v} \cup \bar{u}$;

• R_⊥EvL) U/$R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez),$ Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/Ey, Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥EvR) U/Γ $| =_{IR}^{ \bot }$ Δ, $R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez)$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, Ey;

• R_⊥EvU) ${\text{U}},R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez)/$ Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, Ey/Γ ${{\models}_{IR}}^{\bot}$ Δ.

For renomination of equality predicates we obtain:

• R≡_xxL) U/$R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/≡_xx, Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R≡_xxR) U/Γ $| =_{R}^{ \bot }$ Δ,$R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} )$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ≡_xx;

• R≡_xxU) $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ),{\text{U}}/\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ ≡_xx, U/Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥≡_2L) U/$R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ),\Gamma$ $| =_{IR}^{ \bot }$ Δ ⇔ U/≡_zs, Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥≡_2R) U/Γ $| =_{IR}^{ \bot }$ Δ,$R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ≡_zs;

• R_⊥≡_2U) ${\text{U}},R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )/$Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, ≡_zs/Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥≡_2EL) U/$R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/¬Ez, Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥≡_2ER) U/Γ ${{\models}_{IR}}^{\bot}$ Δ,$R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ¬Ez ;

• R_⊥≡_2EU) ${\text{U}},R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )/$Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, ¬Ez/Γ ${{\models}_{IR}}^{\bot}$ Δ;

• R_⊥≡_1L) U/$R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/≡_zy, Γ ${{\models}_{IR}}^{\bot}$ Δ if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_1R) U/Γ ${{\models}_{IR}}^{\bot}$ Δ,$R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ≡_zy if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_1U) ${\text{U}},R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )/\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, ≡_zy/Γ ${{\models}_{IR}}^{\bot}$ Δ if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_1EL) U/$R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/¬Ey, Γ ${{\models}_{IR}}^{\bot}$ Δ if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_1ER) U/Γ ${{\models}_{IR}}^{\bot}$ Δ,$R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )$ ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ¬Ey if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_1EU) ${\text{U}},R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )/\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, ¬Ey/Γ ${{\models}_{IR}}^{\bot}$ Δ if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_0L) U/$R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/≡_xy, Γ ${{\models}_{IR}}^{\bot}$ Δ if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_0R) U/Γ ${{\models}_{IR}}^{\bot}$ Δ,$R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} )$ $| =_{IR}^{ \bot }$ Δ⇔ U/Γ ${{\models}_{IR}}^{\bot}$ Δ, ≡_xy if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$;

• R_⊥≡_0U) ${\text{U}},R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} )/$Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U, ≡_xy/Γ ${{\models}_{IR}}^{\bot}$ Δ if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$.

Properties of substitution of equals:

• ≡R_⊥r_L) U/$\equiv_{xy} ,R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ ⇔ U/$\equiv_{xy} ,R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (\Phi ),\Gamma$ ${{\models}_{IR}}^{\bot}$ Δ;

• ≡R_⊥r_R) U/$\equiv_{xy} ,\Gamma {}\,|\!=_{{IR}^{ \bot }} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),\Delta$ ⇔ U/$\equiv_{xy} ,\Gamma {}\,|\!=_{{IR}^{ \bot }} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (\Phi ),\Delta$;

• ≡R_⊥r_U) $R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),{\text{U}}/ \equiv_{xy} ,$Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ $R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (\Phi ),R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (\Phi ),{\text{U}}/ \equiv_{xy} ,$Γ ${{\models}_{IR}}^{\bot}$ Δ.

Transitivity of equality:

$$ {\text{Tr}} \equiv ){\text{U}}/ \equiv_{xy} , \equiv_{yz} ,\Gamma | =_{{IR}^{ \bot }} \Delta \Leftrightarrow {\text{U}}/ \equiv_{xy} , \equiv_{yz} , \equiv_{xz} ,\Gamma | =_{{IR}^{ \bot }} \Delta . $$

Property for insertion of variable assignment predicates specify variables –parameters of equality predicate – as assigned or unassigned:

$$ \equiv E){\text{U}}/ \equiv_{xy} ,\Gamma | =_{{IR}^{ \bot }} \Delta \Leftrightarrow {\text{U}}/ \equiv_{xy} ,Ex,Ey,\Gamma | =_{{IR}^{ \bot }} \Delta \,{\text{and}}\,{\text{U}}/ \equiv_{xy} ,\Gamma | =_{{IR}^{ \bot }} \Delta ,Ex,Ey. $$

The following properties describe conditions under which ${{\models}_{IR}}^{\bot}$ holds.

Theorem 3.

For any U, Γ, Δ ⊆ Fr, Φ ∈ Fr we have that:

• C) U/Φ, Γ ${{\models}_{IR}}^{\bot}$ Δ, Φ;

• C_UL) U,Φ/Φ, Γ ${{\models}_{IR}}^{\bot}$ Δ;

• C_UR) U,Φ/Γ ${{\models}_{IR}}^{\bot}$ Δ, Φ;

Proof.

Property C holds because T(Φ_J) ∩ F(Φ_J) = ∅.

For property C_UL we take into consideration that ⊥(Φ_J) ∩ T(Φ_J) = ∅.

For property C_UR we take into consideration that ⊥(Φ_J) ∩ F(Φ_J) = ∅.

Theorem 4.

For any U, Γ, Δ ⊆ Fr, Φ ∈ Fr we have:

• $C \sim_{R} ){\text{U}}/\Gamma | =_{{IR}^{ \bot }} \Delta , \sim \,{\Upphi ;}$

• $C_{R}^{R \bot \equiv } ){\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,R_{{\bar{w}, \bot , \bot , \bot }}^{{\bar{v},\bar{u},x,z}} ( \equiv_{xz} );$

• $C^{R \equiv }_{R} ){\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ,R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} );$

• $C^{ \equiv }_{R} ){\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta , \equiv_{xx} ;$

• $C^{RE}_{L} ){\text{U}}/R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},z}} (Ez),\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $C^{R \equiv }_{U} )R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ),{\text{U}}/\Gamma ^{ \equiv }{{\models}_{IR}}^{\bot} \Delta ;$

• $C^{ \equiv }_{U} ) \equiv_{xy} ,{\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $C^{RE}_{U} )R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez),{\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta ;$

• $C^{E}_{U} )Ey,{\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta .$

Proof.

Properties $C \sim_{R} ,C^{R \bot \equiv }_{R} ,C^{R \equiv }_{R} ,C^{ \equiv }_{R}$ hold due to such equalities:

$$ F({}^{ \sim }\Phi _{J} ) = \varnothing ,F(R_{{\bar{w}, \bot , \bot , \bot }}^{{\bar{v},\bar{u},x,z}} ( \equiv_{xz} )_{J} ) = \varnothing ,F(R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} )_{J} ) = \varnothing ,F( \equiv_{xxJ} ) = \varnothing . $$

Property $C^{RE}_{L}$ holds due to equality $T(R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},z}} (Ez)_{J} ) = \varnothing .$

Properties $C^{R \equiv }_{U} ,C^{ \equiv }_{U} ,C^{RE}_{U} ,C^{E}_{U}$ hold due to equalities:

$$ \bot (R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} )_{J} ) = \varnothing , \bot ( \equiv_{xyJ} ) = \varnothing , \bot (R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez)_{J} ) = \varnothing , \bot (Ey_{J} ) = \varnothing . $$

Based on considered properties of ${{\models}_{IR}}^{\bot}$ a calculus of sequent type for L^R≡ will be constructed.

4 Sequent Calculus for L $^{R \equiv }$

Usually, inference relations are defined by some axiomatic systems (calculi). We present here a system that formalizes logical consequence relation between sets of formulas. Such systems are called sequent calculi.

We construct a sequent calculus $C^{R \equiv }$ that specify relation ${{\models}_{IR}}^{\bot}$ for L $^{R \equiv }$.

The main objects of this calculus are sequents. Here we consider only the case with finite sequents. We construct calculus in the style of semantic tableau, so, we will treat sequents as finite sets of formulas signed (marked, indexed) by symbols _|–, _–|, and _⊥.

Formulas from Γ (they are signed by _|–) are called T-formulas, formulas from Δ (they are signed by _–|) are called F-formulas, and formulas from U (they are signed by _⊥) are called $\bot$-formulas.

Sequents are denoted _|–Γ_⊥U_–|Δ, in abbreviated form Σ.

The rules of sequent calculus are called sequent forms. They are syntactical analogs of the semantic properties of the corresponding relations of logical consequence.

Closed sequents are axioms of the sequent calculus. A closed sequent is specified in such a way that the following condition should hold:

$$ if\;sequent_{{|{-}}}\Gamma _{ \bot } U_{{{-}|}} \Delta \, is\;closed,\,then\;{\text{U}}/\Gamma {{\models}_{IR}}^{\bot} \Delta . $$

Sequent calculus is defined by basic sequent forms and closure conditions of sequents.

For C $^{R \equiv }$ closeness of sequent _|–Γ_⊥U_–|Δ is induced by properties C_LR, C_UL, C_UR, $C \sim_{\text{R}} ,C^{R \bot \equiv }_{R} ,C^{R \equiv }_{R} ,C^{ \equiv }_{R} , C^{RE}_{L} ,C^{R \equiv }_{U} ,C^{ \equiv }_{U} ,C^{RE}_{U} ,C^{E}_{U}$ that guarantee ${{\models}_{IR}}^{\bot}$:

• C_LR) there is formula Φ such that Φ ∈ Γ and Φ ∈ Δ;

• C_UL) there is formula Φ such that Φ ∈ U and Φ ∈ Γ;

• C_UR) there is formula Φ such that Φ ∈ U and Φ ∈ Δ;

• ${\text{C}} \sim_{\text{R}}$) there is formula Φ such that $^{ \sim }\Phi \in \Delta$;

• $C^{{{\text{R}} \bot \equiv }}_{\text{R}} )$ there is formula $R_{{\bar{w}, \bot , \bot , \bot }}^{{\bar{v},\bar{u},x,z}} ( \equiv_{xz} ) \in \Delta$;

• $C^{{{\text{R}} \equiv }}_{\text{R}} )$ there is formula $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in \Delta$;

• $C^{ \equiv }_{\text{R}} )$ there is formula ≡_xx  ∈ Δ;

• $C^{\text{RE}}_{\text{L}} )$ there is formula $R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},z}} (Ez) \in\Gamma$;

• $C^{{{\text{R}} \equiv }}_{\text{U}} )$ there is formula $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in {\text{U}}$;

• $C^{ \equiv }_{\text{U}} )$ there is formula ≡_xy  ∈ U;

• $C^{\text{RE}}_{\text{U}}$ there is formula $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) \in {\text{U}}$;

• $C^{\text{E}}_{\text{U}} )$ there is formula Ey ∈ U.

Sequent _|–Γ_⊥U_–|Δ is closed if the following condition holds:

$$ {\text{C}}_{\text{LR}} \vee {\text{C}}_{\text{UL}} \vee {\text{C}}_{\text{UR}} \vee {\text{C}} \sim_{\text{R}} \vee {\text{C}}_{\text{R}}^{{{\text{R}} \bot \equiv }} \vee {\text{C}}_{\text{R}}^{{{\text{R}} \equiv }} \vee {\text{C}}_{\text{R}}^{ \equiv } \vee {\text{C}}_{\text{L}}^{\text{RE}} \vee {\text{C}}_{\text{U}}^{{{\text{R}} \equiv }} \vee {\text{C}}_{\text{U}}^{ \equiv } \vee {\text{C}}_{\text{U}}^{\text{RE}} \vee {\text{C}}_{\text{U}}^{\text{E}} . $$

Closeness of _|–Γ_⊥U_–|Δ guarantees that U/Γ ^≡${{\models}_{IR}}^{\bot}$ Δ. This follows directly from properties C_LR, C_UL, C_UR (Theorem 3) and $C \sim_{R} ,C^{R \bot \equiv }_{R} ,C^{R \equiv }_{R} ,C^{ \equiv }_{R} ,C^{RE}_{L} ,C^{R \equiv }_{U} ,C^{ \equiv }_{U} ,C^{RE}_{U} ,C^{E}_{U}$ (Theorem 4).

The properties of relation ${{\models}_{IR}}^{\bot}$, presented in the previous sections, induce corresponding basic sequent forms of C^R≡. These are simplification forms (of types R, R_⊥I, R_⊥U, R_⊥↑), forms of equivalent transformations (of types R_⊥R, R_⊥¬, R_⊥∨, ${\text{R}}_{ \bot } {}^{ \sim }$), formula decomposition forms, and special for L^R≡ form ≡E (variable assignments of equality parameters), simplification of renomination in equality (of type R_⊥≡), transitivity of equality Tr≡, and substitution of equals (type of ≡R_⊥r).

The labels of sequent forms are agreed with the labels of properties of ${{\models}_{IR}}^{\bot}$.

Theorem 5.

If sequent _|–Γ_⊥U_–|Δ is closed, then U/Γ ${{\models}_{IR}}^{\bot}$ Δ.

Proof.

The theorem statement follows directly from Theorems 3 and 4.

The sequent forms of decomposition of compositions ∨, ¬, ${}^{ \sim }$ are induced by the corresponding properties of formulas decomposition, in particular, basic sequent forms of C $^{R \equiv }$ calculus are induced by the formula decomposition properties ¬_L, ¬_R, ∨_L, ∨_R, ¬_U, ∨_U, ${}^{ \sim }$ _U,${}^{ \sim }$ _L:

$$ \begin{array}{*{20}l} {{}_{ |- }\neg \frac{{_{ - |}\Phi ,\Sigma }}{{_{ |- } \neg\Phi ,\Sigma }};} \hfill & {{}_{ - |}\neg \frac{{_{| - }\Phi , \,\Sigma }}{{_{ - |} \neg\Phi ,\Sigma }};} \hfill & {{}_{ \bot }\neg \frac{{_{ \bot }\Phi , \,\Sigma }}{{_{ \bot } \neg\Phi , \,\Sigma }};} \hfill \\ {{}_{| - } \vee \frac{{_{| - }\Phi , \,\Sigma \quad _{| - }\Psi , \,\Sigma }}{{_{ |- }\Phi \vee\Psi , \, \varSigma }};} \hfill & {{}_{ - |} \vee \frac{{_{ - |}\Phi , \, _{ - |}\Psi , \,\Sigma }}{{_{ - |}\Phi \vee\Psi , \,\Sigma }};} \hfill & {{}_{ \bot } \vee \frac{{_{ \bot }\Phi ,_{ \, \bot }\upvartheta,\Sigma \quad _{ \bot }\Phi ,_{ \, - |}\upvartheta, \,\Sigma \quad _{ \, - |}\Phi ,_{ \, \bot }\upvartheta, \,\Sigma }}{{_{ \bot }\Phi \vee\upvartheta, \,\Sigma }};} \hfill \\ {_{| - } \sim \frac{{_{ \bot }\Phi , \,\Sigma }}{{_{| - } \sim\Phi , \,\Sigma }};} \hfill & {} \hfill & {_{ \bot } \sim \frac{{_{| - }\Phi , \,\Sigma \quad _{ - |}\Phi , \,\Sigma }}{{_{ \bot } \sim\Phi ,\Sigma }}} \hfill \\ \end{array} $$

Introduction of undefinedness formulas additionally leads to new sequent forms with three premises (rule $_{ \bot } \vee$).

For the composition of extended renomination we use the following forms of simplification:

$$ \begin{array}{*{20}l} {_{{|{-}}} {\text{R}}\frac{{_{| - }\Phi ,\Sigma }}{{_{| - } R(\Phi ),\Sigma }};} \hfill & {_{ - |} {\text{R}}\frac{{_{ - |}\Phi ,\Sigma }}{{_{ - |} R(\Phi ),\Sigma }};} \hfill & {_{ \bot } {\text{R}}\frac{{_{ \bot }\Phi ,\Sigma }}{{_{ \bot } R(\Phi ),\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } {\text{I}}\frac{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{| - } R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill & {_{ - |} {\text{R}}_{ \bot } {\text{I}}\frac{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ - |} R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill & {_{ \bot } {\text{R}}_{ \bot } {\text{I}}\frac{{_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ \bot } R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } {\text{U}}\frac{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{| - } R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill & {_{ - |} {\text{R}}_{ \bot } {\text{U}}\frac{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ - |} R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill & {_{ \bot } {\text{R}}_{ \bot } {\text{U}}\frac{{_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ \bot } R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ),\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \uparrow \frac{{_{| - } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }}{{_{| - } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }};} \hfill & {_{ - |} {\text{R}}_{ \bot } \uparrow \frac{{_{ - |} R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }}{{_{ - |} R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }};} \hfill & {_{ \bot } {\text{R}}_{ \bot } \uparrow \frac{{_{ \bot } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }}{{_{ \bot } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez,\Sigma }};} \hfill \\ \end{array} $$

For R_⊥U-forms the constraint is y ∈ fu(Φ).

Forms of equivalent transformations:

$$ \begin{array}{*{20}l} {_{{|{-}}} {\text{R}}_{ \bot } {\text{R}}\frac{{_{| - } R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ),\Sigma }}{{_{| - } R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )),\Sigma }};} \hfill & {_{{{-}|}} {\text{R}}_{ \bot } {\text{R}}\frac{{_{ - |} R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ),\Sigma }}{{_{ - |} R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )),\Sigma }};} \hfill & {_{ \bot } {\text{R}}_{ \bot } {\text{R}}\frac{{_{ \bot } R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ),\Sigma }}{{_{ \bot } R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )),\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \neg \frac{{_{| - } \neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi ),\Sigma }};} \hfill & {_{{{-}|}} {\text{R}}_{ \bot } \neg \frac{{_{ - |} \neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi ),\Sigma }};} \hfill & {_{{|{-}}} {\text{R}}_{ \bot } \neg \frac{{_{| - } \neg R_{{\bar{x}}}^{{\bar{v}}} (\Phi ),\Sigma }}{{_{| - } R_{{\bar{x}}}^{{\bar{v}}} (\neg\Phi ),\Sigma }}} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \vee \frac{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ),\Sigma }}{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ),\Sigma }}} \hfill & {_{{{-}|}} {\text{R}}_{ \bot } \neg \vee \frac{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ),\Sigma }}{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ),\Sigma }}} \hfill & {_{ \bot } {\text{R}}_{ \bot } \neg \vee \frac{{_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ),\Sigma }}{{_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ),\Sigma }}} \\ {{}_{| - }{\text{R}}_{ \bot } \sim \frac{{_{| - } \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (^{ \sim }\Phi ),\Sigma }};} & {{}_{ - |}{\text{R}}_{ \bot } \sim \frac{{_{ - |} \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (^{ \sim }\Phi ),\Sigma }};} & {{}_{ \bot }{\text{R}}_{ \bot } \sim \frac{{_{ \bot } \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ),\Sigma }}{{_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (^{ \sim }\Phi ),\Sigma }};} \\ {{}_{| - }{\text{R}}_{ \bot } {\text{E}}\frac{{_{| - } Ez,\Sigma }}{{_{| - } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez),\Sigma }};} & {{}_{ - |}{\text{R}}_{ \bot } {\text{E}}\frac{{_{ - |} Ez,\Sigma }}{{_{ - |} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez),\Sigma }};} & {{}_{ \bot }{\text{R}}_{ \bot } {\text{E}}\frac{{_{{_{ \bot } }} Ez,\Sigma }}{{_{{_{ \bot } }} R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez),\Sigma }};} \\ {{}_{| - }{\text{R}}_{ \bot } {\text{E}}_{\text{V}} \frac{{_{| - } Ey,\Sigma }}{{_{| - } R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez),\Sigma }}} & {{}_{ - |}{\text{R}}_{ \bot } {\text{E}}_{\text{V}} \frac{{_{ - |} Ey,\Sigma }}{{_{ - |} R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez),\Sigma }}} & {{}_{ \bot }{\text{R}}_{ \bot } {\text{E}}_{\text{V}} \frac{{_{ \bot } Ey,\Sigma }}{{_{ \bot } R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez),\Sigma }}} \hfill \\ \end{array} $$

For R_⊥E-forms the constraint is $z \notin \bar{v} \cup \bar{u}$.

Forms of renomination of equality:

$$ \begin{array}{*{20}l} {_{{|{-}}} {\text{R}} \equiv_{xx} \frac{{_{| - } \equiv_{xx} , \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ), \,\Sigma }};} \hfill & {_{{{-}|}} R \equiv_{xx} \frac{{_{ - |} \equiv_{xx} , \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}} \equiv_{xx} \frac{{_{ \bot } \equiv_{xx} , \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ), \,\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \equiv_{2} \frac{{_{| - } \equiv_{zs} , \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {_{{{-}|}} R_{ \bot } \equiv_{2} \frac{{_{ - |} \equiv_{zs} , \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}}_{ \bot } \equiv_{2} \frac{{_{ \bot } \equiv_{zs} , \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \equiv_{{2{\text{E}}}} \frac{{_{ - |} Ez, \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {_{{{-}|}} R_{ \bot } \equiv_{{2{\text{E}}}} \frac{{_{| - } Ez, \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}}_{ \bot } \equiv_{{2{\text{E}}}} \frac{{_{ \bot } Ez, \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ), \,\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \equiv_{1} \frac{{_{| - } \equiv_{zy} , \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {_{{{-}|}} R_{ \bot } \equiv_{1} \frac{{_{ - |} \equiv_{zy} , \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}}_{ \bot } \equiv_{1} \frac{{_{ \bot } \equiv_{zy} , \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \equiv_{{1{\text{E}}}} \frac{{_{ - |} Ey, \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {_{{{-}|}} R_{ \bot } \equiv_{{1{\text{E}}}} \frac{{_{| - } Ey, \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}}_{ \bot } \equiv_{{1{\text{E}}}} \frac{{_{ \bot } Ey, \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ), \,\Sigma }};} \hfill \\ {_{{|{-}}} {\text{R}}_{ \bot } \equiv_{0} \frac{{_{| - } \equiv_{xy} , \,\Sigma }}{{_{| - } R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {_{{{-}|}} R_{ \bot } \equiv_{0} \frac{{_{ - |} \equiv_{xy} , \,\Sigma }}{{_{ - |} R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ), \,\Sigma }};} \hfill & {{}_{ \bot }{\text{R}}_{ \bot } \equiv_{0} \frac{{_{ \bot } \equiv_{xy} , \,\Sigma }}{{_{ \bot } R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ), \,\Sigma }}} \hfill \\ \end{array} $$

For R_⊥≡₁ and R_⊥≡_1E-forms the constraint is $y \notin \bar{v} \cup \bar{u}$, $x \ne y$;

For R_⊥≡₀-forms the constraint is $x,y \notin \bar{v} \cup \bar{u}$, $x \ne y$.

Special form for insertion of variable assignment predicates permits to specify variables – parameters equality predicate – as assigned or unassigned:

$$ \equiv {\text{E}}\frac{{_{| - } \equiv_{xy} ,_{| - } Ex,_{| - } Ey, \,\Sigma \quad _{| - } \equiv_{xy} ,_{ - |} Ex,_{ - |} Ey, \,\Sigma }}{{_{| - } \equiv_{xy} , \,\Sigma }}. $$

Form of equality transitivity:

$$ {\text{Tr}} \equiv \frac{{_{| - } \equiv_{xy} , \, _{| - } \equiv_{yz} , \, _{| - } \equiv_{xz} , \,\Sigma }}{{_{| - } \equiv_{xy} , \, _{| - } \equiv_{yz} , \,\Sigma }}. $$

Forms of substitution of equals (P ∈ Ps):

$$ \begin{aligned}_{{|{-}}} \equiv {\text{R}}_{ \bot } {\text{r}}\frac{{_{| - } \equiv_{xy} ,_{ \, | - } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),_{ \, | - } R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P),\Sigma }}{{_{| - } \equiv_{xy} ,_{ \, | - } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),\Sigma }};\quad &_{{{-}|}} \equiv {\text{R}}_{ \bot } {\text{r}}\frac{{_{| - } \equiv_{xy} ,_{ \, - |} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),_{ \, - |} R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P),\Sigma }}{{_{| - } \equiv_{xy} ,_{ \, - |} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),\Sigma }} \\ &_{ \bot } \equiv {\text{R}}_{ \bot } {\text{r}}\frac{{_{| - } \equiv_{xy} ,_{ \, \bot } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),_{ \, \bot } R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P),\Sigma }}{{_{| - } \equiv_{xy} ,_{ \, \bot } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),\Sigma }}. \\ \end{aligned} $$

The above-written closeness conditions and basic sequent forms specify $C^{R \equiv }$ calculus. For basic rules of $C^{R \equiv }$ we have the following main properties.

Theorem 6.

Let $\frac{{_{| - }\Gamma _{1 \bot } {\text{U}}_{ 1- |} \Delta_{1} \ldots\Gamma _{k \bot } {\text{U}}_{k - |} \Delta_{k} }}{{_{| - }\Gamma _{ \bot } {\text{U}}_{ - |} \Delta }}$ be basic sequent form of $C^{R \equiv }$ (k ∈ {1, 2, 3}). Then U/Γ ${{\models}_{IR}}^{\bot}$ Δ ⇔ (U₁/Γ₁ ${{\models}_{IR}}^{\bot}$ Δ₁ and … U_k/Γ_k ${{\models}_{IR}}^{\bot}$ Δ_k ).

Proof.

For each form the proof follows directly from its corresponding property of relation ${{\models}_{IR}}^{\bot}$ formulated in Subsect. 3.4.

The derivation in $C^{R \equiv }$ has the form of a tree, the vertices of which are sequents. Such trees are called sequent trees. Details of the definition of sequent tree can be found in [19]. A sequent tree is closed if every its leaf is a closed sequent. A sequent Σ is derivable if there is a closed sequent tree with the root Σ. During construction of a sequent tree the following cases are possible:

• construction procedure is completed: all sequents on the leaves are closed; we have a finite closed tree;

• construction procedure is not completed; we have a finite or infinite unclosed tree. Such tree has at least one path called unclosed, all vertices of which are unclosed sequents.

We meet the first case while proving soundness and the second one while proving completeness of $C^{R \equiv }$.

5 Soundness and Completeness of C $^{R \equiv }$

Now we prove soundness and completeness theorems for $C^{R \equiv }$.

Theorem 7

(soundness). Let sequent _|–Γ_⊥U_–|Δ be derivable in $C^{R \equiv }$. Then U/Γ ${{\models}_{IR}}^{\bot}$ Δ.

Proof.

If _|–Γ_⊥U_–|Δ is derivable, then a finite closed tree was constructed. From this follows that for any leaf of this tree its sequent _|–Λ_⊥W_–|Κ is closed. Thus, by Theorem 5, W/Λ ${{\models}_{IR}}^{\bot}$ Κ holds. Therefore, for the root of the tree (sequent _|–Γ_⊥U_–|Δ) we have that U/Γ ${{\models}_{IR}}^{\bot}$ Δ holds (Theorem 6).

The completeness 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 sets is used [20].

We apply this method to the $C^{R \equiv }$ calculus.

A Hintikka set for $L^{ \, R \equiv }$ is a set H of signed formulas satisfying two types of conditions:

• (1) uncloseness conditions derived from closeness conditions for sequents;

• (2) decomposition or transformation conditions derived from sequent forms.

Uncloseness conditions for H are the following conditions obtained by negation of closeness conditions of sequents:

• HC_LR) there is no formula Φ such that _|–Φ ∈ H and _–|Φ ∈ H;

• HC_UL) there is no formula Φ such that _⊥Φ ∈ H and _|–Φ ∈ H;

• HC_UR) there is no formula Φ such that _⊥Φ ∈ H and _–|Φ ∈ H;

• ${\text{HC}} \sim_{\text{R}}$) there is no formula Φ such that ${}_{ - |} \sim\Phi \in H$;

• HC^R⊥≡) there is no formula $R_{{\bar{w}, \bot , \bot , \bot }}^{{\bar{v},\bar{u},x,z}} ( \equiv_{xz} )$ such that ${}_{ - |}R_{{\bar{w}, \bot , \bot , \bot }}^{{\bar{v},\bar{u},x,z}} ( \equiv_{xz} ) \in H$;

• HC^R≡) there is no formula $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} )$ such that ${}_{ - |}R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in H$;

• HC^≡) there is no formula ≡_xx such that _–| ≡_xx ∈ H;

• HC^RE) there is no formula $R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},z}} (Ez)$ such that ${}_{| - }R_{{\bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},z}} (Ez) \in H$;

• ${\text{HC}}^{{{\text{R}} \equiv }}_{\text{U}} )$ there is no formula $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} )$ such that ${}_{ \bot }R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in H$;

• ${\text{HC}}^{ \equiv }_{\text{U}} )$ there is no formula ≡_xy such that _⊥≡_xy ∈ H;

• ${\text{HC}}^{\text{RE}}_{\text{U}} )$ there is no formula $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez)$ such that ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) \in H$;

• ${\text{HC}}^{\text{E}}_{\text{U}} )$ there is no formula Ey such that _⊥Ey ∈ H.

Decomposition conditions for propositional compositions:

• H¬_L) if _|–¬Φ ∈ H, then _–|Φ ∈ H;

• H¬_R) if _–|¬Φ ∈ H, then _|–Φ ∈ H;

• H¬_U) if $_{ \bot } \neg\Phi$ ∈ H, then $_{ \bot }\Phi$ ∈ H;

• H∨_L) if _|–Φ∨Ψ ∈ H, then _|–Φ ∈ H or _|–Ψ ∈ H;

• H∨_R) if _–|Φ∨Ψ ∈ H, then _–|Φ ∈ H and _–|Ψ ∈ H;

• H∨_U) if $_{ \bot }\Phi \vee\upvartheta$ ∈ H, then $_{ \bot }\Phi$ ∈ H and $_{ \bot }\upvartheta$ ∈ H

• or $_{ \bot }\Phi$ ∈ H and _–|ϑ ∈ H or _–|Φ ∈ H and $_{ \bot }\upvartheta$ ∈ H;

• ${\text{H}} \sim_{\text{L}}$) if ${}_{| - } \sim\Phi$ ∈ H, then $_{ \bot }\Phi$ ∈ H;

• ${\text{H}} \sim_{\text{U}}$) if ${}_{ \bot } \sim\Phi$ ∈ H, then _|–Φ ∈ H or _–|Φ ∈ H.

Transformation conditions based on forms R, R_⊥I, R_⊥U, R_⊥↑, R_⊥R, R_⊥¬, R_⊥∨, ${\text{R}}_{ \bot } \sim$, and HR_⊥E, HR_⊥Ev_R :

• HR_L) if _|–R(Φ) ∈ H, then _|–Φ ∈ H;

• HR_R) if _–|R(Φ) ∈ H, then _–|Φ ∈ H;

• HR_U) if _⊥R(Φ) ∈ H, then _⊥Φ ∈ H;

• HR_⊥I_L) if ${}_{| - }R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ) \in H,{\text{ then }}{}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥I_R) if ${}_{ - |}R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ) \in H,{\text{ then }}{}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥I_U) if ${}_{ \bot }R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi ) \in H$, then ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥U_L) if y ∈ fu(Φ) and ${}_{| - }R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ) \in H$, then ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥U_R) if y ∈ fu(Φ) and ${}_{ - |}R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ) \in H$, then ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥U_U) if y ∈ fu(Φ) and ${}_{ \bot }R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi ) \in H$, then ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥↑_L) $_{| - } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H \, \Rightarrow \, _{| - } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H$;

• HR_⊥↑_R) $_{ - |} R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H \, \Rightarrow \, _{ - |} R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H$;

• HR_⊥↑_U) $_{ \bot } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H \, \Rightarrow \, _{ \bot } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H$;

• HR_⊥R_L) if ${}_{| - }R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )) \in H$, then ${}_{| - }R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ) \in H$;

• HR_⊥R_R) if ${}_{ - |}R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )) \in H$, then ${}_{ - |}R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ) \in H$;

• HR_⊥R_U) if ${}_{ \bot }R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )) \in H$, then ${}_{ \bot }R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ) \in H$;

• HR_⊥∨_L) if ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H,{\text{ then }}{}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$;

• HR_⊥∨_R) if ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H,{\text{ then }}{}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$;

• HR_⊥∨_U) if ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H$, then ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$;

• R_⊥¬ _L) if ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi ) \in H$, then ${}_{| - }\neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• R_⊥¬ _R) if ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi ) \in H$, then $_{ - |} \neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• R_⊥¬ _U) if ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi ) \in H$, then ${}_{ \bot }\neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• ${\text{HR}}_{ \bot } \sim_{\text{L}}$) if ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ( \sim\Phi ) \in H$, then ${}_{| - } \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• ${\text{HR}}_{ \bot } \sim_{\text{R}}$) if ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ( \sim\Phi ) \in H$, then $_{ - |} \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• ${\text{HR}}_{ \bot } \sim_{\text{U}}$) if ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} ( \sim\Phi ) \in H$, then ${}_{ \bot } \sim R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \in H$;

• HR_⊥E_L) if $z \notin \bar{u} \cup \bar{v}$ and ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) \in H,{\text{ then }}{}_{| - }Ez \in H;$

• HR_⊥E_R) if $z \notin \bar{u} \cup \bar{v}$ and ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) \in H,{\text{ then }}{}_{ - |}Ez \in H;$

• HR_⊥E_U) if $z \notin \bar{u} \cup \bar{v}$ and ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez) \in H,{\text{ then }}{}_{ \bot }Ez \in H;$

• HR_⊥Ev_L) if ${}_{| - }R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez) \in H,{\text{ then }}{}_{| - }Ey \in H;$

• HR_⊥Ev_R) if ${}_{ - |}R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez) \in H,{\text{ then}}{}_{ - |}Ey \in H;$

• HR_⊥Ev_U) if ${}_{ \bot }R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez) \in H,{\text{ then }}{}_{ \bot }Ey \in H.$

Transformation conditions based on forms R≡_xx, R_⊥≡₂, R_⊥≡_2E, R_⊥≡₁, R_⊥≡_1E, R_⊥≡₀ :

• HR≡_xxL) if ${}_{| - }R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in H,{\text{ then }}{}_{| - } \equiv_{xx} \in H$;

• HR≡_xxR) if ${}_{ - |}R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in H,{\text{ then }}{}_{ - |} \equiv_{xx} \in H$;

• HR≡_xxU) if ${}_{ \bot }R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} ) \in H,{\text{ then }}{}_{ \bot } \equiv_{xx} \in H$;

• HR_⊥≡_2L) if ${}_{| - }R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{| - } \equiv_{zs} \in H$;

• HR_⊥≡_2R) if ${}_{ - |}R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{ - |} \equiv_{zs} \in H$;

• HR_⊥≡_2U) if ${}_{ \bot }R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{ \bot } \equiv_{zs} \in H$;

• HR_⊥≡_2EL) if ${}_{| - }R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{ - |}Ez \in H$;

• HR_⊥≡_2ER) if ${}_{ - |}R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{| - }Ez \in H$;

• HR_⊥≡_2EU) if ${}_{ \bot }R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} ) \in H,{\text{ then }}{}_{ \bot }Ez \in H$;

• HR_⊥≡_1L) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{| - }R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{| - } \equiv_{zy} \in H$;

• HR_⊥≡_1R) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ - |}R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{ - |} \equiv_{zy} \in H$;

• HR_⊥≡_1U) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ \bot }R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{ \bot } \equiv_{zy} \in H$;

• HR_⊥≡_1EL) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{| - }R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{ - |}Ey \in H$;

• HR_⊥≡_1ER) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ - |}R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{| - }Ey \in H$;

• HR_⊥≡_1EU) if $y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ \bot }R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} ),{\text{ then }}{}_{ \bot }Ey \in H$;

• HR_⊥≡_0L) if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{| - }R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ),{\text{ then }}{}_{| - } \equiv_{xy} \in H$;

• HR_⊥≡_0R) if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ - |}R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ),{\text{ then }}{}_{ - |} \equiv_{xy} \in H$;

• HR_⊥≡_0U) if $x,y \notin \bar{u} \cup \bar{v}, \, x \ne y$ and ${}_{ \bot }R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} ),{\text{ then }}{}_{ \bot } \equiv_{xy} \in H$.

Transformation conditions related to equality predicates $(P \in Ps)$:

• H≡E) _|– ≡_xy  ∈ H, then _|–Ex, _|–Ey  ∈ H or _–|Ex, _–|Ey  ∈ H;

• HTr≡) _|– ≡_xy  ∈ H and _|– ≡_yz  ∈ H, then _|– ≡_xz  ∈ H;

• H≡R_⊥r_L) if $_{| - } \equiv_{xy} ,_{ \, | - } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P) \in H,$ then $_{| - } \equiv_{xy} ,_{ \, | - } R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),_{ \, | - } R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P) \in H;$

• H≡R_⊥r_R) if $_{| - } \equiv_{xy} ,_{ \, - |} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P) \in H,$ then $_{| - } \equiv_{xy} ,_{ - |} R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),_{ \, - |} R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P) \in H;$

• H≡R_⊥r_U) if $_{| - } \equiv_{xy} ,_{ \, } {}_{ \bot }R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P) \in H,$ then $_{| - } \equiv_{xy} ,{}_{ \bot }R_{{\bar{w}, \bot ,x}}^{{\bar{v},\bar{u},z}} (P),{}_{ \bot }R_{{\bar{w}, \bot ,y}}^{{\bar{v},\bar{u},z}} (P) \in H$.

A set H of signed formulas is called satisfiable if there exist a set A, an interpretation J = (${\mathcal{A}}^{R \equiv }$(V, A), $I_{Q}^{Ps}$), and a nominative set $\updelta \in \;^{V} A$ such that

• if _|–Φ ∈ H, then Φ_J (δ)↓ = T;

• if _–|Φ ∈ H, then Φ_J (δ)↓ = F;

• if $_{ \bot }\Phi$ ∈ H, then Φ_J (δ)↑.

Theorem 8.

Let H be a Hintikka set for $L^{ \, R \equiv }$. Then H is satisfiable.

Proof.

Given a Hintikka set H, we should first construct a set A and a nominative set $\updelta \in \;^{V} A$. Then we specify an interpretation of predicate symbols $I_{Q}^{Ps}$ that gives us an interpretation J. And at last, we prove for all formulas from H satisfiability conditions. These constructions are rather complicated therefore here we do not present the proof in all details but demonstrate its main parts.

Let W = nm(H) \ {x | _–| Ex ∈ H} be a set of names (variables) that are not explicitly specified as unassigned.

Equality predicates induce on W the equivalence relation

$$ x\,\sim \,y \Leftrightarrow \,_{{|{-}}} \equiv_{xy} \in H. $$

Sequent form ≡E guarantees correctness of this definition because when _|– ≡_xy  ∈ H we have that _|– Ex, _|–Ey ∈ H or _–| Ex, _–|Ey ∈ H and it is not possible that _–| Ex, _|–Ey ∈ H or _–| Ey, _|–Ex ∈ H.

Let S = $W/\sim$ be a quotient set of W induced by ~. Let 〈v〉 be an equivalence class represented by v. Take δ = [v↦〈v〉 | v ∈ W ]. Such δ is a surjection of W on S.

For values of predicates Ex on δ we obtain:

• _|–Ex ∈ H gives x ∈ W, therefore Ex_J (δ)↓ = T;

• _–|Ex ∈ H gives x∉W, therefore δ(x)↑, whence Ex_J (δ)↓ = F.

By H≡E from _|– ≡_xy ∈ H follows _|–Ex, _|–Ey ∈ H or _–|Ex, _–|Ey ∈ H. Then in $I_{Q}^{Ps}$ we obtain:

• if _|– ≡_xy ∈ H and _|–Ex, _|–Ey ∈ H, then x ~ y, therefore by construction of δ we have ≡_xy J (δ)↓ = T;

• if _|– ≡_xy ∈ H and _–|Ex, _–|Ey ∈ H, then δ(x)↑ and δ(y)↑, therefore ≡_xy J (δ)↓ = T;

• if _–| ≡_xy ∈ H, then it is not true that x ~ y, therefore by construction of δ we have ≡_xy J (δ)↓ = F.

• it is not possible that _⊥≡_xy ∈ H and not possible that _⊥Ey ∈ H due to ${\text{HC}}^{ \equiv }_{\text{U}}$ and ${\text{HC}}^{\text{E}}_{\text{U}}$.

Let us specify values of basic predicate P ∈ Ps on δ and on the nominative sets of the form ${\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\updelta)$:

• if _|– P ∈ H, then P_J (δ)↓ = T;

• if _–| P ∈ H, then P_J (δ)↓ = F;

• if $_{ \bot } P$ ∈ H, then P_J (δ)↑;

• if ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (P) \in H$, then $P_{{_{J} }}^{{}} ({\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\updelta)){\downarrow} = T$;

• if ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (P) \in H$, then $P_{J} ({\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\updelta)){\downarrow} = F$;

• if $_{ \bot } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (P) \in H$, then $P_{J} ({\text{r}}_{{ \, \bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\updelta)){\uparrow}$.

Values of P on other data can be chosen in arbitrary way with respect to unessential variables from V_U.

No ambiguity arises in these definitions due to uncloseness conditions for H.

For atomic and primitive formulas, the satisfiability statements follow from their definitions.

Now the proof goes on by induction on the formula structure. All decomposition and transformation conditions should be checked except of types H≡E, HTr≡, H≡R_⊥r.

The conditions of the types HR, HR_⊥I, HR_⊥U, HR_⊥R, HR_⊥¬, HR_⊥∨, H ${\text{R}}_{ \bot } \sim$, HR_⊥E, HR_⊥Ev, HR≡_xx, HR_⊥≡₂, HR_⊥≡_2E, HR_⊥≡₁, HR_⊥≡_1E, HR_⊥≡₀ are related to equivalent transformations or simplification of formulas; they are induced by the equality of corresponding predicates.

Let us write explicitly these predicate equalities for the considered conditions:

HR: Φ_J = R(Φ)_J;

HR_⊥I: $R_{{z,\bar{x}, \bot }}^{{z,\bar{v},\bar{u}}} (\Phi )_{J} = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi )_{{_{J} }}$;

HR_⊥U: $R_{{z,\bar{x}, \bot }}^{{y,\bar{v},\bar{u}}} (\Phi )_{J} = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi )_{{_{J} }}$; here y ∈ fu(Φ);

HR_⊥R: $R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} (R_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi ))_{J} = R_{{\bar{y}, \bot }}^{{\bar{v},\bar{z}}} \circ_{{\bar{x}, \bot }}^{{\bar{u},\bar{t}}} (\Phi )_{J}$;

HR_⊥¬: $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\neg\Phi )_{J} = \neg R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi )_{J}$;

HR_⊥∨: $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi )_{J} = R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi )_{J}$;

H ${\text{R}}_{ \bot } \sim$: $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (^{ \sim }\Phi )_{J} = \;^{ \sim } R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi )_{J}$;

HR_⊥E: $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (Ez)_{J} = Ez_{J}$; here $z \notin \bar{v} \cup \bar{u}$;

HR_⊥Ev: $R_{{\bar{x}, \bot ,y}}^{{\bar{v},\bar{u},z}} (Ez)_{J} = Ey_{J}$;

HR≡_xx: $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xx} )_{J} = \; \equiv_{xxJ}$;

HR_⊥≡₂: $R_{{\bar{w}, \bot ,z,s}}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )_{J} = \; \equiv_{{zs_{J} }}$;

HR_⊥≡_2E: $R_{{\bar{w}, \bot ,z, \bot }}^{{\bar{v},\bar{u},x,y}} ( \equiv_{xy} )_{J} =_{{}} \neg Ez_{J}$;

HR_⊥≡₁: $R_{{\bar{w}, \bot ,z}}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )_{J} = \; \equiv_{zyJ}$; here $y \notin \bar{v} \cup \bar{u}, \, x \ne y$;

HR_⊥≡_1E: $R_{{\bar{w}, \bot , \bot }}^{{\bar{v},\bar{u},x}} ( \equiv_{xy} )_{J} =_{{}} \neg Ey_{{_{J} }}$; here $\, y \notin \{ \bar{u},\bar{v}\} , \, x \ne y$;

HR_⊥≡₀: $R_{{\bar{w}, \bot }}^{{\bar{v},\bar{u}}} ( \equiv_{xy} )_{J} = \; \equiv_{xyJ}$; here $x ,y \notin \bar{v} \cup \bar{u}, \, x \ne y$.

Let us prove as an example satisfiability for HR_⊥∨.

Let ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H$. By HR∨_L we have ${}_{| - }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$. By induction hypothesis we have $(R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ))_{J} (\updelta){\downarrow} = T$, whence $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi )_{A} (\updelta){\downarrow} = T$.

Let ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H$. By HR∨_R we have ${}_{ - |}R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$. By induction hypothesis we have $(R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ))_{J} (\updelta){ \downarrow } = F$, whence $R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi )_{J} (\updelta){ \downarrow } = F$.

Let ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi \vee\Psi ) \in H$. By HR∨_U we have ${}_{ \bot }R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ) \in H$. By induction hypothesis we have $(R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Phi ) \vee R_{{\bar{x}, \bot }}^{{\bar{v},\bar{u}}} (\Psi ))_{J} (\updelta){\uparrow }$, whence $R_{{\bar{x}}}^{{\bar{v}}} (\Phi \vee\Psi )_{J} (\updelta){\uparrow }$.

Let us prove the theorem for conditions H¬_L, H¬_R, H¬_U, H∨_L, H∨_R, H∨_U, H $^{ \sim }$ _U, H $^{ \sim }$ _L.

Let _|–¬Φ ∈ H. By H¬_L we have $_{{{-}|}}\Phi \in H$. By induction hypothesis Φ_J (δ)↓ = F, therefore ¬Φ_J (δ)↓ = T.

Let _–|¬Φ ∈ H. By H¬_R we have _|–Φ ∈ H. By induction hypothesis Φ_J (δ)↓ = T, therefore ¬Φ_J (δ)↓ = F.

Let $_{ \bot } \neg\Phi \in H$. By H¬_U we have $_{ \bot }\Phi \in H$. By induction hypothesis Φ_J (δ)↑, therefore ¬Φ_J (δ)↑.

Let _|–Φ∨Ψ ∈ H. By H∨_L we have _|–Φ ∈ H or _|–Ψ ∈ H. By induction hypothesis Φ_J (δ)↓ = T and Ψ_J (δ) = T, therefore (Φ∨Ψ)_J (δ)↓ = T.

Let _–|Φ∨Ψ ∈ H. By H∨_R we have _–|Φ ∈ H and _–|Ψ ∈ H. By induction hypothesis Φ_J (δ)↓ = F and Ψ_J (δ)↓ = F, therefore (Φ∨Ψ)_J (δ)↓ = F.

Let $_{ \bot }\Phi \vee\Psi$ ∈ H. By H∨_U $_{ \bot }\Phi$ ∈ H and $_{ \bot }\Psi$ ∈ H or $_{ \bot }\Phi$ ∈ H and _–|Ψ ∈ H or _–|Φ ∈ H and $_{ \bot }\Psi$ ∈ H. By induction hypothesis Φ_J (δ)↑ and Ψ_J (δ)↑ or Φ_J (δ)↑ and Ψ_J (δ)↓ = F or Φ_J (δ)↓ = F and Ψ_J (δ)↑. Therefore (Φ∨Ψ)_J (δ)↑.

Let ${}_{ \bot } \sim\Phi$ ∈ H. By ${\text{H}} \sim_{\text{U}}$ we have _|–Φ ∈ H or _–|Φ ∈ H. By induction hypothesis Φ_J (δ)↓ = T or Φ_J(δ) = F, this gives Φ_J (δ)↓, therefore $\sim\Phi _{J} (d){\uparrow}$.

Let ${}_{| - } \sim\Phi$ ∈ H. By ${\text{H}} \sim_{\text{L}}$ we have $_{ \bot }\Phi$ ∈ H. By induction hypothesis Φ_J (δ)↑, therefore $\sim\Phi _{J} (d){\downarrow} = T$.

Let us prove the theorem for conditions HR_⊥↑_L, HR_⊥↑_R, HR_⊥↑_U.

Let $_{| - } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H.$ By HR_⊥↑_L we have $_{| - } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )\in H$. By induction hypothesis $R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta){ \downarrow } = T,$ then δ(z)↑ since _–|Ez ∈ H, whence $R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\delta ) = R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta) = T$.

Let $_{ - |} R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H.$ By HR_⊥↑_R we have $_{ - |} R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )\in H$. By induction hypothesis $R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\delta ){ \downarrow } = F,$ then δ(z)↑ since _–|Ez ∈ H, whence $R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta) = R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta) = F$.

Let $_{ \bot } R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi ),_{ \, - |} Ez \in H.$ By HR_⊥↑_U we have $_{ \bot } R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )\in H$. By induction hypothesis $R_{{ \, \bar{x}, \bot , \bot }}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta){ \uparrow },$ then _–|Ez ∈ H since δ(z)↑, whence $R_{{ \, \bar{x}, \bot ,z}}^{{\bar{v},\bar{u},y}} (\Phi )_{J} (\updelta){ \uparrow }$.

Theorem 9.

For C $^{R \equiv }$ there exists a sequent tree construction procedure such that unclosed paths form Hintikka sets.

Proof.

Such procedure for constructing a sequent tree in C $^{R \equiv }$ is defined in the same way as for other sequent calculi for finite sequents [19], therefore we will not go into details.

The completeness theorem follows from Theorems 8 and 9.

Theorem 10

(completeness). Let U/Γ ${{\models}_{IR}}^{\bot}$ Δ hold. Then sequent _|–Γ_⊥U_–|Δ is derivable in C $^{R \equiv }$.

Proof.

Assume that U/Γ ${{\models}_{IR}}^{\bot}$ Δ and _|–Γ_⊥U_–|Δ is not derivable. In this case a sequent tree for _|–Γ_⊥U_–|Δ is not closed. Thus, an unclosed path ℘ exists in this tree. Let H be the set of all formulas of this path. By Theorem 9, H is a Hintikka set. By Theorem 8 this means that a counter-model for _|–Γ_⊥U_–|Δ was constructed. But this contradicts to U/Γ ${{\models}_{IR}}^{\bot}nnnnn$ Δ.

6 Conclusion

The efficiency of program verification heavily depends on program logics supporting corresponding verification methods. Traditional Floyd-Hoare logic and its variants are oriented on total pre- and post-conditions (total predicates) and do not support partial predicates. In this paper we have studied a new predicate logic used in constructing sound program logics. This program-oriented predicate logic includes the compositions of predicate complement, extended renominations, and equality predicates.

For this logic we have defined and investigated a special consequence relation called irrefutability consequence relation with undefinedness conditions. For a case of quantifier-free predicate logic of partial quasiary predicates (renominative level) we have constructed a calculus of sequent type and proved its soundness and completeness.

In the future we plan to construct and implement sequent calculi for first-order predicate logic and a logic over hierarchical nominative data and prove their soundness and completeness. Such logics more adequately represent data structures used in programming. First steps in this direction were made in [21, 22].