Dual Tableau for Propositional Logic with Identity

Abstract

In this chapter we consider propositional logic with identity, referred to as SCI (Sentential Calculus with Identity) introduced in [Sus68]. It is two-valued as the classical logic, but it rejects the main assumption of Frege’s philosophy that the meaning of a sentence is its logical value. Non-fregean logics are based on the principle that denotations of sentences of a given language are different from their truth values. SCI is obtained from the classical propositional logic by endowing its language with an operation of identity, $\equiv$,and the axioms which say that formula φ ≡ ψ is interpreted as ‘φ has the same denotation as ψ’. Identity axioms together with two-valuedness imply that the set of denotations of sentences has at least two elements. Any other assumptions about the range of sentences or properties of the identity operation lead to axiomatic extensions of SCI. In general, the identity operation is different from the equivalence operation, that is two sentences with the same truth values may have different denotations. If we add (φ ↔ ψ) ≡ (φ ≡ ψ) to the set of SCI axioms, then we obtain the classical propositional logic, where the identity and equivalence operations are indistinguishable. In this way the Fregean axiom can be formulated in SCI. Some extensions of SCI are known to correspond to modal logics S4 and S5 and to the three-valued Łukasiewicz logic (see [Sus71a]). Decidability of the logic SCI is proved in [Sus71c].

1 Introduction

In this chapter we consider propositional logic with identity, referred to as SCI (Sentential Calculus with Identity) introduced in [Sus68]. It is two-valued as the classical logic, but it rejects the main assumption of Frege’s philosophy that the meaning of a sentence is its logical value. Non-fregean logics are based on the principle that denotations of sentences of a given language are different from their truth values. SCI is obtained from the classical propositional logic by endowing its language with an operation of identity, $\equiv$,and the axioms which say that formula φ ≡ ψ is interpreted as ‘φ has the same denotation as ψ’. Identity axioms together with two-valuedness imply that the set of denotations of sentences has at least two elements. Any other assumptions about the range of sentences or properties of the identity operation lead to axiomatic extensions of SCI. In general, the identity operation is different from the equivalence operation, that is two sentences with the same truth values may have different denotations. If we add (φ ↔ ψ) ≡ (φ ≡ ψ) to the set of SCI axioms, then we obtain the classical propositional logic, where the identity and equivalence operations are indistinguishable. In this way the Fregean axiom can be formulated in SCI. Some extensions of SCI are known to correspond to modal logics S4 and S5 and to the three-valued Łukasiewicz logic (see [Sus71a]). Decidability of the logic SCI is proved in [Sus71c].

Non-fregean logics were an inspiration for some other logical systems. In the paper [BS73] it is indicated that Lindenbaum algebras, obtained by the Tarski–Lindenbaum method and further developed by Rasiowa and Sikorski, are too weak for studying some logical systems. For example, propositional logics with identity and the first-order non-fregean logics are not algebraizable in the Rasiowa–Sikorski style. This fact inspired an introduction of abstract logics in [BS73], aimed at generalizing of the concept of a logical system. Many ideas from the paper [BS73] have been studied within the theory of abstract algebraic logics.

Basic definitions and main results concerning non-fregean logics can be found in [Sus71c, BS72, Sus73, Sus72], and [GPH05], among others.

2 A Propositional Logic with Identity

The vocabulary of the language of the non-fregean propositional logic, SCI, consists of the symbols from the following pairwise disjoint sets:

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

• $\{\neg, \vee, \wedge, \rightarrow, \leftrightarrow, \equiv \}$– the set of propositional operations of negation ¬, disjunction ∨, conjunction ∧, implication →, equivalence ↔, and identity $\equiv$.

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

An SCI -modelis a structure $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$, where Uis a non-empty set, Dis any non-empty subset of U, and ∼, ⊔, ⊓, ⇒, ⇔, ∘ are operations on Uwith arities 1, 2, 2, 2, 2, 2, respectively, such that:

For all a, b∈ U,

(SCI1) ∼ a∈ Diff a∉ D;

(SCI2) a⊔ b∈ Diff a∈ Dor b∈ D;

(SCI3) a⊓b∈ Diff a∈ Dand b∈ D;

(SCI4) a⇒ b∈ Diff a∉ Dor b∈ D;

(SCI5) a⇔ b∈ Diff a∈ Diff b∈ D;

(SCI6) a∘ b∈ Diff a= b.

Let $\mathcal{M}$be an SCI-model. A valuation in $\mathcal{M}$is any mapping $v: \mathbb{V} \rightarrow U$. A valuation vextends homomorphically to all the formulas:

v( ¬φ) = ∼ v(φ);

v(φ ∨ ψ) = v(φ) ⊔ v(ψ);

v(φ ∧ ψ) = v(φ) ⊓v(ψ);

v(φ → ψ) = v(φ) ⇒ v(ψ);

v(φ ↔ ψ) = v(φ) ⇔ v(ψ);

v(φ ≡ ψ) = v(φ) ∘ v(ψ).

Let vbe a valuation in an SCI-model $\mathcal{M}$. An SCI-formula φ is satisfied by vin $\mathcal{M}$, $\mathcal{M},v\models \varphi$, whenever v(φ) ∈ D. An SCI-formula φ is true in $\mathcal{M}$if it is satisfied by all valuations in $\mathcal{M}$. A formula is SCI-valid if it is true in all SCI-models.

The logic SCI is two valued. We may define the logical value of a formula φ in a model $\mathcal{M}$as:

