BRICS RS-95-6 I. Walukiewicz: A Complete Deductive System for the μ-Calculus

BRICS

Basic Research in Computer Science

A Complete Deductive System for the μ-Calculus

Igor Walukiewicz

BRICS Report Series RS-95-6 ISSN 0909-0878 January 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

A Complete Deductive System for the μ-Calculus

Igor Walukiewicz^{1,2}

BRICS^{3}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract The propositional μ-calculus as introduced by Kozen in [12] is considered. In that paper a finitary axiomatisation of the logic was presented but its completeness remained an open question. Here a different finitary axiomatisation of the logic is proposed and proved to be complete. The two axiomatisations are compared.

1 Introduction

It is now common to view computer programs as state transformers, that is actions that can change one state of computer hardware to another. In contrast with classical logics the notion of change is intrinsic in modal logics. Within modal logic, one can speak about multiple possible worlds and relations between them, as, for example, the changes of an environment during time. This property makes the modal logic a valuable tool for description of program behaviour that is itself observable through the changes of computer states.

The properties of logic we should consider, when we have program verification in mind, are expressiveness, completeness and decidability. The more expressive is the logic, the more properties of the systems we can describe. A complete axiom system allows us to reason about the properties. This facilitates “proof theoretic” approach to specification and verification. Decidability and particularly computational complexity of the decision procedure is important for machine aided verification. Finally, there is a question of model checking, i.e., establishing the truth of a formula in a given state of a (usually very large) structure, which describes a behaviour of a complex program.

We consider propositional μ-calculus in the form introduced by Kozen in [12]. It turned out that this logic is very well suited for specification and verification purposes. First it is very expressive and most of the other logics of programs can be encoded into the μ-calculus. On binary trees the logic is as expressive as monadic second order logic of two successors [18, 6]. On the other hand the logic is manageable. Satisfiability problem for the logic was shown to be EXPTIME-complete [15, 23, 4] which means that it is of the same complexity as for many much less expressive logics. The best known upper bound for the model checking problem is exponential but it is polynomial if nesting of fixpoints is bounded [3, 1].

1This work was partially supported by Polish KBN grant No. 2 1192 91 01

2

On the leave from: Institute of Informatics, Warsaw University, Banacha 2,

02-097 Warsaw, POLAND

3Basic Research in Computer Science, Centre of the Danish National Research Foundation.

One of lacking elements in this picture was finitary complete axiomatisation of the logic (infinitary axiomatisation was given in [13]). There exist finitary axiomatisations for many weaker propositional logics of programs like PDL [8, 19, 14, 11, 16], CTL^{∗} [5] or Process Logic [9]. Completeness proofs for these logics use the so called Henkin method which consists of constructing a model for a non refutable formula. The use of this method depends on the ability of syntactic model construction which is provided by collapsed model theorem or a result of similar kind. For several more expressive logics of programs like: PDLΔ, PAL, temporal μ-calculus (see [10, 22]) the completeness problem remains open. One of the reasons for this is that these logics, as well as the μ-calculus, do not enjoy the collapsed model property (see for example [10]), hence known methods do not work in this case.

In [12] Kozen proposed a natural axiom system and showed that it can prove all valid formulas satisfying some syntactic restrictions. In the present paper a different finitary axiomatisation is proposed and shown to be complete for the whole logic. The systems differ only in one, the most important, rule. The original system has Park’s rule:

\frac{α(φ) ⇒ φ}{μX.α(X) ⇒ φ}

which expresses the property that the least fixpoint is the least pre-fixpoint. The rule proposed here is derived from Knaster-Tarski characterisation of the least fixpoint as the limit of a chain of approximations. We show that Park’s rule is derivable in our system but our rule is not derivable in Kozen’s system. Hence the presented completeness result cannot be used to prove the completeness of the, weaker, Kozen’s axiomatisation.

Although our rule may seem to be less natural than Park’s rule we think that our proof system has some advantages.

First we think that it is easy to prove the facts in this system mainly due the strength of our rule. Although we have a cut rule in the system, the completeness proof gives an algorithm for constructing a proof of a given valid formula. Hence there is a way of controlling cut’s.

We believe that the system can be naturally integrated with a decidability algorithm. This allows construction of a tool which given a formula will construct either a proof of it or a counterexample model. Moreover this tool should also allow interaction with the user who can speed up some proving steps.

For propositional modal logics of programs reduction to ω-automata is a general method of model construction. As our method of proving completeness is closely related to this technique we hope that it can be also generalised to other logics.

The outline of the paper is as follows. We begin by giving basic definitions and recalling a result from [17] which we will use. Next we present our axiomatisation, prove some of its properties and relate it to Kozen’s system. Finally we present the completeness proof.

Acknowledgements

I am very grateful to Dexter Kozen for his introduction to the μ-calculus and sharing with me his understanding of the subject. Damian Niwiński was the one from whom I learned automata theory. Long discussions with him made development of this material possible. Results presented here come from my PhD thesis. Jerzy Tiuryn guided development of the thesis and was always ready with help and advice. I would also like to thank my PhD referees: Dexter Kozen, Andrzej W. Mostowski and Paweł Urzyczyn for their valuable comments. I am indebted to my first two supervisors: Leszek Holenderski and Grażyna Mirkowska, without whom I would not have started the subject at all.

2 Preliminary definitions

In this section we will give basic definitions and recall a result from [17] which we will use in the completeness proof.

Let Prop = {p, q, …} be a set of propositional letters, Var = {X, Y, …} a set of variables and Act = {a, b, …} a set of actions. Formulas of the μ-calculus over this three sets can be defined by the following grammar:

F := Var | Prop | ¬F | F ∨ F | F ∧ F | ⟨Act⟩F | [Act]F | μVar.F |νVar.F

Additionally we require that in formulas of the form μX.α(X) and νX.α(X), variable X occurs in α(X) only positively, i.e., under even number of negations. We will use σ to denote μ or ν. We use ff as an abbreviation for a formula p ∧ ¬p for some propositional constant p. Formulas are interpreted in Kripke models of the form M = ⟨S, R, ρ⟩, where:

• S is a nonempty set of states,

• R : Act → P(S × S) is a function assigning a binary relation on S to each action in Act.

• ρ : Prop → P(S) is a function assigning a set of states to each propositional letter in Prop.

For a given model M and a valuation Val : Var → P(S), the set of states in which a formula α is true, ∥ α ∥_{V al}^{M} is defined inductively as follows (we will omit superscript M when it causes no ambiguity):

∥ X ∥_{V al} = V al(X)
∥ p ∥_{V al} = ρ(p)
∥ ¬α ∥_{V al} = S − ∥ α ∥_{V al}

∥ α ∧ β ∥_{V al} = ∥ α ∥_{V al} ∩ ∥ β ∥_{V al}
∥ α ∨ β ∥_{V al} = ∥ α ∥_{V al} ∪ ∥ β ∥_{V al}
∥ ⟨a⟩α ∥_{V al} = {s : ∃s′.(s, s′) ∈ R(a) ∧ s′ ∈ ∥ α ∥_{V al}}
∥ [a]α ∥_{V al} = {s : ∀s′.(s, s′) ∈ R(a) ⇒ s′ ∈ ∥ α ∥_{V al}}
∥ μX.α(X) ∥_{V al} = ⋂{S′ ⊆ S : ∥ α ∥_{V al[S′/X]} ⊆ S′}
∥ νX.α(X) ∥_{V al} = ⋃{S′ ⊆ S : S′ ⊆ ∥ α ∥_{V al[S′/X]}}

When we write M, s, Val ⊧ α we mean that s ∈ ∥ α ∥_{V al}^{M}. For a set of formulas Γ and a formula β, we write Γ ⊧ β to mean that for any structure M, state s and valuation Val: if M, s, Val ⊧ Γ then M, s, Val ⊧ β. If Γ = {α} is one element set we just write α ⊧ β.

A sequent is pair of finite sets of formulas which we write Γ ⊢ Δ. The meaning of such a sequent is that a conjunction of formulas from Γ implies a disjunction of formulas from Δ, in other words it is equivalent to a formula ¬(⋀ Γ) ∨ ⋁ Δ. We use ⋀ Γ and ⋁ Γ for respectively conjunction and disjunction of formulas from Γ. Conjunction of the empty set is true and disjunction of the empty set is false.

Definition 2.1 We call a formula positive iff all negations in the formula appear only before propositional constants and free variables.

Variable X in μX.α(X) is guarded iff every occurrence of X in α is in the scope of some modality operator ⟨⟩ or []. We say that a formula is guarded iff every bound variable in the formula is guarded.

Proposition 2.2 (Kozen) Every formula is equivalent to a positive guarded formula.

Proof Let φ be arbitrary formula. We first show how to obtain an equivalent guarded formula. The proof proceeds by induction on the structure of the formula with the only difficult case for fixpoint formulas.

Let φ be of the form μX.α(X) with α(X) a guarded formula. Suppose X is unguarded in some subformula of α(X) of the form σY.β(Y, X). As α(X) is guarded, Y must be guarded in σY.β(Y, X). Equivalence σY.β(Y, X) ≡ β(σY.β(Y, X), X) gives us a formula with all unguarded occurrences of X outside the fixpoint operator. Repeating this process we obtain a formula equivalent to α(X) with all unguarded occurrences of X not in the scope of a fixpoint operator.

Now using the laws of classical propositional logic we can transform this formula to a conjunctive normal form (considering fixpoint formulas and formulas of the form ⟨a⟩γ and [a]γ) as propositional constants. This way we obtain a formula

(X ∨ α_{1}(X)) ∧ … ∧ (X ∨ α_{i}(X)) ∧ β(X)  (1)

where all occurrences of X in α_{1}(X), …, α_{i}(X), β(X) are guarded. Variable X occurs only positively in (1) because it did so in our original formula. Formula (1) is equivalent to

(X ∨ (α_{1}(X) ∨ … ∨ α_{i}(X))) ∧ β(X)

We will show that μX.(X ∨ ᾱ(X)) ∧ β(X) is equivalent to μX.ᾱ(X) ∧ β(X). It is obvious that

(μX.ᾱ(X) ∧ β(X)) ⇒ (μX.(X ∨ ᾱ(X)) ∧ β(X))

Let γ(X) stand for ᾱ(X)∧β(X). To prove the other implication it is enough to observe that μX.γ(X) is a prefixpoint of μX.(X ∨ᾱ(X))∨β(X) as the following calculation shows:

