Signed Dual Tableau for Gödel–Dummett Logic

Abstract

In 1933 Kurt Gödel [Göd33] introduced a family of finitely many-valued propositional logics. His goal was to show that the intuitionistic logic cannot be characterized by a finite matrix. Dummett in [Dum59] generalized them to infinite-valued logics and presented their complete Hilbert-style axiomatization. It consists of the axioms of the intuitionistic propositional logic and the linearity axiom (φ → ψ) ∨ (ψ → φ). It is known that the set of tautologies of these logics is the same for any infinite set of truth values. Kripke-style semantics for these logics is determined by the intuitionistic Kripke models which are linearly ordered. The logic LC is an intersection of the sets of tautologies of all finite-valued Gödel logics. Gödel–Dummett logics have many applications both in logic and in computer science. Logic LC is employed in the investigations of the provability logic of the intuitionistic arithmetic [Vis82] and relevant logics [DM71]. It is applied to the foundations of logic programming [Pea99] and also it is considered as one of the most important fuzzy logics [Háj98].

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In 1933 Kurt Gödel [Göd33] introduced a family of finitely many-valued propositional logics. His goal was to show that the intuitionistic logic cannot be characterized by a finite matrix. Dummett in [Dum59] generalized them to infinite-valued logics and presented their complete Hilbert-style axiomatization. It consists of the axioms of the intuitionistic propositional logic and the linearity axiom (φ → ψ) ∨ (ψ → φ). It is known that the set of tautologies of these logics is the same for any infinite set of truth values. Kripke-style semantics for these logics is determined by the intuitionistic Kripke models which are linearly ordered. The logic LC is an intersection of the sets of tautologies of all finite-valued Gödel logics. Gödel–Dummett logics have many applications both in logic and in computer science. Logic LC is employed in the investigations of the provability logic of the intuitionistic arithmetic [Vis82] and relevant logics [DM71]. It is applied to the foundations of logic programming [Pea99] and also it is considered as one of the most important fuzzy logics [Háj98].

This chapter presents a signed dual tableau decision procedure for logic LC developed in [AK01]. Two signs T (True) and F (False) are used. There is an analogy between signed dual tableaux and relational dual tableaux. In relational dual tableaux there are decomposition rules determined by all the relational operations and by their Boolean complements. In signed dual tableaux every operation of a logic in question determines two rules applicable to formulas built with that operation and endowed with signs T and F, respectively. They are the counterparts to the positive and complemented occurrence of the term in a relational formula which is a translation of the formula from the original language of the logic. The method of proving completeness of signed dual tableaux is also analogous to the completeness proofs of relational dual tableaux. It involves constructing a branch structure and proving the branch model property and the satisfaction in branch model property. However, in the case of signed formulas the satisfaction in branch model property involves two cases, namely, satisfaction of formulas signed with T and F, respectively. Following this method, completeness for the LC-dual tableau is proved in the present chapter.

2 Gödel–Dummett Logic

The language of the logic LC is that of the intuitionistic logic, that is its vocabulary consists of symbols from the following pairwise disjoint sets:

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

• { ∨, ∧, → } – the set of propositional operations;

• { ⊥ } – the set consisting of the propositional constant interpreted as falsity.

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

An LC -model is a structure:

$$\mathcal{M} = (N \cup \{ \omega \},\leq, v)$$

such that N is the set of natural numbers, ω ∉ N, ω is the greatest element of N ∪{ ω}, ≤ is the natural ordering of N, and $v: \mathbb{V} \cup \{\perp \}\rightarrow N \cup \{ \omega \}$ is a valuation such that:

• v(p) ∈ N ∪{ ω}, for every propositional variable p;

• v( ⊥ ) = 0;

valuation v extends to all the LC-formulas as follows:

• v(φ ∨ ψ) = max(v(φ), v(ψ));

• v(φ ∧ ψ) = min(v(φ), v(ψ));

