Dual Tableaux for Some Logics Based on Intuitionism

Abstract

Intuitionistic logic encompasses the principles of reasoning which were used by L. Brouwer in developing his intuitionistic mathematics, beginning in [Bro07]. Intuitionistic logic can be succinctly described as classical logic without the law ϕ ∨ ¬ϕ of excluded middle. Brouwer observed that this law was abstracted from finite situations and its application to statements about infinite collections is not justified. One of the consequences of the rejection of the law of excluded middle is that every intuitionistic proof of an existential sentence can be effectively transformed into an intuitionistic proof of an instance of that sentence. More precisely, if a formula of the form ∃xϕ(x) without free variables is provable in the intuitionistic predicate logic, then there is a term t without free variables such that ϕ(t) is provable. In particular, if ϕ ∨ ψ is provable, then either ϕ or ψ is provable. In that sense intuitionistic logic may provide a logical basis for constructive reasoning. A formal system of intuitionistic logic was proposed in [Hey30]. A relationship between the classical propositional logic PC and intuitionistic propositional logic INT was proved by Glivenko in [Gli29], namely a PC-formula ϕ is PC-provable if and only if ¬ ¬ϕ is INT-provable. Kripke semantics for intuitionistic logic was developed in [Kri65].

1 Introduction

Intuitionistic logic encompasses the principles of reasoning which were used by L. Brouwer in developing his intuitionistic mathematics, beginning in [Bro07]. Intuitionistic logic can be succinctly described as classical logic without the law ϕ ∨ ¬ϕ of excluded middle. Brouwer observed that this law was abstracted from finite situations and its application to statements about infinite collections is not justified. One of the consequences of the rejection of the law of excluded middle is that every intuitionistic proof of an existential sentence can be effectively transformed into an intuitionistic proof of an instance of that sentence. More precisely, if a formula of the form ∃xϕ(x) without free variables is provable in the intuitionistic predicate logic, then there is a term t without free variables such that ϕ(t) is provable. In particular, if ϕ ∨ ψ is provable, then either ϕ or ψ is provable. In that sense intuitionistic logic may provide a logical basis for constructive reasoning. A formal system of intuitionistic logic was proposed in [Hey30]. A relationship between the classical propositional logic PC and intuitionistic propositional logic INT was proved by Glivenko in [Gli29], namely a PC-formula ϕ is PC-provable if and only if ¬ ¬ϕ is INT-provable. Kripke semantics for intuitionistic logic was developed in [Kri65].

In this chapter we present relational dual tableaux for the propositional intuitionistic logic INT, for the minimal intuitionistic logic of Johansson, and for some axiomatic extensions of INT, namely for the Scott’s logic and the logic of weak excluded middle. All these logics are decidable. We also develop a dual tableau for the logic proposed in [FM95] for hardware verification. It is an intuitionistic logic endowed with a propositional operation which enables us to specify the propagation of signals along the gates of combinatorial circuits. Dual tableaux presented in this chapter are modifications of the deduction systems presented in [FO95] within the context of relational logics of Chap. 2.

2 Relational Formalization of Intuitionistic Logic

In this section we present the relational formalization of an intuitionistic logic, INT.The vocabulary of INT-language consists of symbols from the following pairwise disjoint sets:

• $\mathbb{V}$– a countable set of propositional variables;

• ¬, ∨, ∧, → } – the set of propositional operations.

The set of INT-formulas is the smallest set including the set $\mathbb{V}$and closed with respect to all the propositional operations.

An INT-model is a structure $\mathcal{M} = (U,R,m)$such that U is a non-empty set of states, R is a reflexive and transitive relation on U, and m is a meaning function such that the following conditions are satisfied:

• m(p) ⊆ U, for every propositional variable $p \in \mathbb{V}$;

• For all s, s′ ∈ U the following heredity condition holds:

  $$\mbox{ (her) \; If $(s,s) \in R$ and $s \in m(p)$, then $s \in m(p)$.}$$

Let $\mathcal{M} = (U,R,m)$be an INT-model and let s ∈ U. Satisfaction of INT-formula ϕ in $\mathcal{M}$by state s, $\mathcal{M},s\models \phi$for short, is defined inductively as follows:

• $\mathcal{M},s\models p$iff s ∈ m(p), for any propositional variable p;

• $\mathcal{M},s\models \neg \phi$iff for every s′ ∈ U, if (s, s′) ∈ R, then $\mathcal{M},s^{\prime}\neq \phi$;

• $\mathcal{M},s\models \phi \vee \psi$iff $\mathcal{M},s\models \phi$or $\mathcal{M},s\models \psi$;

• $\mathcal{M},s\models \phi \wedge \psi$iff $\mathcal{M},s\models \phi$and $\mathcal{M},s\models \psi$;

• $\mathcal{M},s\models (\phi \rightarrow \psi )$iff for every s′ ∈ U, if (s, s′) ∈ R and $\mathcal{M},s\models \phi$, then $\mathcal{M},s\models \psi$.

It is known that the heredity condition holds for every formula ϕ, i.e., if (s, s′) ∈ R and $\mathcal{M},s\models \phi$, then $\mathcal{M},s\models \phi$.