((μX.γ(X)) ∨ ᾱ(μX.γ(X))) ∧ β(μX.γ(X)) ⇒
((ᾱ(μX.γ(X)) ∧ β(μX.γ(X))) ∨ ᾱ(μX.γ(X))) ∧ β(μX.γ(X)) ⇒
ᾱ(μX.γ(X) ∧ β(μX.γ(X))

If φ is a guarded formula then we use dualities of the μ-calculus like ¬[a]α ≡ ⟨a⟩¬α or ¬μX.α(X) ≡ νX.¬α(¬X) to produce an equivalent positive formula. It is easy to see that it will still be a guarded formula.

In our completeness proof we will need a result from [17] which gives a characterisation of the validity of the μ-calculus formulas by means of infinite tableaux. We will briefly recall the result here.

First we introduce the concept of a definition list [21] which will name the fixpoint subformulas of a given formula in order of their nesting.

We extend vocabulary of the μ-calculus by a countable set Dcons of fresh symbols that will be referred to as definition constants and usually denoted U, V, … These new symbols are now allowed to appear positively in formulas, like propositional variables.

A definition list is a finite sequence of equations :

D = ((U_{1} = σ_{1}X.α_{1}(X)), …, (U_{n} = σ_{n}X.α_{n}(X))  (2)

where U_{1}, …, U_{n} ∈ DCons and σ_{i}X.α_{i}(X) is a formula such that all definition constants appearing in α_{i} are among U_{1}, …, U_{i−1}. We assume that U_{i} ≠ U_{j} and α_{i} ≠ α_{j}, for i ≠ j. If i < j then U_{i} is said to be older than U_{j} (U_{j} younger than U_{i}) with respect to the definition list D.

We construct a definition list for a formula γ by means of the contraction operation [⟩γ⟨] which is defined recursively as follows:

1. [⟩p⟨] = [⟩¬p⟨] = [⟩X⟨] = [⟩U⟨] = ∅;

2. [⟩¬α⟨] = [⟩⟨a⟩α⟨] = [⟩[a]α⟨] = [⟩α⟨];

3. [⟩α ∧ β⟨] = [⟩α ∨ β⟨] = [⟩α⟨] ∘ [⟩β⟨], operation ∘ is defined below;

4. [⟩μX.α(X)⟨] = ((U = μX.α(X)), [⟩α(U)⟨]) where U is new;

5. [⟩νX.α(X)⟨] = ((U = νX.α(X)), [⟩α(U)⟨]) where U is new.

The operation [⟩α⟨] ∘ [⟩β⟨] is defined as follows. First we make sure that the definition constants used in [⟩α⟨] are disjoint form those used in [⟩β⟨]. Then if it happens that (U = γ) ∈ [⟩α⟨] and (V = γ) ∈ [⟩β⟨], we delete the definition from list [⟩β⟨] and replace V with U in [⟩β⟨]. This may cause other formulas to be doubly defined and we deal with them in the same way.

We will say that U is a μ-constant if (U = μX.β(X)) ∈ D, if (U = νX.β(X)) ∈ D, constant U will be called a ν-constant. Observe that every constant occurring in D is either μ or ν-constant.

For a formula α and a definition list D containing all definition constants occurring in α we define the expansion operation ⟨[α]⟩_{D}, which subsequently replaces definition constants appearing in the formula by the right hand sides of the defining equations,

⟨[α]⟩_{D} = [σ_{n}X.α_{n}(X)/U_{n}] … [σ_{1}X.α_{1}(X)/U_{1}] , where D is as in (2)

A tableau sequent is a pair (Γ, D), where D is a definition list and Γ is a set of tableau formulas such that the only constants that occur in them are those from D. We will denote (Γ, D) by Γ ⊢_{D} . A tableau sequent Γ ⊢_{D} will be called tableau axiom iff p, ¬p ∈ Γ for some propositional letter or variable p. Remark: We have two kinds of sequents. Ordinary ones are two sided sequents of formulas without definition constants. In a tableau sequent Γ ⊢_{D} formulas may contain definition constants from definition list D. Index D also allows us to distinguish between an ordinary sequent Γ ⊢ which happens to have empty right hand side and a tableau sequent Γ ⊢_{D} .

Definition 2.3 Let S be the following set of tableau rules:

(∧_{t})  \frac{α, β, Γ ⊢_{D}}{α ∧ β, Γ ⊢_{D}}

(∨_{t})  \frac{α, Γ ⊢_{D} β, Γ ⊢_{D}}{α ∨ β, Γ ⊢_{D}}

(const)  \frac{α(U), Γ ⊢_{D}}{U, Γ ⊢_{D}} (U = σX.α(X)) ∈ D
(σ_{t})  \frac{U, Γ ⊢_{D}}{σX.α(X), Γ ⊢_{D}} (U = σX.α(X)) ∈ D

(⟨⟩_{t})  \frac{α, \{β : [a]β ∈ Γ\} ⊢_{D}}{⟨a⟩α, Γ ⊢_{D}}

Notice that if we assume that a tableau sequent Γ ⊢_{D} denotes ordinary sequent {⟨[γ]⟩_{D} : γ ∈ Γ}⊢ then tableau rules become sound logical rules.

Definition 2.4 Given a positive guarded formula γ and definition list D = [⟩γ⟨], a tableau for γ is any labeled tree ⟨K, L⟩, where K is a tree and L a labeling function, such that

1. the root of K is labeled with γ ⊢_{D} ,

2. if L(n) is a tableau axiom then n is a leaf of K,

3. if L(n) is not an axiom then the sons of n in K are created and labeled according to the rules of the system S, i.e. in such a way that L(n) is the conclusion and the labels of the sons assumptions of a rule from S.

Remark: We see applications of rules as a process of reduction. Given a finite set of formulas Γ we want to derive, we look for the rule the conclusion of which matches our set. Then we apply the rule and obtain the assumptions of the instance of the rule in which Γ is the conclusion.

Definition 2.5 Let T = ⟨K, L⟩ be a tableau for a formula γ with D = [⟩γ⟨]. Let P = (v_{1}, v_{2}, …) be an infinite path in the tree K, i.e. each v_{i+1} is a son of v_{i}. A trace on the path P is any sequence of formulas (α_{1}, α_{2}, …) such that α_{n} ∈ L(v_{n}) and α_{n+1} is either: (i) α_{n} if the formula α_{n} is not reduced by the rule applied in v_{n} or (ii) if α_{n} is reduced in v_{n} then α_{n+1} is one of the resulting formulas.

This last notion should be clear for all the rules other then (⟨⟩_{t}). For the rule:

(⟨⟩_{t})  \frac{α, \{β : [a]β ∈ Γ\} ⊢_{D}}{⟨a⟩α, Γ ⊢_{D}}

we have: α_{n+1} = α if α_{n} = ⟨a⟩α, and α_{n+1} = β if α_{n} = [a]β for some β; in all other cases the trace ends on α_{n}.

Definition 2.6 A constant U regenerates on the trace (α_{1}, α_{2}, …) if for some i, α_{i} = U and α_{i+1} = α(U), where (U = σX.α(X)) ∈ D. A trace is called μtrace iff it is an infinite trace on which the oldest constant regenerated infinitely often is a μ-constant.

Definition 2.7 A tableau T for γ is called a refutation of γ iff every leaf of T is labeled with a tableau axiom and on every infinite path of T there exists a μ-trace.

Theorem 2.8 (Characterisation) For every positive guarded formula γ: γ is not satisfiable iff there is a refutation of γ

3 Axiomatisation

This section is divided into three parts. In the first subsection we present a finitary axiom system for the μ-calculus. Next we prove some basic properties of the system. In the third subsection we relate the axiomatisation to the one proposed by Kozen in [12].

3.1 The system

We will present the system in a sequent calculus form. We prefer this formalisation because sequent calculus rules closely correspond to the tableau rules.

It will be convenient to introduce one piece of notation. For a finite set of atomic actions P = {a_{1}, …, a_{n}} ⊆ Act and a μ-calculus formula α we let ⟨P^{∗}⟩α to be an abbreviation of the formula μX.⟨a_{1}⟩X ∨ … ∨ ⟨a_{n}⟩X ∨ α. Intuitively such a formula says that a state satisfying α is reachable by sequence of actions from P.

Our system consists of two groups of rules and some additional axioms. First we take the rules of the simple propositional modal logic.

(¬)  \frac{Γ⊢Δ, α}{Γ, ¬α⊢Δ}  \frac{Γ, α⊢Δ}{Γ⊢¬α, Δ}

(∧)  \frac{α, β, Γ⊢Δ}{α ∧ β, Γ⊢Δ}  \frac{Γ⊢α, Δ Γ⊢β, Δ}{Γ⊢α ∧ β, Δ}

(∨) \frac{α, Γ⊢Δ β, Γ⊢Δ}{α ∨ β, Γ⊢Δ}  \frac{Γ⊢α, β, Δ}{Γ⊢α ∨ β, Δ}

(⟨⟩)  \frac{α, \{β : [a]β ∈ Γ\}⊢\{γ : ⟨a⟩γ ∈ Δ\}}{⟨a⟩α, Γ⊢Δ}

(cut)  \frac{Γ⊢Δ, γ Σ, γ ⊢Ω}{Γ, Σ⊢Δ, Ω}

Then we add the rules concerning fixpoints

(μ)  \frac{Γ⊢α(μX.α(X)), Δ}{Γ⊢μX.α(X), Δ}

(ind) \frac{φ(ff )⊢Δ φ(α(μX.Z ∧ α(X)))⊢Δ, ⟨P^{∗}⟩φ(μX.Z ∧ α(X))}{φ(μX.α(X))⊢⟨P^{∗}⟩Δ}
Z ∉ F V (φ(μX.α(X)), Δ)

In the last rule P ⊆ Act is a finite set of actions, ⟨P^{∗}⟩Δ is an abbreviation of {⟨P^{∗}⟩δ : δ ∈ Δ} and Z is a new propositional variable not occurring free in φ(μX.α(X))⊢Δ.

In the above notation φ(μX.α(X)) stands for the result of the substitution φ[μX.α(X)/[]] where [] is a distinguished variable. A substitution φ[α/X] is legal only if no free variable of α becomes bound in φ[α/X].

Finally because we had chosen to include constructions [a]α and νX.α(X) into the language we have to define them using other connectives by adding the following sequents as specific axioms:

\begin{matrix}([]L) & [a]α⊢¬⟨a⟩¬α & ([]R) & ⟨a⟩α⊢¬[a]¬α \\ (νL) & νX.α(X)⊢¬μX.¬α(¬X) & (νR) & μX.α(X)⊢¬νX.¬α(¬X) \end{matrix}

Definition 3.1 A finite tree constructed with the use of the above rules will be called diagram. A proof will be a diagram whose all leaves are labeled with axioms, i.e., instances of the axiom sequents above or sequents with the same formula on both sides.

Remark: Observe the difference between diagrams and tableaux. The first are always finite while the second not necessary so. They are also constructed using different, although similar, sets of rules.

Let us give some intuitions about rule (ind). Especially we would like to hint what well ordered set we are interested in and what kind of induction stands behind the rule. First let us consider the following rule:

\frac{φ(ff )⊢Δ φ(α^{n+1}(ff ))⊢Δ, ⟨P^{∗}⟩φ(α^{n}(ff ))}{φ(μX.α(X))⊢⟨P^{∗}⟩Δ}  (3)

where n ranges over the natural numbers and α^{n}(ff ) stands for n-unfolding: α(… α(ff ) …). Of course because n is treated as a variable, this rule is not a finitary rule of the μ-calculus.

Suppose that the assumptions of rule (3) are valid in a finite structure M. We would like to show that the conclusion of the rule is valid. This follows from two observations. First using the assumptions and induction on n we can show that φ(α^{n}(ff )) ⊢ ⟨P^{∗}⟩Δ is valid for any n. Then it is enough to observe that in a finite structure M with, say k, states, formula μX.α(X) is equivalent to α^{k}(ff ).

Rule (3) would be sufficient for our purposes but it is not a rule of the μ-calculus. We can easily weaken the rule to:

\frac{φ(ff )⊢Δ φ(α(Z))⊢Δ, ⟨P^{∗}⟩φ(Z)}{φ(μX.α(X))⊢⟨P^{∗}⟩Δ}  (4)

where Z is a fresh variable. This rule is much weaker because the second assumption is much stronger. In (3) we required the property to hold only for the approximations of μX.α(X) in present rule we want it to be true for all sets of states. We don’t know whether the system with this rule is complete. Our rule (ind) is the stronger version of (4) which is still a finitary rule of the μ-calculus. Instead of taking just free variable Z we take μX.Z ∧ α(X). The following fact shows that for Z being a finite approximation of μX.α(X) the two formulas are equivalent. Nevertheless in general the assumption of (ind) rule is much weaker than that of rule (4)

Fact 3.2 For any structure M, formula μX.α(X) and valuation Val such that Val(Z) = ∥ α^{k}(ff ) ∥_{V al} for some k ∈ N and Z ∉ F V (α(ff )) we have:

∥ μX.Z ∧ α(X) ∥_{V al} = Val(Z)

Proof: Let Val(Z) = ∥ α^{k}(ff ) ∥_{V al} then

∥ μX.Z ∧ α(X) ∥_{V al} = ∥ μX.α^{k}(ff ) ∧ α(X ) ∥_{V al} = ∥ α^{k}(ff ) ∥_{V al}

Inclusion of a cut rule into our system also deserves a comment. Since the rule (ind) has the specific shape of reducing connective which can be “hidden” deep into the formula, the addition of the cut rule seems to be a reasonable way to make the system usable. The completeness proof will give us an algorithm for constructing a proof of a valid formula and as we will see this proof will have some kind of subformula property even though cuts will be used in it. The conclusion is that cuts in the proof can be used in a very restricted way and one can substitute them by appropriate rules which may be added to the system. Addition of the cut rule makes the system simpler and since we have an algorithm for automatic construction of a proof of a valid sequent we prefer the presented formulation.

The next proposition states soundness of the system. There are at least three possible notions of soundness of a rule in a modal logic:

• The strongest will be to require that if the assumptions of a rule are satisfied in a state of a structure with a given valuation then the conclusion must be satisfied in this state and valuation. It is easy to see that rules (neg), (and), (or), (cut) and (μ) are sound in this sense.

• The other would be to require that for any structure M, if all assumptions of the rule are valid in the structure (i.e. satisfied in every state and every valuation) then the conclusion must be valid in this structure. The rule (⟨⟩) is sound in this sense. We will show in the next subsection that all the rules of Kozen’s axiomatisation are also sound in this sense.

• The weakest of the three is the condition that if all the assumptions of the rule are valid then the conclusion is valid. The rule (ind) is sound in this sense and as we will show in the next subsection it is not sound in the sense of any of the two preceding notions of soundness. Of course this type of soundness is all that we need for an axiomatisation of the validity relation. In the following by soundness we will always understand this weak notion of soundness.

Proposition 3.3 All the rules of our system are sound and all the axioms are valid

Proof Validity of the axioms is standard. Also standard is validity of all the rules except (ind) which soundness we prove below.

Let us assume conversely that the rule (ind) is not sound. Then from the finite model property we have a finite structure M such that the sequents:

φ(ff )⊢Δ φ(α(μX.Z ∧ α(X)))⊢Δ, ⟨P^{∗}⟩φ(μX.Z ∧ α(X))

are valid in M and φ(μX.α(X)) ⊢ ⟨P^{∗}⟩Δ is not. We assume that the variable Z does not appear free in φ(μX.α(X)) or Δ. Let k be the smallest integer for which there exists a state s of M and valuation Val satisfying: M, s, Val ⊧ φ(α^{k}(ff )) and for all δ ∈ Δ, M, s, Val |̸= ⟨P^{∗}⟩δ.

We have two cases depending on whether k = 0 or not.

If k = 0 then M, s, Val ⊧ φ(ff ) hence from the assumption that φ(ff ) ⊢ Δ is valid in M we have that M, s, Val ⊧ δ for some δ ∈ Δ, contradiction.

If k > 0 then let Val′ be identical to Val except that for the variable Z and let Val′(Z) = ∥ α^{k−1}(ff ) ∥_{V al}. Hence M, s, Val′ ⊧ φ(α(Z)) and from Fact 3.2 it follows that M, s, Val′ ⊧ φ(α(μX.Z ∧ α(X))). From the validity of the second premise we have that either: M, t, Val′ ⊧ φ(μX.Z ∧ α(X)) for some state t reachable from s by P, or M, s, Val ⊧ δ for some δ ∈ Δ. The second case is impossible by assumption.

If M, t, Val′ ⊧ φ(μX.Z ∧ α(X)) then by Fact 3.2 M, t, Val′ ⊧ φ(Z), hence M, t, Val ⊧ φ(α^{k−1}(ff )). By the choice of k there must exist δ ∈ Δ s.t. M, t, Val ⊧ ⟨P^{∗}⟩δ. But then because t is reachable from s by a sequence of actions from P we also have that M, s, Val ⊧ ⟨P^{∗}⟩δ. Contradiction.

3.2 Some properties of the system

In this subsection we would like to prove some properties of the presented system. First we show that a substitution of equals for equals is admissible.

Fact 3.4 Let ψ(X_{1}, …, X_{n}) be a formula with variables X_{1}, …, X_{n} occurring only positively in ψ. If for any i = 1, …, n a sequent δ_{i} ⊢ γ_{i} is provable then the sequent ψ(δ_{1}, …, δ_{n})⊢ψ(γ_{1}, …, γ_{n}) is provable.

This will follow from

Lemma 3.5 Let X⃗ and Y⃗ denote the sequences of variables X_{1}, …, X_{n} and Y_{1}, …, Y_{n} respectively. Let φ(X⃗) be a formula with free variables among X⃗ each of them occurring only positively or only negatively in it. Let P = {a_{1}, …, a_{i}} be the set of all the actions occurring in φ(X⃗). For any finite set of formulas Δ there is a diagram of φ(X⃗) ⊢ φ(Y⃗), ⟨P^{∗}⟩Δ in which the only leaves which are not axioms are of the form X_{i} ⊢Y_{i}, ⟨P^{∗}⟩Δ, if X_{i} occurs only positively, and Y_{i} ⊢X_{i}, ⟨P^{∗}⟩Δ, if X_{i} occurs only negatively in φ(X_{1}, …, X_{n}).

Proof We proceed by induction on the structure of φ.

— if φ is one of the free variables or some propositional constant then the lemma is obvious.

— if φ = ¬ψ then the application of the derivable rule

\frac{ψ(Y⃗)⊢ψ(X⃗), ⟨P^{∗}⟩Δ}{¬ψ(X⃗)⊢¬ψ(Y⃗), ⟨P^{∗}⟩Δ}

gives us the desired conclusion.

— if φ = ψ_{1} ∧ ψ_{2} then we use the derivable rule

\frac{ψ_{1}(X⃗)⊢ψ_{1}(Y⃗), ⟨P^{∗}⟩Δ ψ_{2}(X⃗)⊢ψ_{2}(Y⃗), ⟨P^{∗}⟩Δ}{ψ_{1}(X⃗) ∧ ψ_{2}(X⃗)⊢ψ_{1}(Y⃗) ∧ ψ_{2}(Y⃗), ⟨P^{∗}⟩Δ}

— if φ = ⟨a⟩ψ then the rule to use is (⟨⟩)

\frac{ψ(X⃗)⊢ψ(Y⃗), ⟨P^{∗}⟩Δ}{⟨a⟩ψ(X⃗)⊢⟨a⟩ψ(Y⃗), ⟨P^{∗}⟩Δ}

— if φ = μV.β(V) then we use rule (ind) to the sequent

μV.β(V, X⃗), νV.¬β(¬V, Y⃗)⊢⟨P^{∗}⟩Δ  (5)

from which the sequent

μV.β(V, X⃗)⊢μV.β(V, Y⃗), ⟨P^{∗}⟩Δ

can be obtained by a (cut) with an axiom. The sequents:

ff , νV .¬β(¬V , Y⃗ ) ⊢ ⟨P^{∗}⟩Δ  (6)

β(μV.Z ∧ β(V, X⃗), X⃗), νV.¬β(¬V, Y⃗) ⊢

⟨P^{∗}⟩((μV.Z ∧ β(V, X⃗)) ∧ νV.¬β(¬V, Y⃗)), ⟨P^{∗}⟩Δ (7)

are assumptions of the instance of (ind) rule in which (5) is the conclusion.

Clearly (6) is provable so it has a diagram with all the leaves labeled by axioms. Sequent (7) can be obtained by cut rule from an axiom and the sequent:

\begin{matrix}β(μV.Z ∧ β(V, X⃗), X⃗) ⊢ \\ β(μV.β(V, Y⃗), Y⃗), ⟨P^{∗}⟩((μV.Z ∧ β(V, X⃗)) ∧ νV.¬β(¬V, Y⃗)), ⟨P^{∗}⟩Δ \end{matrix} (8)

By induction hypothesis there is a diagram for (8) which leaves are labeled by axioms or sequents of one of the forms:

X_{i} ⊢Y_{i}, ⟨P^{∗}⟩((μV.Z ∧ β(V, X⃗)) ∧ νV.¬β(¬V, Y⃗)), ⟨P^{∗}⟩Δ  (9)
Y_{i} ⊢X_{i}, ⟨P^{∗}⟩((μV.Z ∧ β(V, X⃗)) ∧ νV.¬β(¬V, Y⃗)), ⟨P^{∗}⟩Δ (10)
μV.Z ∧ β(V, X⃗)⊢
μV.β(V, Y⃗), ⟨P^{∗}⟩((μV.Z ∧ β(V, X⃗)) ∧ νV.¬β(¬V, Y⃗)), ⟨P^{∗}⟩Δ (11)

Sequents of the form (9) and (10) can be put into the desired form after application of weakening to the right side. Sequent (11) is clearly provable hence it has a diagram with all the leaves labeled by axioms.

— in cases when φ = ψ_{1} ∨ ψ_{2}, φ = [a]ψ or φ = νV.β(V) we can just use the fact that these connectives are defined by the connectives we have already considered.

The next proposition allows us to restrict attention to positive guarded formulas.

Proposition 3.6 Any formula is provably equivalent to some positive guarded formula

Proof The proof is a repetition of the arguments from Proposition 2.2. Fact 3.4 allows us to show that all the steps use provable equivalences. One can show that μX.(X ∨ ᾱ(X)) ∧ β(X) is provably equivalent to μX.ᾱ(X) ∧ β(X) using Lemma 3.5.

3.3 Comparison with Kozen’s axiomatisation

Here we would like to relate presented axiomatisation to Kozen’s axiom system from [12]. Let us call this system Kμ here.

The system Kμ uses a different form of judgement. It has the form of equality φ = ψ with the meaning that the formulas φ and ψ are semantically equivalent. Inequality φ ≤ ψ is considered as an abbreviation of φ ∨ ψ = ψ.

Apart from the axioms and rules of equational logic (including substitution of equals by equals) there are the following axioms and rules:

(K1) axioms for Boolean algebra
(K2) ⟨a⟩φ ∨ ⟨a⟩ψ = ⟨a⟩(φ ∨ ψ)
(K3) ⟨a⟩φ ∧ [a]ψ ≤ ⟨a⟩(φ ∧ ψ)
(K4)  ⟨a⟩ff = ff
(K5) α(μX.α(X)) ≤ μX.α(X)
(K6)  \frac{α(φ) ≤ φ}{μX.α(X) ≤ φ}

Our sequent Γ⊢Δ corresponds to inequality ⋀ Γ ≤ ⋁ Δ in this notation. We will call a rule derivable in system Kμ iff there is a way to derive the conclusion of the rule, assuming all the premises of the rule.

Proposition 3.7 Every rule derivable in the system Kμ must have the property: for any structure M, if all the premises of the rule are valid in M (i.e. true in every state of M) then the conclusion is valid in M

The proposition follows directly from the observation that all the rules of Kμ have this property. We will show that the rule (ind) of our system does not have this property hence it cannot be derived in Kμ.

Proposition 3.8 There is a structure M and an instance of (ind) rule such that the premises are true in M but the conclusion is not.

Proof Consider a structure M = ⟨S, R, ρ⟩ such that:

• S = N ∪ {∞}

• R(a) = {(i + 1, i) : i ∈ N } ∪ {(∞, i) : i ∈ N }

• ρ(p) = {∞}

Here a is some action, p is some propositional constant and N is the set of natural numbers.

Consider a sequent:

p ∧ [a]μX.[a]X ⊢

which is not valid in M because M, ∞ ⊧ p ∧ [a]μX.[a]X. If we were to prove this sequent we could use rule (ind) directly and have the premises:

p, [a]ff ⊢  (12)
p, [a]([a]μX.Z ∧ [a]X)⊢p ∧ [a]μX.Z ∧ [a]X  (13)

Clearly sequent (12) is true in M. To see why sequent (13) is true in M suppose that for some valuation Val we have M, ∞, Val ⊧ p ∧ [a][a](μX.Z ∧ [a]X) then clearly N ⊆ Val(Z) hence also by Fact 3.2, N ⊆ ∥ μX.Z ∧ α(X) ∥_{V al} which means that M, ∞, Val ⊧ p ∧ [a](μX.Z ∧ [a]X).

Of course Proposition 3.8 does not imply incompleteness of the system Kμ even though our system is strictly stronger than Kμ as the following proposition shows.

Proposition 3.9 All the axioms of the system Kμ are provable in our system. All the rules of Kμ are derivable in our system

Proof Provability of the axioms is easy, so is also deriveability of all the rules other then (K6) and substitution of equals by equals. This second rule is derivable by Fact 3.4.

For rule (K6) let us assume α(φ) ⊢ φ. We will show how to prove ¬φ ∧ μX.α(X) ⊢ . Let P = {a_{1}, …, a_{i}} be the set of all the actions occurring in α(φ).

We can obtain ¬φ ∧ μX.α(X)⊢ from (ind) rule if we prove

ff ∧ ¬φ⊢ and ¬φ ∧ α(μX.Z ∧ α(X))⊢⟨P^{∗}⟩¬φ ∧ μX.Z ∧ α(X)

The first sequent is clearly provable. Using assumption that α(φ) ⊢ φ we will have a proof of the second sequent if we only prove:

¬α(φ) ∧ α(μX.Z ∧ α(X))⊢⟨P^{∗}⟩¬φ ∧ μX.Z ∧ α(X)

This in turn is equivalent to proving

α(μX.Z ∧ α(X))⊢α(φ), ⟨P^{∗}⟩¬φ ∧ μX.Z ∧ α(X)

By Lemma 3.5 there is a diagram for this sequent in which the only leaves which are not axioms are of the form

μX.Z ∧ α(X)⊢φ, ⟨P^{∗}⟩¬φ ∧ μX.Z ∧ α(X)

But such sequent is easily provable.

4 Completeness

In this section we will prove completeness of our system. Let us fix an unsatisfiable positive guarded formula φ_{0} of the μ-calculus. We also fix D_{φ_{0}} to denote the definition list [⟩φ_{0}⟨] = (W_{1} = σX.γ_{1}(X)) … (W_{d} = σX.γ_{d}(X)). We will consider only definition constants from D_{φ_{0}} and when we will say that a definition constant is older (younger) than the other we will mean that it is older (younger) with respect to the definition list D_{φ_{0}}. Our goal in this section will be to construct a proof of the sequent φ_{0} ⊢ in our system.

4.1 Overview of the proof method

Let us now give an overview of the proof method we will use. We would like to show that it is an extension of a very natural method of proving completeness for system K of modal logic.

Let us consider only positive formulas of simple modal logic, that is positive formulas of the μ-calculus without fixpoint operators. We consider sequents of such formulas of the form Γ⊢. The interpretation of such a sequent is standard, i.e., that the conjunction of formulas in Γ is not satisfiable. For such sequents of this simple logic the system consisting of one side versions of (∧), (∨) and (⟨⟩) rules is sufficient. This are exactly rules (∧_{t}), (∨_{t}) and (⟨⟩_{t}) of our tableau system as there are no definition constants in this case.

A proof of a sequent Γ ⊢ in this system is a diagram obtained using the rules mentioned above with the root labeled by Γ⊢ and all the leaves labeled by sequents containing some propositional letter and its negation.

For completeness proof we will use tableaux which will be constructed with the above rules except (⟨⟩_{t})-rule which is replaced by:

(all⟨⟩) \frac{\{α, \{β : [a]β ∈ Γ\}⊢: ⟨a⟩α ∈ Γ\}}{Γ⊢}

This rule has as many assumptions as the number of formulas of the form ⟨a⟩α in Γ. When there are no such formulas at all then we cannot apply this rule. Rule (all⟨⟩) can be seen as a very weak logical rule but it is probably better not to look at it this way. It is rather different type of rule, because it is enough to prove only one of the assumptions of the rule to prove the conclusion, while for other rules we have to prove all the assumptions. This distinction will be elaborated below.

Given a sequent Γ ⊢ of positive formulas, we construct a tableau for it in this tableau system. We would like tableaux to be maximal in a sense that rule (all⟨⟩) is used only to sequents Σ ⊢ such that each formula in Σ is either a propositional constant, its negation or a formula of the form ⟨b⟩β or [b]β for some action b and a formula β. A tableau constructed in this way is obviously finite. Some of the leaves are axioms and others are unreducible sequents which are not axioms.

The general property of such a tableau for Γ ⊢ is that one can either find a proof of Γ ⊢ in the tableau or one can read a finite model for the formula ⋀ Γ from it. To see this let us apply the following simple marking procedure.

We mark all the leaves labeled with axiom sequents with 1 and all other leaves with 0. Then if in a node of the tableau rule (∧_{t}) was used we mark it by the same number as its only son. If (∨_{t}) was used in a node and both sons are labeled by 1 then we mark the node by 1 otherwise we mark it by 0. For each node where (all⟨⟩) was used we mark it with 0 if all the sons of it are marked with 0, otherwise we mark it with 1. It should be obvious that if the root of the tableau is marked with 1 then there is a proof of Γ ⊢ in the tableau. If the root of the tableau is labeled by 0 then we can find a model for ⋀ Γ in the tableau.

When we try to apply the above method to the full μ-calculus we meet one complication. It seems that the only obvious rules we can add for dealing with fixpoints are unwinding rules of the form:

α(μX.α(X)), Γ⊢
μX.α(X), Γ⊢

But tableaux constructed with this rule may not be finite and finiteness of tableaux was crucial for the above completeness proof.

In case of the full μ-calculus Theorem 2.8 takes the place of the marking procedure. In system K for any unsatisfiable formula the marking procedure gave us a finite tree designated by 1’s. By Theorem 2.8 any unsatisfiable formula of the μ-calculus has a refutation. Refutation is very similar to the tree obtained from the marking procedure except that it may have infinite paths. While marking procedure gave us a proof right away here we will have to work hard to transform a refutation into a proof which must be a finite tree.

The difficulty we face is as follows. On any infinite path of a refutation for φ_{0} there is a μ-trace, i.e., there is an occurrence of a μ-formula which regenerates i.o. and never disappears. It was already shown by Kozen [12] how to use some derivable rules of his system in such a clever way that it is possible to “cut” such a path, i.e., arrive at an axiom sequent after a finite number of steps. We can of course apply such a cutting strategy to each path of a refutation. The problem is that we will obtain a set of finite paths, each of them ending with an axiom, but usually it would be impossible to compose them back to a tree.

There is a similar problem in automata theory, when one wants to construct a tree automaton recognising trees the paths of which are accepted by a nondeterministic Büchi automaton. The solution there is to determinize the automaton first. In our case it means that we need a deterministic strategy of transforming a path of a refutation into a path of a proof. Here deterministic means that the actions we perform in a node depend only on the predecessors of the node and not on the whole path.

First step of the proof is construction of a deterministic Rabin automaton on infinite words A_{φ_{0}} recognising paths of a tableau for φ_{0} with μ-trace on them. Later states of A_{φ_{0}} will be used to guide our converting procedure hence the simpler automaton we construct the simpler will be our procedure. This is why we do not use any standard determinization constructions but define A_{φ_{0}} from the scratch. The construction is nevertheless based on Safra’s determinization [20].

From A_{φ_{0}} we construct an appropriate Rabin automaton over one letter alphabet TA_{φ_{0}} whose runs closely correspond to refutations of φ_{0}. This allows us to conclude that there is a small graph G_{φ_{0}}, with states of TA_{φ_{0}} as nodes, which unwinds to an accepting run of TA_{φ_{0}}.

Next step is to examine the structure of G_{φ_{0}}. It turns out that in this graph special nodes, which we call loop nodes, can be distinguished. This nodes can be seen as “witnesses” that unwinding of G_{φ_{0}} is accepted by the automaton. On every cycle there is exactly one loop node which “confirms” that the unwinding of the cycle is accepted by A_{φ_{0}}. Another important thing is that there is a natural partial order on loop nodes. In this way we can put some order of “importance” on different loops we have in G_{φ_{0}}.

We use this ordering to unwind G_{φ_{0}} into T_{φ_{0}} which is a finite tree with back edges, i.e., edges from some of the leaves to their ancestors. The last step is construction of a sound sequent assignment for T_{φ_{0}}; that is assign φ_{0} ⊢ to the root, assign an easily provable sequent to every leaf of T_{φ_{0}}, and for any other node assign a sequent which is provable from the sequents assigned to its sons.

The rest of this section is organised as follows. In the next subsection we describe the construction of the automaton A_{φ_{0}}. Subsection 4.3 is devoted to the construction of T_{φ_{0}}. Finally we define a sound sequent assignment for T_{φ_{0}}.

4.2 Automaton

Our goal here is to construct a special Rabin automaton TA_{φ_{0}} on trees over one letter alphabet, which accepting runs closely correspond to the refutations of φ_{0}. We do this by constructing a special deterministic Rabin automaton A_{φ_{0}} on paths, which recognises exactly the paths of a tableau for φ_{0} with μ-trace on them.

Let us first observe that the set of formulas which can appear in a refutation for φ_{0} is finite. Let us call this set F L(φ_{0}) as it is almost Fisher-Ladner closure [7] of φ_{0}. It is not exactly the closure because we have definition constants around.

Definition 4.1 For any formula φ, possibly with definition constants, we define the FL-closure of φ, F L(φ) as the set of all formulas which can occur in a sequent Σ ⊢_{D_{φ_{0}}} obtainable from φ ⊢_{D_{φ_{0}}} by application of some number of the tableau rules.

Lemma 4.2 For any formula φ the size of F L(φ) is linear in the size of ⟨[φ]⟩_{D_{φ_{0}}} , which is φ with all definition constants replaced by appropriate formulas.

There is of course simple nondeterministic Büchi automaton recognising the paths with a μ-trace. This automaton goes along a path and picks one formula from each tableau sequent in such a way that the sequence of chosen formulas forms a trace. Acceptance conditions are such that this chosen trace is accepted iff it is a μ-trace. Obviously this automaton is nondeterministic because of the tableau rule (and). If we have chosen formula α ∧ β in a sequent α ∧ β, Γ ⊢_{D} then after application of rule (and) we obtain a sequent α, β, Γ ⊢_{D} and we may choose either α or β as the next formula in the trace being constructed.

Instead of determinizing this Büchi automaton we will construct A_{φ_{0}} from the scratch. This construction is an adaptation of the Safra’s determinization construction to the special case we are to deal with. We have to adapt the construction to avoid some redundancies which we would get if we applied Safra’s construction directly.

As in Safra’s construction states of our automaton will be labeled trees. Since we will quickly arrive at trees labeled with states which are itself trees, we will always call nodes of states vertices and nodes of trees of states just nodes.

The idea of Safra’s construction was to construct for a given nondeterministic automaton a deterministic automaton which, for an infinite word σ, calculates during the run the set of states S which has the special property that there are positions k_{1}, k_{2}, … such that:

• every state from S is reachable on the word σ[1, k_{1}], (σ[i, j] stands for the part of σ between positions i and j),

• for any i = 1, 2, … and any state s ∈ S there is a state s′ ∈ S such that the automaton started in s′ will reach s on word σ[k_{i}, k_{i+1}] and go through a green state on the way.

Obviously if there is such a nonempty set of states then there is an accepting run of the original automaton. It turns out that the converse also holds.

We will use the same idea in our case. We will design an automaton which given a path of a tableau (Γ_{1} ⊢_{D_{φ_{0}}} , Γ_{2} ⊢_{D_{φ_{0}}} , …) will calculate a set of formulas Ω and a μ-constant U from D_{φ_{0}} such that there are integers k_{1}, k_{2}, … with the property that:

• Ω ⊆ Γ_{k_{1}},

• for any i = 1, 2, … and any α ∈ Ω there is β ∈ Ω and a trace from occurrence of β in Γ_{k_{i}} to the occurrence α in Γ_{k_{i+1}} on which U is the oldest regenerated constant.

We are now going to construct such an automaton A_{φ_{0}} for a formula φ_{0}. Its states will be trees labeled with formulas. As we have to calculate definition constant we introduce also labeling of the edges with definition constants.

States of the automaton A_{φ_{0}} will be labeled ordered trees, i.e., tuples T = ⟨N, r, p, ≺, nl, el⟩ where:

• N is a set of vertices,

• r ∈ N is a root of the tree,

• p : (N \ {r}) → N is a parenthood function,

• ≺ is a sibling ordering, i.e., partial ordering relation which linearly orders nodes with a common father,

• nl(v), for any vertex v ∈ N, is a non-empty subset of F L(φ_{0}) called a node label of v.

• el(v), for any vertex v ∈ N \ {r}, is a definition constant from D_{φ_{0}} called an edge label of v.

Additionally each vertex can be colored white or green and the following conditions hold:

1. For any vertex v and its son w the label of w is contained in the label of v.

2. For any vertex v the union of the node labels of those sons of v which edge labels are equal el(v) is a proper subset of nl(v).

3. Any two sons of the same vertex have disjoint node labels.

4. If w is a son of v then el(w) is not older than el(v) with respect to the definition list D_{φ_{0}}.

5. If el(v) is a ν-constant then v has no ν-sons, i.e., sons with the edge label being a ν-constant.

6. For any two sons, v and w, of the same vertex, if el(v) is older than el(w) with respect to D_{φ_{0}}, then v ≺ w.

Ordering ≺ can be extended to an ordering between not necessarily ancestral vertices. We say that v is to the left of w iff some (maybe not proper) ancestor of v is smaller in ≺ ordering than some (maybe not proper) ancestor of w. If v is a son of w and el(v) = W then we say that v is a W -son of w. Conditions 1 and 3 guarantee that for any formula ψ occurring in a state s there is the lowest vertex v such that ψ ∈ nl(v). We will call such a vertex the ψ-vertex of s.

The initial state of the automaton will be a tree consisting only of the root labeled {φ_{0}}.

Next we describe the deterministic transition function of the automaton. It will be always the case that after reading a sequent Σ ⊢_{D_{φ_{0}}} the automaton will enter a state with the root labeled by Σ. Suppose the automaton is in a state s after reading Σ ⊢_{D_{φ_{0}}} and the next input is Σ′ ⊢_{D} . The next state is obtained by applying to the tree s the following sequence of actions:

1. Set the color of all the vertices to white.

2. Look at the next sequent Σ′ ⊢_{D_{φ_{0}}} on the path and locally transform the labels of some vertices, depending on the rule applied to obtain this sequent:

— for all the rules other then (const), in all vertices of s replace the reduced formula with the resulting formulas appearing in Σ′. This means that for all the rules other then (⟨⟩_{t}) the reduced formula is replaced by at most two resulting formulas and the other formulas remain intact. In case of the (⟨⟩_{t}) rule:

\frac{⟨a⟩α, Σ ⊢_{D}}{α, \{β : [a]β ∈ Σ\} ⊢_{D_{φ_{0}}}}

we first delete all formulas not of the form [a]β, for some β, except the formula ⟨a⟩α. Then we replace ⟨a⟩α with α and [a]β with β in each node label of s

— Suppose we apply regeneration rule (const):

\frac{U, Γ ⊢_{D_{φ_{0}}}}{α(U), Γ ⊢_{D_{φ_{0}}}}

Let v be the lowest vertex of s such that U ∈ nl(v) and el(v) is not younger (older or equal with respect to D_{φ_{0}}) than U. If there is no such vertex then let v be the root of s. First replace U with α(U) in the node label of v and in the labels of all ancestors of v. Next delete U from node labels of all proper descendants of v. Additionally, if U or el(v) is not a ν-constant, create a son w of v, with labels el(w) = U and nl(w) = {α(U)}. Finally make w ≺-bigger than all its brothers with edge labels not younger than U and smaller from all other brothers.

3. For any vertex v, if a formula φ occurs already in a vertex to the left of v then delete φ from the node label of v.

4. Delete all vertices with empty labels.

5. For any vertex v such that el(v) = U is a μ-constant and nl(v) is equal to the sum of the labels of its U-sons, light v green and delete all descendants of v from the tree.

A run of automaton A_{φ_{0}} is accepting iff there is a vertex which disappears only finitely many times and lights green infinitely many times on the run.

One word must be said about “vertex management”. In clause 2 of the definition of the transition function we are at some point required to add a new vertex to a state, i.e., one not occurring in it already. Clearly we cannot have an infinite supply of vertices because the number of states of the automaton must be finite. The solution is to “reuse” vertices, i.e., when a vertex is deleted we put it into a common pool and when a new vertex is needed just take any vertex from the pool. If we put initially into the pool more vertices then the size of the largest possible state then we would be sure that there is always something in the pool when needed. Hence our first step is to find the bound on the size of the states of A_{φ_{0}}.

Lemma 4.3 The size of a state tree is bounded by n ∗ m + 1 where n is the number of formulas in F L(φ_{0}) and m is the number of definition constants in D_{φ_{0}}. The number of states is finite.

Proof Let s be any state of G_{φ_{0}}. With every vertex v of s, except the root, we can assign a pair (el(v), φ), where φ ∈ nl(v) is a formula not occurring in any el(v)- son of v. This shows the upper bound on the number of states because the assignment is injective.

The second part of the lemma follows directly from the first if we apply the strategy for “reusing vertices” described above.

Hence what we have described is a Rabin automaton on strings. Before proving correctness of the construction let us focus on one more specialised property of the A_{φ_{0}} which we will need in the future.

Lemma 4.4 For any μ-constant U_{i} = μX.α_{i}(X) in D_{φ_{0}}, state s reachable from the start state of the automaton A_{φ_{0}} and vertex v of s such that el(v) = U_{i}, the formula μX.α_{i}(X) does not belong to nl(v).

Proof Let us take a μ-constant U_{i} as above and define the set of formulas Cl as the smallest set such that:

• α(U_{i}) belongs to Cl,

• if ψ ∈ Cl then all subformulas of ψ belong to Cl,

• if σX.β(X) ∈ Cl and there is a definition constant W such that (W = σX.β(X)) is in D_{φ_{0}} then β(W) belongs to Cl.

Observe that μX.α_{i}(X) ∉ Cl because all formulas in Cl are shorter. For any state s and its vertex v, s.t. el(v) = U_{i} we show by induction on the number of steps needed to reach state s, that nl_{s}(v) ⊆ Cl.

The base step is when the vertex v is created in a state s. It’s label is then exactly {α(U_{i})}. The induction step is straightforward.

Finally we show correctness of the construction

Proposition 4.5 The automaton accepts a path P of a tableau for φ_{0} iff there exists an infinite μ-trace on P.

The proof of the proposition is very similar to the proof of correctness of the Safra’s construction. First let us prove left to right implication.

Lemma 4.6 If the automaton A_{φ_{0}} accepts a path P of a tableau for φ_{0} then there exists an infinite μ-trace on the path.

Proof Consider an accepting run of the automaton s_{0}, s_{1}, ... We will denote by nl_{i}, el_{i} the node labeling and the edge labeling of the state s_{i} respectively. Let v be a vertex which lights green i.o. in this run and disappears only finitely many times. Consider two positions i, j, after v disappears last time, such that v lights green in s_{i} and next time it lights green in s_{j}.

First we would like to show that for every formula in nl_{j}(v) there exists a trace from some formula in nl_{i}(v) such that the oldest constant regenerated on the trace is el_{i}(v) = el_{j}(v). Clearly el_{i}(v) is a μ-constant. To do this we show that for any s_{k}, between s_{i} and s_{j}, and any formula φ ∈ nl_{k}(v):

• if φ ∈ nl_{k}(w) for some son w of v, then there is a part of a trace to φ from some formula in nl_{i}(v) such that the highest regeneration on it is that of el_{k}(w)

• otherwise there is a part of a trace to φ from some formula in nl_{i}(v) without any regeneration at all.

The proof is by induction on the distance from s_{i}

• Base step when k = i is trivial.

• All steps except of regenerations are rather straightforward.

• If the last step was regeneration of a constant V then we have two cases. The first is when V ∉ nl_{k}(v) or V is older than el_{k}(V). This case is easy because the only thing which can happen is that some formula can be removed from the labels of all the vertices in the subtree of v.

In the other case when V ∈ nl_{k}(v) and el_{k}(v) is not younger than V we have two possibilities

– If there is a son w of v, such that V ∈ nl_{k}(w) and el_{k}(w) is not younger than V then no new son of v is created and V is replaced by an appropriate α(V) in the label of w. This is sound as there is a trace to α(V) with the oldest regeneration being that of el_{k}(w) because there was one to V by induction hypothesis.

– If, on the other hand, V is older than el_{k}(w) or there is no w at all then from the induction hypothesis there is a trace to V on which no constant older than V was regenerated. Hence there is a trace to α(V) where V is the oldest regenerated constant. According to the definition of the transition function a new son w′ of v is created with the node label {α(V)} and edge label V. Additionally V is deleted from the label of w. These are exactly the steps which must be done to make the induction thesis satisfied.

Observe that vertices with edges labeled with ν-constants were needed in the last step of the above induction.

Now consider a graph with the set of nodes

{(φ, k) : φ ∈ nl_{k}(v), v lights green in s_{k}}

and an edge from (φ_{1}, k_{1}) to (φ_{2}, k_{2}) whenever there is a trace from φ_{1} in s_{k_{1}} to φ_{2} in s_{k_{2}} on which el(v) is the oldest regenerated constant. Here v is our node which lights green infinitely often on the run. From what we have shown above it follows that at for any (φ, k) there is an edge leading to it from some (φ′, k′). This is because v lights green only when the sum of the labels of its el(v)-sons is equal nl(v). This means that at least a part of this graph is an infinite connected directed acyclic graph. The degree of every vertex of it is of course finite hence there must exist an infinite path in this graph. This path is a μ-trace we were looking for.

Lemma 4.7 If there is a μ-trace on a path P of a tableau for φ_{0} then the automaton A_{φ_{0}} accepts P.

Proof Let us consider a path P with a μ-trace and the run of the automaton, s_{0}, s_{1}, … on it. The trace on P is a sequence of formulas {α_{i}}_{i∈N}, s.t. α_{i} occurs in the i-th tableau sequent of P. On the other hand the automaton A_{φ_{0}} has the property that after reading a tableau sequent Σ ⊢_{D_{φ_{0}}} , the root of its current state is labeled by Σ. Hence α_{i} is always present in the root of the state s_{i}.

From some moment j_{0}, the oldest constant regenerated on the trace is some μ-constant U. We can assume, without loss of generality, that α_{j_{0}} occurs in a son of the root with edge label, not younger than U. Indeed, otherwise we just have to wait, in the worst case, for the next regeneration of U. From that moment formulas from the trace can only move to the left according to clause 3 of the description of the transition function. But because they can do it only finitely many times, after some time the trace must settle in some son of the root, say v_{0}, forever.

If v_{0} lights green i.o. then we are done. If not then let j_{1} be the last moment v_{0} lights green. Not later than the next regeneration of U the formula from the trace will appear in some W_{1}-son of v_{0} where W_{1} is not younger than U. After some moves to the left it must settle in some v_{1} forever. If v_{1} lights green i.o. we are done if not we repeat the reasoning and find a son of v_{1}, v_{2} an so on. Observe that we cannot go this way forever because each state is a tree of bounded size.

Together Lemmas 4.7 and 4.6 prove Proposition 4.5 thereby showing correctness of the construction.

Automaton A_{φ_{0}} expands to a nondeterministic automaton on trees over one letter alphabet TA_{φ_{0}}, such that its accepting runs closely correspond to the refutations of φ_{0}. Automaton TA_{φ_{0}} nondeterministically constructs a refutation for φ_{0} and runs A_{φ_{0}} on each path. There is no need to remember refutation separately because sequents which are read by A_{φ_{0}} are remembered in the roots of the corresponding states. Hence states of TA_{φ_{0}} are exactly the states of A_{φ_{0}}. The roots of the states of an accepting run of TA_{φ_{0}} give us a refutation of φ_{0}. Other way around given a refutation of φ_{0} we can run the path automaton A_{φ_{0}} on each path of the refutation separately and because it is deterministic we will obtain a tree which is an accepting run of TA_{φ_{0}}.

In [2] the following theorem is (implicitly) stated

Theorem 4.8 (Emerson) Suppose A is a Rabin automaton over a single letter alphabet. If A accepts some tree then there is a graph G with states of A as nodes which unwinds to an accepting run of A.

Because we know that there is a refutation of φ_{0}, from this theorem we conclude that there is a graph G_{φ_{0}}, with states of A_{φ_{0}} as nodes, which unwinds to an accepting run of TA_{φ_{0}}. In the next sections we will show how to construct a proof of φ_{0} ⊢ from this graph.

4.3 Constructions on the graph

In this section we investigate the properties of the graph G_{φ_{0}}. We define several concepts which in turn will allow us to define an unwinding of G_{φ_{0}} into a finite tree with “back edges” T_{φ_{0}}.

Let us examine the structure of G_{φ_{0}}. Since the unwinding of G_{φ_{0}} is accepted by TA_{φ_{0}}, we know that on any infinite path of it there is a confirming vertex, i.e., a vertex which lights green i.o. and disappears only finitely many times. The crucial observation is that for any state s of G_{φ_{0}} and any path P passing i.o. through s, a confirming vertex of P belongs to s. Moreover we can linearly order such confirming vertices. Intuitively, if we have this ordering Ord(s) = (v_{1}, …, v_{k}) we know that on any cycle going through s, some v_{i} lights green and none of v_{1}, …, v_{i−1} disappears.

More formally let us start by fixing some arbitrary linear ordering on the set of all the vertices occurring in G_{φ_{0}}, then Ord(s) can be described as follows:

Definition 4.9 For any node s of G_{φ_{0}} we define an ordering of some of the vertices from s. Let Ord(s) be the list (v_{1}, …, v_{k}) such that for each i = 1, …, k, v_{i} is defined by the following rule:

Consider a graph obtained from G_{φ_{0}} by deleting all the nodes where one of the vertices v_{1}, …, v_{i−1} lights green. Let C_{i} be the nontrivial strongly connected component of this graph containing node s. Then v_{i} is the smallest vertex, in our fixed linear ordering on all vertices, such that v_{i} does not disappear in any node of C_{i} and lights green in some node of C_{i}.

It easy to check that we can always find a vertex v_{i} required in the above definition. If there were no such vertex then we would take a cycle through all the nodes of the strongly connected component and unwind it to an infinite path which would not be accepted by the automaton A_{φ_{0}}. This would be a contradiction with the assumption that G_{φ_{0}} unwinds to an accepting run of TA_{φ_{0}}.

The ordering Ord(s) allows us to distinguish some special nodes of G_{φ_{0}}, namely such that a vertex from Ord(s) lights green in s. Observe that such a vertex must be the last vertex in Ord(s).

Definition 4.10 A node s of G_{φ_{0}} is called a loop node if Ord(s) = (v_{1}, …, v_{i}) and v_{i} lights green in s. Vertex v_{i} will be called the green vertex of s.

Loop nodes are the nodes where we will apply our induction rule. This is why we duplicate each loop node in the definition of T_{φ_{0}} below.

Definition 4.11 We will unwind graph G_{φ_{0}} to a finite tree with back edges T_{φ_{0}}. Nodes of T_{φ_{0}} will be sequences consisting of nodes from G_{φ_{0}} and pairs (node, 0 or 1). For any sequence n and a node or a pair x we denote by nx a path obtained by concatenating x to the end of n; we denote the last element of the sequence by n ↓. Hence nx ↓= x. It will be also convenient to extend the definition of Ord, we let Ord((s, 1)) = Ord((s, 0)) = Ord(s). Tree T_{φ_{0}} is defined as follows:

• The root of T_{φ_{0}} is the sequence consisting only of the initial node of G_{φ_{0}}.

• A node n of T_{φ_{0}} is final iff one of the conditions holds:

1. There is a prefix m(m ↓, 0) of n such that for the green vertex v of m ↓ we have: (i) definition constant el(v) appears in the node label of v in n ↓, and (ii) v appears in Ord(m′ ↓), for any prefix m′ of n longer than m.

2. There is a prefix m(n↓, 1) of n with the property that for any longer prefix m′ of n, Ord(n↓) is a prefix of Ord(m′ ↓). In this case we will say that there is a back edge from n to m.

Finial nodes will have no prolongation in T_{φ_{0}}.

• If not final node n belongs to T_{φ_{0}} and n↓ is not a loop node then for any son s in G_{φ_{0}} of the last state in n we add a node ns.

• If not final node n belongs to T_{φ_{0}}, and n↓ is a loop node then we add two nodes n(n↓, 0) and n(n↓, 1).

Fact 4.12 Tree T_{φ_{0}} constructed above is finite.

Proof Suppose that there is an infinite path P in T_{φ_{0}} without taking a back edge. Let us take any node s of G_{φ_{0}} which occurs infinitely often on this path. Consider Ord(s) = (v_{1}, …, v_{k}). By definition of Ord(s) on any path of G_{φ_{0}} between any two occurrences of s some vertex from v_{1}, …, v_{k} must light green. Let us take the smallest i s.t. v_{i} lights green i.o. on P.

Let s′ be the state which occurs i.o. on the path and where v_{i} lights green. Because from some point v_{1}, …, v_{i−1} don’t light green on P there must be a cycle in G_{φ_{0}} from s to s′ and back to s on which none of v_{1}, …, v_{i−1} lights green. It follows from the definition of Ord(s) that none of v_{1}, …, v_{i} disappears on such a cycle. Hence Ord(s′) = (v_{1}, …, v_{i}). So s′ is a loop node and v_{i} is its green vertex.

Let ms′ and ns′ be two nodes of P such that none of v_{1}, …, v_{i−1} lights green in the nodes in between. It should be clear that for any node o between ms′ and ns′, Ord(s′) is a prefix of Ord(o↓). To light green v_{i} must have at least one el(v_{i})-son and this may be created only when el(v_{i}) ∈ nd(v_{i}). If the next node after ms′ were ms′(s′, 0) then between ms′ and ns′ we could find a final node of the first type. So the next node after ms′ is ms′(s′, 1). But in this case ns′ is a final node of the second type.

The next concept is very important although quite straightforward. We will need to assign provable sequents to final nodes. To do this for any node n we need to know all its ancestors to which we may come by taking a back edge. This set will be called the set of active nodes of a node. We will use it for final nodes of the second type. For final nodes of the first type it is enough to keep track of all the prefixes which may cause some descendant of a node to become a final node. This gives us the set AN_{0}.

Definition 4.13 For any node n of T_{φ_{0}} we define the set of active nodes of n, AN (n), as the smallest set such that:

• if there is a back edge from n or some descendant of n to some proper ancestor m of n then m ∈ AN (n),

• if m ∈ AN (n) then AN (m) ⊆ AN (n).

Let AV (n) = {v : m ∈ AN (n), v the green vertex of m↓}. We call it the set of active vertices of n. Observe that only nodes m with m ↓ being a loop node can belong to AN(n).

Let AN_{0}(n) be the set of nodes m such that m(m ↓, 0) is a, maybe not proper, prefix of n and the green vertex of m ↓ appears in Ord(m′ ↓) for any prefix m′ of n longer than m.

Let AV_{0}(n) = {v : m ∈ AN_{0}(n), v the green vertex of m↓}.

Final lemma of this subsection presents the properties of active sets we will use in the last step of the proof.

Lemma 4.14 For any node n of T_{φ_{0}} and v ∈ AV (n), v is a vertex of n↓. For any node nx of T_{φ_{0}}:

• if x is not a pair then AN (n) ⊆ AN (nx) and AN_{0}(n) ⊆ AN_{0}(nx),

• otherwise

AN (n(n↓, 0)) ⊆ AN (n)  AN (n(n↓, 1)) ⊆ AN (n) ∪ {n}
AN_{0}(n(n↓, 0)) = AN_{0}(n) ∪ {n} AN_{0}(n(n↓, 1)) = AN_{0}(n)

Proof To prove the first part of the lemma observe that if m is an ancestor of n to which leads a back edge from some descendant of n then Ord(m ↓) is a prefix of Ord(n↓). From this follows that for any m ∈ AN (n) sequence Ord(m↓) is a prefix of Ord(n↓). Of course all vertices from Ord(n↓) appear in n↓.

The second part of the lemma follows directly from the definition of T_{φ_{0}} and sets of active nodes.

4.4 Overview of the sequent assignment

The last step in the completeness proof is to construct a proof of φ_{0} ⊢from T_{φ_{0}}. This will be done by assigning a sequent to every node of T_{φ_{0}} in such a way that leaves will be assigned provable sequents and a sequent assigned to a father will be provable from the sequents assigned to its sons. Here we would like to give some intuitions about the way it is done. For n a node of T_{φ_{0}} we will use Γ_{n} to denote the set of all the formulas appearing in the last state of n. We will use ⟨[Γ]⟩_{D} as an abbreviation of {⟨[γ]⟩_{D} : γ ∈ Γ}, that is a set of formulas obtained from Γ by replacing definition constants with their definitions form D.

Each node of T_{φ_{0}} is a sequence consisting of states of A_{φ_{0}} and pairs of the form (state, 0 or 1). There is a very easy way of assigning sequents. To every node n of T_{φ_{0}} assign ⟨[Γ]⟩_{D_{φ_{0}}} ⊢. Expansion operation is used to remove possible occurrences of definition constants. By definition of A_{φ_{0}} for every internal node n the set of formulas Γ_{n} is a conclusion in some tableau rule in which sets of formulas occuring in the sons of n are the assumptions. Our simple sequent assignment transforms such a rule into a rule of our system. Hence this assignment is locally sound, that is a sequent assigned to some internal node of T_{φ_{0}} is provable from the sequents assigned to its sons. If all the leaves of T_{φ_{0}} were labeled by axioms than the result would be a proof of φ_{0} ⊢.

In general in T_{φ_{0}} we may have also final nodes which are not axioms and after the simple assignment defined above this nodes will not be labeled by axioms. We need more refined assignment to get axioms in finial nodes. Let us describe its idea.

There are two types of final nodes. Let n be a final node of the first type. This means that there is a prefix m(s, 0) of n such that for the green vertex v of s definition constant el(v) appears in the node label of v in n ↓ and v appears in Ord(m′ ↓), for any prefix m′ of n longer than m.

Let U = el(v) and (U = μX.α(X)) ∈ D_{φ_{0}}. For simplicity assume that nd(v) is one element set, say, {φ(U)}. The simple assignment described above would give us for node m the sequent ⟨[Γ_{m}]⟩_{D_{φ_{0}}} ⊢. Now φ(U) ∈ Γ_{m} and ⟨[φ(U)]⟩_{D_{φ_{0}}} is of the form φ′(μX.β(X)). We can apply (ind) rule to this sequent and assign to m(s, 0) the assumption

φ′(ff ), ⟨[Γ_{m} \ {φ(U )}]⟩_{D_{φ0}} ⊢  (14)

we use \ to denote set subtraction. Let D_{φ_{0}}^{0} be a definition list obtained from D_{φ_{0}} by replacing the definition of U by (U = ff ). Sequent (14) can be presented as ⟨[φ(U)]⟩_{D_{φ_{0}}^{0}} , ⟨[Γ]⟩_{D_{φ_{0}}} ⊢. Let o be a descendant of m and let Γ′_{o} be the node label of v in o. We assign to o the sequent ⟨[Γ′_{o}]⟩_{D_{φ_{0}}^{0}} , ⟨[Γ \ Γ′_{o}]⟩_{D_{φ_{0}}} ⊢. This gives us another locally sound assignment if only v does not disappear on the way from m to o.

If v disappears on the path to o and reappears once again then there is no way of restoring ff in formulas from the label of v. An example of a situation of this kind is presented below. This is a schematic representation of a path from m to o. The first row contains unexpanded sequents the second their expanded versions; third row gives the names of the nodes on the path.

φ(U), Γ ⊢_{D_{φ_{0}}}  φ′(ff ), ⟨[Γ ]⟩_{D_{φ0}} ⊢  m(s, 0)
Γ′ ⊢_{D_{φ_{0}}}  ⟨[Γ′]⟩_{D_{φ_{0}}} ⊢ m(s, 0)s′
⋮  ⋮  ⋮
U, Γ′′ ⊢_{D_{φ_{0}}}  μX.β(X), ⟨[Γ′′]⟩_{D_{φ_{0}}} ⊢
α(U), Γ′′ ⊢_{D_{φ_{0}}}  β(μX.β(X)), ⟨[Γ′′]⟩_{D_{φ_{0}}} ⊢  o

Suppose that v disappears in m(s, 0)s′. This means that in this node all the formulas are expanded using D_{φ_{0}}. Next when v reappears in o and has α(U) in the label we cannot use D′_{φ_{0}} for expanding α(U) and have a sound sequent assignment at the same time. This is because the rule

\frac{β(ff ), Σ ⊢}{μX.β(X), Σ⊢}

is not sound.

We know that v does not disappear on the path from m to n and that U appears in the node label of v in n. This means that a sequent assigned to n is of the form ff , Σ ⊢ for some Σ. As ff stands for p ∧ ¬p this sequent is easily provable. This shows how to use induction rule to assign an axiom to a final node of the first type.

Let n be a final node of the other type, i.e., the one with a back edge to some m(m ↓, 1). In this case n ↓ is a loop node, m ↓= n ↓ and for every prefix m′ of n longer than m, Ord(n↓) is a prefix of Ord(m′ ↓).

Let v be the green vertex of n ↓ and let us assume as before that the node label of v is {φ(U)} and ⟨[φ(U)]⟩_{D_{φ_{0}}} = φ′(μX.β(X)). Let Γ̃_{m} denote Γ_{m}\{φ(U)} and let P be the set off all the actions appearing in φ_{0}. To m(m ↓, 0) we have assigned one assumption of the rule (ind) to m(m↓, 1) we will assign the other one:

φ′(β(μX.Z ∧ β(X))), ⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} ⊢⟨P^{∗}⟩(φ′(μX.Z ∧ β(X)) ∧ ⋀⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} ) (15)