• $v(\varphi \rightarrow \psi ) = \left \{\begin{array}{ll} \omega &\quad \mbox{ if $v(\varphi ) \leq v(\psi )$}\\ v(\psi ) &\quad \mbox{ otherwise} \end{array} \right .$

As usual in the intuitionistic logic, negation is definable as ¬φ $\stackrel{df} {=}$ φ → ┴.

An LC-formula φ is said to be true in an LC-model $\mathcal{M} = (N \cup \{ \omega \},\leq, v)$, $\mathcal{M}\models \varphi$, whenever v(φ) = ω, and it is LC-valid whenever it is true in all LC-models.

3 Signed Dual Tableau Decision Procedure for Gödel–Dummett Logic

Rules of a dual tableau for Gödel–Dummett logic apply to signed formulas which are obtained from LC-formulas by prefixing them with the signs T or F. We extend valuations in LC-models to signed formulas as follows:

• v(T(φ)) = ω iff v(φ) = ω;

• v(F(φ)) = ω iff v(φ)≠ω.

Decomposition rules have the following forms:

For all LC-formulas φ, ψ, φ₁, φ₂, ψ₁ and ψ₂,

$$\begin{array}{llll} (\mathbf{T}\vee ) & \frac{\mathbf{T}(\varphi \vee \psi )} {\mathbf{T}(\varphi ),\mathbf{T}(\psi )} & (\mathbf{F}\vee ) & \frac{\mathbf{F}(\varphi \vee \psi )} {\mathbf{F}(\varphi )\,\vert \,\mathbf{F}(\psi )} \\ (\mathbf{T}\wedge ) & \frac{\mathbf{T}(\varphi \wedge \psi )} {\mathbf{T}(\varphi )\,\vert \,\mathbf{T}(\psi )} & (\mathbf{F}\wedge ) & \frac{\mathbf{F}(\varphi \wedge \psi )} {\mathbf{F}(\varphi ),\mathbf{F}(\psi )} \\ (\mathbf{T}\vee \rightarrow ) & \frac{\mathbf{T}(({\varphi }_{1}\vee {\varphi }_{2})\rightarrow \psi )} {\mathbf{T}({\varphi }_{1}\rightarrow \psi )\,\vert \,\mathbf{T}({\varphi }_{2}\rightarrow \psi )} & (\mathbf{F}\vee \rightarrow ) & \frac{\mathbf{F}(({\varphi }_{1}\vee {\varphi }_{2})\rightarrow \psi )} {\mathbf{F}({\varphi }_{1}\rightarrow \psi ),\mathbf{F}({\varphi }_{2}\rightarrow \psi )} \\ (\mathbf{T} \rightarrow \vee ) & \frac{\mathbf{T}(\varphi \rightarrow ({\psi }_{1}\vee {\psi }_{2}))} {\mathbf{T}(\varphi \rightarrow {\psi }_{1}),\mathbf{T}(\varphi \rightarrow {\psi }_{2})} & (\mathbf{F} \rightarrow \vee )& \frac{\mathbf{F}(\varphi \rightarrow ({\psi }_{1}\vee {\psi }_{2}))} {\mathbf{F}(\varphi \rightarrow {\psi }_{1})\,\vert \,\mathbf{F}(\varphi \rightarrow {\psi }_{2})} \\ (\mathbf{T}\wedge \rightarrow ) & \frac{\mathbf{T}(({\varphi }_{1}\wedge {\varphi }_{2})\rightarrow \psi )} {\mathbf{T}({\varphi }_{1}\rightarrow \psi ),\mathbf{T}({\varphi }_{2}\rightarrow \psi )} & \mathbf{F}\wedge \rightarrow ) & \frac{\mathbf{F}(({\varphi }_{1}\wedge {\varphi }_{2})\rightarrow \psi )} {\mathbf{F}({\varphi }_{1}\rightarrow \psi )\,\vert \,\mathbf{F}({\varphi }_{2}\rightarrow \psi )} \\ (\mathbf{T} \rightarrow \wedge ) & \frac{\mathbf{T}(\varphi \rightarrow ({\psi }_{1} \wedge {\psi }_{2}))} {\mathbf{T}(\varphi \rightarrow {\psi }_{1})\,\vert \,\mathbf{T}(\varphi \rightarrow {\psi }_{2})} &(\mathbf{F} \rightarrow \wedge )& \frac{\mathbf{F}(\varphi \rightarrow ({\psi }_{1}\wedge {\psi }_{2}))} {\mathbf{F}(\varphi \rightarrow {\psi }_{1}),\mathbf{F}(\varphi \rightarrow {\psi }_{2})} \\ (\mathbf{T} \rightarrow (\rightarrow ))& \frac{\mathbf{T}(\varphi \rightarrow ({\psi }_{1}\rightarrow {\psi }_{2}))} {\mathbf{T}({\psi }_{1}\rightarrow {\psi }_{2}),\mathbf{T}(\varphi \rightarrow {\psi }_{2})} \\ (\mathbf{F} \rightarrow (\rightarrow )) & \frac{\mathbf{F}(\varphi \rightarrow ({\psi }_{1}\rightarrow {\psi }_{2}))} {\mathbf{F}({\psi }_{1}\rightarrow {\psi }_{2})\,\vert \,\mathbf{F}(\varphi \rightarrow {\psi }_{2})} \\ (\mathbf{T}(\rightarrow ) \rightarrow ) & \frac{\mathbf{T}(({\varphi }_{1}\rightarrow {\varphi }_{2})\rightarrow \psi )} {\mathbf{T}({\varphi }_{2}\rightarrow \psi )\,\vert \,\mathbf{T}(\psi ),\mathbf{F}({\varphi }_{1}\rightarrow {\varphi }_{2})} \\ (\mathbf{F}(\rightarrow ) \rightarrow ) & \frac{\mathbf{F}(({\varphi }_{1}\rightarrow {\varphi }_{2})\rightarrow \psi )} {\mathbf{T}({\varphi }_{1}\rightarrow {\varphi }_{2}),\mathbf{F}({\varphi }_{2}\rightarrow \psi )\,\vert \,\mathbf{F}(\psi )} \end{array}$$