An INT-formula ϕ is said to be true in an INT-model $\mathcal{M} = (U,R,m)$, $\mathcal{M}\models \phi$, whenever for every s ∈ U, $\mathcal{M},s\models \phi$, and it is said to be INT-valid whenever it is true in all INT-models.

In the relational formalization of logic INT we follow the main ideas of the method presented in Sect. 7.4. The vocabulary of the language of the relational logic RL _INT consists of the symbols from the following pairwise disjoint sets:

• ${\mathbb{O}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{INT}}}$– a countable infinite set of object variables;

• ${\mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{INT}}}$– a countable infinite set of relational variables;

• ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{INT}}} =\{ 1,1,R\}$– the set of relational constants;

• $\{-,\cup,\cap,;{,}^{-1}\}$– the set of relational operations.

As in case of modal logics of Sect. 7.4, the constant R represents the accessibility relation from INT-models. Relational terms and formulas of the logic RL _INT are defined as described in Sect. 2.3. The relational variables are intended to represent intuitionistic formulas.

An RL _INT -model is an RL(1, 1′)-model $\mathcal{M} = (U,R,m)$such that the following conditions are satisfied:

• m(P) is a right ideal relation on U, for every $P \in { \mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{INT}}}$;

• R = m(R) is a reflexive and transitive relation on U such that for every $P \in { \mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{INT}}}$and for all x, y, z ∈ U, the following holds:

  $$\mbox{ (her) \, If $(x,y) \in R$ and $(x,z) \in m(P)$, then $(y,z) \in m(P)$.}$$

The translation of INT-formulas into relational terms starts with a one-to-one assignment of relational variables to the propositional variables. Let τ′ be such an assignment. Then the translation τ of formulas is defined inductively:

• τ(p) = τ′(p), for any propositional variable p;

• $\tau (\neg \phi ) = -(R\,;\,\tau (\phi ))$;

• τ(ϕ ∨ ψ) = τ(ϕ) ∪τ(ψ);

• τ(ϕ ∧ ψ) = τ(ϕ) ∩ τ(ψ);

• $\tau (\phi \rightarrow \psi ) = -(R\,;\,(\tau (\phi ) \cap -\tau (\psi )))$.

The translation of atomic INT-formulas cannot be defined as in modal logics (see Sect. 7.4) due to the assumption of heredity. Therefore, in the RL _INT -models relational variables are assumed to be right ideal relations and in the RL _INT -dual tableau the rule (ideal) reflecting this condition is included.

The translation τ is defined so that it preserves validity of formulas.

Proposition 8.2.1.

Let ϕ be an INT-formula. Then for every INT-model $\mathcal{M} = (U,R,m)$ there exists an RL _INT -model $\mathcal{M} = (U,R,m)$ with the same universe and the same relation R as those in $\mathcal{M}$ such that for all s,s′∈ U, $\mathcal{M},s\models \phi$ iff (s,s′) ∈ m′(τ(ϕ)).

Proof.

The proof is similar to the proof of Proposition 7.4.2. Let ϕ be an INT-formula and let $\mathcal{M} = (U,R,m)$be an INT-model. We define an RL _INT -model $\mathcal{M} = (U,R,m)$as follows:

• m′(1) = U ×U;

• m′(1′) is the identity on U;

• m′(τ(p)) = { (x, y) ∈ U ×U : x ∈ m(p)}, for every propositional variable p;

• m′(R) = R;

• m′ extends to all the compound terms as in RL(1, 1′)-models.

The proof is by induction on the complexity of formulas. By way of example, we show the proposition for a compound formula built with the implication operation which has a non-classical semantics in INT-logic.

Let ϕ = ψ → θ and let s′ ∈ U. Then $\mathcal{M},s\models \psi \rightarrow \theta$iff for every t ∈ U, if (s, t) ∈ R and $\mathcal{M},t\models \psi$, then $\mathcal{M},t\models \theta$iff, by the induction hypothesis, for every t ∈ U, if (s, t) ∈ R and (t, s′) ∈ m′(τ(ψ)), then (t, s′) ∈ m′(τ(θ)) iff $(s,s) \in m(-(R\,;\,(\tau (\psi ) \cap -\tau (\theta ))))$iff (s, s′) ∈ m′(τ(ϕ)). □

Proposition 8.2.2.

Let ϕ be an INT-formula. Then for every standard RL _INT -model $\mathcal{M} = (U,R,m)$there exists an INT-model $\mathcal{M} = (U,R,m)$ with the same universe and the same relation R as those in $\mathcal{M}$ such that for all s,s′∈ U, the condition of Proposition 8.2.1 holds.

Proof.

Let ϕ be an INT-formula, let $\mathcal{M} = (U,R,m)$be a standard RL _INT -model. We define an INT-model $\mathcal{M} = (U,R,m)$as follows:

• m(p) = { (x ∈ U : for some y ∈ U, (x, y) ∈ m′(τ(p))}, for every propositional variable p.

Now, the proposition can be proved as Proposition 8.2.1. □

Due to the above propositions we can prove the following (see also Propositions 7.4.4 and 7.4.5):

Proposition 8.2.3.

Let ϕ be an INT-formula. Then for every INT-model $\mathcal{M}$ there exists an RL _INT -model $\mathcal{M}$ such that for any object variables x and y, $\mathcal{M}\models \phi$ iff $\mathcal{M}\models x\tau (\phi )y$ .

Proposition 8.2.4.

Let ϕ be an INT-formula. Then for every standard RL _INT -model $\mathcal{M}$there exists an INT-model $\mathcal{M}$ such that for any object variables x and y, the condition of Proposition 8.2.3 holds.

Finally, from Propositions 8.2.3 and 8.2.4, we get:

Theorem 8.2.1.

For every INT-formula ϕ and for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is INT-valid;

• 2. xτ(ϕ)y is RL _INT -valid.

A dual tableau for the logic RL _INT consists of the axiomatic sets and the rules of dual tableau for RL(1, 1′)-logic adjusted to the language of RL _INT , the rules (ref R) and (tran R) presented in Sects. 6.6 (see also Sect. 7.4) that reflect reflexivity and transitivity of relation R from INT-models, respectively. Furthermore, we have the rules of the following forms:

For every relational variable P and for all object variables x and y,

$$\begin{array}{ll} (\mbox{ rher}) & \frac{xPy} {zRx,xPy\,\vert \,zPy,xPy}\qquad z\mbox{ is any object variable} \\ (\mbox{ ideal})& \frac{xPy} {xPz,xPy}\qquad z\mbox{ is any object variable} \\ \end{array}$$

The rule (rher’) reflects the heredity condition, while the rule (ideal) reflects the fact that every relational variable is interpreted in an RL _INT -model as a right ideal relation. Note that any application of the rules of RL _INT -dual tableau, in particular an application of the specific rules listed above, preserves the formulas built with atomic terms or their complements, and hence the closed branch property holds.

The notions of an RL _INT -set of formulas and correctness of a rule are defined as in Sect. 2.4.

Proposition 8.2.5.

The specific RL _INT -rules are RL _INT -correct.

Proof.

By way of example, we show correctness of the rule (rher’). Correctness of the remaining rules can be proved as in standard modal logics. Let X be a finite set of RL _INT -formulas. Clearly, if X ∪{ xPy} is an RL _INT -set, then so are X ∪{ zRx, xPy} and X ∪{ zPy, xPy}. Now, assume that X ∪{ zRx, xPy} and X ∪{ zPy, xPy} are RL _INT -sets and suppose X ∪{ xPy} is not an RL _INT -set. Then there exist an RL _INT -model $\mathcal{M} = (U,R,m)$and a valuation v in $\mathcal{M}$such that for every ϕ ∈ X ∪{ xPy} $\mathcal{M},v\neq \phi$, which implies (v(x), v(y)) ∉ m(P). By the assumption, $\mathcal{M},v\models zRx$and $\mathcal{M},v\models zPy$. Thus, (v(z), v(x)) ∈ R and (v(z), v(y)) ∈ m(P). Then, by the condition (her’), (v(x), v(y)) ∈ m(P), a contradiction. □

It is easy to see that all the remaining rules of RL _INT -dual tableau are RL _INT -correct and all the RL _INT -axiomatic sets are RL _INT -sets.

The notions of an RL _INT -proof tree, a closed branch of such a tree, a closed RL _INT -proof tree, and RL _INT -provability are defined as in Sect. 2.4.

A branch b of an RL _INT -proof tree is complete whenever it is either closed or it satisfies the completion conditions of RL(1, 1′)-dual tableau and the following completion conditions determined by the rules specific for the RL _INT -dual tableau:

For every relational variable P and for all object variables x and y,

Cpl(rher’) If xPy ∈ b, then for every object variable z, either zRx ∈ b or zPy ∈ b, obtained by an application of the rule (rher’);Cpl(ideal) If xPy ∈ b, then for every object variable z, xPz ∈ b, obtained by an application of the rule (ideal).

The notions of a complete RL _INT -proof tree and an open branch of an RL _INT -proof tree are defined as in RL-logic (see Sect. 2.5).

The branch structure ${\mathcal{M}}^{b} = ({U}^{b},{R}^{b},{m}^{b})$is defined in a standard way, that is m ^b(Q) = { (x, y) ∈ U ^b ×U ^b : xQy ∉ b}, for every $Q \in { \mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{INT}}} \cup \{ R\}$, and R ^b = m ^b(R). The completion conditions enable us to show that R ^b satisfies all the conditions assumed in RL _INT -models. Therefore, the following holds:

Proposition 8.2.6 (Branch Model Property).

For every open branch b of an RL _INT -proof tree, ${\mathcal{M}}^{b}$ is an RL _INT -model.

Proof.

We show that ${\mathcal{M}}^{b}$satisfies the condition (her’) and every relational variable P is interpreted in ${\mathcal{M}}^{b}$as a right ideal relation. Assume that (x, y) ∈ R ^b and (x, z) ∈ m ^b(P), that is xRy ∉ b and xPz ∉ b. Suppose (y, z) ∉ m ^b(P), that is yPz ∈ b. Then, by the completion condition Cpl(rher’), either xRy ∈ b or xPz ∈ b, a contradiction. Hence, ${\mathcal{M}}^{b}$satisfies the condition (her’). Now, assume that (x, y) ∈ m ^b(P), that is xPy ∉ b. Suppose that for some z ∈ U ^b, (x, z) ∉ m ^b(P). Then xPz ∈ b and by the completion condition Cpl(ideal), xPy ∈ b, a contradiction. Therefore, for every relational variable P, m ^b(P) is a right ideal relation on U ^b. □