$$va{l}_{\mathcal{M}}(\varphi )\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} \mbox{ true} &\quad \mbox{ if for every $v$ in $\mathcal{M},v(\varphi ) \in D$ }\\ \mbox{ false} &\quad \mbox{ otherwise } \end{array} \right.$$

The following proposition shows that SCI is extensional in the sense that any subformula ψ of an SCI-formula φ can be replaced with another formula $\mathit{\vartheta}$denoting the same as ψ without affecting the denotation of φ.

Proposition 23.2.1.

Let $\mathcal{M}$ be anSCI -model, let v be a valuation in $\mathcal{M}$ , let φ be anSCI -formula containing a subformula ψ, and let φ′ be the result of replacing some occurrences of ψ in φ by a formula $\mathit{\vartheta}$ . Then, $\mathcal{M},v\models \psi \equiv \mathit{\vartheta}$ implies $\mathcal{M},v\models \varphi \equiv \varphi \prime$ .

Proof.

The proof is by induction on the complexity of formulas. Let φ be a propositional variable pand let $\mathit{\vartheta}$be an SCI-formula. Then pis the only subformula of φ and, clearly, if $v(p) = v(\mathit{\vartheta})$, then the proposition holds. In what follows φ(ψ) denotes a formula φ with a subformula ψ, $\mathit{\vartheta}$denotes any formula such that $v(\psi ) = v(\mathit{\vartheta})$, and φ′denotes a formula resulting from φ by replacing some occurrences of ψ with $\mathit{\vartheta}$.

Let φ(ψ) = ¬ϕ. Then ψ is a subformula of ϕ and v( ¬ϕ(ψ)) = ∼ v(ϕ(ψ)). By the induction hypothesis, $v(\phi (\psi )) = v(\phi (\mathit{\vartheta}))$, hence $\sim v(\phi (\psi )) = \sim v(\phi (\mathit{\vartheta}))$. Therefore v(φ) = v(φ′).

Let φ(ψ) = (ϕ₁∨ ϕ₂). Then ψ is a subformula of ϕ₁or ϕ₂. Without loss of generality, we may assume that ψ is a subformula of ϕ₁. Then, v(ϕ₁(ψ) ∨ ϕ₂) = v(ϕ₁(ψ)) ⊔ v(ϕ₂). By the induction hypothesis, $v({\phi }_{1}(\psi )) = v({\phi }_{1}(\mathit{\vartheta}))$, hence $v({\phi }_{1}(\psi )) \sqcup v({\phi }_{2}) = v({\phi }_{1}(\mathit{\vartheta})) \sqcup v({\phi }_{2})$. Therefore, v(φ) = v(φ′).

Let φ(ψ) = (ϕ₁≡ ϕ₂). Then, ψ is a subformula of ϕ₁or ϕ₂. Without loss of generality, we may assume that ψ is a subformula of ϕ₁. Then, v(ϕ₁(ψ) ≡ ϕ₂) = v(ϕ₁(ψ)) ∘ v(ϕ₂). By the induction hypothesis, $v({\phi }_{1}(\psi )) = v({\phi }_{1}(\mathit{\vartheta}))$, hence $v({\phi }_{1}(\psi )) \circ v({\phi }_{2}) = v({\phi }_{1}(\mathit{\vartheta})) \circ v({\phi }_{2}) = v({\phi }_{1}(\mathit{\vartheta}) \equiv {\phi }_{2})$. Therefore v(φ) = v(φ′).

The proofs of the remaining cases are similar. □

A Hilbert-style axiomatization of SCI consists of the axioms of the classical propositional logic PC, which characterize the operations ¬, ∨, ∧, →, ↔, and the following axioms for the identity operation $\equiv$:

(${\equiv }_{1}$)  φ ≡ φ;

(${\equiv }_{2}$) (φ ≡ ψ) → ( ¬φ ≡ ¬ψ);

(${\equiv }_{3}$) (φ ≡ ψ) → (φ → ψ);

(${\equiv }_{4}$) $[(\varphi \equiv \psi ) \wedge (\mathit{\vartheta} \equiv \xi )] \rightarrow [(\varphi \#\mathit{\vartheta}) \equiv (\psi \#\xi )]$, for $\# \in \{\vee, \wedge, \rightarrow, \leftrightarrow, \equiv \}$.

The only rule of inference is modus ponens. Clearly, all the SCI-axioms are true in every SCI-model. It is known that they provide a complete axiomatization of logic SCI.

Fact 23.2.1.

For everyPC -formula φ, the following conditions are equivalent:

• 1. φ isPC -valid;

• 2. φ isSCI -valid.

Note also that the reduct (U, ∼, ⊔, ⊓) of an SCI-model is not necessarily a Boolean algebra, for example a⊓b= b⊓ais not true in all SCI-models. Consider an SCI-model $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$, where U= { 0, 1, 2}, D= { 1, 2}, and the operations ∼, ⊔, ⊓, ⇒, ⇔, ∘ are defined by:

$\sim a\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a\neq 0$}\\ 1 &\quad \mbox{ otherwise} \end{array} \right.$

$a\sqcup b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a = 0$ and $b = 0$}\\ 1 &\quad \mbox{ otherwise} \end{array} \right.$

$a\sqcap b\mathrm{df} \over =\left \{\begin{array}{ll} 0&\quad \mbox{ if $a = 0$ or $b = 0$}\\ 1 &\quad \mbox{ if $b = 2$ and $a\neq 0$} \\ 2&\quad \mbox{ otherwise } \end{array} \right.$

$a \Rightarrow b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a\neq 0$ and $b = 0$}\\ 1 &\quad \mbox{ otherwise} \end{array} \right.$