The specific rules have the following forms:

For all propositional variables p, q, and r,

$$\begin{array}{ll} \mbox{ (tran)} & \frac{\mathbf{F}(p\rightarrow q),\mathbf{F}(q\rightarrow r)} {\mathbf{F}(p\rightarrow r),\mathbf{F}(p\rightarrow q),\mathbf{F}(q\rightarrow r)} \\ \mbox{ (lmax)}\, \frac{\mathbf{F}(p\rightarrow q),\mathbf{F}(p)} {\mathbf{F}(q),\mathbf{F}(p\rightarrow q),\mathbf{F}(p)}\qquad & \qquad \mbox{ (rmax)}\, \frac{\mathbf{T}(p\rightarrow q)} {\mathbf{T}(q),\mathbf{T}(p\rightarrow q)} \\ \mbox{ (lin)}\, \frac{\mathbf{T}(p\rightarrow q)} {\mathbf{F}(q\rightarrow p),\mathbf{T}(p\rightarrow q)}\qquad & \qquad \mbox{ ($\min \perp $)} \frac{\mathbf{F}(p\rightarrow \perp )} {\mathbf{F}(\perp \rightarrow p),\mathbf{F}(p\rightarrow \perp )} \end{array}$$

A finite set X of signed LC-formulas is said to be LC-axiomatic whenever it includes a subset of either of the following forms:

• {F( ⊥ )};

• {T(φ), F(φ)}, for any LC-formula φ.

A finite set {φ₁, …, φ _n } of signed LC-formulas is said to be an LC-set whenever for every LC-model $\mathcal{M}$ there exists i ∈ { 1, …, n} such that φ _i is true in $\mathcal{M}$. LC-correctness of a rule is defined as in F-logic in Sect. 1.3.

Proposition 21.3.1.

• (1) The LC -decomposition rules are LC -correct;

• (2) The LC -specific rules are LC -correct;

• (3) The LC -axiomatic sets are LC -set.

Proof.

Let X be a finite set of LC-formulas. By way of example, we prove correctness of the rules (T ∨ ), (F ∨ → ), (T → ∧ ), (T( → ) → ), (tran), (rmax), and (lin).

(T ∨ )  Assume X ∪{T(φ ∨ ψ)} is an LC-set. Then, for every LC-model $\mathcal{M}$, either there exists $\mathit{\vartheta} \in X$ such that $\mathcal{M}\models \mathit{\vartheta}$ or $\mathcal{M}\models \mathbf{T}(\varphi \vee \psi )$, that is v(φ ∨ ψ) = ω. Thus, for every LC-model $\mathcal{M}$, either $\mathcal{M}\models \mathit{\vartheta}$ or v(φ) = ω or v(ψ) = ω, which means that either $\mathcal{M}\models \mathit{\vartheta}$ or $\mathcal{M}\models \mathbf{T}(\varphi )$ or $\mathcal{M}\models \mathbf{T}(\psi )$, and hence X ∪{T(φ), T(ψ)} is an LC-set. Assume X ∪{T(φ), T(ψ)} is an LC-set. Then, for every LC-model $\mathcal{M}$, either there exists $\mathit{\vartheta} \in X$ such that $\mathcal{M}\models \mathit{\vartheta}$ or $\mathcal{M}\models \mathbf{T}(\varphi )$ or $\mathcal{M}\models \mathbf{T}(\psi )$, which means that either $\mathcal{M}\models \mathit{\vartheta}$ or v(φ) = ω or v(ψ) = ω. Thus, either $\mathcal{M}\models \mathit{\vartheta}$ or max(v(φ), v(ψ)) = ω, so either $\mathcal{M}\models \mathit{\vartheta}$ or $\mathcal{M}\models \mathbf{T}(\varphi \vee \psi )$. Hence, X ∪{T(φ ∨ ψ)} is an LC-set.