Let D_{φ_{0}}^{1} and D_{φ_{0}}^{2} be definition lists obtained from D_{φ_{0}} by replacing the definition of U by (U = α(μX.Z ∧ α(X))) and by (U = μX.Z ∧ α(X)) respectively. With this notation sequent (15) becomes

⟨[φ(U)]⟩_{D_{φ_{0}}^{1}} , ⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} ⊢⟨P^{∗}⟩(⟨[φ(U)]⟩_{D_{φ_{0}}^{2}} ∧ ⋀⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} )

Let o be a descendant of m and let Γ_{o}^{1}, Γ_{o}^{2} be respectively the label of v in o and the sum of the labels of the U-sons of v in o. We will assign to o the sequent:

⟨[Γ_{o}^{2}]⟩_{D_{φ_{0}}^{2}} , ⟨[Γ_{o}^{1}\Γ_{o}^{2}]⟩_{D_{φ_{0}}^{1}} , ⟨[(Γ_{o}\Γ_{o}^{1})\Γ_{o}^{2}]⟩_{D_{φ_{0}}} ⊢⟨P^{∗}⟩(⟨[φ(U)]⟩_{D_{φ_{0}}^{2}} ∧⋀⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} ) (16)

Compared to the previous case the new element this time is that we consider also sons of v. A son of v is created when definition constant U appears in the node label of v and rule (const) is applied. The previous case was simpler because we terminated a path as soon as U appeared in the node label of v. To see how sons of v come on the scene let us examine what happens when a new son of v is created.