$a \Leftrightarrow b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a\neq 0,b = 0$ or $a = 0,b\neq 0$}\\ 1 &\quad \mbox{ otherwise} \end{array} \right.$

$a\circ b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0 &\quad \mbox{ if $a\neq b$}\\ a &\quad \mbox{ if $a = b$ and $a\neq 0$} \\ 1 &\quad \mbox{ otherwise } \end{array} \right.$

This structure is an SCI-model. Indeed, the following hold:

• ∼ a∈ Diff a= 0 iff a∉ D;

• a⊔ b∈ Diff a≠0 or b≠0 iff a∈ Dor b∈ D;

• a⊓b∈ Diff a≠0 and b≠0 iff a∈ Dand b∈ D;

• a⇒ b∈ Diff a= 0 or b≠0 iff a∉ Dor b∈ D;

• a⇔ b∈ Diff either $a = b = 0$or a≠0≠biff a∈ Diff b∈ D;

• a∘ b∈ Diff a= b.

However, we have 2 ⊓1 = 2, while 1 ⊓2 = 1. Hence, a⊓b= b⊓ais not true in this model.

3 Axiomatic Extensions of the Propositional Logic with Identity

The class of all different SCI-theories is uncountable. Therefore, the question of natural extensions of SCI arises. Let Xbe a set of SCI-formulas. The axiomatic extension of SCI, SCI^X, is the logic obtained from SCI by adding formulas of Xto SCI-axioms. There are three natural and extensively studied axiomatic extensions of SCI, the logics SCI^B, SCI^T, and SCI^H.

LogicSCI ^B

The specific axioms of this logic are:

(B1) $[(\varphi \wedge \psi ) \vee \mathit{\vartheta}] \equiv [(\psi \vee \mathit{\vartheta}) \wedge (\varphi \vee \mathit{\vartheta})]$;

(B2) $[(\varphi \vee \psi ) \wedge \mathit{\vartheta}] \equiv [(\psi \wedge \mathit{\vartheta}) \vee (\varphi \wedge \mathit{\vartheta})]$;

(B3) $[\varphi \vee (\psi \wedge \neg \psi )] \equiv \varphi$;

(B4) $[\varphi \wedge (\psi \vee \neg \psi )] \equiv \varphi$;

(B5) (φ → ψ) ≡ ( ¬φ ∨ ψ);

(B6) (φ ↔ ψ) ≡ [(φ → ψ) ∧ (ψ → φ)].

An SCI ^B -model is an SCI-model $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$such that Dis an ultrafilter on (U, ∼, ⊔, ⊓) and for all a, b∈ U, a∘ b∈ Diff a= b. Any axiomatic extension of SCI which includes SCI^Bis referred to as a Boolean SCI-logic.

In [Sus71a] the following was proved:

Theorem 23.3.1.

ForeverySCI -formula φ, thefollowingconditionsareequivalent:

• 1. φ is true in allSCI ^B -models;

• 2. φ is provable in SCI ^B.

LogicSCI ^T

The logic SCI ^T is an extension of SCI ^B with the following axiom:

(T) φ ≡ ψ, for all formulas φ and ψ such that φ ↔ ψ is provable in SCI.

This logic has many interesting properties (see [Sus71a]). Below we list some of them:

Proposition 23.3.1.

• 1. The set of allSCI T -provable formulas is the smallest set ofSCI ^B -provable formulas closed on the Gödel rule:

  $$(G)\quad \frac{\varphi, \psi } {\varphi \equiv \psi }$$

• 2. The set of all SCI ^T -provable formulas is the smallest set of SCI -provable formulas closed on the quasi-Fregean rule:

  $$(QF)\quad \frac{(\varphi \leftrightarrow \psi )} {\varphi \equiv \psi }$$

An SCI^T-model is an SCI^B-model $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$such that:

For all a, b, c, d, e∈ U,

• a∘ a= e⊔ ∼ e;

• [(a∘ b) ⇒ (a⇔ b)] = e⊔ ∼ e;