(F ∨ → )  Since for every LC-model $\mathcal{M}$, v((φ₁ ∨ φ₂) → ψ)≠ω iff v(φ₁) > v(ψ) or v(φ₂) > v(ψ), correctness of the rule (F ∨ → ) follows.

(T → ∧ )  Correctness of the rule (T → ∧ ) follows from the property: for every LC-model $\mathcal{M}$, v(φ → (ψ₁ ∧ ψ₂))≠ω iff v(φ) ≤ v(ψ₁) and v(φ) ≤ v(ψ₂).

(T( → ) → )  Assume X ∪{T((φ₁ → φ₂) → ψ)} is an LC-set. Then, for every LC-model $\mathcal{M}$, either there exists $\mathit{\vartheta} \in X$ such that $\mathcal{M}\models \mathit{\vartheta}$ or v(φ₁ → φ₂) ≤ v(ψ), which implies v(φ₂) ≤ v(ψ). Suppose that either X ∪{T(φ₂ → ψ)} or X ∪{T(ψ), F(φ₁ → φ₂)} is not an LC-set. The former implies that there exists an LC-model $\mathcal{M}$ such that v(φ₂) > v(ψ), a contradiction. The latter implies that there exists an LC-model $\mathcal{M}$ such that v(ψ)≠ω and v(φ₁ → φ₂) = ω. Hence, v(φ₁ → φ₂) > v(ψ), a contradiction. Assume X ∪{T(φ₂ → ψ)} and X ∪{T(ψ), F(φ₁ → φ₂)} are LC-sets. Then, for every LC-model $\mathcal{M}$, either there exists $\mathit{\vartheta} \in X$ such that $\mathcal{M}\models \mathit{\vartheta}$ or:

$$({_\ast})\;v({\varphi }_{2}) \leq v(\psi )\mbox{ and }(v(\psi ) = \omega \mbox{ or }v({\varphi }_{1} \rightarrow {\varphi }_{2})\neq \omega ).$$

Let $\mathcal{M}$ be an LC-model. If v(φ₁ → φ₂) = ω, then by ( ∗ ) we get v(ψ) = ω, and thus v(φ₁ → φ₂) ≤ v(ψ). Hence, X ∪{T((φ₁ → φ₂) → ψ)} is an LC-set. If v(φ₁ → φ₂)≠ω, then v(φ₁ → φ₂) = v(φ₂). By ( ∗ ), we get v(φ₁ → φ₂) = v(φ₂) ≤ v(ψ). Hence, X ∪{T((φ₁ → φ₂) → ψ)} is an LC-set.

(tran)  Assume X ∪{F(p → q), F(q → r), F(p → r)} is an LC-set. Then for every LC-model $\mathcal{M}$, either there exists $\mathit{\vartheta} \in X$ such that $\mathcal{M}\models \mathit{\vartheta}$ or v(p) > v(q) or v(q) > v(r) or v(p) > v(r). Suppose X ∪{F(p → q), F(q → r)} is not an LC-set. Then there exists an LC-model $\mathcal{M}$ such that v(p) ≤ v(q) and v(q) ≤ v(r). This implies v(p) ≤ v(r), a contradiction. Clearly, if X ∪{F(p → q), F(q → r)} is an LC-set, then so is X ∪{F(p → q), F(q → r), F(p → r)}.

Correctness of the rules (rmax) and (lin) follow from the following properties of LC-models, respectively:

$$v(p) \leq v(q)\mbox{ iff }v(p) \leq v(q)\mbox{ or }v(q) = \omega ;$$

$$v(p) \leq v(q)\mbox{ iff }v(p) \leq v(q)\mbox{ or }v(q) > v(p).$$

The proofs of correctness of the remaining rules are similar.

For (3), note that in every LC-model $\mathcal{M}$, v( ⊥ ) = 0, so v(F( ⊥ )) = ω. Therefore $\mathcal{M}\models \mathbf{F}(\perp )$, hence X ∪{F( ⊥ )} is an LC-set. Since in every LC-model $\mathcal{M}$, either v(φ) = ω or v(φ)≠ω, we get $\mathcal{M}\models \mathbf{T}(\varphi )$ or $\mathcal{M}\models \mathbf{F}(\varphi )$, and hence X ∪{T(φ), F(φ)} is an LC-set. □