Since branch model ${\mathcal{M}}^{b}$is defined in a standard way, the satisfaction in branch model property can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7).

Proposition 8.2.7 (Satisfaction in Branch Model Property).

For every open branch b of an RL _INT -proof tree and for every RL _INT -formula ϕ, if ${\mathcal{M}}^{b},{v}^{b}\models \phi$ , then ϕ∉b.

Hence, the completeness of RL _INT -dual tableau follows.

Theorem 8.2.2 (Soundness and Completeness of RL _INT ).

Let ϕ be an RL _INT -formula. Then the following conditions are equivalent:

• 1. ϕ is RL _INT -valid;

• 2. ϕ is true in all standard RL _INT -models;

• 3. ϕ is RL _INT -provable.

By the above theorem and Theorem 8.2.1, we obtain:

Theorem 8.2.3 (Relational Soundness and Completeness of INT).

Let ϕ be an INT-formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is INT-valid;

• 2. x(τ(ϕ))y is RL _INT -provable.

Example.

Consider the following INT-formula ϕ:

$$\phi = \neg p \rightarrow (p \rightarrow t).$$

The translation of this formula into RL _INT -term is:

$$\tau (\phi ) = -(R\,;\,(-(R\,;\,P) \cap --(R\,;\,(P \cap -T)))),$$

where τ(p) = P and τ(t) = T. INT-validity of ϕ is equivalent to RL _INT -provability of the formula xτ(ϕ)y. Figure 8.1 presents its RL _INT -proof.

3 Relational Formalization of Minimal Intuitionistic Logic

Minimal intuitionistic logic J was introduced by Johansson in [Joh36]. It differs from the intuitionistic logic INT in that the formula ¬ϕ → (ϕ → ψ) is not a theorem of the logic. The language of the logic J is the same as INT-language. However, these logics differ in semantics. A J-model is a structure $\mathcal{M} = (U,R,Q,m)$such that the following conditions are satisfied:

Fig. 8.1

An RL _INT -proof of the formula ¬p → (p → t)

• (U, R, m) is an INT-model;

• Q ⊆ U is such that for every s ∈ U, if s ∈ Q and (s, s′) ∈ R, then s′ ∈ Q.

The satisfaction of a J-formula ϕ in a J-model $\mathcal{M}$by a state s ∈ U is defined as in INT-logic except for the clause for negated formulas:

$$\mathcal{M},s\models \neg \psi \mbox{ iff for all }s \in U,\mbox{ if }(s,s) \in R,\mbox{ then }\mathcal{M},s\neq \psi \mbox{ or }s \in Q.$$

Intuitively, Q is thought of as the set of those states which are inconsistent.

The language of the relational logic RL _J is an RL _INT -language with the following set of relational constants: ${\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{ \mathsf{J}}} =\{ 1,1,R,Q\}$.

An RL _J -model is an RL _INT -model $\mathcal{M} = (U,R,Q,m)$such that the following conditions are satisfied:

• (Q1) Q is a right ideal relation on U;

• (Q2) If (x, z) ∈ Q and (x, y) ∈ R, then (y, z) ∈ Q, for all x, y, z ∈ U.

The translation τ from J-formulas into relational terms coincides with the translation of INT-formulas defined in Sect. 8.2 except for the translation of negated formulas:

$$\tau (\neg \phi )\stackrel{\mathrm{df}}{=}-(R\,;\,(\tau (\phi ) \cap -Q)).$$

Following the method of proving Theorem 8.2.1, we can prove:

Theorem 8.3.1.

For every J-formula ϕ and for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is J-valid;

• 2. xτ(ϕ)y is RL _J -valid.

A dual tableau for the logic RL _J consists of the axiomatic sets and the rules of dual tableau for RL _INT -logic presented in Sect. 8.2 adjusted to the language of RL _J and in addition the rules of the following forms:

For all object variables x and y,

$$\begin{array}{ll} (\mbox{ r}Q1)& \frac{xQy} {xQz,xQy}\qquad z\mbox{ is any object variable} \\ (\mbox{ r}Q2)& \frac{xQy} {zQy,xQy\,\vert \,zRx,xQy}\qquad z\mbox{ is any object variable} \\ \end{array}$$

The above rules reflect the properties of relation Q assumed in RL _J -models. As in RL _INT -dual tableau, any application of the rules listed above preserves the formulas built with atomic terms or their complements, and hence the closed branch property holds.

Proposition 8.3.1.

The RL _J -rules are RL _J -correct.

Proof.