• [[(a∘ b) ⊓(c∘ d)] ⇒ [(a#c) ∘ (b#d)]] = e⊔ ∼ e, for #∈ { ⊔, ⊓, ∘ }.

In [Sus71c] the following was proved:

Theorem 23.3.2.

​For everySCI -formula φ, the following conditions are equivalent:

• 1. φ is true in allSCI ^T -models;

• 2. φ is provable in SCI ^T.

Furthermore, the following was observed:

Theorem 23.3.3.

• 1. Let $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$ be anSCI ^T -model. Then, the structure (U,∼,⊔,⊓,I), where a unary operation I on U is defined as I(a)\stackrel{df }{=}a ∘ (a⊔∼ a), for every a ∈ U, is a topological Boolean algebra, i.e., I is an interior operation.

• 2. Let $\mathcal{T} = (U,\sim, \sqcup, \sqcap, I)$ be a topological Boolean algebra. Then, the structure $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$ such that ⇒ and ⇔ are operations on U satisfying the conditions of SCI -models and, in addition, for all a,b ∈ U, a ∘ b\stackrel{df }{=}I(a ⇔ b) and D is an ultrafilter on U such that a ∘ b ∈ D if and only if a = b, is an SCI ^T -model.

LogicSCI ^H

The logic SCI ^H is an extension of SCI ^B with the following axioms:

(H1) 1 ≡ (φ ∨ ¬φ);

(H2) 0 ≡ (φ ∧ ¬φ);

(H3) (φ ≡ ψ) ≡ [(φ ≡ ψ) ≡ 1];

(H4) $\neg (\varphi \equiv \psi ) \equiv [(\varphi \equiv \psi ) \equiv 0]$,

where 1 and 0 are propositional constants defined as p∨ ¬pand p∧ ¬p, respectively.

An SCI^H-model is an SCI^B-model $\mathcal{M}\,=\,(U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$such that 1 and 0 are the greatest and the smallest element, respectively, of the Boolean algebra (U, ∼, ⊔, ⊓), and the following is satisfied:

$$a\circ b = \left \{\begin{array}{ll} 1&\quad \mbox{ if $a = b$}\\ 0 &\quad \mbox{ otherwise } \end{array} \right.$$

It is easy to see that the operation Idefined as I(a)\stackrel{df} = }}a∘ 1 has the property:

$$I(a) = \left \{\begin{array}{ll} 1&\quad \mbox{ if $a = 1$}\\ 0 &\quad \mbox{ otherwise} \end{array} \right.$$

Theorem 23.3.4.

• 1. Let $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$ be anSCI H -model. Then, the structure (U,∼,⊔,⊓,I), where I is an interior operation on U defined as above, is a topological Boolean algebra with only two open elements;

• 2. Let $\mathcal{H} = (U,\sim, \sqcup, \sqcap, I)$ be a topological Boolean algebra with only two open elements. Then, the structure $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$ such that ⇒ and ⇔ are operations on U satisfying the conditions of SCI -models and, in addition, for all a,b ∈ U, $a\circ b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 1&\quad \mbox{ if $I(a) = I(b)$}\\ 0 &\quad \mbox{ otherwise }\end{array} \right.$ , and D is an ultrafilter on U such that a ∘ b ∈ D if and only if a = b, is anSCI ^H -model.

Theorem 23.3.5.

For everySCI -formula φ, the following conditions are equivalent:

• 1. φ is true in allSCI ^H -models;

• 2. φ is provable in SCI ^H.

There are some relationships between logics SCI^Tand SCI^Hand the modal logics S4 and S5, respectively (see Sect. 7.3).

Let σ be a mapping from the set of SCI-formulas into the set of modal formulas defined inductively as follows:

• σ(p) = p, for every propositional variable p;

• σ(φ) = φ, if $\equiv$does not occur in φ;

• σ(φ ≡ ψ) = [R](σ(φ) ↔ σ(ψ)), where Ris an accessibility relation of modal logics.

The following is known (see [Sus71a]):

Proposition 23.3.2.

For everySCI -formula φ, the following hold:

• 1. φ is true in allSCI ^T -models iff σ(φ) isS4 -valid;

• 2. φ is true in allSCI ^H -models iff σ(φ) isS5 -valid.

Now, consider a mapping σ′from the set of modal formulas into the set of SCI-formulas. The function σ′is defined inductively as follows:

• σ′(p) = p, for every propositional variable p;

• σ′(φ) = φ, if [R] does not occur in φ;

• σ′([R]φ) = (σ′(φ) ≡ (σ′(φ) ∨ ¬σ′(φ))).

The following was proved in [Sus71a]:

Proposition 23.3.3.

For every modal formula φ the following hold:

• 1. φ isS4 -valid iff σ′(φ) is true in all SCI ^T -models;

• 2. φ isS5 -valid iff σ′(φ) is true in all SCI ^H -models.

4 Dual Tableau for the Propositional Logic with Identity

A dual tableau for the logic SCI, developed in [GP07], consists of decomposition rules ( ∨ ), ( ∧ ), ( ¬ ∨ ), ( ¬ ∧ ), ( → ), ( ¬ → ), ( ↔ ), ( ¬ ↔ ), ( ¬) of F-dual tableau (see Sect. 1.3) adjusted to the SCI-language and, in addition, the specific rule:

$$(\equiv )\ \frac{\varphi (\psi )} {\psi \equiv \mathit{\vartheta},\varphi (\psi )\;\vert \;\varphi (\mathit{\vartheta}),\varphi (\psi )}$$

where φ and $\mathit{\vartheta}$are SCI-formulas, ψ is a subformula of φ, and $\varphi (\mathit{\vartheta})$is obtained from φ(ψ) by replacing some occurrences of ψ with $\mathit{\vartheta}$.

Observe that any application of the rules of SCI-dual tableau, in particular an application of the specific rule ($\equiv$), preserves atomic formulas and their negations. Thus, the closed branch property holds.

A finite set of formulas is SCI-axiomatic whenever it includes either of the sets of the following forms:

For any SCI-formula φ,

$$\begin{array}{l} \mbox{ (Ax1)}\quad \{\varphi \equiv \varphi \}; \\ \mbox{ (Ax2)}\quad \{\varphi, \neg \varphi \}\\ \end{array}$$

A finite set Xof SCI-formulas is said to be an SCI-set whenever for every SCI-model $\mathcal{M}$and for every valuation vin $\mathcal{M}$there exists φ ∈ Xsuch that $\mathcal{M},v\models \varphi$. Correctness of a rule is defined in a similar way as in F-logic in Sect. 1.3.

Proposition 23.4.1.

• 1. TheSCI -rules are SCI -correct;

• 2. The SCI -axiomatic sets areSCI -sets.

Proof.

By way of example, we prove correctness of the rule ($\equiv$). Let Xbe a finite set of SCI-formulas and let φ(ψ) be an SCI-formula. Clearly, if X∪{ φ(ψ)} is an SCI-set, then so are $X \cup \{ \psi \equiv \mathit{\vartheta},\varphi (\psi )\}$and $X \cup \{ \varphi (\mathit{\vartheta}),\varphi (\psi )\}$. Assume that $X \cup \{ \psi \equiv \mathit{\vartheta},\varphi (\psi )\}$and $X \cup \{ \varphi (\mathit{\vartheta}),\varphi (\psi )\}$are SCI-sets. Suppose X∪{ φ(ψ)} is not an SCI-set. Then there exist an SCI-model $\mathcal{M}$and a valuation vin $\mathcal{M}$such that for every formula χ ∈ X∪{ φ(ψ)}, $\mathcal{M},v\nvDash \chi$. By the assumption, $\mathcal{M},v\models \psi \equiv \mathit{\vartheta}$and $\mathcal{M},v\models \varphi (\mathit{\vartheta})$, that is $v(\psi ) = v(\mathit{\vartheta})$and $v(\varphi (\mathit{\vartheta})) \in D$. Hence, by Proposition 23.2.1, v(φ(ψ)) ∈ D. Thus $\mathcal{M},v\models \varphi (\psi )$, a contradiction. □

The notions of an SCI-proof tree, a closed branch of such a tree, a closed SCI-proof tree, and SCI-provability are defined in a similar way as in Sect. 1.3.

A branch bof an SCI-proof tree is complete whenever it satisfies the completion conditions that correspond to decomposition rules (see Sect. 1.3) and the completion condition that correspond to the rule ($\equiv$) specific for SCI-dual tableau:

Cpl($\equiv$) If φ ∈ band ψ is a subformula of φ, then for every SCI-formula $\mathit{\vartheta}$, either $\psi \equiv \mathit{\vartheta} \in b$or $\varphi (\mathit{\vartheta}) \in b$.

The notions of a complete SCI-proof tree and an open branch of an SCI-proof tree are defined as in Sect. 1.3.

We define inductively a depthof SCI-formulas as:

For all SCI-formulas φ and ψ,

• $d(p) = d(\varphi \equiv \psi ) = 0$, for every $p \in \mathbb{V}$;

• $d(\neg \varphi ) = d(\varphi ) + 1$;

• $d(\varphi \vee \psi ) = d(\varphi \wedge \psi ) = d(\varphi \rightarrow \psi ) = d(\varphi \leftrightarrow \psi ) =\max (d(\varphi ),d(\psi )) + 1$.

Let ${\mathbb{F}\mathbb{R}}_{\mathrm{SCI}}$be a set of all SCI-formulas and let n≥ 0. By ${\mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n}$we denote the set of all SCI-formulas of the depth n.

Let bbe an open branch of an SCI-proof tree. We define a branch structure ${\mathcal{M}}^{b} = ({U}^{b},{\sim }^{b},{\sqcup }^{b},{\sqcap }^{b},{\Rightarrow }^{b},{\Leftrightarrow }^{b},{\circ }^{b},{D}^{b})$as:

• ${U}^{b} ={ \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}$;

• D ^b= ⋃ _{n∈ ω} D _n ^b, where:

  • ${D}_{0}^{b} =\{ \psi \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{0} : \psi \not\in b\}$,

  • ${D}_{n+1}^{b} = {X}_{1} \cup \ldots \cup {X}_{5}$, where:

    • ${X}_{1} =\{ \neg \psi \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n+1} : \psi \not\in {D}_{n}^{b}\}$,

    • ${X}_{2} =\{ \psi \vee \theta \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n+1} : \psi \in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\mbox{ or }\theta \in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\}$,

    • ${X}_{3} =\{ \psi \wedge \theta \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n+1} : \psi, \theta \in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\}$;

    • ${X}_{4} =\{ \psi \rightarrow \theta \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n+1} : \psi \not\in {\bigcup \nolimits }_{k<n}{D}_{k}^{b}\mbox{ or }\theta \in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\}$;

    • ${X}_{5} =\{ \psi \leftrightarrow \theta \in { \mathbb{F}\mathbb{R}}_{\mathrm{SCI}}^{n+1} : \psi, \theta \in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\mbox{ or }\psi, \theta \not\in {\bigcup \nolimits }_{k\leq n}{D}_{k}^{b}\}$;