An application of a rule $\frac{\Phi } {{\Phi }_{1}}$ (resp. $\frac{\Phi } {{\Phi }_{1}\,\vert \,{\Phi }_{2}}$) to a finite set X of signed LC-formulas is said to be essential whenever the result of an application of the rule to X includes at least one formula which does not appear in X, that is (X ∖ Φ) ∪Φ _i ≠X, for some i ∈ { 1, 2}.

Let φ be an LC-formula. An LC-proof tree for φ is a tree with the following properties:

• the formula T(φ) is at the root of this tree;

• each node except the root is obtained by an essential application of an LC-rule to its predecessor node;

• a node does not have successors whenever it is an LC-axiomatic set of formulas or no rule introducing any new signed formula is applicable to its signed formulas.

Observe that every LC-proof tree is finite.

As usual, a branch of an LC-proof tree is said to be closed whenever it ends with an axiomatic set of formulas. An LC-proof tree for φ is said to be an LC-proof of φ whenever all of its branches are closed. A formula φ is LC-provable whenever there exists an LC-proof for it.

A branch b of an LC-proof tree is complete whenever it is closed or it satisfies the following completion conditions:

For all LC-formulas φ, ψ, φ₁, φ₂, ψ₁ and ψ₂,

Cpl(T ∨ ) (resp. Cpl(F ∧ )) If T(φ ∨ ψ) ∈ b (resp. F(φ ∧ ψ) ∈ b), then both T(φ) ∈ b and T(ψ) ∈ b (resp. F(φ) ∈ b and F(ψ) ∈ b), obtained by an application of the rule (T ∨ ) (resp. (F ∧ ));

Cpl(T ∧ ) (resp. Cpl(F ∨ )) If T(φ ∧ ψ) ∈ b (resp. F(φ ∨ ψ) ∈ b), then either T(φ) ∈ b or T(ψ) ∈ b (resp. F(φ) ∈ b or F(ψ) ∈ b), obtained by an application of the rule (T ∧ ) (resp. (F ∨ ));

Cpl(T ∨ → ) (resp. Cpl(F ∧ → )) If T((φ₁ ∨ φ₂) → ψ)) ∈ b (resp. F((φ₁ ∧ φ₂) → ψ) ∈ b), then either T(φ₁ → ψ) ∈ b or T(φ₂ → ψ) ∈ b (resp. F(φ₁ → ψ) ∈ b or F(φ₂ → ψ) ∈ b), obtained by an application of the rule (T ∨ → ) (resp. (F ∧ → ));

Cpl(T → ∨ ) (resp. Cpl(F → ∧ )) If T(φ → (ψ₁ ∨ ψ₂)) ∈ b (resp. F(φ → (ψ₁ ∧ ψ₂)) ∈ b), then both T(φ → ψ₁) ∈ b and T(φ → ψ₂) ∈ b (resp. F(φ → ψ₁) ∈ b and F(φ → ψ₂) ∈ b), obtained by an application of the rule (T → ∨ ) (resp. (F → ∧ ));

Cpl(T ∧ → ) (resp. Cpl(F ∨ → )) If T((φ₁ ∧ φ₂) → ψ) ∈ b (resp. F((φ₁ ∨ φ₂) → ψ) ∈ b), then both T(φ₁ → ψ) ∈ b and T(φ₂ → ψ) ∈ b (resp. F(φ₁ → ψ) ∈ b and F(φ₂ → ψ) ∈ b), obtained by an application of the rule (T ∧ → ) (resp. (F ∨ → ));

Cpl(T → ∧ ) (resp. Cpl(F → ∨ )) If T(φ → (ψ₁ ∧ ψ₂)) ∈ b (resp. F(φ → (ψ₁ ∨ ψ₂)) ∈ b), then either T(φ → ψ₁) ∈ b or T(φ → ψ₂) ∈ b (resp. F(φ → ψ₁) ∈ b or F(φ → ψ₂) ∈ b), obtained by an application of the rule (T → ∧ ) (resp. (F → ∨ ));

Cpl(T → ( → )) If T(φ → (ψ₁ → ψ₂)) ∈ b, then both T(ψ₁ → ψ₂) ∈ b and T(φ → ψ₂) ∈ b, obtained by an application of the rule (T → ( → ));