Let o be a node in which (const) rule is applied to U, and an U-son of v is created in the result. Roughly speaking obtained state s is constructed from o↓ by adding a son of v with the node label {α(U)}. The only son of o is os. The sequent assigned to o is of the form (16). Because a new son of v is created we know that U ∈ Γ_{o}^{1} \ Γ_{o}^{2}. Hence the sequent assigned to os is exactly the same as the sequent assigned to o. In other words this application of (const) becomes an identity under our assignment but a “category” of one of the formulas was changed and this will allow us to prove a sequent assigned to n.

It is quite easy to check that such an assignment is sound for all the nodes o such that on the path from m to o, vertex v does not disappear. This condition on v is important for the same reasons as in the previous case.

We know that v does not disappear on the path from m to n and the last states of m and n are the same. Moreover v lights green in n ↓. By definition of A_{φ_{0}} this means that the label of v is equal to the sum of the labels of its U-sons hence to all formulas in the label of v we can use D_{φ_{0}}^{2}. Hence the sequent assigned to n is:

⟨[φ(U)]⟩_{D_{φ_{0}}^{2}} , ⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} ⊢⟨P^{∗}⟩(⟨[φ(U)]⟩_{D_{φ_{0}}^{2}} ∧ ⋀⟨[Γ̃_{m}]⟩_{D_{φ_{0}}} )