• ∼ ^bψ = ¬ψ;

• ψ ⊔ ^bθ = (ψ ∨ θ);

• ψ ⊓^bθ = (ψ ∧ θ);

• ψ ⇒ ^bθ = (ψ → θ);

• ψ ⇔ ^bθ = (ψ ↔ θ);

• ψ ∘ ^bθ = (ψ ≡ θ).

Fact 23.4.1.

Let ψ be anSCI -formula and let d(ψ) = n, for some n ≥ 0. Then, ψ ∈ D ^b if and only if ψ ∈ D _n ^b .

Let v ^bbe a valuation in ${\mathcal{M}}^{b}$such that v ^b(p) = p, for all $p \in \mathbb{V}$. By the definition of ${\mathcal{M}}^{b}$, v ^b(φ) = φ, for every SCI-formula φ.

Proposition 23.4.2.

Let b be an open branch of anSCI -proof tree. Then, for everySCI -formula ψ, if ψ ∈ D ^b , then ψ∉b.

Proof.

The proof is by induction on the depth of formulas. For formulas of the depth 0, the proposition holds by the definition of the set D ^b. Let ψ = ¬θ, for some formula θ such that d(θ) = 0. Assume ψ ∈ D ₁ ^b. By the definition of D ^b, θ ∉ D ₀ ^b, thus θ ∈ b. Hence, ¬θ ∉ b, and so ψ ∉ b.