Cpl(F → ( → )) If F(φ → (ψ₁ → ψ₂)) ∈ b, then either F(ψ₁ → ψ₂) ∈ b or T(φ → ψ₂) ∈ b, obtained by an application of the rule (F → ( → ));

Cpl(T( → ) → ) If T((φ₁ → φ₂) → ψ) ∈ b, then either T(φ₂ → ψ) ∈ b or both T(ψ) ∈ b and F(φ₁ → φ₂) ∈ b, obtained by an application of the rule (T( → ) → );

Cpl(F( → ) → ) If F((φ₁ → φ₂) → ψ) ∈ b, then either both T(φ₁ → φ₂) ∈ b and F(φ2 → ψ) ∈ b or F(ψ) ∈ b, obtained by an application of the rule (F( → ) → );

For all propositional variables p, q, and r,

Cpl(tran) If F(p → q) ∈ b and F(q → r) ∈ b, then F(p → r) ∈ b, obtained by an application of the rule (tran);

Cpl(lmax) If F(p → q) ∈ b and F(p) ∈ b, then F(q) ∈ b, obtained by an application of the rule (lmax);

Cpl(rmax) If T(p → q) ∈ b, then T(q) ∈ b, obtained by an application of the rule (rmax);

Cpl(lin) If T(p → q) ∈ b, then F(q → p) ∈ b, obtained by an application of the rule (lin);

Cpl(min ⊥ ) If F(p → ⊥ ) ∈ b, then F( ⊥ → p) ∈ b, obtained by an application of the rule (min ⊥ ).

The notions of a complete LC-proof tree and an open branch of an LC-proof tree are defined as in F-logic (see Sect. 1.3). Note that the rules of LC-dual tableau guarantee that if b is a complete branch of an LC-proof tree and both T(p → q) ∈ b and F(p → q) ∈ b, then there is a node in b containing these two formulas. Therefore, we obtain:

Proposition 21.3.2 (Closed Branch Property).

Let b be an open branch of an LC -proof tree. Then for all $p,q \in \mathbb{V} \cup \{\perp \}$, T(p → q) ∈ b iff F(p → q)∉ b.

Proposition 21.3.3.

For every open branch b of an LC -proof tree, there are no ${p}_{1},\ldots, {p}_{n} \in \mathbb{V} \cup \{\perp \}$ , n ≥ 1, such that all the following conditions are satisfied:

• p ₁ = p _n

• For every i ∈{ 1,…,n − 1}, F(p _i → p _i+1 ) ∈ b or T(p_i+1 → p_i) ∈ b;

• For some i,j ∈{ 1,…,n}, T(p _i → p _j ) ∈ b.

Proof.

Suppose there are ${p}_{1},\ldots, {p}_{n} \in \mathbb{V} \cup \{\perp \}$ such that p ₁ = p _n , and for every i ∈ { 1, …, n − 1}, F(p _i → p _{i + 1}) ∈ b or T(p _{i + 1} → p _i ) ∈ b, and for some i, j ∈ { 1, …, n}, T(p _i → p _j ) ∈ b. Then, by the completion condition Cpl(lin), for every i ∈ { 1, …, n − 1}, F(p _i → p _{i + 1}) ∈ b, and by the completion condition Cpl(tran), for all i, j ∈ { 1, …, n}, F(p _i → p _j ) ∈ b. Since for some i, j ∈ { 1, …, n}, T(p _i → p _j ) ∈ b, there exists i, j ∈ { 1, …, n} such that F(p _i → p _j ) ∈ b and T(p _i → p _j ) ∈ b, which contradicts Proposition 21.3.2. □

Let ${q}_{1},\ldots, {q}_{l},p \in \mathbb{V} \cup \{\perp \}$, l ≥ 1, and let n ≥ 0. A sequence q ₁, …, q _l is said to be n-sequence for p whenever the following conditions are satisfied:

• p = q _l ;

• For every i ∈ { 1, …, l − 1}, F(q _i → q _{i + 1}) ∈ b or T(q _{i + 1} → q _i ) ∈ b;

• For n different i’s, T(q _{i + 1} → q _i ) ∈ b.

By Proposition 21.3.3, for every $p \in \mathbb{V} \cup \{\perp \}$, there exists a maximal n for which there is an n-sequence for p.

Let b be an open branch of an LC-proof tree. The branch structure is a system ${\mathcal{M}}^{b} = (N \cup \{ \omega \},\leq, {v}^{b})$ such that for every $p \in \mathbb{V} \cup \{\perp \}$, v ^b(p) = ω if F(p) ∈ b, otherwise v ^b(p) = max{n : there exists n-sequence for p}. Valuation v ^b extends to all the LC-formulas as in LC-models.

