⋆ Luca

Alberucci 1⋆⋆

Alessandro Facchini
email: alessandro.facchini@unil.ch

On Modal µ-Calculus and Gödel-Löb Logic

Keywords: Fixpoint, Modal µ-Calculus, Gödel-Löb Logic. ⋆

We show that the modal µ-calculus over GL collapses to the modal fragment by showing that the fixpoint formula is reached after two iterations and answer to a question posed by van Benthem in [vBe06]. Further, we introduce the modal µ ∼ -calculus by allowing fixpoint constructors for any formula where the fixpoint variable appears guarded but not necessarily positive and show that this calculus over GL collapses to the modal fragment, too. The latter result allows us a new proof of the de Jongh, Sambin Theorem and provides a simple algorithm to construct the fixpoint formula.

Introduction

The modal µ-calculus is an extension of propositional modal logic, with least and greatest fixpoint operators. The term "µ-calculus" and the idea of extending modal logic with fixpoints appeared for the first time in the paper of Scott and De Bakker [START_REF] Scott | A Theory of Programs[END_REF] and was further developed by others. Nowadays, the term "modal µ-calculus" stands for the formal system introduced by Kozen [START_REF] Kozen | Results on the Propositional Mu-Calculus[END_REF]. The standard semantics of the modal µ-calculus is given by transition systems. As usual, formulae are interpreted as subsets of a system, the set of states where the property expressed by the formula holds. Many natural properties such as "there is an infinite path" can be expressed by a modal µ-formula. Indeed, it is a powerful logic of programs subsuming dynamic and temporal logics like PDL, PLTL, CTL and CTL * . We refer to Bradfield and Stirling's tutorial article [START_REF] Bradfield | Modal Logic and Mu-Calculi[END_REF] or Stirling's book [START_REF] Stirling | Modal and Temporal Properties of Processes[END_REF] for a thorough introduction to this system.

Gödel-Löb logic, GL, is used to investigate what arithmetical theories can express in a restricted language about their provability predicates. As a modal logic, provability logic has been studied since the early seventies, and has had important applications in the foundations of mathematics. Beside the arithmetical interpretation there is also a semantics given, as for almost all modal logics, by transition systems. The class of all transitive and upward well-founded systems forms a complete semantics for GL.

Fixpoints and fixpoint theorems play an important role in GL. The most famous one, the existence of a fixpoint for guarded formulae was proved by de Jongh and Sambin independently (c.f., [START_REF] Smorynski | Self-Reference and Modal Logic[END_REF]). Even though it is formulated and proved by strictly modal methods, the fixpoint theorem still has great arithmetical significance. The uniqueness of the fixpoint was proved later by Bernardi, de Jongh and Sambin independently (c.f., [START_REF] Smorynski | Self-Reference and Modal Logic[END_REF]).

Since the modal µ-calculus is a general framework to study fixpoints in modal logic, studying the modal µ-calculus over GL is a promising work. This has been done by van Benthem in [START_REF] Van Benthem | Modal Frame Correspondences and Fixed-Points[END_REF] and Visser in [START_REF] Visser | Löb's Logic Meets the µ-Calculus[END_REF]. Both authors establish, by using the de Jongh, Sambin fixpoint theorem, that the modal µ-calculus over GL collapses to its modal fragment. But since they use the already known fixpoint theorem in order to establish this collapse in [START_REF] Van Benthem | Modal Frame Correspondences and Fixed-Points[END_REF] van Benthem writes: "Our . . . analysis does not explain why provability fixed-points are explicitly definable in the modal base language. Indeed, the general reason seems unknown."

In this paper we answer this question. More precisely, we prove the collapse of the modal µ-calculus over GL without using the de Jongh, Sambin Theorem by showing that fixpoints are reached after two iterations of well-named fixpoint formulae.

Fixpoint theorems in GL hold also for modal formulae where the variable appears guarded but not necessarily positively and, from this point of view, this first result is not completely satisfactory since modal µ-calculus allows fixpoint constructors only for syntactically positive formulae. Therefore, we also introduce the modal µ ∼ -calculus which allows fixpoint constructors for formulae where the fixpoint variable appears guarded. As can be done also for the standard µ-calculus we define the semantics by way of games, in this case only over transitive and upward well-founded transition systems and, by using gametheoretical, we show that the modal µ ∼ -calculus collapses to the modal fragment by providing an explicit syntactical translation of the modal µ ∼ -calculus into GL which preserves logical equivalence. As a corollary of the collapse, we obtain a new version of the de Jongh, Sambin Fixpoint Theorem with a simple algorithm which shows how the fixpoint can be computed. In this sense we give an answer to a generalisation of van Benthem's question. Summing up, the modal µ ∼calculus allows us to apply techniques similar as those known from the standard µ-calculus to GL and could be regarded as a starting point for further studies in this direction.

Both the collapse of the modal µ-calculus over GL and the one of the µ ∼calculus over the same class of models are proved by using techniques and results from [AF∞].

In the next section we repeat the preliminaries and some results which are already known. In Section 3 we analyse the modal µ-calculus over GL and show that it collapses to the modal fragment. In the last section we introduce the modal µ ∼ -calculus and show a collapse to the modal fragment. The result is then used to provide a new proof of the uniqueness theorem of Bernardi, de Jongh and Sambin and of the existence theorem of de Jongh, Sambin. For the last one we also give a simple algorithm which shows how the fixpoint can be computed.

Preliminaries

Gödel-Löb Logic GL

We start from an infinite countable set Prop of propositional variables. Then the collection L GL of GL-formulae is given by:

ϕ ::= p | ∼p | ⊤ | ⊥ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | ♦ϕ | ϕ
where p ∈ Prop. If all propositional variables occurring in ϕ are in P ⊆ Prop, we write ϕ ∈ L GL (P). If ψ is a subformula of ϕ, we write ψ ≤ ϕ. We write ψ < ϕ when ψ is a proper subformula. sub(ϕ) is the set of all subformulae of ϕ. The formula ¬ϕ is defined by using de Morgan dualities for boolean connectives and the modal dualities for ♦ and and the law of double negation. As usual, we introduce implication ϕ → ψ as ¬ϕ ∨ ψ and equivalence ϕ ↔ ψ as (ϕ → ψ) ∧ (ϕ → ψ). We say that p ∈ Prop is guarded in ϕ if p ≤ ϕ and all occurrences of p are in the scope of a modal operator.

The axioms and inference rules below give a deduction system for GL. As usual we write GL ⊢ ϕ if there is a derivation of ϕ in the system presented below.

Axioms As for all modal logics the semantics of GL is given by transition systems. A transition system T is of the form (S, → T , λ T ) where S is a set of states, → T is a binary relation on S called the accessibility relation and λ : Prop → ℘(S) is a valuation for all propositional variables. A transition system T with a distinguished state s is called a pointed transition system and denoted by (T , s). T denotes the class of all pointed transition systems. The accessibility relation is called upward well-founded if there is no infinite chain of the form

s 0 → T s 1 → T s 2 → . . . .
By T wft we denote the subclass of pointed transition systems such that the accessibility relation is transitive and upward well-founded. Given a transition system T , the denotation of ϕ in T , ϕ T , that is, the set of states satisfying a formula ϕ is defined inductively on the structure of ϕ. For all transition systems we set

-p T = λ(p) and ∼p T = S \ λ(p) for all p ∈ Prop, -α ∧ β T = α T ∩ β T , -α ∨ β T = α T ∪ β T , - α T = {s ∈ S | ∀t((s → T t) ⇒ t ∈ α T )}, and -♦α T = {s ∈ S | ∃t((s → T t) ∧ t ∈ α T )}.
We say that a pointed transition system (T , s) is a model of a GL-formula if and only if s ∈ ϕ T . If all pointed transition systems (T , s) ∈ T wft are a model of ϕ then we write GL |= ϕ. A proof of the next theorem can be found in [START_REF] Boolos | The Logic of Provability[END_REF].

Theorem 1. For all GL-formulae ϕ we have that GL ⊢ ϕ if and only if GL |= ϕ.

The modal µ-calculus

The language of the modal µ-calculus results by adding greatest and least fixpoint operators to propositional modal logic. More precisely, given an infinite countable set Prop of propositional variables, the collection L µ of modal µ-formulae (or simply µ-formulae) is defined as follows:

ϕ ::= p | ∼p | ⊤ | ⊥ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | ♦ϕ | ϕ | µx.ϕ | νx.ϕ
where p, x ∈ Prop and x occurs only positively in ηx.ϕ (η ∈ {ν, µ}), that is, ∼x is not a subformula of ϕ.