which is easily provable.

Important point is that while describing this sequent assignment, we have taken a leaf of T_{φ_{0}} first and only then constructed a part of a proof. This approach does not guarantee that if we transform every path of T_{φ_{0}} separately we will obtain a set of paths composing back to a tree. The simplest solution seems to be to apply (ind) rule in every node m of T_{φ_{0}} for which m ↓ is a loop node and consequently m has two sons m(m ↓, 0) and m(m ↓, 1). Such a strategy would be deterministic and this is what we will do but there is one subtle point here.

Schematically our procedure looks like this. Each application of (ind) rule allows us to remember one node ending in a loop node. Remembered information is represented by variables Z added to μ-formulas. When arriving at a final node we can use the information we remembered to obtain an axiom sequent.

[figure: m_{1}; n; m_{2}]

Figure 1: An example

Suppose we have a situation as pictured in Figure 1. Nodes m_{1} and m_{2} are places where we are to apply (ind) rule and there is a back edge from n to m_{2}. First we remember node m_{1} and, say, use Z_{1} for this. Next we remember m_{2} and use Z_{2}. This means that m_{2} has assigned a sequent of the form

φ_{2}(μX.β_{2}(X)), Γ⊢⟨P^{∗}⟩Δ

and we assign sequents

\begin{aligned}φ_{2}(ff ), Γ & ⊢ & ⟨P^{∗}⟩Δ \\ φ_{2}(β(μX.Z_{2} ∧ β_{2}(X))), Γ & ⊢ & ⟨P^{∗}⟩Δ, ⟨P^{∗}⟩(φ_{2}(μX.Z_{2} ∧ β(X)) ∧ ⋀ Γ) \end{aligned}