Proposition 21.3.4 (Branch Model Property).

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

Proof.

We will show that v ^b( ⊥ ) = 0. Since b is an open branch, F( ⊥ ) ∉ b. Therefore, v ^b( ⊥ )≠ω. Now, let q ₁, …, q _l be an n-sequence for ⊥. Since for every i ∈ { 1, …, l − 1}, F(q _i → q _{i + 1}) ∈ b or T(q _{i + 1} → q _i ) ∈ b, by the completion condition Cpl(lin), for every i ∈ { 1, …, l − 1}, F(q _i → q _{i + 1}) ∈ b. By the completion conditions Cpl(min ⊥ ) and Cpl(tran), for every i, j ∈ { 1, …, l}, F(q _i → q _j ) ∈ b. By Proposition 21.3.3, the only n for which an n-sequence for ⊥ exists is n = 0. Hence, v ^b( ⊥ ) = 0. □

Proposition 21.3.5 (Satisfaction in Branch Model Property).

For every open branch b and for every LC -formula φ, the following hold:

• (1) If T(φ) ∈ b, then ${\mathcal{M}}^{b}\nvDash \varphi$;

• (2) If F(φ) ∈ b, then ${\mathcal{M}}^{b}\models \varphi$ .

Proof.

The proof is by induction on the complexity of formulas.

Let $\varphi = p \in \mathbb{V}$. Then, F(p) ∈ b iff v ^b(p) = ω iff ${\mathcal{M}}^{b}\models p$. Since b is an open branch, if F(p) ∈ b, then T(p) ∉ b. Therefore, if ${\mathcal{M}}^{b}\models p$, then F(p) ∈ b, and hence T(p) ∉ b.

Let φ = (p → q). Assume T(p → q) ∈ b. By the completion condition Cpl(lin), F(q → p) ∈ b. By the completion condition Cpl(rmax), T(q) ∈ b, and by the induction hypothesis v ^b(q)≠ω. Let q ₁, …, q _l , l ≥ 1, be an n-sequence for q. Note that for every i ∈ { 1, …, l}, q _i ≠p, because otherwise F(p → q) ∈ b and hence b would be closed. On the other hand, since F(q → p) ∈ b and T(p → q) ∈ b, a sequence q ₁, …, q _l , p is an n + 1-sequence for p. Therefore v ^b(p) > v ^b(q), and hence ${\mathcal{M}}^{b}\nvDash \varphi$. Now, assume F(p → q) ∈ b. If F(p) ∈ b, then by the completion condition Cpl(lmax), we get F(q) ∈ b, so ${v}^{b}(p) = {v}^{b}(q) = \omega$. Therefore, ${\mathcal{M}}^{b}\models \varphi$. If F(p) ∉ b, then v ^b(p)≠ω. Let p ₁, …, p _l be an n-sequence for p. Then p ₁, …, p _l , q is an n-sequence for q, hence v ^b(p) ≤ v ^b(q). Therefore, ${\mathcal{M}}^{b}\models \varphi$.

Now, we prove (1) or (2) for some exemplary formulas.

Let $\varphi = ({\varphi }_{1} \wedge {\varphi }_{2})$. Assume T(φ₁ ∧ φ₂) ∈ b. By the completion condition Cpl(T ∧ ), either T(φ₁) ∈ b or T(φ₂) ∈ b. By the induction hypothesis, v ^b(φ₁)≠ω or v ^b(φ₂)≠ω. Thus, min(v ^b(φ₁), v ^b(φ₂))≠ω, and hence ${\mathcal{M}}^{b}\nvDash {\varphi }_{1} \wedge {\varphi }_{2}$.

Let φ = ((φ₁ ∨ φ₂) → ψ). Assume that F(φ) ∈ b. By the completion condition Cpl(F ∨ → ), both F(φ₁ → ψ) ∈ b and F(φ₂ → ψ) ∈ b. By the induction hypothesis, v ^b(φ₁) ≤ v ^b(ψ) and v ^b(φ₂) ≤ v ^b(ψ). Thus, max(v ^b(φ₁), v ^b(φ₂)) ≤ v ^b(ψ), and hence ${\mathcal{M}}^{b}\models \varphi$.