Suppose the proposition holds for all formulas of depth not greater than nand their negations. Assume $d(\psi ) = n + 1$and ψ ∈ D _{n+ 1} ^b.

• Let ψ = θ ∨ χ for some formulas θ and χ such that max(d(θ), d(χ)) = n. Since ψ ∈ D _{n+ 1} ^b, θ ∈ ⋃ _{k≤ n} D _k ^bor χ ∈ ⋃ _{k≤ n} D _k ^b. By the induction hypothesis, θ ∉ bor χ ∉ b. Suppose ψ ∈ b. The completion condition Cpl( ∨ ) implies both ψ ∈ band θ ∈ b, a contradiction.

• Let ψ = ¬ ¬χ. Then ¬χ ∉ D _n ^b. Suppose ψ ∈ b. By the completion condition Cpl( ¬), χ ∈ b. By the induction hypothesis, χ ∉ D _{n− 1} ^b. By the definition of the set D ^b, if a formula χ of the depth n− 1 satisfies χ ∉ D _{n− 1} ^b, then ¬χ ∈ D _n ^b, a contradiction.

• Let ψ = ¬(θ ∨ χ). Then (θ ∨ χ) ∉ D _n ^b. Suppose ¬(θ ∨ χ) ∈ b. By the completion condition Cpl( ¬ ∨ ), either ¬θ ∈ bor ¬χ ∈ b. By the induction hypothesis, either ¬θ ∉ D ^bor ¬χ ∉ D ^b. Therefore, either θ ∈ D ^bor χ ∈ D ^b. So by the construction of the set D ^b, we have (θ ∨ χ) ∈ D _n ^b, a contradiction.

The proofs of the remaining cases are similar. □

Let us define the relation R _∘on the set of SCI-formulas as:

$$(\psi, \theta ) \in {R}_{\circ }\stackrel{\mathrm{df}}{\Longleftrightarrow}(\psi \circ \theta ) \in {D}^{b}.$$

Proposition 23.4.3.

For every open branch b of anSCI -proof tree, R _∘ is an equivalence relation on the set U ^b .

Proof.

If for some ψ ∈ U ^b, (ψ, ψ) ∉ R _∘, then ψ ≡ ψ ∈ b, which would mean that bis closed, a contradiction. Let (ψ, θ) ∈ R _∘and suppose that (θ, ψ) ∉ R _∘. Then (ψ ≡ θ) ∉ band (θ ≡ ψ) ∈ b. By the completion condition Cpl($\equiv$), (ψ ≡ θ) ∈ bor (θ ≡ θ) ∈ b. The first case contradicts (ψ ≡ θ) ∉ b, the second one implies that the branch is closed, a contradiction. Let (ψ, θ) ∈ R _∘, (θ, χ) ∈ R _∘, and suppose that (ψ, χ) ∉ R _∘. Then, (ψ ≡ θ) ∉ b, (θ ≡ χ) ∉ b, and $(\psi \equiv \chi ) \in b$. By the completion condition Cpl($\equiv$), either (ψ ≡ θ) ∈ bor (θ ≡ χ) ∈ b, a contradiction. □

Let bbe an open branch of an SCI-proof tree. We define the quotient structure ${\mathcal{M}}_{q}^{b} = ({U}_{q}^{b},{\sim }_{q}^{b},{\sqcup }_{q}^{b},{\sqcap }_{q}^{b},{\circ }_{q}^{b},{D}_{q}^{b})$as:

• ${U}_{q}^{b} =\{\| \psi \| : \psi \in {U}^{b}\}$, where $\|\psi \|$is the equivalence class of R _∘generated by ψ;

• ${D}_{q}^{b} =\{\| \psi \| : \psi \in {D}^{b}\}$;

• ${\sim }_{q}^{b}\|\psi \| =\|{ \sim }^{b}\psi \|$;

• $\|\psi \| {\sqcup }_{q}^{b}\|\theta \| =\| \psi {\sqcup }^{b}\theta \|$;

• $\|\psi \| {\sqcap }_{q}^{b}\|\theta \| =\| \psi {\sqcap }^{b}\theta \|$;

• $\|\psi \| {\Rightarrow }_{q}^{b}\|\theta \| =\| \psi {\Rightarrow }^{b}\theta \|$;

• $\|\psi \| {\Leftrightarrow }_{q}^{b}\|\theta \| =\| \psi {\Leftrightarrow }^{b}\theta \|$;

• $\|\psi \| {\circ }_{q}^{b}\|\theta \| =\| \psi {\circ }^{b}\theta \|$.

Let v _q ^bbe a valuation such that ${v}_{q}^{b}(p) =\| p\|$, for every $p \in \mathbb{V}$.

Proposition 23.4.4 (Branch Model Property).

• (1) The structure ${\mathcal{M}}_{q}^{b}$ is anSCI -model;

• (2) For everySCI -formula φ, v ^b (φ) ∈ D ^b iff v _q ^b (φ) ∈ D _q ^b.

Proof.

We show that the model ${\mathcal{M}}_{q}^{b}$satisfies all the conditions of SCI-models. D _q ^bis a non-empty subset of U _q ^b, since D ^bis a non-empty subset of U ^b. Indeed, D ^bis non-empty, since for every SCI-formula ψ, a formula ψ ≡ ψ ∉ b, hence ψ ≡ ψ ∈ D ^b.

Let ψ, θ ∈ U ^band let max(d(ψ), d(φ)) = n, n≥ 0. Then, the following hold:

^bψ ∈ D ^biff ¬ψ ∈ D ^biff for some n, ψ ∉ D _n ^biff ψ ∉ D ^b;