By way of example, we prove correctness of the rule (rQ2). Correctness of the other rules can be proved as in standard modal logics. Let X be any finite set of RL _J -formulas. Clearly, if X ∪{ xQy} is an RL _J -set, then so are X ∪{ zQy, xQy} and X ∪{ zRx, xQy}. Now, assume that X ∪{ zQy, xQy} and X ∪{ zRx, xQy} are RL _J -sets. Suppose X ∪{ xQy} is not an RL _J -set. Then there exist an RL _J -model $\mathcal{M} = (U,R,Q,m)$and a valuation v in $\mathcal{M}$such that for every ϕ ∈ X ∪{ xQy} $\mathcal{M},v\neq \phi$, which implies (v(x), v(y)) ∉ m(Q). By the assumption, $\mathcal{M},v\models zQy$and $\mathcal{M},v\models zRx$. Thus, (v(z), v(y)) ∈ Q and (v(z), v(x)) ∈ R. By property (Q2) assumed in RL _J -models, (v(x), v(y)) ∈ Q, a contradiction. Therefore, the rule (rQ2) is RL _J -correct. □

The completion conditions determined by the rules (rQ1) and (rQ2) are:

For all object variables x and y, Cpl(rQ1) If xQy ∈ b, then for every object variable z, xQz ∈ b;Cpl(rQ2) If xQy ∈ b, then for every object variable z, either zQy ∈ b or zRx ∈ b.

The branch model is defined in a standard way, i.e., m ^b(T) = { (x, y) ∈ U ^b ×U ^b : xTy ∉ b}, for every $T \in \mathbb{R}\mathbb{V}_{\mathsf{RL}_{\mathsf{J}}} \cup \{ R,Q\}$. The relation Q ^b satisfies all the conditions assumed in RL _J -models, therefore we have:

Proposition 8.3.2 (Branch Model Property).

For every open branch b of an RL _J -proof tree, ${\mathcal{M}}^{b}$ is an RL _J -model.

Proof.

We show that Q ^b is well defined. It can be easily proved that Q ^b is a right ideal relation on U ^b. Now, assume that (x, z) ∈ Q ^b and (x, y) ∈ R ^b, that is xQz ∉ b and xRy ∉ b. Suppose (y, z) ∉ Q ^b, that is yQz ∈ b. Then, by the completion condition Cpl(rQ2), either xQz ∈ b or xRy ∈ b, a contradiction. □

Satisfaction in branch model property can be proved as in RL(1, 1′)-logic, hence we get:

Theorem 8.3.2 (Soundness and Completeness of RL _J ).

Let ϕ be an RL _J -formula. Then the following conditions are equivalent:

• 1. ϕ is RL _J -valid;

• 2. ϕ is true in all standard RL _J -models;

• 3. ϕ is RL _J -provable.

By the above theorem and Theorem 8.3.1, we have:

Theorem 8.3.3 (Relational Soundness and Completeness of J).

Let ϕ be a J-formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is J-valid;

• 2. x(τ(ϕ))y is RL _J -provable.

Example.

Consider the following J-formula ϕ:

$$\phi = p \rightarrow \neg \neg p.$$

The translation of ϕ into an RL _J -term is:

$$\tau (\phi ) = -(R\,;\,(P \cap --(R\,;\,(-(R\,;\,(P \cap -Q)) \cap -Q)))),$$

where τ(p) = P. J-validity of ϕ is equivalent to RL _J -provability of the formula xτ(ϕ)y. Figure 8.2 presents its RL _J -proof.

In the previous section we constructed an RL _INT -proof for the formula ϕ = ¬p → (p → t) which showed its INT-validity. This formula is not J-valid. Its translation into RL _J -term is:

$$\tau (\phi ) = -(R\,;\,(-(R\,;\,(P \cap -Q)) \cap --(R\,;\,(P \cap -T)))),$$

where τ(p) = P and τ(t) = T. Since ϕ is not J-valid, any RL _J -proof tree must not close. Figure 8.3 presents an RL _J -proof tree of xτ(ϕ)y in which there is a branch that cannot be closed. Consider the node (B) in that tree which consists of the following formulas: x − Rz, z − Rw, w − Py, wTy, α − Qy, z(R ; (P ∩ − Q))y, where a variable α is arbitrary. The only decomposition rule that can be applied to node (B) is the rule (; ), which generates, among others, a node consisting of the same formulas as (B) and a formula β − Qy, where β may be an arbitrary variable. We can observe that no application of the rule (; ) would close the branch. Also, no application of a specific rule would close the branch. The rules (1′1) and (1′2) can be applied only to the formula wTy. As the result we obtain a node that consists of the same formulas as node (B) and the formula y1′β or w1′β. Since node (B) does not contain a formula built with the complement of 1′, the branch can be closed neither by an application of the rule (1′1) nor (1′2). The rules (ref R) and (tran R) cannot be applied to the node (B), because it does not contain a formula built with the atomic term R. Similarly, the rules (rQ1) and (rQ2) cannot be applied. The rules (rher’) and (ideal) can be applied only to the formula wTy. However, observe that any application of the rule (rher’) generates a node consisting of the same formulas as (B) together with the formula βTy. It is easy to see that it cannot close the branch. In a similar way, one can show that the same holds for the rule (ideal). Thus, the branch cannot be closed.

Fig. 8.2

An RL _J -proof of the formula p → ¬ ¬p

Fig. 8.3