Let φ = (φ₁ ∧ φ₂). Assume that T(φ) ∈ b. By the completion condition Cpl(T → ∧ ), either $\mathbf{T}(\mathit{\vartheta} \rightarrow {\psi }_{1}) \in b$ or $\mathbf{T}(\mathit{\vartheta} \rightarrow {\psi }_{2}) \in b$. By the induction hypothesis, ${v}^{b}(\mathit{\vartheta}) > {v}^{b}({\psi }_{1})$ or ${v}^{b}(\mathit{\vartheta}) > {v}^{b}({\psi }_{2})$. Thus, ${v}^{b}(\mathit{\vartheta}) >\max ({v}^{b}({\psi }_{1}),{v}^{b}({\psi }_{2}))$, and hence ${\mathcal{M}}^{b}\nvDash \varphi$.

Let $\varphi = (\mathit{\vartheta} \rightarrow ({\psi }_{1} \rightarrow {\psi }_{2}))$. Assume that F(φ) ∈ b. By the completion condition Cpl(F → ( → )), either F(ψ₁ → ψ₂) ∈ b or $\mathbf{F}(\mathit{\vartheta} \rightarrow {\psi }_{2}) \in b$. By the induction hypothesis, v ^b(ψ₁ → ψ₂) = ω or ${v}^{b}(\mathit{\vartheta}) \leq {v}^{b}({\psi }_{2})$. Note that v ^b(φ) equals ω or v ^b(ψ₂). Therefore ${v}^{b}(\mathit{\vartheta}) \leq {v}^{b}({\psi }_{1} \rightarrow {\psi }_{2})$, and hence ${\mathcal{M}}^{b}\models \varphi$.

Let φ = ((φ₁ → φ₂) → ψ). Assume that F(φ) ∈ b. Then, by the completion condition Cpl(F( → ) → ), either both T(φ₁ → φ₂) ∈ b and F(φ₂ → ψ) ∈ b or F(ψ) ∈ b. If both T(φ₁ → φ₂) ∈ b and F(φ₂ → ψ) ∈ b, then by the induction hypothesis ${\mathcal{M}}^{b}\nvDash {\varphi }_{1} \rightarrow {\varphi }_{2}$ and ${\mathcal{M}}^{b}\models {\varphi }_{2} \rightarrow \psi$. Thus, v ^b(φ₁ → φ₂) = v ^b(φ₂) and v ^b(φ₂) ≤ v ^b(ψ). Therefore, v ^b(φ₁ → φ₂) ≤ v ^b(ψ), and hence ${\mathcal{M}}^{b}\models \varphi$. If F(ψ) ∈ b, then by the induction hypothesis ${\mathcal{M}}^{b}\models \psi$. Thus, v ^b(ψ) = t. Therefore, v ^b(φ₁ → φ₂) ≤ v ^b(ψ), and hence ${\mathcal{M}}^{b}\models \varphi$.

The proofs of the remaining cases are similar. □

Proposition 21.3.6.

Let φ be an LC -formula. If φ is LC -valid, then φ is LC -provable.

Fig. 21.1

An LC-proof of the formula p → ((p → ⊥ ) → ⊥ )

Fig. 21.2

An LC-proof of the formula (p → q) → [(q → r) → (p → r)]

Fig. 21.3

An LC-proof of the formula p → (q → (p ∧ q))

Proof.

Assume φ is LC-valid. Suppose there is no any closed LC-proof tree for φ. Then there exists a complete LC-proof tree for φ with an open branch, say b. Since T(φ) ∈ b, by Proposition 21.3.4, ${\mathcal{M}}^{b}\nvDash \varphi$. Hence, by Proposition 21.3.5 φ is not LC-valid, a contradiction. □

By Propositions 21.3.1 and 21.3.6, we get:

Theorem 21.3.1 (Soundness and Completeness of LC).

For every LC -formula φ, the following conditions are equivalent:

• 1. φ is LC -valid;

• 2. φ is LC -provable.

Since every LC-proof tree is finite and the rules of LC-dual tableau preserve and reflect validity of LC-formulas, LC-dual tableau is a decision procedure for the logic LC.

Example.

Consider the following LC-formulas:

$$\begin{array}{rcl} \varphi & =& p \rightarrow ((p \rightarrow \perp ) \rightarrow \perp ), \\ \psi & =& (p \rightarrow q) \rightarrow [(q \rightarrow r) \rightarrow (p \rightarrow r)], \\ \mathit{\vartheta}& =& p \rightarrow (q \rightarrow (p \wedge q))\end{array}$$

(1)

Their LC-proofs are presented in Figs. 21.1–21.3, respectively.