The fixpoint operators µ and ν can syntactically be viewed as quantifiers. Therefore we use the standard terminology and notations as for quantifiers and, for instance, free(ϕ) denotes the set of all propositional variables occurring free in ϕ and bound(ϕ) those occurring bound. Further, we define var(ϕ) = free(ϕ) ∪ bound(ϕ). If ψ is a subformula of ϕ, we write ψ ≤ ϕ. We write ψ < ϕ when ψ is a proper subformula. sub(ϕ) is the set of all subformulae of ϕ. We write ϕ ∈ L µ (P) if it holds that free(ϕ) ⊆ P, with P ⊆ Prop.

The negation ¬ϕ of a µ-formula ϕ is defined inductively as for GL-formulae and, further, for µ and ν we use ¬µx.ϕ(x) ≡ νx.¬ϕ(x)[x/¬x] and ¬νx.ϕ(x) ≡ µx.¬ϕ(x)[x/¬x].

Given a µ-formula ϕ, for all sets of bound variables X ⊆ bound(ϕ), the formula ϕ free(X) is obtained from ϕ by eliminating all fixpoint operators binding a variable x ∈ X but leaving the previously bound variables x as a free occurrences. When X = bound(ϕ), sometimes we simply write ϕ free .

Let ϕ ∈ L µ (P). An alternating µ-chain in ϕ of length k is a sequence

ϕ ≥ µx 0 .ψ 0 > νx 1 .ψ 1 > • • • > µ/ν k-1 .ψ k-1
where for every i < k -1 the variable x i is free in every ψ such that ψ i ≥ ψ ≥ ψ i+1 . The maximum length of an alternating µ-chain in ϕ is denoted by max µ (ϕ). ν-chains and max ν (ϕ) are defined analogously. The alternation depth of a µ-formula ϕ, denoted by ad(ϕ), is the maximum of max µ (ϕ) and max ν (ϕ).

If ϕ is a purely modal formula, we set ad(ϕ) = 0. The axioms and inference rules below define the deduction system Koz. As usual we write Koz ⊢ ϕ if there is a derivation of ϕ in the system presented below.

Axioms: All classical propositional tautologies and the Distribution Axiom from modal logic and the fixpoint axioms ηx.ϕ(x) ↔ ϕ(ηx.ϕ(x)), η ∈ {µ, ν}.

Inference Rules: Beside the classical Modus Ponens and the Necessitation Rule we have the Induction Rule

ϕ → α[x/ϕ] ϕ → νx.α .
It can be shown that the fixpoint axioms can be replaced by the following weaker axioms: νx.ϕ(x) → ϕ(νx.ϕ(x)) and µx.ϕ(x) ← ϕ(µx.ϕ(x)).

We say that a variable x ∈ bound(ϕ) is well-bound in ϕ if no two distinct occurrences of fixpoint operators in ϕ bind x, and x occurs only once in ϕ. A propositional variable p is guarded in a formula ϕ ∈ L µ if every occurrence of p in ϕ is in the scope of a modal operator. A formula ϕ of L µ is said to be well-named if every x ∈ bound(ϕ) is guarded and well-bounded in ϕ. For all well-named ϕ, if x is bound in ϕ then there is exactly one subformula occurrence ηx.δ ≤ ϕ which bounds x, this formula is denoted by ϕ x . In Lemma 4 we will see that any µ-formula ϕ is equivalent to a well-named formula wn(ϕ), therefore, if nothing else mentioned, we assume that all formulae are well-named.

Let ϕ(x) be a µ-formula. If x is free and occurs only positively in ϕ, then we define ϕ n (x) for all n inductively such that ϕ 1 (x) = ϕ(x) and such that

ϕ k+1 (x) ≡ ϕ[x/ϕ k (x)].
ϕ n (⊤) and ϕ n (⊥) are obtained by substituting x with ⊤ or ⊥ respectively.

The rank, rank(ϕ), of a formula ϕ is an ordinal number defined inductively as follows:

-rank(p) = rank(∼ p) = 1 -rank(△ α) = rank(α) + 1 where △∈ { , ♦} -rank(α • β) = max{rank(α), rank(β)} + 1 where • ∈ {∧, ∨} -rank(ηx.α) = sup{rank(α n (x)) + 1 ; n ∈ N} where η ∈ {ν, µ}.
In the joint work with Krähenbühl [AK∞] (see also [Alb∞]) one of the authors shows that the algorithm for rank terminates. Further, it is an easy exercise to show that for all formulae ϕ we have that rank(ϕ) = rank(¬ϕ). The next lemma shows that well-naming iterated formulae which are already well-named does not affect the rank.

Lemma 2 For all well-named formulae ϕ such that x appears only positively and all n ∈ N we have that

rank(ϕ n (⊤)) = rank(wn(ϕ n (⊤))).
Similarly for ⊥.

Proof. The result follows from the fact that since ϕ is well-named the equivalent well-named formula is given by simply renaming bound variables in ϕ n (⊥). This can be verified by showing by induction on n that there are no free occurrences of a variable x in ϕ n (⊤) which becomes bound in ϕ(ϕ n (⊤)). ⊣

As for GL the semantics of modal µ-calculus is given by transition systems. In order to define the denotation to fixpoint formulae let λ be a valuation, p a propositional variable and S ′ a subset of states S; we set for all propositional variables p

′ λ[p → S ′ ](p ′ ) = S ′ if p ′ = p, λ(p ′ ) otherwise.
Given a transition system T = (S, → T , λ T ), then T [p → S ′ ] denotes the transition system (S, → T , λ T [p → S ′ ]). Given a transition system T , the denotation of ϕ in T , ϕ T , that is, the set of states satisfying a formula ϕ is defined inductively on the structure of ϕ as it was for GL and, in addition we set

-νx.α T = {S ′ ⊆ S | S ′ ⊆ α(x) T [x →S ′ ] }, and -µx.α T = {S ′ ⊆ S | α(x) T [x →S ′ ] ⊆ S ′ }.
For a formula ϕ(x) and set of states S ′ ⊆ S we sometimes write ϕ(S ′ ) T instead of ϕ(x) T [x →S ′ ] . When clear from the context we use ϕ(x) T for the function

ϕ(x) T : ℘(S) → ℘(S) S ′ → ϕ(S ′ ) T .
By the Tarski-Knaster Theorem, c.f. [Tar55], νx.α(x) T is the greatest fixpoint and µx.α(x) T the least fixpoint of the operator α(x) T . Also for the modal µ-calculus we have a completeness theorem, due to Walukiewicz.

Theorem 3 ([Wal00]

). For all µ-formulae ϕ we have that

|= ϕ if and only if Koz ⊢ ϕ.
The next lemma states some basic properties of denotations.

Lemma 4 For all transition systems T = (S, → T , λ T ) and all formulae ϕ we have that

1. ¬ϕ T = S \ ϕ T , 2. ηx.ηy.ϕ(x, y) T = ηx.ϕ(x, x) T , where η ∈ {µ, ν}, 3. νx.ϕ(x) T = ϕ(⊤) T , if x is not guarded, 4. µx.ϕ(x) T = ϕ(⊥) T , if x is not guarded. 5.
There is a well-named formula wn(ϕ) such that ϕ T = wn(ϕ) T .

Proof. Part 1 to part 4 are classical properties of the modal µ-calculus. Part 5 is a straightforward consequence of parts 2 to 4. ⊣

From now on, we assume that wn is a function associating to every formula ϕ a well-named formula wn(ϕ) and by L wn µ we denote the set of all well-named µ-formulae.

Embedding GL into the modal µ-calculus

In this subsection we define an embedding t from GL into the modal µ-calculus. First, we define the function () * : L GL (P ) → L µ (P ) recursively on the structure of the formula such that

-(p) * ≡ p and (∼p) * ≡∼p, -(α ∧ β) * ≡ (α) * ∧ (β) * and (α ∨ β) * ≡ (α) * ∨ (β) * -( α) * ≡ νx. (x ∧ (α) * ), and -(♦α) * ≡ µx.♦(x ∨ (α) * ).
The embedding t : L GL (P ) → L µ (P ) is now defined as

t(ϕ) ≡ µx. x → (ϕ) * .
The following theorem is due to van Benthem [START_REF] Van Benthem | Modal Frame Correspondences and Fixed-Points[END_REF]. It shows that GL which semantically lives on transitive and upward well-founded transition systems can be translated into the modal µ-calculus over arbitrary transition systems. For the first equivalence van Benthem provides a syntactical proof without using completeness results.

Theorem 5 [START_REF] Van Benthem | Modal Frame Correspondences and Fixed-Points[END_REF]). For all formulae ϕ ∈ L GL we have that

(GL ⊢ ϕ ⇔ Koz ⊢ t(ϕ)) and (|= GL ϕ ⇔ |= t(ϕ)).

Parity games

Let V be a set. By V * we denote the set of finite sequences on V , and by V + we denote the set of nonempty sequences. Finally, by V ω we denote the set of infinite sequences over V .

A game G is defined in terms of an arena A and a winning condition W . In our case an arena is simply a bi-partite graph