ψ ⊔ ^bθ ∈ D ^biff (ψ ∨ θ) ∈ D ^biff ψ ∈ ⋃ _{k≤ n} D _k ^bor θ ∈ ⋃ _{k≤ n} D _k ^biff ψ ∈ D ^bor θ ∈ D ^b;

ψ ⊓^bθ ∈ D ^biff (ψ ∧ θ) ∈ D ^biff ψ, θ ∈ ⋃ _{k≤ n} D _k ^biff ψ ∈ D ^band θ ∈ D ^b;

ψ ⇒ ^bθ ∈ D ^biff (ψ → θ) ∈ D ^biff ψ ∉ ⋃ _{k< n} D _k ^bor θ ∈ ⋃ _{k≤ n} D _k ^biff ψ ∉ D ^bor θ ∈ D ^b;

ψ ⇔ ^bθ ∈ D ^biff (ψ ↔ θ) ∈ D ^biff ψ, θ ∈ ⋃ _{k≤ n} D _k ^bor ψ, θ ∉ ⋃ _{k≤ n} D _k ^biff ψ ∈ D ^bif and only if θ ∈ D ^b.

The above properties together with the definition of ${\mathcal{M}}_{q}^{b}$and Proposition 23.4.3imply: ${\sim }_{q}^{b}\|\psi \| \in {D}_{q}^{b}\mbox{ iff }{\sim }^{b}\psi \in {D}^{b}\mbox{ iff }\psi \not\in {D}^{b}\mbox{ iff }\|\psi \|\not\in {D}_{q}^{b}$;

$\|\psi \| {\sqcup }_{q}^{b}\|\theta \| \in {D}_{q}^{b}\mbox{ iff }\psi \in {D}^{b}\mbox{ or }\theta \in {D}^{b}\mbox{ iff }\|\psi \| \in {D}_{q}^{b}\mbox{ or }\|\theta \| \in {D}_{q}^{b}$;

$\|\psi \| {\sqcap }_{q}^{b}\|\theta \| \in {D}_{q}^{b}\mbox{ iff }\psi \in {D}^{b}\mbox{ and }\theta \in {D}^{b}\mbox{ iff }\|\psi \| \in {D}_{q}^{b}\mbox{ and }\|\theta \| \in {D}_{q}^{b}$;

$\|\psi \| {\Rightarrow }_{q}^{b}\|\theta \| \in {D}_{q}^{b}\mbox{ iff }\psi \not\in {D}^{b}\mbox{ or }\theta \in {D}^{b}\mbox{ iff }\|\psi \|\not\in {D}_{q}^{b}\mbox{ or }\|\theta \| \in {D}_{q}^{b}$;

$\|\psi \| {\Leftrightarrow }_{q}^{b}\|\theta \| \in {D}_{q}^{b}\mbox{ iff }\psi \not\in {D}^{b}\mbox{ iff }\theta \in {D}^{b}\mbox{ iff }\|\psi \| \in {D}_{q}^{b}\mbox{ iff }\|\theta \| \in {D}_{q}^{b}$;

$\|\psi \| {\circ }_{q}^{b}\|\theta \| \in {D}_{q}^{b}\mbox{ iff }\|\psi {\circ }^{b}\theta \| \in {D}_{q}^{b}\mbox{ iff }\psi {\circ }^{b}\theta \in {D}^{b}\mbox{ iff }(\psi, \theta ) \in {R}_{\circ }\mbox{ iff }\|\psi \| =\| \theta \|$.

Thus, ${\mathcal{M}}_{q}^{b}$is an SCI-model.

(2) follows directly from the definition of D _q ^b. □

By Propositions 23.4.2and 23.4.4, we have:

Proposition 23.4.5.

Let b be an open branch of anSCI -proof tree. Then, for everySCI -formula φ, if ${\mathcal{M}}_{q}^{b},{v}_{q}^{b}\models \varphi$ , then φ∉b.

Theorem 23.4.1 (Soundness and Completeness of SCI).

Let φ be anSCI -formula. Then the following conditions are equivalent:

• (1) φ isSCI -valid;

• (2) φ isSCI -provable.

Proof.

The implication (1) → (2) holds by Proposition 23.4.1. Now, assume that φ is SCI-valid. Suppose there is no any closed SCI-proof tree for φ. Then, there exists a complete SCI-proof tree for φ with an open branch, say b. Since φ ∈ b, by Proposition 23.4.5, we get ${\mathcal{M}}_{q}^{b}\nvDash \varphi$. Hence, by Proposition 23.4.4, φ is not SCI-valid, a contradiction. □

Example.

We show that all SCI-axioms characterizing $\equiv$are SCI-provable.

Clearly, the axiom $({\equiv }_{1})$of the form $\varphi \equiv \varphi$is SCI-provable, since $\{\varphi \equiv \varphi \}$is an SCI-axiomatic sets. In Figs. 23.1and 23.2we present SCI-proofs of axiom $({\equiv }_{2})$and axiom $({\equiv }_{3})$, respectively.

Figure 23.3presents an SCI-proof of (${\equiv }_{4}$), for any $\# =\{ \vee, \wedge, \rightarrow, \leftrightarrow, \equiv \}$.

Fig. 23.1

An SCI-proof of SCI-axiom (${\equiv }_{2}$)

Fig. 23.2

An SCI-proof of SCI-axiom (${\equiv }_{3}$)

5 Dual Tableaux for Axiomatic Extensions of the Propositional Logic with Identity