to m_{2}(m_{2} ↓, 0) and m_{2}(m_{2} ↓, 1) respectively. We have used here without mentioning an equivalence of ⟨P^{∗}⟩Δ with ⟨P^{∗}⟩⟨P^{∗}⟩Δ. Observe that Z_{1} may appear in Γ as well as in φ_{2}.

Arriving at n we hope to have something like

φ_{2}(μX.Z_{2} ∧ β_{2}(X)), Γ⊢⟨P^{∗}⟩(φ_{2}(μX.Z_{2} ∧ β(X)) ∧ ⋀ Γ), ⟨P^{∗}⟩Δ′  (17)

with Z_{1} occuring in Γ. But if the green vertex of m_{1} disappears on the way to n then instead of Γ on the left side we would obtain set Γ with Z_{1} erased. Such a sequent is not valid in general hence it is also not provable. In this situation we can save ourself by forgetting about Z_{1} before applying rule (ind) in m_{2}. This can be done using (cut) rule. But what if there is a leaf below m_{2} where we need Z_{1}?

This is the place where sets of active nodes come to rescue. The solution is to remember only active nodes. This means that we start our assignment from the root of T_{φ_{0}} and at a node m_{2} we first use weakening rule to remove all Z’s connected with nodes which are not in AN (m_{2}) and all ff connected with nodes not in AN_{0}(m_{2}). Only then we apply (ind) rule as described above.

In our example we either forget about Z_{1} before reaching m_{2} but then we know by definition of T_{φ_{0}} and AN that Z_{1} will not be needed below m_{2}, or we have Z_{1} around but then the green node of m_{1} will not disappear on the path to n. By definition we have that AN (m_{2}) = AN (n) ∪ {m_{2}} and AN_{0}(m_{2}) ⊆ AN_{0}(n). This means that all Z’s we had in m_{2} are present in n and at least the same occurrences of definition constants are replaced by ff . Hence in n we get a sequent like (17) but maybe with even stronger left hand side.

4.5 Construction of a proof

In this final subsection we will show that sequent φ_{0} ⊢ is provable thereby proving completeness of our axiomatisation. We will do it in two steps. First we will define a sequent S(n) for very node n of T_{φ_{0}}. Next we will show that such a sequent assignment is sound. That is we will show that sequents assigned to the leaves are provable and for any other node n, sequent S(n) is provable from the sequents assigned to the sons of n. As we will assign φ_{0} ⊢ to the root of T_{φ_{0}} this will show that φ_{0} ⊢ is provable.

Recall that D_{φ_{0}} denotes the definition list [⟩φ_{0}⟨]. In what follows we will use the convention that W_{i} stands for i-th definition constant in D_{φ_{0}} and γ_{i} for the formula it defines. Similarly we denote by U_{i} the i-th μ-constant in D_{φ_{0}} and let α_{i}(X) be such that (U_{i} = μX.α_{i}(X)) ∈ D_{φ_{0}}. Letters d and d_{μ} will stand for the number of definition constants in D_{φ_{0}} and the number of μ-constants in D_{φ_{0}} respectively. Let P be the set of all the actions appearing in φ_{0}. We will assume that we have a fresh variable Z_{m} for every node m of T_{φ_{0}} such that m↓ is a loop node. This variables do not appear in φ_{0}.

Definition of S(n) will be done in a several steps. With any node n of T_{φ_{0}} is associated a set of formulas Γ_{n} which is the set of all the formulas in the root of n↓ (n↓ being a state of A_{φ_{0}} is itself a tree). We start with determining a definition list for each vertex of n ↓, we call it signature of a vertex. Next we define definition list D(n, φ) for every formula φ ∈ Γ_{n}. For every φ ∈ Γ_{n} there is the lowest vertex in n ↓ containing φ. Let us call it the φ-vertex of s. We then define D(n, φ) from the signature of this vertex. The sequent S(n) assigned to a node n will have a form {⟨[φ]⟩_{D(n,φ)} : φ ∈ Γ_{n}} ⊢ ⟨P^{∗}⟩Δ, where Δ will be somehow defined from the structure of n↓ and AN (n).

Definition 4.15 Let n be a node of T_{φ_{0}}. For any vertex v of n ↓ we define its signature, ∥ v ∥_{n}, to be a sequence of formulas (δ_{1}, …, δ_{d^{μ}}) where for each i = 1, …, d^{μ} formula δ_{i} is defined as follows:

• First find the lowest ancestor u of v with el(u) = U_{i}.

• Let N be the set of nodes o ∈ AN (n) such that the green vertex of o is an ancestor of u and has U_{i} as an edge label. Let m be the closest to n, in T_{φ_{0}}, node from N.

• Finally let V = ⋀{Z_{o} : o ∈ N} and V′ = ⋀{Z_{o} : o ∈ N, o ≠ m}. We define δ_{i} by cases:

1. if u ∈ AV_{0}(n) then δ_{i} = ff