A = V 0 , V 1 , E , where V 0 ∩V 1 = ∅ and the edge relation, or set of moves, is E ⊆ (V 0 ∪ V 1 ) × (V 0 ∪ V 1 ). Let V = V 1 ∪ V 2
be the set of vertices, or positions, of the arena. Given two vertices a, b ∈ V , we say that b is a successor of a, if (a, b) ∈ E. The set of all successors of a is sometimes denoted by aE or E(a). We say that b is reachable from a if there are a 1 , . . . , a n ∈ V such that a 1 = a, a n = b and for every 0 < i < n, a i+1 ∈ a i E.

A play in the arena A can be finite or infinite. In the former case, the play is a non empty finite path π = a 1 . . . a n ∈ V + such that for every 0 < i < n, a i+1 ∈ a i E and a n E = ∅. In the last case, the play consists in an infinite path π = a 1 . . . a n • • • ∈ V ω with a i+1 ∈ a i E for every i > 0. Thus a finite or infinite play in a game can be seen as the trace of a token moved on the arena by two Players, Player 0 and Player 1, in such a way that if the token is in position a ∈ V i , then Player i has to choose a successor of a where to move the token.

The set of winning conditions W is a subset of V ω . Thus, given a game G = (A, W ) a play π is winning for Player 0 iff 1. if π is finite, then the last position a n of the play is in V 1 , 2. if π is infinite, then it must be a member of W .

A play is winning for Player 1 if it is not winning for Player 0. In this framework we are interested in what is called a parity winning condition. That is, given a set of vertices V , we assume a colouring or ranking function Ω : V → ω such that Ω[V ] is bounded. Then, the set W of winning conditions is defined as the set of all infinite sequences π such that the greatest priority appearing infinitely often in Ω(π) is even.

Let A be an arena. A strategy for Player i is simply a function σ i : V * V i → V , with i = 0, 1. A prefix a 1 . . . a n of a play is said to be compatible or consistent with σ i iff for every j with 1 ≤ j < n and a j ∈ V i , it holds that σ i (a 1 . . . a j ) = a j+1 . A finite or infinite play is compatible or consistent with σ i if each of its prefixes which is in V * V i is compatible with σ i . The strategy σ i is said to be a winning strategy for Player i on W if every play consistent with σ i is winning for Player i. A position a ∈ V is winning for Player i in the parity game G iff there is a strategy σ for Player i such that every play compatible with σ which starts from a is winning for Player i. A winning strategy σ is called memoryless if σ(a 1 . . . a n ) = σ(b 1 . . . b n ), when a n = b n . For parity games we have a memoryless determinacy result.

Theorem 6 ([EJ91,Mos91]) In a parity game, one of the Players has a memoryless winning strategy from each vertex.

Having in mind this theorem, in the sequel we assume that all winning strategies are memoryless, that is, a winning strategy in a parity games for Player 0 is a function σ : V 0 → V , analogously for Player 1.

Evaluation games for the modal µ-calculus

In this subsection we will see, given ϕ ∈ L µ and a pointed transition system (T , s 0 ) with T = (S, → T , λ T ), how to determine the corresponding parity game E(ϕ, (T , s 0 )), called also the evaluation game of ϕ over (T , s 0 ).

The arena of E(ϕ, (T , s 0 )) is the triple

V 0 , V 1 , E which is defined recursively such that ϕ, s 0 ∈ V (remember that V = V 0 ∪ V 1 )
and such that if ψ, s ∈ V then we distinguish the following cases:

-If ψ ≡ (∼)p and p ∈ free(ϕ). In this case we set E ψ, s = ∅ and

ψ, s ∈ V 1 iff s ∈ λ T (ψ) if ψ ≡ p s ∈ λ T (ψ) if ψ ≡∼p.
-If ψ ≡ x and x ∈ bound(ϕ). Given ϕ x , s ∈ V , in this case we set ( ψ, s , ϕ x , s ) ∈ E and we have ψ, s ∈ V 0 iff x is a µ-variable.

-If ψ ≡ α ∧ β. In this case we have ψ, s ∈ V 1 and ( ψ, s , α, s ) ∈ E and ( ψ, s , β, s

) ∈ E -If ψ ≡ α ∨ β.
In this case we have ψ, s ∈ V 0 and ( ψ, s , α, s ) ∈ E and ( ψ, s , β, s

) ∈ E -If ψ ≡ α.
In this case we have ψ, s ∈ V 1 and ( ψ, s , α, s ′ ) ∈ E for all s ′ such that s → T s ′ .

-If ψ ≡ ♦α. In this case we have ψ, s ∈ V 0 and ( ψ, s , α, s ′ ) ∈ E for all s ′ such that s → T s ′ .

-If ψ ≡ νx.α. In this case we have ψ, s ∈ V 1 and ( ψ, s , α, s ) ∈ E.

-If ψ ≡ µx.α. In this case we have ψ, s ∈ V 0 and ( ψ, s , α, s ) ∈ E.

We complete the definition of the parity game E(ϕ, (T , s 0 )) by defining the partial priority function Ω : V → ω. The function is only defined on states of the form ηx.δ, s ∈ V , where η ∈ {µ, ν}. In this case we have that:

Ω( ψ, s ) =       
ad(ηx.δ) if η = µ and ad(ηx.δ) is odd, or η = ν and ad(ηx.δ) is even; ad(ηx.δ) -1 if η = µ and ad(ηx.δ) is even, or η = ν and ad(ηx.δ) is odd.

Remember that if the play π is finite, Player 0 wins iff the last vertex of the play belongs to V 1 , and if the play π is infinite, Player 0 wins iff the greatest priority appearing infinitely often is even.

Theorem 7 ([ES89]) (T , s) ∈ ϕ iff Player 0 has a winning strategy for E(ϕ, (T , s)).

This result can be seen as the "game-theoretical version" of what is usually called the Fundamental Theorem of the semantic of the modal µ-calculus.

The next lemma verifies that over upward well-founded transition systems, least fixpoints and greatest fixpoints coincide.

Lemma 8 Let T be an upward well-founded transition system. Then, for every ϕ(x) ∈ L µ such that x is guarded and positive it holds that µx.ϕ(x) T = νx.ϕ(x) T .

Proof. Note, that in an evaluation game there are no infinite regeneration of x since then we would have an infinite chain of the form

s 0 → T s 1 → T s 2 . . . .
Therefore, a winning play for νx.ϕ is also a winning play for µx.ϕ. With Theorem 7 we get the result. ⊣

3 The modal µ-calculus over GL

In this section we show that the expressivity of the modal µ-calculus over GL, that is, over transitive and upward well-founded transition systems, is the same as the one of the modal base language. In this sense we answer to van Benthem's question cited in the introduction.

In [AF∞] the authors showed that over transitive transition systems every µ-formula is equivalent to a µ-formula without alternation of fixpoint operators. Moreover, they showed that under certain conditions a fixpoint operator can be eliminated by regenerating the formula: Theorem 9 ([AF∞]) Let T be a transitive transition system, and let ϕ(x) be a well-named µ-formula such that x ∈ free(ϕ) and occurs only once. Then 1. If x is in the scope of a in νx.ϕ(x) then νx.ϕ(x) T = ϕ 2 (⊤) T .

If

x is in the scope of a ♦ in µx.ϕ(x) then µx.ϕ(x) T = ϕ 2 (⊥) T .

Definition 1. The translation τ : L wn µ (P ) → L GL (P ) is defined recursively on the rank of the formula such that τ ((∼)p) ≡ (∼)p, such that τ distributes over boolean and modal connectives and such that for all η ∈ {µ, ν} we have

τ (ηx.ϕ) = τ (wn(ϕ 2 (⊤)))
x is in the scope of a in ϕ, τ (wn(ϕ 2 (⊥))) else.

Obviously, by first well-naming a formula and then applying τ we get a translation from L µ (P ) to L GL (P ).

Given the fact that over well-founded transition systems greatest and least fixpoint coincide, this result gives us the collapse of the modal µ-calculus over GL into its modal fragment.

Theorem 10. On transitive and upward well-founded transition systems we have that the following holds for every ϕ ∈ L µ :

ϕ T = τ (wn(ϕ)) T .
Proof. By Lemma 4 we can assume that ϕ is well-named. The proof is by induction on rank(ϕ). The base case and the case where rank(ϕ) is a successor ordinal are straightforward. If rank(ϕ) is a limit ordinal then ϕ is of the form ηx.α (η ∈ {µ, ν}). Assume that ϕ is of the form νx.ϕ. If x is in the scope of a in ϕ then the induction step follows from Theorem 9.1. Else, x is only in the scope of some ♦ in ϕ. In this case by Lemma 8 we have that νx.ϕ T = µx.ϕ T and by applying Theorem 9.2 we get the induction step. The case where ϕ is of the form µx.ϕ is shown by analogous arguments. ⊣