A failed proof search of the formula ¬p → (p → t)

4 Relational Formalization of Some Intermediate Logics

Intermediate logics are the logics whose valid formulas include all the formulas that are valid in intuitionistic logic but not necessarily all the tautologies of classical propositional logic. In that sense, intermediate logics are between intuitionistic and classical logic. The common language of intermediate logics is the INT-language.

In this section we consider two intermediatelogics $\mathsf{IN{T}_{\mathsf{{L}_{1}}}}$and $\mathsf{IN{T}_{\mathsf{{L}_{2}}}}$whose models are the INT-models satisfying the following conditions, respectively:

• (L1 ) ∀x ∀y ∀z ∀t[((x, y) ∈ R ∧ (x, z) ∈ R ∧ (y, t) ∈ R) → ((y, z) ∈ R ∨ (z, y) ∈ R ∨ (z, t) ∈ R)];

• (L2 ) ∀x ∀y ∀z[((x, y) ∈ R ∧ (x, z) ∈ R) → ∃t((y, t) ∈ R ∧ (z, t) ∈ R)].

The specific axioms of the logics $\mathsf{IN{T}_{\mathsf{{L}_{1}}}}$and $\mathsf{IN{T}_{\mathsf{{L}_{2}}}}$in their Hilbert-style axiomatizations are:

• (A1) [( ¬ ¬ϕ → ϕ) → ( ¬ϕ ∨ ϕ)] → ( ¬ϕ ∨ ¬ ¬ϕ);

• (A2) ¬ϕ ∨ ¬ ¬ϕ.

$\mathsf{IN{T}_{\mathsf{{L}_{1}}}}$is referred to as Scott’s logic and $\mathsf{IN{T}_{\mathsf{{L}_{2}}}}$is the logic of weak excluded middle.

The common language of a relational logic ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$for an intermediate logic L ∈ {L ₁, L ₂} is the RL _INT -language. Models of ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$satisfy all the conditions assumed in INT _L-models for the accessibility relation R and (L ₁) or (L ₂), respectively. The translation of INT _L-formulas into relational terms is defined as for INT-formulas in Sect. 8.2. To obtain dual tableaux for these logics, we add to RL _INT -dual tableau the rules reflecting the specific semantic conditions that are assumed in their models. The specific rules reflecting the conditions (L ₁) and (L ₂) have the following forms:

For all object variables x, y, z, and t,

$$\begin{array}{ll} (r\mathsf{{L}_{1}})& \frac{yRz,zRy,zRt} {xRy,yRz,zRy,zRt\,\vert \,xRz,yRz,zRy,zRt\,\vert \,yRt,yRz,zRy,zRt} \\ (r\mathsf{{L}_{2}})& \frac{} {xRy\,\vert \,xRz\,\vert \,y- (R\,;\, {R}^{-1 } )z} \\ \end{array}$$

The above rules have the property of preserving formulas built with atomic terms or their complements. Hence, the closed branch property holds. An alternative form of rule (rL ₂) is discussed in Sect. 25.9.

Theorem 8.4.1 (Correspondence).

Let $\mathcal{K}$ be a class of RL _INT -models and let i ∈{1,2}. Then, ${\mathcal{K}}$ is a class of ${\mathsf{RL}}_{{\mathsf{INT}}_{\mathsf{{L}_{ i}}}}$ -models iff the rule (r L _i) is $\mathcal{K}$-correct.

Proof.

• ( → ) By way of example, we show it for $\mathsf{i} \,= \,1$. Let $\mathcal{K}$be a class of ${\mathsf{RL } }_{{\mathsf{INT}}_{\mathsf{{L}_{ 1}}}}$-models, that is every model from ${\mathcal{K}}$satisfies the condition (L ₁ ). Let X be a finite set of RL _INT -formulas. Clearly, if X ∪{ yRz, zRy, zRt} is a $\mathcal{K}$-set, then so are X ∪{ xRy, yRz, zRy, zRt}, X ∪{ xRz, yRz, zRy, zRt}, and X ∪{ yRt, yRz, zRy, zRt}. Assume X ∪{ xRy, yRz, zRy, zRt}, X ∪{ xRz, yRz, zRy, zRt}, and X ∪{ yRt, yRz, zRy, zRt} are $\mathcal{K}$-sets. Suppose X ∪{ yRz, zRy, zRt} is not a $\mathcal{K}$-set. Then there exist an ${\mathsf{RL } }_{{\mathsf{INT}}_{\mathsf{{L}_{ 1}}}}$-model $\mathcal{M} = (U,R,m)$and a valuation v in $\mathcal{M}$such that for every ϕ ∈ X ∪{ yRz, zRy, zRt}, $\mathcal{M},v\neq \phi$, in particular, (v(y), v(z)) ∉ R, (v(z), v(y)) ∉ R, and (v(z), v(t)) ∉ R. However, by the assumption, model $\mathcal{M}$and valuation v satisfy (v(x), v(y)) ∈ R, (v(x), v(z)) ∈ R, and (v(y), v(t)) ∈ R. By the condition (L ₁ ), it means that either (v(y), v(z)) ∈ R or (v(z), v(y)) ∈ R or (v(z), v(t)) ∈ R, a contradiction.