2. if u ∈ AV (n) then δ_{i} = V′ ∧ α_{i}(μX.V ∧ α_{i}(X))

3. otherwise δ_{i} = μX.V ∧ α_{i}(X)

For n ↓ being a loop node we define \overline{∥ v ∥}_{n} and ˆ∥ v ∥_{n} to be identical to ∥ v ∥_{n} if v is not the green vertex of n ↓. In case v is the green vertex of n ↓ then el(v) = U_{i} for some μ-constant U_{i} in D_{φ_{0}} and the difference between ∥ v ∥_{n} and \overline{∥ v ∥}_{n} or ˆ∥ v ∥_{n} is only at index i, we let \overline{δ}_{i} = μX.V ∧ α_{i}(X) and δ̂_{i} = μX.V ∧ Z_{n} ∧ α_{i}(X).

Definition 4.16 Let n be a node of T_{φ_{0}}, φ ∈ Γ_{n} and let v be the φ-vertex of m ↓. Let (δ_{1}, …, δ_{d^{μ}}) = ∥ v ∥_{n}. We define D(n, φ) to be a definition list obtained from D_{φ_{0}} by replacing for every i = 1, …, d^{μ} a definition of i-th μconstant U_{i} by (U_{i} = δ_{i}). Similarly we define \overline{D}(n, φ) and D̂(n, φ) but using \overline{∥ v ∥}_{n} and ˆ∥ v ∥_{n} respectively.

For any formula φ ∈ Γ_{n} we define ∥ φ ∥_{n}, \overline{∥ φ ∥}_{n} and ˆ∥ φ ∥_{n} to be ⟨[φ]⟩_{D(n,φ)}, ⟨[φ]⟩_{\overline{D}(n,φ)} and ⟨[φ]⟩_{_{D}(n,φ)} respectively. For a node n we define three formulas

\begin{matrix}F (n) = ⋀\{∥ φ ∥_{n} : φ ∈ Γ_{n}\}, & \overline{F} (n) = ⋀\{\overline{∥ φ ∥}_{n} : φ ∈ Γ_{n}\} \\ F̂(n) = ⋀\{ ˆ∥ φ ∥_{n} : φ ∈ Γ_{n}\} \end{matrix}

Finally we associate a sequent with every node n of T_{φ_{0}}. If n ↓ is not a loop node then S(n) is

F (n)⊢{⟨P^{∗}⟩F̂(m) : m ∈ AN (n)}

and if n↓ is a loop node we let S(n) to be

\overline{F} (n)⊢\{⟨P^{∗}⟩F̂(m) : m ∈ AN (n)\}

Probably a few more words is needed to justify this definition of the sequent assignment. The right hand side of the sequent is used to keep the labels of the nodes to which we may return. The real work is done on the left hand side using formulas F (n). These are expansions of Γ_{n} with Z-variables in places designated by n and AN(n). Formula \overline{F} (n) is different from F (n) only when n ↓ is a loop node and the green vertex v of n ↓ belongs to AV (n). In this situation \overline{F} (n) is a stronger version of F (n). It is possible to have this stronger formula because we know that v lights green in n↓ hence its label was equal to the sum of the labels of its el(v)-sons. Formula F̂(p) is what we would obtain on the right hand side of the longer assumption if we applied (ind) rule to \overline{F} (m). The left hand side of the assumption will be just F (m(m↓, 1)) hence we don’t need special symbol for this one.

Having defined sequent assignment for T_{φ_{0}} we are ready to prove its properties. In a sequence of lemmas we will prove that if m is a leaf then S(m) is provable and if m has sons m_{1}, …, m_{k} then S(m) is provable form S(m_{1}), …, S(m_{k}). Let us first show why all the leaves of T_{φ_{0}} are easily provable.

Lemma 4.17 Every leaf of T_{φ_{0}} has assigned a provable sequent.

Proof There are three kinds of leaves in T_{φ_{0}}. First there are nodes n such that n↓ has no son in G_{φ_{0}}. In this case we know that some propositional constant p and its negation occur in Γ_{n}. By definition of F (n), we have p, ¬p ∈ F (n).

Next case is when n is a final node from which there is no back edge. This means that there is a prefix m(m ↓, 0) of n and the green vertex v of m ↓ such that: (i) definition constant el(v) appears in the node label of v in n ↓, and (ii) for any prefix m′ of n longer than m, v appears in Ord(m′ ↓). Hence v ∈ AV_{0}(n).

Now el(v) = U_{i} is some, say i-th, μ-definition constant form D_{φ_{0}} and by definition i-th component of ∥ v ∥_{n} is ff . It is easy to see that v cannot have any U_{i}-sons so v is the U_{i}-vertex of n ↓. Hence we have that ∥ U_{i} ∥_{n} = ff and ff ∈ F (n).

The last case is when n is a final node from which there is a back edge to some node m. Because n↓ is a loop node, S(n) is of the form:

\overline{F} (n)⊢\{⟨P^{∗}⟩F̂(m) : m ∈ AN (n)\}

We know that m ↓= n ↓ and for any prefix m′ of n longer than m, Ord(n ↓) is a prefix of Ord(m′ ↓). From definition it follows that AN (n) = AN (m) ∪ {m} and AN_{0}(m) ⊆ AN_{0}(n). It is easy to check that for every vertex v of n↓, every j ∈ \{1, …, d^{μ}\} and δ_{j}^{m}, δ_{j}^{n} j-th components of ˆ∥ v ∥_{m} and \overline{∥ v ∥}_{n} respectively the sequent δ_{j}^{n} ⊢δ_{j}^{m} is provable. Because all occurrences of definition constants are positive we have by Lemma 3.4 that \overline{F} (n) ⊢ F̂(m) is provable. Hence \overline{F} (n)⊢⟨P^{∗}⟩F̂(m) is provable.

Next our goal is to prove that the sequent associated with a father is provable from the sequents associated with its sons. Let us start by showing a few technical lemmas.

Lemma 4.18 Let n be a node of T_{φ_{0}} and let v, w be two vertices of n↓, such that v is an ancestor of w. Suppose δ_{i}, δ′_{i} are i-th components of ∥ v ∥_{s} and ∥ w ∥_{s} respectively for some i = 1, …, d^{μ}, then the sequent δ′_{i} ⊢δ_{i} is provable.

Proof Let us choose any i ∈ {1, …, d^{μ}}. If w_{i}, the lowest ancestor of w s.t. el(w_{i}) = U_{i}, is also an ancestor of v then δ_{i} = δ′_{i} and we are done. Otherwise let v_{i} be either the lowest ancestor of v s.t. el(v_{i}) = U_{i} or the root if there is no such ancestor.

• if w_{i} ∈ AN_{0}(n) then δ′_{i} = ff and of course δ′_{i} ⊢δ_{i} is provable.

• if w_{i} ∈ AN (n) then

\begin{matrix}δ′_{i} = V′ ∧ α(μX.V ∧ α(X)) \\ V = ⋀\{Z_{o} : o ∈ N\} & V′ = ⋀\{Z_{o} : o ∈ N, o ≠ m\} \end{matrix}

where N is the set of nodes o ∈ AN (n) such that some ancestor u′ of w_{i} with el(u′) = U_{i} is the green vertex in o↓, and m is the closest to n node form N.

There are two possibilities for δ_{i}

δ_{i} = V′_{1} ∧ α(μX.V_{1} ∧ α(X)) or δ_{i} = μX.V_{1} ∧ α(X)

where

V_{1} = ⋀{Z_{o} : o ∈ N_{1}} V′_{1} = ⋀{Z_{o} : o ∈ N_{1}, o ≠ m_{1}}

and N_{1}, m_{1} are defined as above but with respect to v_{i}. Because w_{i} is a proper descendant of v_{i} and w_{i} ∈ AN (n), we have N_{1} ⊆ N \ {m}. Hence V′ ⊢V_{1} is provable. Because all occurrences of V, V′, V_{1}, V′_{1} are positive we have the proof of δ′_{i} ⊢δ_{i} by Lemma 3.4.

• In case w_{i} ∉ AN (n) the argument is very similar.

Lemma 4.19 The notion of a signature of a vertex v from a state n↓ depends on the sets AN (n) and AN_{0}(n). It is easy to generalise the notion to arbitrary sets of nodes R, R_{0} such that R ∩ R_{0} = ∅. So we can have something like ∥ v ∥_{n}^{R,R_{0}}. This way we can also define F_{R_{0}}^{R}(n). If we do so then F_{R_{0}}^{R}(n)⊢F (n) will be provable for any R ⊇ AN (n), R_{0} ⊇ AN_{0}(n).

Proof Let v be a vertex of m↓ and R ⊇ AN (n), R_{0} ⊇ AN_{0}(n). It is enough to show that for any i and δ_{r}, δ being i-th elements of ∥ v ∥_{n}^{R,R_{0}} and ∥ v ∥_{n} respectively, the sequent δ_{r} ⊢δ is provable.

If δ_{r} = ff then it is obvious. Suppose δ_{r} = V′_{r} ∧ α_{i}(μX.V_{r} ∧ α_{i}(X)) where V_{r} = ⋀{Z_{o} : o ∈ N}, V′_{r} = ⋀{Z_{o} : o ∈ N, o ≠ m} and N is the set of nodes o ∈ R such that the green vertex of o is an ancestor of v and has U_{i} as an edge label; m is the closest to n node from N. According to Definition 4.15

δ = V′ ∧ α_{i}(μX.V ∧ α_{i}(X)) or δ = μX.V ∧ α_{i}(X)

where V and V′ are defined similarly but with respect to AN (n). Because R ⊇ AN (n) it should be clear that V′_{r} ⊢ V is provable hence also δ_{r} ⊢ δ is provable. The remaining case is similar.

Lemma 4.20 Let n be a node of T_{φ_{0}}. Suppose a state r is obtained from n ↓ by applying all but the fifth step of the transition function and t is the state resulting after the application of this last step, i.e., some of the vertices of r might light green in t and have all its sons deleted. For sequence nr we can define F (nr) in a similar way we defined F (nt). The sequent F (nr) ⊢ F (nt) is provable and moreover if t is a loop node then F (nr)⊢\overline{F} (nt) is provable.

Proof Let Γ be the label of the root of r which is the same as the label of the root of t. By the construction of the states, Γ is also the set of all the formulas occurring in r as well as in t. For any formula ψ ∈ Γ, the ψ-vertex in t, call it v_{t}, is either an ancestor of the ψ-vertex in r, denoted v_{r}, or vertices v_{t} and v_{r} are the same. If they are the same then ∥ ψ ∥_{nr} = ∥ ψ ∥_{nt}. Otherwise let (δ_{1}, …, δ_{d^{μ}}) = ∥ v_{t} ∥_{nr} = ∥ v_{t} ∥_{nt} and (δ′_{1}, …, δ′_{d^{μ}}) = ∥ v_{r} ∥_{nr}. Because v_{r} is a descendant of v_{t} in r then from Lemma 4.18 it follows that δ′_{i} ⊢ δ_{i} is provable for i = 1, …, d^{μ}. Hence the sequent ∥ ψ ∥_{nr} ⊢∥ ψ ∥_{nt} is provable by Lemma 3.4 because all occurrences of definition constants are positive. This shows that F (nr)⊢F (nt) is provable.

To see why F (nr) ⊢ \overline{F} (nt) is provable when t is a loop node, first observe that ∥ ψ ∥_{nt} = \overline{∥ ψ ∥}_{nt} if the ψ-vertex of t is not the green vertex of t.

Let u be the green vertex of t, ψ ∈ nl(u) and let el(u) = U_{i} be i-th μdefinition constant in D_{φ_{0}}. Because u lights green in t there must be a descendant u′ of u, in r s.t. ψ ∈ nl(u′) and el(u′) = el(u). The only difference between \overline{∥ u ∥}_{nt} = (δ_{1}, …, δ_{d^{μ}}) and ∥ u′ ∥_{nr} = (δ′_{1}, …, δ′_{d^{μ}}) may be at position i. But from the definition of signatures it follows that δ′_{i} ⊢δ_{i} is provable. Then using once again Lemma 3.4 we have that ∥ ψ ∥_{nr} ⊢\overline{∥ ψ ∥}_{nt} is provable.

We are now ready to prove that the sequent associated with a father node is provable from the sequents associated with its sons. We do it by cases depending on the rule which was used in the node.

Lemma 4.21 Suppose that the only son m′ of m was obtained from m by application of (∧_{t}) rule:

\frac{α, β, Γ ⊢_{D_{φ_{0}}}}{α ∧ β, Γ ⊢_{D_{φ_{0}}}}

that is Γ_{m} = {α∧β}∪Γ and automaton A_{φ_{0}} goes from m↓ to m′ ↓ after reading α, β, Γ ⊢_{D_{φ_{0}}} . In this case sequent S(m) is provable from S(m′).

Proof Let r be a state obtained from m↓ by applying all but the last fifth step of the transition function on the input α, β, Γ ⊢_{D_{φ_{0}}} . This means that r was obtained from m ↓ by first setting the color of all the vertices in m ↓ to white. Then formula α ∧ β was replaced by two formulas, α and β. Next, if a formula α or β occured in a vertex v and in a vertex to the left of it then the formula was deleted from the label of v. Finally the vertices with empty labels were removed. Observe that in r there may still occur vertices which would light green and have all its sons removed if the last step of transition function were applied. We will show that

F (m)⊢F (mr)

is provable.

For any formula φ ∈ Γ, φ ≠ α, φ ≠ β we have ∥ φ ∥_{m} = ∥ φ ∥_{mr} because φ-vertices in m↓ and r are the same.

If also α∧β-vertex in m↓ is the same as α-vertex in r then clearly ∥ α ∧ β ∥_{m} ⊢ ∥ α ∥_{mr}. If it is not the case then it must be because α ∈ Γ and α occurs to the left of α ∧ β in m ↓. But then α-vertices in m ↓ and r are the same and ∥ α ∥_{m} = ∥ α ∥_{mr}. We can use similar argument for formula β.