4 The modal µ ∼ -calculus

In this section we introduce a new language, called the modal µ ∼ -calculus, which, in some sense, can be seen as an extension of the guarded fragment of the modal µ-calculus. The main novelty is that we allow the µ-operator to bind negative (and guarded) occurrences of propositional variables. Therefore, the modal µ ∼calculus allows us to refer explicitly, that is, in a µ-calculus style, to fixpoints of guarded formulae. For example, the fixpoint of the "equation" p ↔ α(p) where α(x) is a guarded formula can be directly denoted as µx.α(x). As it can be done for the modal µ-calculus the semantics of the modal µ ∼ -calculus is defined by way of games over transitive and upward well-founded transition systems.

We provide an explicit syntactical translation of the modal µ ∼ -calculus into GL which preserves logical equivalence. As a corollary of the collapse, we obtain a new version of the de Jongh, Sambin Fixpoint Theorem. The modal µ ∼ -calculus could be seen as a starting point for the application of tools of the standard µ-calculus, as for example games, to GL.

Basic notions and results

The language of the modal µ ∼ -calculus, L µ ∼ , is almost the same as the one for the modal µ-calculus with the only difference that we allow fixpoint constructors also when the bound variable is appearing negatively, that is, modal µ ∼ -formulae (or simply µ ∼ -formulae) are defined as follows:

ϕ ::= p | ∼p | ⊤ | ⊥ | (ϕ ∧ ϕ) | (ϕ ∨ ϕ) | ♦ϕ | ϕ | µx.ϕ
where p, x ∈ Prop and where x appears guarded in ϕ. All syntactical notions, such as L µ ∼ (P), bound variable, rank of a formula, ϕ x , ϕ free(X) etc., are defined as for the modal µ-calculus. Without loss of generality, we always suppose that bound(ϕ) ∩ free(ϕ) = ∅.

We say that a µ ∼ -formula ϕ is in normal form if bound(ϕ) ∩ free(ϕ) = ∅ and if for all subformulae of ϕ of the form µx.µy.α we have that -α is not of the form µz.β, and -x occurs only negatively in α and y has only positive occurrences in α.

For the substitution, if x ∈ free(ϕ), then ϕ[x/ψ] is given by substituting ¬ψ to every negative occurrence ∼ x and by substituting ψ to every positive occurrence x. As for the modal µ-calculus negation is defined by using de Morgan laws and the duality of and ♦, in addition we set

¬µx.α ≡ µx.¬α[x/¬x].
The last equivalence can be rather surprising at a first look. It is motivated by the fact that the modal µ ∼ -calculus will be interpreted over upward well-founded models, where least and greatest fixpoint coincide.

Note that, for every y ∈ bound(µx.α), y is negative in µx.α if and only if y is negative in ¬µx.α.

The semantics for the modal µ ∼ -calculus over GL is given by evaluation games on pointed upward well-founded and transitive transition systems. These evaluation games are similar to the ones for the modal µ-calculus. Let ϕ ∈ L µ ∼ and (T , s) ∈ T wft .

-First we construct recursively the two arenas V + 0 , V + 1 , E + from ϕ and (T , s) and V - 0 , V - 1 , E -from ¬ϕ and (T , s) as it is done for the modal µ-calculus, then, for each vertex of the form ∼x, t which was generated in the recursion defining the arena V + 0 , V + 1 , E + we add the condition ∼x, t ∈ V + 0 and E + ( ∼x, t ) = ∅, and if it was generated in the recursion defining the arena

V - 0 , V - 1 , E -we set ∼x, t ∈ V - 0 and E -( ∼x, t ) = ∅.
-Then the arena of E(ϕ, (T , s)) is the triple V 0 , V 1 , E defined by taking the disjoint union of the two arenas, with the following modification:

• For every vertex of the form ∼x, t where x ∈ bound(ϕ) we set

E( ∼ x, t ) = { ¬ϕ x , t } ⊆ V -if ∼x, t ∈ V + 0 { ϕ x , t } ⊆ V + if ∼x, t ∈ V - 0 .
Since we are on upward well-founded models and that all regenerated variables are guarded, all plays are finite. Therefore, we have that Player 0 wins if and only if the last vertex of the play belongs to Player 1. Since therefore we do not have to care about priorities the definition of evaluation game for µ ∼ -formulae is admissible and well-defined4 . We say that a pointed upward well-founded transitive transition system (T , s) is a model of a µ ∼ -formula if and only if Player 0 has a winning strategy in E(ϕ, (T , s)). Further, we define

ϕ W T = {s ∈ S | (T , s) is a model of ϕ}.
By ϕ W we denote the class of all upward well-founded and transitive models of ϕ, that is, all pointed transition systems (T , s), transitive and upward wellfounded, such that s ∈ ϕ W .

Example 1. Consider the formula µx.♦ ∼x. This formula says that Player 0 can always force the number of the states visited in a play to be even. Because the considered models are transitive, this implies that the formula says that the root of the models has at least one accessible state.

The next lemma states some basic properties of denotation.

Lemma 11 For all transition systems T = (S, → T , λ T ) and all µ ∼ -formulae µx.ϕ we have that

1. µx.µy.ϕ(x, y) W T = µx.ϕ(x, x) W T , 2. µx 1 . . . µx n .ϕ W T = µx p(1) . . . µx p(n) .ϕ W T
, where p is any permutation over {1, . . . , n}, 3. There is a well-named formula wn(ϕ) such that ϕ W T = wn(ϕ) W T , 4. There is a formula nf(ϕ) in normal form such that ϕ T = nf(ϕ) T .

Proof. Part 1 is by definition of the evaluation game for the modal µ ∼ -calculus. Part 2 is proved by an easy induction on the length of the prefix. Part 3 is a straightforward consequence of part 1. Part 4 is a straightforward consequence of part 1 and part 2. ⊣

The next lemma shows that over upward well-founded models, the positively bounded fragment of the modal µ ∼ -calculus coincides with the guarded fragment of the standard modal µ-calculus.

Lemma 12 Let ϕ ∈ L µ ∩ L µ ∼ . Then for every upward-well founded model T ϕ W T = ϕ T .
Proof. This follows by applying Theorem 7 to the fact that, for every ϕ ∈ L µ ∩ L µ ∼ , the evaluation games for L µ ∼ and the evaluation games for the µ-calculus coincide over upward well-founded models. ⊣

The next lemma shows that negation behaves as expected.

Lemma 13 Let ϕ be a µ ∼ -formula and T = (S, → T , λ T ) an upward wellfounded transition system. We have that

¬ϕ W T = S \ ϕ W T .
Proof. Consider the evaluation game E(ϕ, (T , s)) where Player 0 starts to play as Player 1 and vice versa. Clearly Player 0 (resp. Player 1) has a winning strategy in this modified game iff she has a winning strategy in E(¬ϕ, (T , s)). From this fact we get the claim. ⊣

The next lemma shows that in the modal µ ∼ -calculus formulae of the form µx.ϕ indeed define a fixpoint.

Lemma 14 For every µx.ϕ ∈ L µ ∼ and every upward well-founded transition system T it holds that

µx.ϕ W T = ϕ[x/µx.ϕ] W T .
Proof. This result follows straightforwardly by definition of the evaluation game for the modal µ ∼ -calculus. ⊣

The unicity of fixpoints

Let T be a upward well-founded and transitive transition system and ϕ a µ ∼formula. Consider an arbitrary (memoryless) strategy σ for Player 0, not necessarily winning. We define the restriction of E(ϕ, (T , s 0 )) on σ, denoted by E| σ (ϕ, (T , s 0 )), as follows:

-The set of positions V | σ of the restriction is given by all nodes which are the positions of some play compatible with σ starting from position ϕ, s 0 , -The arena of E| σ (ϕ, (T , s 0 )) is the triple

V 0 | σ , V 1 | σ , E| σ where: 1. V 0 | σ = ∅, 2. V 1 | σ = V | σ , 3. if ψ, s ∈ V | σ ∩ V 1 then E| σ ( ψ, s ) = E( ψ, s ), and 4. if ψ, s ∈ V | σ ∩ V 0 then E| σ ( ψ, s ) = {σ( ψ, s )}.
We have that in E| σ (ϕ, (T , s 0 )) the only Player who can move is Player 1. This can be done because the moves for Player 0 are already completely determined by the (memoryless) strategy σ. Clearly, any play in E| σ (ϕ, (T , s 0 )) is a play in E(ϕ, (T , s 0 )) compatible with σ. We say that a play π in E| σ (ϕ, (T , s 0 )) is winning for Player 0 if and only if the play π is winning for Player 0 in E(ϕ, (T , s 0 )). If σ is a winning strategy for Player 0 then any play in E| σ (ϕ, (T , s 0 )) is winning for Player 0.

