Finally, we show that if Γ is satisable, then Γ is open. Suppose it is not.

Then if Γ is 
losed by def. 19-(i) or (ii), we immediately nd a 
ontradi
tion.

Suppose that Γ is 
losed by 
ondition (iii), then x : ¬x¬A in Γ for some formula x : ¬x¬A. Sin
e Γ is satisable, we would have that there is y ∈ ∆
su h that y ≺f(x) f(x), obtaining a 
ontradi
tion (by 
entering and asymmetry).

In order to show ompleteness, we need the following denition:

## Denition 22 (Saturated Tableau Set). We Say That A Tableau Set Γ Is Saturated If:

(T⊓) If x : A ⊓ B ∈ Γ then x : A ∈ Γ and x : B ∈ Γ .

(F⊓) If x : ¬(A ⊔ B) ∈ Γ then x : ¬A ∈ Γ or x : ¬B ∈ Γ .

(NEG) If x : ¬¬A ∈ Γ then x : A ∈ Γ .

(T ⇔) If x : (A ⇔ B) ∈ Γ then for al l y ∈ LabΓ , either y : ¬B ∈ Γ and
¬¬A ∈ Γ , or y : B and y : ¬x¬A are in Γ .

(F ⇔) If x : ¬(A ⇔ B) ∈ Γ then either (i) x : ¬A ∈ Γ , or (ii) x : B ∈ Γ , or
(iii) x : ¬A and x : ¬B are in Γ and there exists y ∈ LabΓ su
h that y : B
and y : x¬A are in Γ .

(Tx) If z : x¬A ∈ Γ and y <x z ∈ Γ , then y : ¬A and y : x¬A are in Γ .

(Fx) If z : ¬x¬A ∈ Γ , then either (i) x : A ∈ Γ , or (ii) x : ¬A ∈ Γ and there exists y ∈ LabΓ su
h that y <x z , y : A and y : x¬A are in Γ .

(T) If x : ¬A ∈ Γ , then for al l y ∈ LabΓ , y : ¬A and y : ¬A are in Γ . (F) If x : ¬¬A ∈ Γ , then there is y ∈ LabΓ su
h as y : A ∈ Γ .

(**Cent**) For al l x, y ∈ LabΓ su
h that x 6= y, x <x y is ∈ Γ .

(Mod) If y <x z ∈ Γ , then for al l labels u ∈ WΓ , either u <x z ∈ Γ , or y <x u ∈ Γ .

We say that Γ is saturated wrt. a rule R if Γ satises the 
orresponding saturation ondition for R of above denition.

The following lemma shows that the preferen e relations <x satises the Limit Assumption for an open tableau set.

Lemma 23. Let Γ be an open tableau set 
ontaining only a nite number of positive ⇔-formulas x : A0 ⇔ B0 , x : A1 ⇔ B1 , x : A2 ⇔ B2 , . . . , x : An−1 ⇔ Bn−1. Then Γ does not 
ontain any innite des
ending 
hain of labels y1 <x y0, y2 <x y1, . . . , yi+1 <x yi**, . . .** .

Proof. By absurdity, let Γ 
ontain a des
ending 
hain of labels **. . . , y**i+1 <x yi <x . . . <x y1 <x y0 . This 
hain may only be generated by su

essive appli
ations of (T ⇔) and (F2x) to formulas x : Ai ⇔ Bi for 0 ≤ **i < n**. Γ then 
ontains the following formulas for 0 ≤ **i < n**: yi: ¬x¬Ai
, yi+1 <x yi
, yi+1 : Ai
,

yi+1 : x¬Ai
.

Here (T ⇔) has been applied to every formula x : Ai ⇔ Bi on
e and with parameter yi previously (and newly) generated by (F2x) from yi−1 : ¬x¬Ai−1 . The only way to make the 
hain longer is by applying (T ⇔) a se ond time to one of the positive ⇔-formulas labelled x on Γ . Let this formula