This shows that the sequent F (m) ⊢ F_{AN_{0}(m)}^{AN (m)}(mr) is provable. We know from Lemma 4.14 that AN (mr) ⊆ AN (m) and AN_{0}(mr) ⊆ AN_{0}(m) hence by Lemma 4.19 the sequent F (m) ⊢ F (mr) is provable. From Lemma 4.20 we obtain that either F (m) ⊢ F (mt) or F (m) ⊢ \overline{F} (mt) is provable depending on whether t is a loop node or not. This shows that we can prove S(m) from S(mt).

Similar arguments also work in case of the other tableau rules. This is summarised in the following lemma.

Lemma 4.22 If m_{1}, …, m_{k} are the sons of m and one of the rules: (∨_{t}), (μ), (ν), (const) or (⟨⟩_{t}) was applied in m then the sequent S(m) is provable from S(m_{1}), …, S(m_{k}). (Actually k = 1 or k = 2.)

Proof Let us just show one case. This is the case where Lemma 4.4 is needed. Assume that the rule applied was:

\frac{U_{i}, Γ ⊢_{D_{φ_{0}}}}{μX.α_{i}(X), Γ ⊢_{D_{φ_{0}}}}

then, as before, let r be a state obtained form m↓ by applying all but the last fifth step of the transition function on the input U_{i}, Γ ⊢_{D_{φ_{0}}} . We will show that the sequent

F (m)⊢F (mr)

is provable.

For any φ ∈ Γ, φ ≠ U_{i}, φ-vertices in m↓ and r are the same hence ∥ φ ∥_{m} = ∥ φ ∥_{mr}. For formula U_{i} we have two possibilities. The first possibility is that U_{i}-vertices in m↓ and r are the same. In this case also ∥ U_{i} ∥_{m} = ∥ U_{i} ∥_{mr}.

Otherwise the U_{i}-vertex in r is a μX.α(X)-vertex in m ↓, call it v. By Definition 4.16, ∥ μX.α_{i}(X) ∥_{m} = μX.α_{i}(X)[γ′_{d}/W_{d}] … [γ′_{1}/W_{1}] where each γ′_{i} is determined using the signature ∥ v ∥_{m}. Now ∥ U_{i} ∥_{mr} = U_{i}[γ′_{d}/W_{d}] … [γ′_{1}/W_{1}] for the same formulas γ′_{j}, j = 1, …, d, because v is the U_{i}-vertex in r.

By construction of the definition list, only constants older then U_{i} can appear in μX.α_{i}(X). From Lemma 4.4 it follows that neither v nor any of its ancestors have U_{i} as its edge label. This means that in the signature ∥ v ∥_{m} = (δ_{1}, …, δ_{d^{μ}}), its i-th coordinate δ_{i} is μX.α_{i}(X). Hence

∥ μX.α_{i}(X) ∥_{m} = μX.α_{i}(X)[γ_{j}/W_{j}] … [γ_{1}/W_{1}]
∥ U_{i} ∥_{mr} = U_{i}[μX.α_{i}(X)/U_{i}][γ_{j}/W_{j}] … [γ_{1}/W_{1}]

where W_{j} is the youngest definition constant older than U_{i}.

Having shown that F (m)⊢F (mr) is provable it is enough to use Lemma 4.20 to complete this case.

Finally we have to take care of the situation when m ↓ is a loop node and m has two sons m(m ↓, 0) and m(m ↓, 1). This is the only situation when the set of active nodes can increase and we get new nodes to “remember”.

Lemma 4.23 Suppose m ends in a loop node and has two sons m(m↓, 0) and m(m↓, 1) then we can prove S(m) from S(m(m↓, 0)) and S(m(m↓, 1)).

Proof Suppose v is the green node of m↓ and i, l are such that U_{i} = W_{l} = el(v). Let μX.β(X) be i-th element of \overline{∥ v ∥}_{m} and let \{ψ_{1}, …, ψ_{k}\} be the node label of v in m↓. We take definition list \overline{D}(m, ψ_{1}) = (W_{1} = γ′_{1}) … (W_{d} = γ′_{d}) as described in Definition 4.16 and set

ψ′_{j} = ψ_{j}[γ′_{n}/W_{n}] … [γ′_{l+1}/W_{l+1}][γ′_{l−1}/W_{l−1}] … [γ′_{1}/W_{1}]; j = 1, …, k
ψ = ⋀{ψ′_{j} : j = 1, …, k}
δ(X) = β(X)[γ′_{l−1}/W_{l−1}] … [γ′_{1}/W_{1}]
γ = ⋀\{\overline{∥ ϕ ∥}_{n} : ϕ ∈ Γ_{m} \ \{ψ_{1}, …, ψ_{k}\}\}

Sequent S(m) is by definition \overline{F} (m) ⊢ \{⟨P^{∗}⟩F̂(n) : n ∈ AN (m)\} and with the notation introduced above \overline{F} (m) can be presented as ψ[μX.δ(X)/U_{i}] ∧ γ. Hence S(m) is of the form of the conclusion of (ind) rule with the assumptions:

ψ[ff /U_{i}] ∧ γ ⊢ {⟨P^{∗}⟩F̂(n) : n ∈ AN (m)}
ψ[δ(μX.Z_{m} ∧ δ(X))/U_{i}] ∧ γ ⊢ {⟨P^{∗}⟩F̂(n) : n ∈ AN (m)},
⟨P^{∗}⟩(ψ[μX.Z_{m} ∧ δ(X)/U_{i}] ∧ γ)

Because v is the U_{i}-vertex on m↓, the first sequent is just

F_{AN_{0}(m)∪{m}}^{AN (m)}(m(m↓, 0))⊢{⟨P^{∗}⟩F̂(n) : n ∈ AN (m)}

and we can prove it from S(m(m↓, 0)) using Lemma 4.19 because by Lemma 4.14 AN (m(m↓, 1)) ⊆ AN (m) and AN_{0}(m(m↓, 1)) = AN_{0}(m) ∪ {m}. Similarly the second sequent is

F_{AN_{0}(m)}^{AN (m)∪{m}}(m(m↓, 1))⊢{⟨P^{∗}⟩F̂(n) : n ∈ AN (m)} ∪ {⟨P^{∗}⟩F̂(m)}

and by Lemmas 4.14 and 4.19 we can prove it from S(m(m↓, 1)).

Let us summarise the development of this section in the completeness theorem.

Theorem 4.24 (Completeness) For any unsatisfiable formula φ_{0}, the sequent φ_{0} ⊢ is provable.

Proof By Proposition 3.6 we can assume that φ_{0} is positive and guarded. For this formula we construct an automaton A_{φ_{0}} as described in Section 4.2. From it we obtain a tree T_{φ_{0}} defined in Section 4.3. Then we associate a sequent S(n) with every node n of T_{φ_{0}} in a way described in Definition 4.16. By Lemma 4.17 we know that all the leaves of T_{φ_{0}} have associated provable sequents. Using induction on the height of a node and Lemmas 4.21, 4.22 and 4.23 we show that the sequent associated with the root of T_{φ_{0}} is provable. But it is just φ_{0} ⊢.

5 Conclusions

We have presented a finitary proof system for the propositional μ-calculus and proved its completeness. The system is stronger than original Kozen’s system. We think that this is an advantage of this system as it is easier to prove facts in it. Of course original system is so natural that its completenes is still a very interesting question.

The presented system has also this advantage that it is closely connected with a decision procedure for the logic. This shows a possibility of integrating the two in the way we now describe.

Essentially the only know method for checking satisfiability of the μ-calculus formulas comes from the tableau method and the use of automata theory [23]. For a given formula the algorithm constructs an automaton over infinite trees which accepts models of the formula. Then, if formula is satisfiable, a model is constructed from an accepting run of the automaton. In [17] it was shown that the process of checking satisfiability can be viewed as a game between two players. The strategy for one player gives a model for a formula. The strategy for the second gives a refutation. Moreover it was show that for a given formula there is an algorithm which in exponential time constructs a model or a refutation. This gives a complete setting for analysing μ-calculus formulas: given a formula the algorithm either gives an example of a model in which the formula holds or gives “proof” that this formula is unsatisfiable. Our completeness proof gives an algorithm of converting a refutation of a formula into a proof of the negation of the formula. Moreover the rules of the system are closely connected with construction of refutations. This means that it may be possible to interfere with the algorithm to help it in what is essentially task of exponential complexity.

As we have shown our completeness proof is an extension of some completeness proof method for modal system K. This method is really two methods put together as it can be also used for model construction. Conversions to ω-automata are general method of model construction for propositional logics of programs. Such conversions can be seen as an extensions of the model construction technique for system K. Our proof technique seams to be “the other side of the coin” for this conversions. One can expect that it should also work for other logics. It would be particularly interesting to apply the method to the temporal μ-calculus.

References

[1] J.R. Brunch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 10^{20} states and beyond. Information & Computation, 98(2):142–170, 1992.

[2] E. Allen Emerson. Automata, tableaux and temporal logic. In Colledge Conference on Logic of Programs, volume 193 of LNCS. Springer-Verlag, 1985.

[3] E. Allen Emerson and C.L.Lei. Efficient model checking in fragments of propositional mu-calculus. In First IEEE Symp. on Logic in Computer Science, pages 267–278, 1986.

[4] E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. In 29th IEEE Symp. on Foundations of Computer Science, 1988.

[5] E.Allen Emerson and J.Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1–24, 1985.

[6] E.Allen Emerson and C.S. Jutla. Tree automata, mu calculus and determinacy. In Proc. FOCS 91, 1991.

[7] M.J. Fisher and R.E. Ladner. Propositional modal logic of programs. In 9th ACM Ann. Aymp. on Theory of Computing, pages 286–294, 1977.

[8] D. Gabbay. Axiomatizations of logics of programs. Unpublished manuscript, Bar-Ilan Univ., 1977.

[9] D. Harel, D Kozen, and R. Parikh. Process logic: Expressiveness, decidability and completeness. Journal of Computer and System Sciences, 25:144–201, 1982.

[10] David Harel. Dynamic logic. In Handbook of Philosophical Logic Vol II, pages 497–604. D.Reidel Publishing Company, 1984.

[11] P.M.W. Knijnenburg and J. van Leeuwen. On models for propositional dynamic logic. Theoretical Computer Science, 91:181–203, 1991.

[12] Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.

[13] Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studa Logica, 47(3):234–241, 1988.

[14] Dexter Kozen and R. Parikh. An elementary proof of the completeness of the PDL. Theoretical Computer Science, 14:113–118, 1981.

[15] Dexter Kozen and R.J.Parikh. A decision procedure for the propositional mu-calculus. In Second Workshop on Logics of Programs, 1983.

[16] Dexter Kozen and Jerzy Tiuryn. Logics of programs. In J.van Leeuven, editor, Handbook of Theoretical Computer Science Vol.B, pages 789–840. Elsvier, 1990.

[17] D. Niwiński and I. Walukiewicz. Games for μ-calculus. Technical Report TR 94-03(192), Institute of Informatics, Warsaw Univeristy, February 1994.

[18] Damian Niwiński. Fixed points vs. infinite generation. In Proc. 3rd. IEEE LICS, pages 402–409, 1988.

[19] R. Parikh. The completeness of propositional dynamic logic. In Proc 7th Symp on Mathematical Foundations of Computer Science, volume 64 of LNCS, pages 403–415, 1978.

[20] Shmuel Safra. On the complexity of ω-automata. In 29th IEEE Symp. on Foundations of Computer Science, 1988.

[21] Colin P. Stirling and David J. Walker. Local model checking in the modal mu-calculus. In International Joint Conference in Theory and Practice of Software Development, volume 351 of LNCS, pages 369–382. Springer-Verlag, 1989.

[22] C.S. Stirling. Modal and temporal logics. In S.Abramsky, D.Gabbay, and T.Maibaum, editors, Handbook of Logic in Comuter Science, pages 477– 563. Oxford University Press, 1991.

[23] Robert S. Street and E. Allan Emerson. An automata theoretic procedure for the propositional mu-calculus. Information & Computation, 81:249– 264, 1989.

Recent Publications in the BRICS Report Series

RS-95-6 Igor Walukiewicz. A Complete Deductive System for the μ-Calculus. January 1995. 39 pp.

RS-95-5 Luca Aceto and Anna Ing� olfsd� ottir. A Complete Equational Axiomatization for Pre�x Iteration with Silent Steps. January 1995. 27 pp.

RS-95-4 Mogens Nielsen and Glynn Winskel. Petri Nets and Bisimulations. January 1995. 36 pp. To appear in TCS.

RS-95-3 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part I: A Denotational Model and Its Complete Axiomatization. January 1995. 37 pp.

RS-95-2 Franc�ois Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. January 1995. 21 pp.

RS-95-1 Gudmund Skovbjerg Frandsen, Thore Husfeldt, Peter Bro Miltersen, Theis Rauhe, and S�ren Skyum. Dynamic Algorithms for the Dyck Languages. January 1995. 21 pp.

RS-94-48 Jens Chr. Godskesen and Kim G. Larsen. Synthesizing Distinguishing Formulae for Real Time Systems. December 1994. 21 pp.

RS-94-47 Kim G. Larsen, Bernhard Steffen, and Carsten Weise. A Constraint Oriented Proof Methodology based on Modal Transition Systems. December 1994. 13 pp.

RS-94-46 Amos Beimel, Anna G� al, and Mike Paterson. Lower Bounds for Monotone Span Programs. December 1994. 14 pp.

RS-94-45 J�rgen H. Andersen, K� are J. Kristoffersen, Kim G. Larsen, and Jesper Niedermann. Automatic Synthesis of Real Time Systems. December 1994. 17 pp.

RS-94-44 Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. December 1994. PhD thesis. viii+224 pp.