Definition 2. Let T be a upward well-founded transitive transition system, ϕ a µ ∼ -formula and σ any strategy for Player 0 in the parity game E(ϕ, (T , s 0 )). Then, for every position ψ, s of E| σ (ϕ, (T , s 0 )), we define a measure d( ψ, s ):

d( ψ, s ) = 0 if E| σ ( ψ, s ) = ∅ sup{d( ψ, s ′ ) + 1 : ψ, s ′ ∈ E| σ ( ψ, s )} otherwise.
Note that, since T is upward well-founded, there cannot be an infinite chain of the form a 0 , a 1 , a 2 , . . . such that for every i ≥ 0, a i , a i+1 ∈ E| σ . Therefore for all evaluation games E(ϕ, (T , s 0 )) and all vertices ψ, v in the arena d( ψ, v ) is a well-defined ordinal number, such that if a vertex α, v ′ is reachable from a vertex β, v ′′ then we have that d( α, v ′ ) < d( β, v ′′ ).

The next theorem shows that a fixpoint formula µx.α(x) in the modal µ ∼calculus defines a fixpoint, as proved in Lemma 14, and that any other fixpoint of a formula α(x) is identical to µx.α(x). In this sense it is an existence and uniqueness theorem, and it is the central result of the section.

Theorem 15 Let ϕ(x) ∈ L µ ∼ and x ∈ free(ϕ) a guarded variable. Let T be a upward well-founded transitive transition system. Then, for every A ⊆ S we have

ϕ(A) W T = A if and only if A = µx.ϕ(x) W T .
Proof. The implication from right to left follows from Lemma 14. In order to prove the implication from left to right, suppose ϕ(A) W T = A. From the definition of evaluation game we straightforwardly can derive the inclusion A ⊆ µx.ϕ(x) W T . For the other inclusion, suppose that s ∈ µx.ϕ(x) W T . We have that Player 0 has a winning strategy σ in E(µx.ϕ, (T , s)). Consider the restricted evaluation game E| σ (µx.ϕ, (T , s)). For each vertex α, v in E| σ (µx.ϕ, (T , s)), we have that d( α, v ) is a well-defined measure. Clearly, with the following claim we finish the proof.

Claim: For all vertices of the form α, s ′ in E| σ (µx.ϕ, (T , s)) if α = µx.ϕ then s ′ ∈ A, and, if α = µx.¬ϕ then s ′ / ∈ A.

The proof of the claim is by induction on d. Since d( µx.ϕ, s ′ ) > 0 and d( µx.¬ϕ, s ′ ) > 0 the induction base is trivial. For the induction step assume first that we have a vertex µx.ϕ, s ′ in E| σ (µx.ϕ, (T , s)). We distinguish two cases:

1. If from µx.ϕ, s ′ there is no a reachable vertex of the form µx.ϕ, s ′′ or µx.¬ϕ, s ′′ then we have that s ′ ∈ ϕ(A ′ ) W T for all sets of states A ′ and, therefore, we also have s ′ ∈ ϕ(A) W T . Since by assumption ϕ(A) T ⊆ A we finish the induction step for the case α = µx.ϕ(x).

The induction step for a vertex of the form µx.¬ϕ, s ′ is verified in the same way by using the fact that by Lemma 13 we have that ¬ϕ(A) W T = S \ ϕ(A) W T and, therefore, by assumption that ¬ϕ(A) W T = S \ A. ⊣ Corollary 1. Let ϕ and ψ be two µ ∼ -formulae. If for all upward well-founded transitive transition system T we have that ψ W T = ϕ W T then for all variables x and all T we have that µx.ψ W T = µx.ϕ W T Proof. By the "if" direction of Theorem 15 we have that

µx.ψ W T = ψ W T [x → µx.ψ W T ]
and with the premise of the corollary we get

µx.ψ W T = ϕ W T [x → µx.ψ W T ]
. Applying the "only if" direction of Theorem 15 we obtain that µx.ψ W T = µx.ϕ W T .

⊣

The next theorem provides a new proof of Bernardi, de Jongh, Sambin Theorem (c.f. Chapter 8 in [START_REF] Boolos | The Logic of Provability[END_REF] or [START_REF] Smorynski | Self-Reference and Modal Logic[END_REF]) using our results on the modal µ ∼ -calculus.

Theorem 16. Let ϕ(x) ∈ L GL , where x is guarded. We have that

GL ⊢ s (p ↔ ϕ(p)) ∧ s (q ↔ ϕ(q)) → (p ↔ q)
where s ϕ :≡ ϕ ∧ ϕ.

Proof. By Theorem 5 it is enough to show that for all ϕ(x) ∈ L GL it holds that

|= µx. x → ((( s )(p ↔ ϕ(p)) ∧ ( s )(q ↔ ϕ(q))) → (p ↔ q)) * .
And this can be shown by showing for all ϕ(x) ∈ L GL that we have

|= µx. x → (p ↔ ϕ(p) ∧ q ↔ ϕ(q) ∧ * (q ↔ ϕ(q)) ∧ * (q ↔ ϕ(q)) → (p ↔ q))
(1) where * γ ≡ νx. (x ∧ γ).

Assume, that we have

s ∈ µx. x ∧ p ↔ ϕ(p) ∧ q ↔ ϕ(q) ∧ * (q ↔ ϕ(q)) ∧ * (q ↔ ϕ(q)) T .
Then, (T , s) is well-founded and we have for s and for all reachable states s ′ from s that q ↔ ϕ(q) and p ↔ ϕ(p). Therefore, if we assume that T consists of s and all reachable states from s, which is an admissible assumption, we get that we have λ T (p) = ϕ(λ T (p)) W T and λ T (q) = ϕ(λ T (q)) W T .

By Theorem 15 we get that λ T (p) = µx.ϕ(x) W T and λ T (q) = µx.ϕ(x) W T .

and therefore we obtain that s ∈ p ↔ q T .

We have shown Equation 1 and finished the proof. ⊣

Collapsing the modal µ ∼ -calculus

In this subsection we provide an explicit syntactical translation of the modal µcalculus into GL which preserves logical equivalence. As a corollary, we obtain a new proof of the de Jongh, Sambin Fixpoint Theorem which provides an explicit construction of the fixpoint formula based on the syntactical translation defining the collapse. First of all, remember that, by Lemma 11.4, we can suppose that every µ ∼formula is in normal form.

Lemma 17 Let α(x) be a modal formula such that x appears only negatively and guarded. Then, for every T ∈ T wft we have that µx.(α[x/α(x)]) W T = µx.α(x) W T .

Proof. Let A be µx.α(x) W T . By the "if" direction of Theorem 15 we have that α(A) W T = A. We can iterate this equivalence twice and get Everything is now set up in order to prove that the modal µ ∼ -calculus over GL collapses to its modal fragment. Lemma 18 The translation I is well-defined and, moreover, if ϕ ∈ L µ ∼ (P ) then I(ϕ) ∈ L GL (P ).

Proof. By induction on the structure of the formula. The only critical case is when ϕ ≡ µx.α. By induction hypothesis, I(α(x)) ∈ L GL . Therefore α(y, z) ∈ L GL . By definition of normal form, z occurs only negatively and y occurs only positively in µz.µy.α(y, z). Thus, µy.α(y, z) ∈ L µ . This implies that wn(µy.α(y, z)) is well-defined and by Theorem 10 that τ (wn(µy.α(y, z))) ∈ L GL . Note that y occurs only positively in α(y, z) and wn(µy.α(y, z)) is given by duplicating and renaming y. Therefore, it follows that z occurs only positively in τ (wn(µy.α(z, y)))[z/τ (wn(µy.α(z, y)))]).

This implies that µz.β(z) ∈ L µ and therefore that wn(µz.β(z)) is well-defined. Thence by Theorem 10 we have that τ (wn(µz.β(z))) ∈ L GL .

Theorem 19 Let ϕ ∈ L µ ∼ . On upward well-founded and transitive transition systems T we have that ϕ W T = I(ϕ) W T .

Proof. The proof goes by induction on rank(ϕ). If rank(ϕ) = 1 or rank(ϕ) is a successor ordinal the induction step is straightforward. If rank(ϕ) is a limit ordinal then ϕ is of the form µx.α. In this case by Lemma 11 we have that µx.I(α) W T = µz.µy.α(z, y) W T .

Since by induction hypothesis we have that I(α) W T = α W T , with Corollary 1 we get that µx.I(α) W T = µx.α W T and therefore that W T = µz.µy.α(z, y) W T .

(2)

Since by Lemma 18 and by construction of normal forms, α is a modal formula we have that µy.α ∈ L µ . With Theorem 10 and Lemma 11 we get that for all upward well-founded and transitive T we have that µy.α W T = τ (wn(µy.α)) W T .

By Corollary 1 it holds that Theorem 20. Let ϕ(x) ∈ L GL (P), where x is guarded. We have that GL ⊢ I(µx.ϕ) ↔ ϕ(I(µx.ϕ)).