• ( ← ) By way of example, we show it for i = 2. Let $\mathcal{K}$be a class of RL _INT -models. Assume the rule (rL ₂ ) is $\mathcal{K}$-correct. Let $X\stackrel{\mathrm{df}}{=}\{x-Ry,x-Rz,y(R\,;\,{R}^{-1})z\}$. Clearly, the sets X ∪{ xRy}, X ∪{ xRz}, and $X \cup \{ y-(R\,;\,{R}^{-1})z\}$are $\mathcal{K}$-sets. Thus, by the assumption, X must be a $\mathcal{K}$-set. Therefore, for every model $\mathcal{M} = (U,R,m)$from $\mathcal{K}$and for all x, y, z ∈ U, if (x, y) ∈ R and (x, z) ∈ R, then (y, z) ∈ R ; R ^{− 1}. Since (y, z) ∈ R ; R ^{− 1} is equivalent to ∃t((y, t) ∈ R and (z, t) ∈ R), $\mathcal{K}$is a class of ${\mathsf{RL } }_{{\mathsf{INT}}_{\mathsf{{L}_{ 2}}}}$-models. □

The completion conditions determined by the rules (rL ₁) and (rL ₂) are:

For all object variables x, y, z, and t,

Cpl(rL ₁) If the formulas yRz, zRy, and zRt are in b, then either xRy ∈ b or xRz ∈ b or yRt ∈ b;Cpl(rL ₂) Either xRy ∈ b or xRz ∈ b or $y-(R\,;\,{R}^{-1})z \in b$.

In order to prove completeness, we need to show that the branch structure is an ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$-model, for L ∈ {L ₁, L ₂}.

Proposition 8.4.1 (Branch Model Property).

Let L ∈{L ₁ , L ₂} and let b be an open branch of an ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$-proof tree. Then, ${\mathcal{M}}^{b}$is an ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$-model.

Proof.

It suffices to show that if ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$-dual tableau includes a rule (rL _i), then ${\mathcal{M}}^{b}$satisfies the condition (L _i), for i ∈ {1,2}. By way of example, we show it for i = 2. Indeed, by the completion condition Cpl(rL ₂), for all x, y, z ∈ U ^b, either xRy ∈ b or xRz ∈ b or $y-(R\,;\,{R}^{-1})z \in b$. Thus, by the completion conditions Cpl(; ) and Cpl(${-}^{-1}$), for all x, y, z ∈ U ^b, either xRy ∈ b or xRz ∈ b or there exists t ∈ U ^b such that y − Rt ∈ b and z − Rt ∈ b. So (x, y) ∉ R ^b or (x, z) ∉ R ^b or there exists t ∈ U ^b such that (y, t) ∈ R ^b and (z, t) ∈ R ^b. Therefore, for all x, y, z ∈ U ^b, if (x, y) ∈ R ^b and (x, z) ∈ R ^b, then there exists t ∈ U ^b such that (y, t) ∈ R ^b and (z, t) ∈ R ^b, hence the condition (L ₂) is satisfied. □

Since the language of the logics ${\mathsf{RL}}_{{\mathsf{INT}}_{\mathsf{{L}_{ 1}}}}$and ${\mathsf{RL}}_{{\mathsf{INT}}_{\mathsf{{L}_{ 2}}}}$is the same as in RL _INT -logic, the satisfaction in branch model property holds. Thus, the proof of completeness is similar as in RL _INT -logic.

Theorem 8.4.2 (Soundness and Completeness of ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$).

Let L ∈{L ₁ , L ₂} and let ϕ be an ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$-formula. Then the following conditions are equivalent:

• 1. ϕ is ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$ -valid;

• 2. ϕ is true in all standard ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$ -models;

• 3. ϕ is ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$ -provable.

Theorem 8.4.3 (Relational Soundness and Completeness of INT _L).

Let L ∈{L ₁ L ₂} and let ϕ be an INT _L -formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is INT _L-valid;

• 2. x(τ(ϕ))y is ${\mathsf{RL}}_{\mathsf{IN{T}_{L}}}$ -provable.

Example.

Consider the following ${\mathsf{INT}}_{{\mathsf{L}}_{2}}$-formula:

$$\phi = \neg p \vee \neg \neg p.$$

The translation of ϕ into ${\mathsf{RL}}_{{\mathsf{INT}}_{{\mathsf{L}}_{ 2}}}$-term is:

$$\tau (\phi ) = -(R\,;\,P) \cup -(R\,;\,-(R\,;\,P)),$$

where τ(p) = P. ${\mathsf{INT}}_{{\mathsf{L}}_{ 2}}$-validity of ϕ is equivalent to ${\mathsf{RL}}_{{\mathsf{INT}}_{{\mathsf{L}}_{ 2}}}$-provability of the formula xτ(ϕ)y. Figure 8.4 presents its ${\mathsf{RL}}_{{\mathsf{INT}}_{{\mathsf{L}}_{ 2}}}$-proof.

5 Relational Formalization of a Logic for Hardware Verification

In this section we consider a propositional logic PLL which has been proposed as a tool for a formal verification of computer hardware (see [FM95, Men90, Men93]).