In Sect. 23.3axiomatic extensions SCI^Tand SCI^Hof the logic SCI were presented. By Proposition 23.3.2, an SCI-formula φ is true in all SCI^T-models (resp. SCI^H-models) if and only if σ(φ) is S4-valid (resp. S5-valid), where σ is the translation of SCI-formulas into modal formulas defined in Sect. 23.3.

Fig. 23.3

An SCI-proof of SCI-axiom (${\equiv }_{4}$)

On the other hand, in Sects. 7.4 and 7.5 we showed that S4-validity (resp. S5-validity) of a modal formula ψ is equivalent to RL_S4-provability (resp. RL_S5-provability) of the translation of ψ, τ(ψ), into a relational formula defined in Sect. 7.4 (see Theorem 7.4.1, p. 147).

We can define a translation of SCI-formulas into relational terms of standard modal logics by χ(φ)\stackrel{df} = }}τ(σ(φ)). Let χ′be a one-to-one assignment of relational variables to the propositional variables. Then, the translation χ of SCI-formulas is defined inductively as:

• χ(p) = χ′(p) ; 1, for any propositional variable $p \in \mathbb{V}$;

• $\chi (\neg \varphi ) = -\chi (\varphi )$;

• χ(φ ∨ ψ) = χ(φ) ∪χ(ψ);

• χ(φ ∧ ψ) = χ(φ) ∩ χ(ψ);

• $\chi (\varphi \rightarrow \psi ) = -\chi (\varphi ) \cup \chi (\psi )$;

• $\chi (\varphi \leftrightarrow \psi ) = (-\chi (\varphi ) \cup \chi (\psi )) \cap (-\chi (\psi ) \cup \chi (\varphi )))$;

• $\chi (\varphi \equiv \psi ) = -(R\,;\,-\chi (\varphi \leftrightarrow \psi ))$.

By Proposition 23.3.2and Theorem 7.4.1, an SCI-formula φ is true in all SCI^T-models (resp. SCI^H-models) if and only if χ(φ) is RL_S4-provable (resp. RL_S5-provable).

Theorem 23.5.1.

For everySCI -formula φ and for all object variables x and y, the following conditions are equivalent:

• 1. φ is true in allSCI ^T -models (resp.SCI ^H -models);

• 2. xχ(φ)y is RL _S4 -provable (resp. RL _S5 -provable).

It follows that RL_S4-dual tableau (resp. RL_S5-dual tableau) can be used as a dual tableau to verify SCI^T-validity (resp. SCI^H-validity) of SCI-formulas.

Example.

Consider SCI-formulas φ and ψ:

$$\varphi = (p \vee \neg p) \equiv (q \vee \neg q);\qquad \psi = (p \wedge \neg p) \equiv (q \wedge \neg q).$$

These formulas are not SCI-valid. Indeed, let $\mathcal{M} = (U,\sim, \sqcup, \sqcap, \Rightarrow, \Leftrightarrow, \circ, D)$, be an SCI-model such that U= { 0, 1, 2, 3}, D= { 2, 3}, and the operations ∼, ⊔, ⊓, ⇒, ⇔, ∘ are defined as:

$\sim a\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a = 2$}\\ 1 &\quad \mbox{ if $a = 3$} \\ 2&\quad \mbox{ if $a = 0$}\\ 3 &\quad \mbox{ if $a = 1$}\\ \end{array} \right.$ $a\circ b\stackrel{\mathrm{df}}{=}\left \{\begin{array}{ll} 0&\quad \mbox{ if $a\neq b$}\\ 3 &\quad \mbox{ otherwise} \end{array} \right.$

a⊔ b\stackrel{df} = }}max(a, b) a⊓b\stackrel{df} = }}min(a, b)

a⇒ b\stackrel{df} = }}max( ∼ a, b) a⇔ b\stackrel{df} = }}min(max( ∼ a, b), max( ∼ b, a))

Fig. 23.4

An RL_S5-proof of SCI^H-validity of SCI-formula (p∨ ¬p) ≡ (q∨ ¬q)

Fig. 23.5

An RL_S5-proof of SCI^H-validity of SCI-formula (p∧ ¬p) ≡ (q∧ ¬q)

This structure is an SCI-model. Let vbe a valuation in $\mathcal{M}$such that v(p) = 0 and v(q) = 3. Then:

$$\begin{array}{rcl} & v(p \vee \neg p) = 2\ \mbox{ and}\ v(p \wedge \neg p) = 0;& \\ & v(q \vee \neg q) = 3\ \mbox{ and}\ v(q \wedge \neg q) = 1.& \\ \end{array}$$

Therefore, v((p∨ ¬p) ≡ (q∨ ¬q)) = 0 and v((p∧ ¬p) ≡ (q∧ ¬q)) = 0. Hence, φ and ψ are not true in $\mathcal{M}$. However, by Theorem 23.3.4, formulas φ and ψ are true in all SCI^H-models. The translations of these formulas into relational terms are:

$\chi (\varphi )\stackrel{\mathrm{df}}{=}-(R\,;\,-((-(P \cup -P) \cup (Q \cup -Q)) \cap (-(Q \cup -Q) \cup (P \cup -P))))$;

$\chi (\psi )\stackrel{\mathrm{df}}{=}-(R\,;\,-((-(P \cap -P) \cup (Q \cap -Q)) \cap (-(Q \cap -Q) \cup (P \cap -P))))$,

where χ′(p) = Pand χ′(q) = Q. Figures 23.4and 23.5present an RL_S5-proof of χ(φ) and χ(ψ), respectively, which by Theorem 23.5.1show that φ and ψ are true in all SCI^H-models.