Further if ϕ ∈ L GL (P) then we have that I(µx.ϕ) ∈ L GL (P \ {x}).

Proof. The fact that I(µx.ϕ) ∈ L GL (P \ {x}) follows from Lemma 18. For the provable equivalence, we show that GL |= I(µx.ϕ) ↔ ϕ(I(µx.ϕ)). Note, that on upward-well-founded transitive transition system T , it holds that ♦ ♦ ⊤ T = ¬ ⊥ T .

Example 3. Consider the modal equation x ↔ ( (x → q) → ∼x). This is the same as x ↔ ♦(x∧ ∼q) ∨ ∼x.

(5)

By Theorem 20 the formula I(µx.♦(x∧ ∼q) ∨ ∼x) is a solution of Equation 5. Let's trace the construction of the fixpoint given by Definition 3:

We have that α ≡ ♦(x∧ ∼q) ∨ ∼y and that τ (µx.α) ≡ ♦((♦(⊥∧ ∼q) ∨ ∼y)∧ ∼q) ∨ ∼y.

The formula τ (µx.α) can be simplified by using the following equivalence τ (µx.α) T = ♦( ∼y∧ ∼q) ∨ ∼y T .

:

  All classical propositional tautologies, the Distribution Axiom from modal logic ( (α → β) ∧ α) → β and the Löb Axiom ( α → α) → α. Inference Rules: Beside the classical Modus Ponens α α → β β we have the Necessitation Rule α α .

  α[x/α(A)] W T = A. Applying the "only if" direction of Theorem 15 gives us µx.((α[x/α(x)]) W T = A and therefore the proof of this lemma. ⊣ Note that, if x ∈ bound(µx.α) appears only negatively, then x occurs only positively in µx.(α[x/α(x)]).

Definition 3 .

 3 The syntactical translation I : L µ ∼ → L GL uses the translation τ from L µ to L GL of Definition 1. It is defined recursively as follows: -I(p) = p and I(∼p) =∼p. -I(⊥) = ⊥ and I(⊤) = ⊤. -I(α • β) = I(α) • I(β), where • ∈ {∧, ∨}. -I(△ β) =△ I(β), where △∈ { , ♦}. -Assume that nf(µx.I(α(x))) is of the form µz.µy.α(z, y). We set I(µx.α) = τ (wn(µz.β(z))), where β(z) ≡ τ (wn(µy.α(z, y)))[z/τ (wn(µy.α(z, y)))]).

  µz.µy.α W T = µz.τ (wn(µy.α)) W T and with Equation 2 that µx.α W T = µz.τ (wn(µy.α)) W T .(3)Remember that y occurs only positively and z only negatively in α. Moreover wn(µy.α(y, z)) is obtained by multiplying and renaming y. Therefore, since z appears only negatively in µy.α(y, z) it appears only negatively in wn(µy.α(y, z)), too. Now, note that by definition of τ we are "regenerating" the formula only on positive occurrences and, therefore, we have that z appears only negatively in τ (µy.α), too. By Lemma 17 it holds that µz.(τ (wn(µy.α))) W T = µz. τ (wn(µy.α))[z/τ (wn(µy.α))](z) W T .With Equation 3 we get µx.α W T = µz. τ (wn(µy.α))[z/τ (wn(µy.α))](z) W T .By Lemma 11 and Theorem 10 we finish the induction step. ⊣The last theorem of the paper is a new version of the de Jongh, Sambin Fixpoint Theorem. Our version provides an explicit construction of the fixpoint formula based on the definition of I.

  The proof then follows by Theorem 1. Let T ∈ T wft . We haves ∈ I(µx.ϕ(x)) T ⇔ s ∈ µx.ϕ(x) W T Lemma 12 and Theorem 19, ⇔ s ∈ ϕ(µx.ϕ(x)) W T Lemma 14, ⇔ s ∈ ϕ(x) W T [x → µx.ϕ W T ]Definiton of evaluation game,⇔ s ∈ ϕ(x) W T [x → I(µx.ϕ) W T ] Theorem 19, ⇔ s ∈ ϕ(x) T [x → I(µx.ϕ) T ] Lemma 12, ⇔ s ∈ ϕ(I(µx.ϕ)) TDefinition of denotation.⊣We end with two examples where we apply our translation in order to find a solution of a modal equation.Example 2. Consider the modal equation x ↔ ¬ x. This is the same asx ↔ ♦ ∼x.(4)By Theorem 20 the µ ∼ -formula µx.♦ ∼ x is the solution of Equation4. By definition of I we have that I(µx.♦ ∼x) = τ (µx.♦¬♦ ∼x) = τ (µx.♦ x) = ♦ ♦ ⊤.

  W T = A we proved the claim. 2. Otherwise we distinguish two subcases given by the first vertex reached which is of either the form µx.ϕ, s ′′ or µx.¬ϕ, s ′′ . (a) If the first vertex reached of such kind is µx.ϕ, s ′′ , then, since we have that d( µx.ϕ, s ′ ) > d( µx.ϕ, s ′′ ), by induction hypothesis we get s ′′ ∈ A. (b) If the first vertex reached of such kind is µx.¬ϕ, s ′′ , then, since we have that d( µx.ϕ, s ′ ) > d( µx.¬ϕ, s ′′ ), by induction hypothesis we get s ′′ / ∈ A. Therefore, for each play consistent with σ starting from µx.ϕ, s ′ it holds that if it reaches first a vertex of the form µx.ϕ, s ′′ (or equivalently of the form x, s ′′ ) we have that s ′′ ∈ A, and, if it reaches first a vertex of the form µx.¬ϕ, s ′′ (or equivalently of the form ∼x, s ′′ ) we have that s ′′ ∈ A. But it can easily be seen that this implies s ′ ∈ ϕ(A) W T . Since by assumption ϕ(A) W

Note that on non well-founded models a play can be infinite. Thus, since in this kind of plays it is possible that Player 0 and Player 1 "switch" their roles infinitely often, it is not clear how to extend our game-theoretical approach also to non wellfounded models by adding a natural and uniform (parity) winning conditions for infinite plays.

Acknowledgments

We thank two anonymous referees for valuable comments.

Research supported by the Hasler Foundation ⋆ ⋆ ⋆ Research supported by a grant from the Swiss National Science Foundation, n.

200021-116508: Project "Topological Complexity, Games, Logic and Automata".

Now, we calculate β(y) of Definition 3 by using the simplified τ (µx.α) above and get β(y) ≡ ♦( ¬(♦( ∼y∧ ∼q) ∨ ∼y)∧ ∼q) ∨ ¬(♦( ∼y∧ ∼q) ∨ ∼y).

By definition of negation, we get

Note that the following semantical equivalences hold -♦( ( (♦y ∨ q) ∧ ♦y)∧ ∼q) T = ♦( ⊥∧ ∼q) T , and

Therefore, we get

Since I(µx.♦(x∧ ∼ q) ∨ ∼ x) ≡ τ (wn(µy.β(y))) it follows that the formula ( ⊥ → q) → ⊥ is a solution of Equation 5.


Anthony Soive
email: anthony.soive@cerema.fr

Véronique Baroghel-Bouny
email: ronique.baroghel-bouny@ifsttar.fr

Francis Lavergne
email: francis.la-vergne@cerema.fr

Numerical Strategy to Simulate Seawater Ingress in RC Concrete Blocks Exposed to Wetting-Drying Cycles in Field Conditions During 19 years

Keywords: Concrete, Chloride Binding, Seawater, Long-Term Exposure, Field Condition

Numerical results are compared to experimental data on concretes exposed in field conditions for 19 years and subjected to wetting/drying cycles in seawater after a couple of curing days. They were obtained thanks to a hydration model assuming fully hydrated concretes (19 years of curing time) and a reactive transport model in saturated conditions taking into account precipitation/dissolution of minerals and their kinetics and adsorption of ionic species on C-S-H. Numerical results show surprisingly rather good results, especially for concretes with fly ash. For OPC, although model considers average bulk porosity modifications, the experimental apparent diffusion coefficient increases much more. For concretes with silica fume, numerical results also show underestimations of total chloride content also experimental apparent diffusion coefficients are constant. Analysis of hydration calculations show that concretes are not fully hydrated after 19 years. Additional chloride content from reactions between anhydrous phases and chloride ingress may appear.

Introduction