Fig. 8.4

An ${\mathsf{RL}}_{{\mathsf{INT}}_{{\mathsf{L}}_{ 2}}}$-proof of the formula ¬p ∨ ¬ ¬p

The logic PLL is obtained from the logic INT by endowing its language with a unary propositional operation ○ that models a delay of propagation of signals. Signals are conceived as Boolean valued functions, where Boolean values are denoted by 1 and 0. To input and output signals of the gates we assign propositional variables. If p is such a variable, then truth of p in a model is interpreted as ‘p is stable at 1”, truth of ¬p means “p is stable at 0’, truth of ○ p means ‘p is going to stabilize to 1’, and truth of ○ ¬p means ‘p is going to stabilize to 0’.

A PLL-model is a structure $\mathcal{M} = (U,R,S,m)$such that (U, R, m) is an INT-model and S is a reflexive and transitive relation on U such that S ⊆ R. Then, the satisfaction of formulas of the form ○ ϕ is defined as follows: $\mathcal{M},s\models \bigcirc \phi \mbox{ iff for every }s \in U,\mbox{ if }(s,s) \in R,$then there exists t ∈ U such that $(s,t) \in S\mbox{ and }\mathcal{M},t\models \phi$.

The language of the relational logic RL _PLL is the language of RL _INT -logic endowed with the relational constant S.

An RL _PLL -model is a structure $\mathcal{M} = (U,R,S,m)$such that (U, R, m) is an RL _INT -model and S is a reflexive and transitive relation on U satisfying S ⊆ R.

The translation τ from PLL-formulas into relational terms is defined as the translation in Sect. 8.2 with the following clause for formulas of the form ○ ϕ:

$$\tau (\bigcirc \phi )\stackrel{\mathrm{df}}{=}-(R\,;\,-(S\,;\,(\tau (\phi )))).$$

Much the same as we proved Theorem 8.2.1, we can show:

Theorem 8.5.1.

For every PLL-formula ϕ and for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is PLL-valid;

• 2. xτ(ϕ)y is RL _PLL -valid.

A dual tableau for the logic RL _PLL consists of the axiomatic sets and the rules of dual tableau for RL _INT -logic (see Sect. 8.2) adjusted to the language of RL _PLL , the rules (ref S) and (tran S) reflecting reflexivity and transitivity of S, respectively (see Sect. 6.6), and in addition the rule (SR) of the following form:

For all object variables x and y,

$$(SR)\quad \frac{xRy} {xSy,xRy}$$

The above rule reflects the condition S ⊆ R. The rule (SR) preserves formulas built with atomic terms. Hence, the closed branch property holds. It is easy to see that the rule (SR) is RL _PLL -correct.

Proposition 8.5.1.

The RL _PLL -rules are RL _PLL -correct.

The completion condition determined by the rule (SR) is:

For all object variables x and y, Cpl(SR) If xRy ∈ b, then xSy ∈ b.

The branch model is defined in a standard way, that is m ^b(T) = { (x, y) ∈ U ^b ×U ^b : xTy ∉ b}, for every $T \in { \mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{PLL}}} \cup \{ R,S\}$.

Proposition 8.5.2 (Branch Model Property).

For every open branch b of an RL _PLL -proof tree, ${\mathcal{M}}^{b}$ is an RL _PLL -model.

Proof.

It suffices to show that S ^b satisfies all the conditions assumed in RL _PLL -models. Reflexivity and transitivity of S ^b can be proved as in Theorem 6.6.1. Now, assume that (x, y) ∈ S ^b, that is xSy ∉ b. Suppose (x, y) ∉ R ^b, that is xRy ∈ b. Then, by the completion condition Cpl(SR), we get xSy ∈ b, a contradiction. Hence, ${\mathcal{M}}^{b}$is an RL _PLL -model. □

Since the branch model ${\mathcal{M}}^{b}$is defined in a standard way (see Sect. 2.6, p. 43), the satisfaction in branch model property can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7). Hence, completeness of RL _PLL -dual tableau follows.

Theorem 8.5.2 (Soundness and Completeness of RL _PLL ).

Let ϕ be an RL _PLL -formula. Then the following conditions are equivalent:

• 1. ϕ is RL _PLL -valid;

• 2. ϕ is true in all standard RL _PLL -models;

• 3. ϕ is RL _PLL -provable.

By the above theorem and Theorem 8.5.1, we have:

Fig. 8.5

An RL _PLL -proof of the formula p → ○ p

Theorem 8.5.3 (Relational Soundness and Completeness of PLL).

Let ϕ be a PLL-formula. Then for all object variables x and y, the following conditions are equivalent:

• 1. ϕ is PLL-valid;

• 2. x(τ(ϕ))y is RL _PLL -provable.

Example.

Consider the following PLL-formula:

$$\phi = p \rightarrow \bigcirc p.$$

The translation of ϕ into RL _PLL -term is:

$$\tau (\phi ) = -(R\,;\,(P \cap --(R\,;\,-(S\,;\,P)))),$$

where τ(p) = P. PLL-validity of ϕ is equivalent to RL _PLL -provability of the formula xτ(ϕ)y. Figure 8.5 presents its RL _PLL -proof.