Numerical study of reinforced concrete durability exposed to seawater in field conditions is difficult in several aspects. Environmental conditions can play a significant role in the chloride ingress (temperature, RH, wetting-drying cycles, orientation, wind). Curing time is also important because of possible interactions between concrete and seawater as well as initial presence of chloride in mixing water [START_REF] Suryavanshi | Stability of Friedel's salt in carbonated concrete structural elements[END_REF][START_REF] Caré | Effect of temperature on porosity and on chloride diffusion in cement pastes[END_REF] to cite a few). Previously reactive transport model taking into account precipitation and dissolution of mineral species with their kinetics as well as adsorption of ionic species on C-S-H were successfully used in order to simulate chloride ingress in laboratory concrete specimens (fully hydrated, controlled exposure conditions, saturated conditions) [START_REF] Tran | Modelisation of chloride reactive transport in concrete including thermodynamic equilibrium, kinetic control and surface complexation[END_REF]. However, in field conditions, concrete is not fully hydrated when they are exposed to seawater. Influence of hydration degree on chloride binding capacity of concrete is interesting.

Numerical simulations were done and compared to experimental data on concretes exposed in field conditions for 19 years and subjected to wet-ting/drying cycles in seawater after a couple of curing days. A hydration model following by a reactive transport model taking into account precipita-tion/dissolution of mineral species with their kinetics as well as adsorption of ionic species on C-S-H were used. Regarding all the phenomena to take into account, severe hypotheses were done such as saturated materials and 19 curing years. The aim of this study is to identify if such a severe hypothesis is sufficient in order to give a good approximation of chloride ingress.

Experimental Study and Numerical Approach

Experimental Study

Several concretes from the French project BHP2000 are exposed to sea-water and wettingdrying cycles in La Rochelle harbor (western French coast) since 19 years after 1 curing day [START_REF] Baroghel-Bouny | Ageing and durability of concrete in lab and in field conditions: Investigation of chloride penetration[END_REF]. 4 HPCs with or without silica fume (SF) and 3 normalstrength FA concretes which can appear as interesting mixtures with respect to current sustainable-de-velopment considerations were studied. All concretes described in this article were casted with the same cement (CEM I 52.5 PM ES CP2, see Table 1). Concrete mixdesign are described in Table 2.

Numerical Approach

A physically and chemically based model was developed to simulate ionic ingress in the materials. Calculations are managed with TOUGHREACT software [START_REF] Xu | TOUGHREACT User's Guide: A Simulation Program for Nonisothermal Multiphase Reactive Transport in Variably Saturated Geologic Media[END_REF]. The chemical part uses the thermodynamical database Cemdata18 [START_REF] Lothenbach | Cemdata18: A chemical thermodynamic database for hydrated Portland cements and alkali-activated materials[END_REF]. Hydration and interstitial solution calculations precede this reactive transport simulation (see Figure 1 for the description of the simulation steps). Input data are limited to chemical and mineralogical composition of the binder, concrete mix-design, average bulk porosity and effective diffusion coefficient of concrete. The reactive transport model considers precipitation and dissolution of mineral species and their kinetics and adsorption of several ionic species on C-S-H (Cl -, Na + , K + , Ca 2+ , SO 2-). It has been validated on different experimental data such as laboratory concretes exposed to different solutions containing chloride [START_REF] Tran | Modelisation of chloride reactive transport in concrete including thermodynamic equilibrium, kinetic control and surface complexation[END_REF]. Nevertheless, ingress of seawater in concrete exposed to field conditions after only few curing days is a difficult subject. In the case studied here, hydration was not complete when concretes were exposed to seawater leading to interactions between ionic species contained in seawater and anhydrous phases.

Although concretes are exposed to wetting-drying cycles, the present numerical model assumes that concrete is saturated by adopting a pure fickian approach (see Equation below). In fact, the wetting-drying cycle period is short (12 hours) and the mean value of the relative humidity in La Rochelle harbor is high (close to 67% [START_REF] Baroghel-Bouny | Ageing and durability of concrete in lab and in field conditions: Investigation of chloride penetration[END_REF]). Except for the first millimeters where carbonation can occur, this hypothesis seems to be reasonable [START_REF] Soive | Requirements and possible simplifications for multi-ionic transport models -Case of concrete subjected to wetting-drying cycles in marine environment[END_REF].

(1

)
where φ is the average bulk porosity, cj the concentration of species j [mol.m -3 of solution], De the effective diffusion coefficient [m 2 .s -1 ] (supposed to be equal for all species) and qj source or sink term [mol.m -3 .s -1 ]. Ions can chemically react with the matrix to precipitate minerals (e.g. ettringite, brucite, Kuzel and Friedel's salts) or to dissolve others (portlandite, monosulfate). They also can be bound (adsorbed or absorbed) to the surface of the matrix. As described in previous studies [START_REF] Baroghel-Bouny | Ageing and durability of concrete in lab and in field conditions: Investigation of chloride penetration[END_REF][START_REF] Soive | Requirements and possible simplifications for multi-ionic transport models -Case of concrete subjected to wetting-drying cycles in marine environment[END_REF], all mineral precipitation/dissolution kinetics also need to be taken into account. In addition, the effective diffusion coefficient De can evolve with average bulk porosity value change as follows:

𝐷𝐷 𝑒𝑒 = 𝜙𝜙𝜙𝜙𝐷𝐷 𝑤𝑤 (2)
where τ and Dw are the tortuosity and the diffusion coefficient of ionic species in water. A 1D diffusion model is adopted. 250 elements are used to simulate ionic species ingress in 10cm structural depth. By sake of simplicity and to avoid complex calculations of ionic species ingress during hydration, hydration duration is supposed to be equal to the greater exposition duration (19 years). Of course, this is a very first approximation owing to the competition between hydration and seawater ingress at first time exposure. Chemical reactions between seawater and anhydrous species are not considered.

Results and Discussion

Total chloride content profiles were measured after 2, 4, 10, 16 and 19 years of exposure. Comparison between experimental data and numerical results with 19 curing years is exposed in Figure 2. Knowing the limited number of input data and the difficulty to catch all the phenomena, the numerical simulations show hopeful results.

Three aspects can be underlined: the "convection zone", the evolution of apparent diffusion coefficient as a function of time and possible chemical reactions between chloride and anhydrous phases.

The « Convection Zone »

For concretes with fly ash (M25FA, M30FA, M50FA), results are rather good except in the first millimeters and although numerical model does not consider wetting/drying cycles. The depth at which total chloride content is maximum is to underline. This zone is often associated with the "convection zone". Nevertheless, even with a model that simulate the ingress of ionic species in saturated concrete such as the present one, this phenomenon is observed. As reported by [START_REF] Jakobsen | Elemental zonation in marine concrete[END_REF], chemical and mineral zonation appear. Three zones (magnesium, sulfur and chloride-rich zones) are found irrespective of the age, location or binder composition.

The Evolution of Apparent Diffusion Coefficient with Time

For OPC (M50, M75), whereas profiles are close to experimental data after 2-year exposure, total chloride contents are underestimated for greater exposure durations. These differences can be partly explained by the fact that apparent diffusion coefficient (which includes both effective diffusion and binding) for M50 and M75 increases with time (by inverse analysis calculations on experimental data) from 1.6 10 -13 to 2 10 -13 m 2 .s -1 and 3.6 10 -13 to 1.6 10 -12 m 2 .s -1 , respectively (see Figure 4). The present model considers microstructure evolution (average bulk porosity) due to mineral dissolution or precipitation (see Equation 2). It is also able to compute the evolution of chloride binding. However, the apparent coefficient increase is much greater than the one computed. Deeper experimental data investigations must be done in order to determine if other phenomena that are not modeled can appear, such as cracks, properties differences between concrete first millimeters and deeper.

Possible Chemical Reactions between Chloride and Anhydrous Phases

For concretes with silica fume (M75SF, M100SF), underestimations ap-pear after 2-year exposure. Nevertheless, as can be seen in Figure 4 and contrary to M50 and M75, the apparent diffusion coefficients are constant. By analyzing hydration results of M75SF thanks to a hydration model developed at Cerema [START_REF] Lavergne | Estimating the mechanical properties of hydrating blended cementitious materials: An investigation based on micromechanics[END_REF] (see Figure 5), results show that anhydrous phases are still present after 19 curing years (6500 days) as well as a lack of monosulfate. These results confirm that hydration is slower for these concretes. However, presence of seawater can affect the hydration process by accelerating hydration or precipitating minerals containing chloride (Friedel's salt) [START_REF] Li | The role of seawater in interaction of slag and silica fume with cement in low water-to-binder ratio pastes at the early age of hydration[END_REF]. Unfortunately, the present model is not able to calculate chloride ingress in concretes that continue to hydrate.

Conclusion

Figure 5. Hydration results after 1, 3, 10, 300 and 6500 curing days.

Experimental data on concretes exposed to tidal zone in field conditions for 19 years and subjected to wetting-drying cycles in seawater after a couple of curing days were compared to numerical results. Two OPCs, three concretes with fly ash and two concretes with silica fume with the same cement were studied. The numerical results were obtained thanks to a hydration model and a reactive transport model considering precipitation/dissolution of minerals and their kinetics and adsorption of ionic species on C-S-H. A pure fickian approach in saturated materials is assumed. In addition, due to difficulties to model interactions between ingress of ionic species and hydration, numerical model assumes that hydration lasts for 19 years (last measurement value).

Knowing the limited number of input data and the difficulty to catch all the phenomena, the numerical simulations show hopeful results, especially for concrete with fly ash. In addition, the model can qualitatively simulate chemical and mineral zonation (magnesium, sulfur and chloride-rich zones) as reported in the literature. For OPC and concretes with silica fume, numerical results underestimate chloride content. For OPC, although numerical model considers porosity change due to mineral precipitation/dissolution, it is not able to simulate increase of apparent diffusion coefficient as observed on experimental data. Further investigations must be done in order to observe if cracks are visible. For concretes with silica fume, underestimation cannot be fully explained yet. One explanation can be the lack of additional chloride content coming from reactions between chloride and remaining anhydrous phases. Indeed, by analyzing results of hydration calculations, results show that anhydrous phases are still present even after 19 years and that additional chloride content can exist.

ORCID

Previous the references list, the authors' ORCID must be provided, in 10pt Times New Roman, as in the example: Anthony Soive: https://orcid.org/0000-0002-2368-6848 Véronique Baroghle-Bouny: Francis Lavergne: https://orcid.org/0000-0001-6984-3784

Figure 1 .

 1 Figure 1. Flow chart of the reactive transport model.

Figure 2 .

 2 Figure 2. Comparison between experimental data and numerical results for total chloride profiles for 2, 4, 10, 16 and 20 years of exposure (19 curing years).

  Figure 3show that the model can qualitatively simulate these zones. However, in this "convection zone", results are very different from experimental data. The use of a model considering wetting-drying cycles is necessary in order to catch phenomena in this zone (convection, local chloride concentration increase).

Figure 3 .

 3 Figure 3. Ionic species ingress after 2, 4, 10, 16 and 20 years of exposure for M25FA (19 curing years)

Figure 4 .

 4 Figure 4. Apparent diffusion coefficient calculations by inverse analysis.

Table 1 .

 1 Chemical and mineralogical composition of the binder (%).

		SiO2 Al2O3 Fe2O3 CaO MgO SO3 K2O Na2O
	CEMI	21.39 3.49	4.16 65.12 0.82 2.86 0.30 0.12
	Fly Ash	55.86 25.40 6.05	1.83 0.63 0.11 4.77 0.24
	Silica Fume 94.75 0.07	0.08	0.34 0.28 0.05 0.28 0.18

Table 2 .

 2 Mix-design, along with average 28 days cylinder compressive strength and 90 days porosity accessible to water (measured after water curing).

	Concrete Gravel/sand Cement FA SF Water W/binder	σc	Porosity
	M25FA	992/905	195	48	-	187	0.77	23.5	0.157
	M30FA	986/879	223	95	-	166	0.52	48.5	0.141
	M50FA	956/809	325	79	-	181	0.45	53.0	0.150
	M50	937/806	410	-	-	197	0.48	55.5	0.145
	M75	1025/808	461	-	-	146	0.32	75.0	0.114
	M75SF	1044/877	360	-	22	136	0.36	85.5	0.100
	M100SF	1049/871	377	-	38	124	0.30	109.0	0.084


Carlo Rovelli

Relations and Panpsychism

20th century physics has revealed a pervasive relational aspect of the physical world. This fact is relevant in view of some of the motivations for panpsychism. In facts, it may be seen as a vindication of the panpsychist idea of a monist continuity where some aspects of the consciousness' perspectivalism are universal. But this same fact undermines the motivations for genuine forms of panpsychism.

If some aspects of mind are universal, which ones are so? I point out in this note that 20th Century physics has already vindicated a -very mild-form of panpsychism. This is because of the profoundly relational aspect this physics, manifest in general relativity, but especially in quantum mechanics. 20thCentury physics is not about how individual entities are by themselves. It is about how entities manifest themselves to one another. It is about relations. This is particularly evident for quantum theory, especially (but not uniquely) if one reads it in terms of its relational interpretation [START_REF] Rovelli | Relational quantum mechanics[END_REF][START_REF] Laudisa | Relational Quantum Mechanics[END_REF]. Niels Bohr expressed this 'contextual' aspect of quantum theory by saying that a physical system can only be described taking into account the systems it is interacting with. The current account of the world in fundamental physics is therefore always the account of how a system affects another system. This implies that the most effective way of thinking about the world is not in terms of entities with properties, but rather in terms of systems that have properties in relation to other systems. In turn, this implies that any physical description of a system is necessarily perspectival: relative to another system.

In the textbook Copenhagen formulation of quantum theory, the physical system with respect to which properties take value is variously and a bit obscurely interpreted as 'the apparatus', 'the observer', 'the macroscopic world' and similar. In relational quantum mechanics, the properties of a system S are defined with respect to any other physical system O with which S interacts, and are relative to O [START_REF] Laudisa | Relational Quantum Mechanics[END_REF]. Similarly, in the many-worlds interpretation of quantum mechanics, variables have values only in relation to (components in a branch of) other systems when the two have got entangled [START_REF] Saunders | Many Worlds?: Everett, quantum theory, and realism[END_REF].

A direct consequence is that our physics today is not a physics of the world seen from the outside. It is a physics or the world always seen from the perspective a physical system. This is perhaps not panpsychism, because there is nothing specifically psychic or mental in the relational properties of a system with respect to another system. But there is definitely something in common with panpsychism, because the world is not described from the outside: it is always described relative to a physical system [START_REF] Dorato | Rovelli' s relational quantum mechanics, monism and quantum becoming[END_REF]. So, physical reality is, in our current physics, perspectival reality [START_REF] Rovelli | [END_REF].

On the other hand, this very relationalism may suffice to resolve the very problems that motivated panpsychism in the first place: do we really need elementary physics to include more aspects in common with the mental world than this? Which ones? All phenomena of which I am aware that are more related to psyche or mind are connected to a brain, a neural system, sensory organs, feed back loops or the like. I cannot imagine anything even vaguely more like psyche or mind, without some structure like those.

A motivation for panpsychism is the idea that there is a 'hard problem' of consciousness [START_REF] Chalmers | Facing Up to the Problem of Consciousness[END_REF]. This is the expectation that even if we had figured out how our body works in terms of our current science, there would still be something mysterious about 'consciousness'. This expectation is based upon an intuition: that subjective experience, the 'first person perspective', must be incompatible with the world as we describe it now in physics. For instance, Chalmers argues that it is conceivable to imagine a body with the same physics as my body, but with no subjective experience; hence subjective experience must be over and above this physics [START_REF] Chalmers | Facing Up to the Problem of Consciousness[END_REF].

I do not know how Chalmers can 'conceive' this: I can't. The point is that what we can 'conceive' depends on the conceptual structure we have, and this keeps changing and includes a big deal of presuppositions, sometimes wrong. History of science should warn us that trusting 'intuition' blindly can freeze us into wrong ideas. We do not yet fully understand the physics of thunderstorms, but trusting the compelling 'intuition' that lightning and thunder are evidence for the rage of Odin may not be very wise.

More specifically, the intuition of a tension between mental and physical is based on two assumptions. The first is that the subject of experience is an irreducible entity. The second is that the material world is formed by substances having properties. There is indeed a tension between these two concepts that appear radically distinct. In particular, mental phenomena are intentional: they are relative to something else. Material phenomena at first may seem incompatible with this.

Both these assumptions seems to me to be wrong. There is a vast philosophical literature about the first and I will not go into it. Rather, I focus here on the second. The intuition of the 'material world' as formed by substance with properties, for instance just particles moving in space, is based on 18th century physics. Today we have a much more subtle view of the physical world. In particular, as I mentioned above, physics today is about relations between systems, about how systems affect one another. In a precise sense, quantum mechanics, in particular, has undermined the idea of an elementary level where components matter can be described independently from anything else.

If our basic understanding of the physical world is in terms of more or less complex systems that interact with one another and affect one another, the discrepancy between the mental ad the physical seems much less dramatic, and I do not see the need for stronger versions of panpsychism.

This obviously is not a solution to the 'easy problem' of consciousness-figuring out the physics of the body when mental processes happen. But it definitely under-cuts, seems to me, the intuition underpinning the belief that there is any 'hard' problem of consciousness. Mental phenomena are like other complex phenomena, and the existence of a subjective perspective is precisely the generic situation in physics: how systems 'appear to one another'.

So, relationalism can be seen as a very mild form of panpsychism. That is, there is something in common between mind and matter: they are ways reality of physical systems manifest itself to other physical systems, which is precisely what our physics currently describes.

The world as we know it today in physics is neither the material world of 18th century mechanic philosophy, neither embodied with any peculiar proto-consciousness. It is a world where physical systems -simple and complexmanifest themselves to other systems -systems and complex-in a way that our physics describes. I see no reason to belief that this should not be sufficient to account for stones, thunderstorms and thoughts.