Pierre Pradic

Colin Riba

A Dialectica-Like Interpretation of a Linear MSO on Infinite Words

Keywords: Linear Logic, Dialectica Interpretation, MSO on Infinite Words

We devise a variant of Dialectica interpretation of intuitionistic linear logic for LMSO, a linear logic-based version MSO over infinite words. LMSO was known to be correct and complete w.r.t. Church's synthesis, thanks to an automata-based realizability model. Invoking Büchi-Landweber Theorem and building on a complete axiomatization of MSO on infinite words, our interpretation provides us with a syntactic approach, without any further construction of automata on infinite words. Via Dialectica, as linear negation directly corresponds to switching players in games, we furthermore obtain a complete logic: either a closed formula or its linear negation is provable. This completely axiomatizes the theory the realizability model of LMSO. Besides, this shows that in principle, one can solve Church's synthesis for a given ∀∃-formula by only looking for proofs of either that formula or its linear negation.

Introduction

Monadic Second-Order Logic (MSO) over ω-words is a simple yet expressive language for reasoning on non-terminating systems which subsumes non-trivial logics used in verification such as LTL (see e.g. [START_REF] Thomas | Languages, Automata, and Logic[END_REF][START_REF] Baier | Principles of Model Checking[END_REF]). MSO on ω-words is decidable by Büchi's Theorem [6] (see e.g. [START_REF] Thomas | Automata on Infinite Objects[END_REF][START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]), and can be completely axiomatized as a subsystem of second-order Peano's arithmetic [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF]. While MSO admits an effective translation to finite-state (Büchi) automata, it is a non-constructive logic, in the sense that it has true (i.e. provable) ∀∃-statements which can be witnessed by no continuous stream function.

On the other hand, Church's synthesis [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF] can be seen as a decision problem for a strong form of constructivity in MSO. More precisely (see e.g. [START_REF] Thomas | Facets of Synthesis: Revisiting Church's Problem[END_REF][START_REF] Finkbeiner | Synthesis of Reactive Systems[END_REF]), Church's synthesis takes as input a ∀∃-formula of MSO and asks whether it can be realized by a finite-state causal stream transducer. Church's synthesis is known to be decidable since Büchi-Landweber Theorem [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF], which gives an effective solution to ω-regular games on finite graphs generated by ∀∃-formulae. In traditional (theoretical) solutions to Church's synthesis, the game graphs are induced from deterministic (say parity) automata obtained by McNaughton's Theorem [START_REF] Mcnaughton | Testing and generating infinite sequences by a finite automaton[END_REF]. Despite its long history, Church's synthesis has not yet been amenable to tractable solutions for the full language of MSO (see e.g. [START_REF] Finkbeiner | Synthesis of Reactive Systems[END_REF]).

In recent works [START_REF] Pradic | A Curry-Howard Approach to Church's Synthesis[END_REF][START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF], the authors suggested a Curry-Howard approach to Church's synthesis based on intuitionistic and linear variants of MSO. In particular, [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] proposed a system LMSO based on (intuitionistic) linear logic [START_REF] Girard | Linear Logic[END_REF], in which via a translation (-) L : MSO → LMSO, the provable ∀∃(-) L -statements exactly correspond to the realizable instances of Church's synthesis. Realizer extraction for LMSO is done via an external realizability model based on alternating automata, which amounts to see every formula ϕ(a) as a formula of the form (∃u)(∀x)ϕ D (u, x, a), where ϕ D represents a deterministic automaton.

In this paper, we use a variant of Gödel's "Dialectica" functional interpretation as a syntactic formulation of the automata-based realizability model of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]. Dialectica associates to ϕ(a) a formula ϕ D (a) of the form (∃u)(∀x)ϕ D (u, x, a). In usual versions formulated in higher-types arithmetic (see e.g. [START_REF] Avigad | Gödel's functional ("Dialectica") interpretation[END_REF]15]), the formula ϕ D is quantifier-free, so that ϕ D is a prenex form of ϕ. This prenex form is constructive, and a constructive proof of ϕ can be turned to a proof of ϕ D with an explicit witness for ∃u. Even if Dialectica originally interprets intuitionistic arithmetic, it is structurally linear, and linear versions of Dialectica were formulated at the very beginning of linear logic [19,[START_REF] De Paiva | A Dialectica-like Model of Linear Logic[END_REF]21].

We show that the automata-based realizability model of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] can be obtained by a suitable modification of the usual linear Dialectica interpretation, in which the formula ϕ D essentially represents a deterministic automaton on ω-words and is in general not quantifier-free, and whose realizers are exactly the finitestate accepting strategies in the model of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]. In addition to provide a syntactic extraction procedure with internalized and automata-free correctness proof, this reformulation has a striking consequence, namely that an extension LMSO(C) of LMSO is complete in the sense that for each closed formula ϕ, it either proves ϕ or its linear negation ϕ ⊥. Since LMSO(C) has realizers for all provable ∀∃(-) Lstatements, its completeness contrasts with the classical setting, in which due to provable non-constructive statements, one can not decide Church's synthesis by only looking for proofs of ∀∃-statements or their negations. Besides, LMSO(C) has a linear choice axiom which is realizable in the sense of both (-) D and [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF], but whose naive MSO counterpart is false.

The paper is organized as follows. We present our basic setting in §2, with a particular emphasis on particularities of (finite-state) causal functions to model strategies and realizers. Our variant of Dialectica and the corresponding linear system are discussed in §3, while §4 defines the systems LMSO and LMSO(C) and shows the completeness of LMSO(C).

Preliminaries

Alphabets (denoted Σ, Γ, etc) are finite non-empty sets of the form 2 p for some p ∈ N. We let 1 := 2 0 . Note that alphabets are closed under Cartesian products and set-theoretic function spaces. It follows that taking o := 2, we have an alphabet τ for each simple type τ ∈ ST, where σ, τ ∈ ST ::

= 1 | o | σ × τ | σ → τ
We often write (τ )σ for the type σ → τ . Given an ω-word (or stream) B ∈ Σ ω and n ∈ N, we write B n for the finite word B(0). • • • .B(n -1) ∈ Σ * .

Church's Synthesis and Causal Functions. Church's synthesis consists in the automatic extraction of stream functions from input-output specifications (see e.g. [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF][START_REF] Finkbeiner | Synthesis of Reactive Systems[END_REF]). These specifications are in general asked to be ω-regular, or equivalently definable in MSO over ω-words. In practice, proper subsets of MSO (and even of LTL) are assumed (see e.g. [START_REF] Bloem | Synthesis of reactive (1) designs[END_REF][START_REF] Filiot | Antichains and compositional algorithms for LTL synthesis[END_REF][START_REF] Finkbeiner | Synthesis of Reactive Systems[END_REF]). As an example, the relation

(∃ ∞ k)B(k) ⇒ (∃ ∞ k)C(k) resp. (∀ ∞ k)B(k) ⇒ (∃ ∞ k)C(k) (1)
with input B ∈ 2 ω and output C ∈ 2 ω specifies functions F : 2 ω → 2 ω such that F (B) ∈ 2 ω P(N) is infinite whenever B ∈ 2 ω P(N) is infinite (resp. the complement of B is finite). One may also additionally require to respect the transitions of some automaton. For instance, following [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF], in addition to either case of (1) one can ask C ⊆ B and C not to contain two consecutive positions:

(∀n)(C(n) ⇒ B(n)) and (∀n)(C(n) ⇒ ¬C(n + 1)) (2)
In any case, the realizers must be (finite-state) causal functions. A stream function F : Σ ω → Γ ω is causal (notation F : Σ → S Γ ) if it can produce a prefix of length n of its output from a prefix of length n of its input. Hence F is causal if it is induced by a map f : Σ + → Γ as follows:

F (B)(n) = f (B(0) • . . . • B(n))
(for all B ∈ Σ ω and all n ∈ N)

The finite-state (f.s.) causal functions are those induced by Mealy machines. A Mealy machine M : Σ → Γ is a DFA over input alphabet Σ equipped with an output function λ : Q M × Σ → Γ (where Q M is the state set of M). Writing ∂ * : Σ * → Q M for the iteration of the transition function ∂ of M from its initial state, M induces a causal function via (a.a ∈ Σ + ) → (λ(∂ * (a), a) ∈ Γ ). Causal and f.s. causal functions form categories with finite products. Let S be the category whose objects are alphabets and whose maps from Σ to Γ are causal functions F : Σ ω → Γ ω . Let M be the wide subcategory of S whose maps are finite-state causal functions.

Example 1. (a) Usual functions Σ → Γ lift to (pointwise, one-state) maps Σ → M Γ . For instance, the identity Σ → M Σ is induced by the Mealy machine with ∂, λ : (-, a) → (-, a). (b) Causal functions 1 → S Σ correspond exactly to ω-words B ∈ Σ ω . (c) The conjunction of (2) with either side of (1) is realized by the causal function F : 2 → M 2 induced by the machine M : 2 → 2 displayed on Fig. 1 (left, where a transition a|b outputs b from input a), taken from [START_REF] Thomas | Solution of Church's Problem: A tutorial[END_REF].

Proposition 1. The Cartesian product of Σ 1 , . . . , Σ n (for n ≥ 0) in S, M is given by the product of sets Σ 1 × • • • × Σ n (so that 1 is terminal). The Logic MSO(M). Our specification language MSO(M) is an extension of MSO on ω-words with one function symbol for each f.s. causal function. More precisely, MSO(M) is a many-sorted first-order logic, with one sort for each simple type τ ∈ ST, and with one function symbol of arity (σ 1 , . . . , σ n ; τ ) for each map σ 1 ו • •× σ n → M τ . A term t of sort τ (notation t τ ) with free variables among x σ1 1 , . . . , x σn n (we say that t is of arity (σ 1 , . . . , σ n ; τ )) thus induces a map t :

σ 1 × • • • × σ n → M τ . Given a valuation x i → B i ∈ σ i ω S[1, σ i ]
for i ∈ {1, . . . , n}, we then obtain an ω-word An instance of Church's synthesis problem is given by a closed formula (∀x σ )(∃u τ )ϕ(u, x). A positive solution (or realizer) of this instance is a term t(x) of arity (σ; τ ) such that (∀x σ )ϕ(t(x), x) holds.

t • B 1 , . . . , B n ∈ S[1, τ ] τ ω MSO(M)
Proposition 1 implies that MSO(M) proves the following equations:

π i ( t 1 , . . . , t n ) . = σi t i and t . = σ1ו••×σn π 1 (t), . . . , π n (t) (3)
Hence each formula ϕ(a σ1 1 , . . . , a σn n ) can be seen as a formula ϕ(a

F (B)(n) = f (B(0) • . . . • B(n -1)) (for all B ∈ Σ ω and all n ∈ N)
Finite-state eager functions are those induced by eager (Moore) machines (see also [START_REF] Filiot | Antichains and compositional algorithms for LTL synthesis[END_REF]). An eager machine E : Σ → Γ is a Mealy machine Σ → Γ whose output function λ : Q E → Γ is does not depend on the current input letter. An eager E : Σ → Γ induces an eager function via the map (a ∈ Σ * ) → (λ E (∂ * E (a)) ∈ Γ ). We write F : Σ → E Γ when F : Σ → S Γ is eager and F : Σ → EM Γ when F is f.s. eager. All functions F : Σ → M 1, and more generally, constants functions F : Σ → S Γ are eager. Note also that if F : Σ → S Γ is eager, then F : Σ → EM Γ . On the other hand, if F : Σ → EM Γ is induced by an eager machine E then F is finite-state causal as beeing induced by the Mealy machine with same states and transitions as E, but with output function (q, a) → λ E (q). Eager functions do not form a category since the identity of S is not eager. On the other hand, eager functions are closed under composition with causal functions.

Proposition 2. If F is eager and G, H are causal then H • F • G is eager.
Isolating eager functions allows a proper treatment of strategies in games and realizers w.r.t. the Dialectica interpretation. Since Σ + → Γ Σ * → Γ Σ , maps Σ → E Γ Σ are in bijection with maps Σ → S Γ . This easily extends to machines. Given a Mealy machine M : Σ → Γ , let Λ(M) : Σ → Γ Σ be the eager machine defined as M but with output map taking

q ∈ Q M to (a → λ M (q, a)) ∈ Γ Σ . Example 2. Recall the Mealy machine M : 2 → 2 of Ex. 1.(c). Then Λ(M) : 2 → 2 2
is the eager machine displayed in Fig. 1 (right, where the output is indicated within states). Eager f.s. functions will often be used with the following notations. First, let @ be the pointwise lift to M of the usual application function Γ Σ × Σ → Γ . We often write (F )G for @(F, G). Consider a Mealy machine M : Σ → Γ and the induced eager machine Λ(M) : Σ → Γ Σ . We have

F M (B) = @(F Λ(M) (B), B) (for all B ∈ Σ ω )
Given F : Γ → E Σ Γ , we write e(F ) for the causal @(F (-), -) : Γ → S Σ. Given F : Γ → S Σ, we write Λ(F ) for the eager Γ → E Σ Γ such that F = e(Λ(F )).

We extend these notations to terms. Eager functions admit fixpoints similar to those of contractive maps in the topos of tree (see e.g. [4,Thm. 2.4]).

Proposition 3. For each F : Σ × Γ → E Σ Γ there is a fix(F ) : Γ → E Σ Γ s.t. fix(F )(C) = F e(fix(F ))(C) , C) (for all C ∈ Γ ω ) If F is induced by the eager machine E : Σ × Γ → Σ Γ , then fix(F ) is induced by the eager H : Γ → Σ Γ defined as E but with ∂ H : (q, b) → ∂ E q, ((λ E (q))b, b) .
Games. Traditional solutions to Church's synthesis turn specifications to infinite two-player games with ω-regular winning conditions. Consider an MSO(M) formula ϕ(u τ , x σ ) with no free variable other than u, x. We see this formula as defining a two-player infinite game G(ϕ)(u τ , x σ ) between the Proponent P (∃loïse), playing moves in τ and the Opponent O (∀bélard), playing moves in σ . The Proponent begins, and then the two players alternate, producing an infinite play of the form

χ := u 0 x 0 • • • u n x n • • • ((u k ) k , (x k ) k ) ∈ τ ω × σ ω
The play χ is winning for P if ϕ((u k ) k , (x) k ) holds. Otherwise χ is winning for O. Strategies for P resp. O in this game are functions

σ * -→ τ resp. τ + -→ σ τ * -→ σ τ
Hence finite-state strategies are represented by f.s. eager functions. In particular, a realizer of (∀x σ )(∃u τ )ϕ(u, x) in the sense of Church is a f.s. P-strategy in

G ϕ((u)x, x) u (τ )σ , x σ
Most approaches to Church's synthesis reduce to Büchi-Landweber Theorem [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF], stating that games with ω-regular winning conditions are effectivelly determined, and that the winner always has a finite-state winning strategy. We will use Büchi-Landweber Theorem in following form. Note that an O-strategy in the game G(ϕ)(u τ , x σ ) is a P-strategy in the game G ¬ϕ(u, (x)u) x (σ)τ , u τ .

Theorem 1 ([7]

). Let ϕ(u τ , x σ ) be an MSO(M)-formula with only u, x free. Then either there is an eager term u(x) of arity (σ; τ ) such that |= (∀x)ϕ(u(x), x) or there is an eager term x(u) of arity (τ ; (σ)τ ) such that |= (∀u)¬ϕ(u, e(x)(u)). It is deciable which case holds and the terms are computable from ϕ.

Curry-Howard Approaches. Following the complete axiomatization of MSO on ω-words of [START_REF] Siefkes | Decidable Theories I : Büchi's Monadic Second Order Successor Arithmetic[END_REF] (see also [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]), one can axiomatize MSO(M) with a deduction system based on arithmetic (see §4.1). Consider an instance of Church's synthesis (∀x σ )(∃u τ )ϕ(u, x). Then we get from Theorem 1 the alternative

MSO(M) (∀x)ϕ e(u)(x), x or MSO(M) (∀u)¬ϕ (u)(x(u)), x(u) (4)
for an eager term u(x) or a causal term x(u). By enumerating proofs and machines, one thus gets a (naïve) syntactic algorithm for Church's synthesis. But it seems however unlikely to obtain a complete classical system in which the provable ∀∃-statments do correspond to the realizable instances of Church's synthesis, because MSO(M) has true but unrealizable ∀∃-statments. Besides, note that

(∀x σ )ϕ e(u)(x), x MSO(M) (∀x σ )(∃u τ )ϕ(u, x) (∀u (τ )σ )¬ϕ (u)(x(u)), x(u) MSO(M) (∀u (τ )σ )(∃x σ )¬ϕ (u)x, x ¬(∀x σ )(∃u τ )ϕ(u, x) MSO(M) (∀u (τ )σ )(∃x σ )¬ϕ (u)x, x
while it is possible both for realizable and unrealizable instances to have

MSO(M) (∀x σ )(∃u τ )ϕ(u, x) ∧ (∀u (τ )σ )(∃x σ )¬ϕ (u)x, x (5)
In previous works [START_REF] Pradic | A Curry-Howard Approach to Church's Synthesis[END_REF][START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF], the authors devised intuitionsitic and linear variants of MSO on ω-words in which, thanks to automata-based polarity systems, proofs of suitably polarized existential statments correspond exactly to realizers for Church's synthesis. In particular, [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] proposed a system LMSO based on (intuitionistic) linear logic [START_REF] Girard | Linear Logic[END_REF], such that via a translation (-) L : MSO → LMSO, provable ∀∃(-) L -statments exactly correspond to realizable instances of Church's synthesis, while (4) exactly corresponds to alternatives of the form

LMSO (∀x σ )(∃u τ ) ϕ (u)x, x L or LMSO (∀u (τ )σ )(∃x σ ) ¬ϕ (u)x, x L (6)
This paper goes further. We show that the automata-based realizability model of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] can be obtained in a syntactic way, thanks to a (linear) Dialecticalike interpretation of a variant of LMSO, which turns a formula ϕ to a formula ϕ D of the form (∃u)(∀x)ϕ D (u, x), where ϕ D (u, x) essentially represents a deterministic automaton. While the correctness of the extraction procedure of [START_REF] Pradic | A Curry-Howard Approach to Church's Synthesis[END_REF][START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] relied on automata-theoretic techniques, we show here that it can be performed syntactically. Second, by extending LMSO with realizable axioms, we obtain a system LMSO(C) in which, using an adaptation of the usual Characterization Theorem for Dialectica stating that ϕ ˛ϕD (see e.g. [15]), alternatives of the form (6) imply that for a closed ϕ,

LMSO(C) ϕ or LMSO(C) ϕ ⊥
where (-) ⊥ is a linear negation. We thus get a complete linear system with extraction of suitably polarized ∀∃-statments. Such a system can of course not have a standard semantics, and indeed, LMSO(C) has a functional choice axiom

(∀x σ )(∃y τ )ϕ(x, y) - (∃f (τ )σ )(∀x σ )ϕ(x, (f )x) (LAC)
which is realizable in the sense of both (-) D and [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF], but whose translation to MSO(M) (which precludes [START_REF] Bloem | Synthesis of reactive (1) designs[END_REF]) is false in the standard model.

A Monadic Linear Dialectica-like Interpretation

Gödel's "Dialectica" functional interpretation associates to ϕ(a) a formula ϕ D (a) of the form (∃u τ )(∀x σ )ϕ D (u, x, a). In usual versions formulated in higher-types arithmetic (see e.g. [START_REF] Avigad | Gödel's functional ("Dialectica") interpretation[END_REF]15]), the formula ϕ D is quantifier-free, so that ϕ D is a prenex form of ϕ. This prenex form is constructive, and a constructive proof of ϕ can be turned to a proof of ϕ D with an explicit (closed) witness for ∃u. We call such witnesses realizers of ϕ. Even if Dialectica originally interprets intuitionistic arithmetic, it is structurally linear: in general, realizers of contraction

ϕ(a) -→ ϕ(a) ∧ ϕ(a)
only exist when the term language can decide ϕ D (u, x, a), which is possible in arithmetic but not in all settings. Besides, linear versions of Dialectica were formulated at the very beginning of linear logic [19,[START_REF] De Paiva | A Dialectica-like Model of Linear Logic[END_REF]21].

In this paper, we use a variant of Dialectica as a syntactic formulation of the automata-based realizability model of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]. The formula ϕ D essentially represents a deterministic automaton on ω-words and is in general not quantifier-free. Moreover, we extract f.s. causal functions, while the category M is not closed. As a result, a realizer of ϕ is an open (eager) term u(x) of arity (σ; τ ) satisfying ϕ D (u(x), x). Thanks to Büchi-Landweber Theorem, contractions on closed ϕ have realizers which are correct in the standard model. But this is generally not the case for open ϕ(a). We thus work in a linear system, in which we obtain witnesses for ∀∃(-) L -statements (and thus for realizable instances of Church's synthesis), but not for all ∀∃-statements.

ϕ ϕ ϕ γ, ϕ ψ, γ ψ ϕ, ψ ϕ , ψ ϕ, ϕ, ψ, ψ ϕ ϕ, ψ, ϕ, ψ ϕ ϕ ϕ , ϕ, ψ, ψ ϕ ϕ , ψ, ϕ, ψ ϕ ψ ϕ, I ψ I ϕ, ϕ0, ϕ1 ϕ ϕ, ϕ0 ⊗ ϕ1 ϕ ϕ ϕ, ϕ ψ ψ, ψ ϕ, ψ ϕ ⊗ ψ, ϕ , ψ ϕ, ϕ ψ ϕ ϕ ψ ⊥ ϕ ψ ϕ ⊥, ψ ϕ, ϕ ϕ ψ, ψ ψ ϕ, ψ, ϕ `ψ ϕ , ψ ϕ ϕ0, ϕ1, ϕ ϕ ϕ0 `ϕ1, ϕ ϕ ϕ, ϕ ψ, ψ ψ ϕ, ψ, ϕ ψ ϕ , ψ ϕ, ϕ ϕ ϕ, (∃z τ )ϕ ϕ ϕ ϕ[t τ /x τ ], ϕ ϕ (∃x τ )ϕ, ϕ ϕ, ϕ[t τ /x τ ] ϕ ϕ, (∀x τ )ϕ ϕ ϕ ϕ ϕ (∀z τ )ϕ
Fix a set of atomic formulae At containing all (t τ . = u τ ).

The Multiplicative Fragment

Our linear system is based on full intuitionistic linear logic (see [START_REF] Hyland | Full Intuitionistic Linear Logic (Extended Abstract)[END_REF]). The formulae of the multiplicative fragment MF are given by the grammar:

ϕ, ψ ::= I | ⊥ | α | ϕ ψ | ϕ ⊗ ψ | ϕ `ψ | (∃x τ )ϕ | (∀x τ )ϕ
(where α ∈ At). Deduction is given by the rules of Fig. 2 and the axioms

t τ . = t τ t τ . = u τ , ϕ[t τ /x τ ] ϕ[u τ /x τ ] t τ = u τ t τ . = u τ (7)
Each formula ϕ of MF can be mapped to an MSO(M)-formula ϕ (where I, , ⊗, `are replaced resp. by , →, ∧, ∨). Hence ϕ holds whenever ϕ.

The Dialectica interpretation of MF is the usual one rewritten with the connectives of MF, but for the disjunction `that we treat similarly as ⊗. To each formula ϕ(a) with only a free, we associate a formula ϕ D (a) with only a free, as well as a formula ϕ D with possibly other free variables. For atomic formulae we let ϕ D (a) := ϕ D (a) := ϕ(a). The inductive cases are given on Fig. 3, where ϕ D (a) = (∃u)(∀x)ϕ D (u, x, a) and ψ D (a) = (∃v)(∀y)ψ D (v, y, a).

Dialectica is such that ϕ D is equivalent to ϕ via possibly non-intuitionistic but constructive principles. The tricky connectives are implication and universal quantification. Similarly as in the intuitionistic case (see e.g. [15,[START_REF] Avigad | Gödel's functional ("Dialectica") interpretation[END_REF][START_REF] Troelstra | Metamathematical Investigation of Intuitionistic Arithmetic and Analysis[END_REF]), (ϕ ψ) D is prenex a form of ϕ D ψ D obtained using (LAC) together with linear variants of the Markov and Independence of premises principles. In our case, the equivalence ϕ ˛ϕD also requires additional axioms for ⊗ and `. We give details for the full system in §3.3.

(ϕ ⊗ ψ) D (a) := ∃ u, v ∀ x, y . (ϕ ⊗ ψ) D ( u, v , x, y , a) := ∃ u, v ∀ x, y . ϕD(u, x, a) ⊗ ψD(v, y, a) (ϕ `ψ) D (a) := ∃ u, v ∀ x, y . (ϕ `ψ) D ( u, v , x, y , a) := ∃ u, v ∀ x,
The soundness of (-) D goes as usual, excepted that we extract open eager terms: from a proof of ϕ(a κ ) we extract a realizer of (∀a)ϕ(a), that is an open eager term u(x, a) s.t. ϕ D (@(u(x, a), a), x, a). Composition of realizers (in part. required for the cut rule) is given by the fixpoints of Prop. 3. Note that a realizer of a closed ϕ is a finite-state winning P-strategy in G( ϕ D )(u, x).

Polarized Exponentials

It is well-known that the structure of Dialectica is linear, as it makes problematic the interpretation of contraction:

ϕ(a) - ϕ(a) ⊗ ϕ(a)
and ϕ(a) `ϕ(a) -ϕ(a)

In our case, the Büchi-Landweber Theorem implies that all closed instances of contraction have realizers which are correct in the standard model. But this is in general not true for open instances.

Example 3. Realizers of ϕ ϕ ⊗ ϕ for a closed ϕ are given by eager terms

U 1 (u, x 1 , x 2 ), U 2 (u, x 1 , x 2 ), X(u, x 1 , x 2 ) which must represent P-strategies in the game G(Φ)( U 1 , U 2 , X , u, x 1 , x 2 ), where Φ is ϕ D (u, (X)ux 1 x 2 ) -→ ϕ D ((U 1 )u, x 1 ) ∧ ϕ D ((U 2 )u, x 2 )
By the Büchi-Landweber Theorem 1, either there is an eager term U(x) such that ϕ D (U(x), x) holds, so that

ϕ D (u, x 1 ) -→ ϕ D (e(U)(x 1 ), x 1 ) ∧ ϕ D (e(U)(x 2 ), x 2 )
or there is an eager term X(u) such that ¬ ϕ D (u, e(X)(u)) holds, so that

ϕ D (u, e(X)(u)) -→ ϕ D (u, x 1 ) ∧ ϕ D (u, x 2 ) Example 4.
Consider the open formula ϕ(a o ) := (∀x o )(t(x, a) . = 0 ω ) where t (B, C) = 0 n+1 1 ω for the first n ∈ N with C(n+1) = B(0) if such n exists, and such that t (B, C) = 0 ω otherwise. The game induced by ((∀a)(ϕ

ϕ ⊗ ϕ)) D is G(Φ)(X, x 1 , x 1 , a ), where Φ is t((X)x 1 x 2 a, a) . = 0 ω -→ t(x 1 , a) . = 0 ω ∧ t(
(resp. negative) if ϕ D (a) is of the form ϕ D (a) = (∃u τ )ϕ D (u, -, a) (resp. ϕ D (a) = (∀x σ )ϕ D (-, x, a)).
Quantifier-free formulae are thus both positive and negative. We only have exponentials for polarized formulae. First, following the usual polarities of linear logic, we can let

(!(ϕ + )) D (a) := (∃u)(!(ϕ + )) D (u, -, a) := (∃u)!ϕ D (u, -, a) (?(ψ -)) D (a) := (∀y)(?(ψ -)) D (-, y, a) := (∀x)?ψ D (-, y, a) (8)
Hence !ϕ is positive for a positive ϕ and ?ψ is negative for a negative ψ. The following exponential contraction axioms are then interpreted by themselves:

!(ϕ + ) - !(ϕ + ) ⊗ !(ϕ + ) and ?(ψ -) `?(ψ -) - ?(ψ -)
Second, we can have exponentials !(ψ -) and ?(ϕ + ) with the automata-based reading of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]. Positive formulae are seen as non-deterministic automata, and ? on positive formulae is determinization on ω-words (McNaughton's Theorem [START_REF] Mcnaughton | Testing and generating infinite sequences by a finite automaton[END_REF]). Negative formulae are seen as universal automata, and ! on negative formulae is to co-determinization (an instance of the Simulation Theorem [START_REF] Emerson | Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)[END_REF]18]). Formulae which are both positive and negative (notation (-) ± ) correspond to deterministic automata, and are called deterministic. We let

ψ ψ ψ, !ϕ ψ ψ, !ϕ, !ϕ ψ ψ, !ϕ ψ ϕ, ϕ ϕ ϕ, !ϕ ϕ !ϕ ϕ, ?ψ !ϕ !ϕ, ?ψ ϕ, !ϕ ψ, ?ψ ϕ !ϕ ψ, ?ψ ψ ψ ψ ?ϕ, ψ ψ ?ϕ, ?ϕ, ψ ψ ?ϕ, ψ ϕ ϕ, ψ ϕ ?ϕ, ψ !ϕ, ϕ ?ψ !ϕ, ?ϕ ?ψ ϕ ϕ, ?ψ ϕ (∀z)ϕ, ?ψ
(!(ψ -)) D (a) := (!(ψ -)) D (-, -, a) := !(∀x)ψ D (-, x, a) (?(ϕ + )) D (a) := (?(ϕ + )) D (-, -, a) := ?(∃u)ϕ D (u, -, a) (9)
So !(ψ -) and ?(ϕ + ) are always deterministic. The corresponding exponential contraction axioms are interpreted by themselves. This leads to the following polarized fragment PF (the deduction rules for exponentials are given on Fig. 4):

ϕ ± , ψ ± ::= I | ⊥ | α | !(ϕ -) | ?(ϕ + ) | ϕ ± ⊗ ψ ± | ϕ ± `ψ± | ϕ ± ψ ± ϕ + , ψ + ::= ϕ ± | !(ϕ + ) | (∃x σ )ϕ + | ϕ + ⊗ ψ + | ϕ + `ψ+ | ϕ - ψ + ϕ -, ψ -::= ϕ ± | ?(ϕ -) | (∀x σ )ϕ -| ϕ -⊗ ψ -| ϕ -`ψ-| ϕ + ψ -

The Full System

The formulae of the full system FS are given by the following grammar:

ϕ, ψ ::= ϕ + | ϕ -| ϕ ψ | ϕ ⊗ ψ | ϕ `ψ | (∃x τ )ϕ | (∀x τ )ϕ
Deduction in FS is given by Fig. 2, Fig. 4 and [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF]. We extend -to FS with !ϕ := ?ϕ := ϕ . Hence ϕ holds when ϕ is derivable. The Dialectica interpretation of FS is given by Fig. 3 and ( 8), (9) (still taking ϕ D (a) := ϕ D (a) := ϕ(a) for atoms). Note that (-) D preserves and reflects polarities.

Theorem 2 (Soundness). Let ϕ be closed with ϕ D = (∃u τ )(∀x σ )ϕ D (u, x).
From a proof of ϕ in FS one can extract an eager term u(x) such that FS proves

(∀x σ )ϕ D (u(x), x).
As usual, proving ϕ ˛ϕD requires extra axioms. Besides (LAC), we use the following (linear ) semi-intuitionistic principles (LSIP), with polarities as shown:

(∀a)(ϕ -(a) ⊗ ψ -) - (∀a)ϕ -(a) ⊗ ψ - (∀a)(ϕ -(a) `ψ-) - (∀a)ϕ -(a) `ψ- (∃a)ϕ -(a) `ψ - (∃a)(ϕ -(a) `ψ) (ψ - (∃a)ϕ -(a)) - (∃a)(ψ - ϕ -(a)) ((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± ) (LSIP)
as well as the following deterministic exponential axioms (DEXP):

δ - !δ and ?δ - δ (δ deterministic)
All these axioms but (LAC) are true in the standard model (via -). Moreover: Theorem 3 (Characterization). We have

FS+(LAC)+(LSIP)+(DEXP) ϕ(a) ˛ϕD (a) (ϕ FS-formula) FS+(LSIP)+(DEXP) ϕ(a) ˛ϕD (a) (ϕ PF-formula) Corollary 1 (Extraction). Consider a closed formula ϕ := (∀x σ )(∃u τ )δ(u, x) with δ deterministic. From a proof of ϕ in FS + (LAC) + (LSIP) + (DEXP) one can extract a term t(x) such that |= (∀x σ ) δ(t(x), x) .
Note that FS + (DEXP) proves δ `(δ ⊥) for all deterministic δ.

Translations of Classical Logic

There are many translations from classical to linear logic. Two canonical possibilities are the (-)

T and (-) Q -translation of [9] (see also [16]) targeting resp. negative and positive formulae. Both take classical sequents to linear sequents of the form !(-) ?(-), which are provable in FS in part. thanks to the PF rules ϕ, !ϕ ψ, ?ψ ϕ !ϕ ψ, ?ψ ϕ ϕ, ?ψ ϕ (∀z)ϕ, ?ψ For the completeness of LMSO(C) (Thm. 6, §4), we shall actually require a translation (-) L such that the linear equivalences (with polarities as displayed)

?ϕ + ˛ ϕ + L δ ± ˛ δ ± L !ψ -˛ ψ -L (10)
are provable possibly with extra axioms that we require to realize themselves. In part., [START_REF] Emerson | Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)[END_REF] implies (DEXP), and (-) L should give deterministic formulae. While (-)

T and (-) Q can be adapted accordingly, [START_REF] Emerson | Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)[END_REF] induces axioms which make the resulting translations equivalent to the deterministic (-) L -translation of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]:

⊥ L := ⊥ L := I α L := α (ϕ ∨ ψ) L := ϕ L `ψL (∃x σ .ϕ) L := ?(∃x σ )ϕ L (ϕ → ψ) L := ϕ L ψ L (ϕ ∧ ψ) L := ϕ L ⊗ ψ L (∀x σ .ϕ) L := !(∀x σ )ϕ L
Proposition 5. The scheme [START_REF] Emerson | Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)[END_REF] is equivalent in FS to (DEXP)+(PEXP), where (PEXP) are the following polarized exponential axioms, with polarities as shown: Note that ϕ L is deterministic and that ϕ L = ϕ.

?(ϕ + ) - ?!(ϕ + ) !?(ψ -) - !(ψ -) !(ϕ -) ?(ψ + ) - ?(ϕ - ψ + ) ?(ϕ + ) !(ψ -) - !(ϕ + ψ -) ?(ϕ + ) ⊗ ?(ψ + ) - ?(ϕ + ⊗ ψ + ) !(ϕ -⊗ ψ -) - !(ϕ -) ⊗ !(ψ -) ?(ϕ + ) `?(ψ + ) - ?(ϕ + `ψ+ ) !(ϕ -`ψ-) - !(ϕ -) `!(ψ -) Proposition 6. If ϕ is provable

Completeness

In §3 we devised a Dialectica-like (-) D providing a syntactic extraction procedure for ∀∃(-) L -statements. In this Section, building on an axiomatic treatment of MSO(M), we show that LMSO, an arithmetic extension of FS + (LSIP) + (DEXP) + (PEXP) adapted from [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF], is correct and complete w.r.t. Church's synthesis, in the sense that the provable ∀∃(-) L -statements are exactly the realizable ones. We then turn to the main result of this paper, namely the completeness of LMSO(C) := LMSO + (LAC). We fix the set of atomic formulae

α ∈ At ::= t τ . = u τ | t o ⊆ u o | E(t o ) | N(t o ) | S(t o , u o ) | 0(t o ) | t o ≤ u o 4.1 The Logic MSO(M)
MSO(M) is many-sorted first-order logic with atomic formulae α ∈ At. Its sorts and terms are those given in §2, and standard interpretation extends that of §2 as follows: ⊆ is set inclusion, E holds on B iff B is empty, N (resp. 0) holds on B iff B is a singleton {n} (resp. the singleton {0}), and S(B, C) (resp. B ≤ C) holds iff B = {n} and C = {n + 1} for some n ∈ N (resp. B = {n} and C = {m} for some n ≤ m). We write x ι for variables x o relativized to N, so that (∃x ι )ϕ and (∀x ι )ϕ stand resp. for (∃x o )(N(x) ∧ ϕ) and (∀x o )(N(x) → ϕ). Moreover,

x ι ∈ t stands for x ι ⊆ t, so that t o ⊆ u o is equivalent to (∀x ι )(x ∈ t → x ∈ u).
The logic MSO + [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] is MSO(M) restricted to the type o, hence with only terms for Mealy machines of sort (2, . . . , 2; 2). The MSO of [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] is the purely relational (term-free) restriction of MSO + . Recall from [24, Prop. 2.6], that for each Mealy machine M : 2 p → 2, there is an MSO-formula δ M (X, x) such that for all n ∈ N and all B ∈ (2 ω ) p , we have

F M (B)(n) = 1 iff δ M ({n}, B) holds.
The axioms of MSO(M) are the arithmetic rules of Fig. 5, the axioms (7) and the following, where M : 2 p → 2 and y, z, X are fresh.

(∀X o )(∀x ι ) x ∈ f M (X) ↔ δ M (x, X) (∃X o )(∀x ι ) (x ∈ X ↔ ϕ) ϕ, 0(z) ϕ[z/x], ϕ ϕ, S(y, z), ϕ[y/x] ϕ[z/x], ϕ ϕ (∀x ι )ϕ, ϕ
The axioms of MSO(M) completely axiomatize its standard model. This extends [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]Thm. 2.11 (via [25])].

Theorem 4 (Completeness of MSO(M)). For closed MSO(M)-formulae ϕ, we have |= ϕ if and only if

MSO(M) ϕ. E(t) t ⊆ u ϕ t ⊆ z, ϕ ϕ E(t), ϕ ϕ, z ⊆ t E(z), z . = t, ϕ ϕ N(t), E(t), ϕ ϕ, N(z), z ⊆ t z ⊆ u, ϕ ϕ t ⊆ u, ϕ N(t), E(t) t ⊆ t t ⊆ u, u ⊆ v t ⊆ v t ⊆ u, u ⊆ t t . = u N(t), u ⊆ t E(u), u . = t S(t, u), 0(u) N(t) t ≤ t t ≤ u, u ≤ v t ≤ v t ≤ u, u ≤ t t . = u S(t, u) t ≤ u 0(t) N(t) ϕ, 0(z) ϕ ϕ ϕ S(u, v), t ≤ v t . = v, t ≤ u t ≤ u N(t) t ≤ u N(u) S(t, u) N(t) ϕ, S(t, z) ϕ ϕ ϕ 0(t), 0(u) t . = u S(t, u), S(t, v) u . = v S(u, t), S(v, t) u . = v S(t, u) N(u)
Fig. 5. The Arithmetic Rules of MSO(M) and LMSO (with terms of sort o and z fresh).

The Logic LMSO

The system LMSO is FS + (LSIP) + (DEXP) + (PEXP) extended with Fig. 5 and

(∀X o )(∀x ι ) x ∈ f M (X) ˛δL M (x, X) ?(∃X o )!(∀x ι ) (x ∈ X ˛δ± ) !ϕ, 0(z) ϕ -[z/x], ?ϕ !ϕ, S(y, z), !ϕ -[y/x] ϕ -[z/x], ?ϕ !ϕ (∀x ι )ϕ -, ?ϕ
Let LMSO(C) := LMSO + (LAC). Note that MSO(M) ϕ whenever LMSO ϕ. Proposition 6 extends so that similarly as in [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF] we have Proposition 8. If MSO(M) ϕ then LMSO ϕ L . In part., for a realizable instance of Church's synthesis (∀x σ )(∃u τ )ϕ(u, x), we have LMSO (∀x σ )(∃u τ )ϕ L (u, x).

Moreover, the soundness of (-) D extends to LMSO. It follows that LMSO(C) is coherent and proves exactly the realizable ∀∃(-) L -statements.

Theorem 5 (Soundness). Let ϕ be closed with ϕ D = (∃u τ )(∀x σ )ϕ D (u, x). From a proof of ϕ in LMSO(C) one can extract an eager term u(x) such that LMSO proves (∀x σ )ϕ D (u(x), x).

Corollary 2 (Extraction). Consider a closed formula

ϕ := (∀x σ )(∃u τ )δ(u, x) with δ deterministic. From a proof of ϕ in LMSO(C) one can extract a term t(x) such that |= (∀x σ ) δ(t(x), x) .

Completeness of LMSO(C)

The completeness of LMSO(C) follows from a couple of important facts. First, LMSO(C) proves the elimination of linear double negation, using (via Thm. 3) the same trick as in [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF].

Lemma 1. For all LMSO-formula ϕ, we have (ϕ

⊥) ⊥ LMSO(C) ϕ.
Combining Lemma 1 with (LAC) gives classical linear choice.

Corollary 3. (∀f )(∃x)ϕ(x, (f )x) LMSO(C) (∃x)(∀y)ϕ(x, y).
The key to the completeness of LMSO(C) is the following quantifier inversion.

Lemma 2. (∀x σ )ϕ(t τ (x), x) LMSO(C) (∃u τ )(∀x σ )ϕ(u, x), where t(x) is eager.

Lemma 2 follows (via Cor. 3) from the fixpoints on eager machines (Prop. 3). Fix an eager t τ (x σ ). Taking the fixpoint of (f )t(x) :

σ × (σ)τ → EM σ (σ)τ gives a term v σ (f (σ)τ ) such that v(f ) . = @(f, t(v(f ))). Then conclude with (∀x σ )ϕ(t(x), x) LMSO ϕ t(v(f )) , v(f ) LMSO ϕ t(v(f )) , @(f, t(v(f ))) LMSO (∃u τ )ϕ u, (f )u LMSO (∀f (σ)τ )(∃u τ )ϕ u, (f )u LMSO(C) (∃u τ )(∀x σ )ϕ(u, x)
Completeness of LMSO(C) then follows via (-) D , Proposition 5, completeness of MSO(M) and Büchi-Landweber Theorem 1. The idea is to lift a f.s. winning

P- strat. in G( ϕ D (u, x) )(u, x) to a realizer of ϕ D = (∃u)(∀x)ϕ D (u, x) in LMSO(C).
Theorem 6 (Completeness of LMSO(C)). For each closed formula ϕ, either

LMSO(C) ϕ or LMSO(C) ϕ ⊥.

Conclusion

We provided a linear Dialectica-like interpretation of LMSO(C), a linear variant of MSO on ω-words based on [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF]. Our interpretation is correct and complete w.r.t. Church's synthesis, in the sense that it proves exactly the realizable ∀∃(-) L -statements. We thus obtain a syntactic extraction procedure with correctness proof internalized in LMSO(C). The system LMSO(C) is moreover complete in the sense that for every closed formula ϕ, it proves either ϕ or its linear negation. While completeness for a linear logic necessarily collapse some linear structure, the corresponding axioms (DEXP) and (PEXP) do respect the structural constraints allowing for realizer extraction from proofs. The completeness of LMSO(C) contrasts with that of the classical system MSO(M), since the latter has provable unrealizable ∀∃-statements. In particular, proof search in LMSO(C) for ∀∃(-) L -formulae and their negation is correct and complete w.r.t.

Church's synthesis. The design of the Dialectica interpretation also clarified the linear structure of LMSO, as it allowed us to decompose it starting from a system based on usual full intuitionistic linear logic (see e.g. [3] for recent references on the subject). An outcome of witness extraction for LMSO(C) is the realization of a simple version of the fan rule (in the usual sense of e.g. [15]). We plan to investigate monotone variants of Dialectica for our setting. Thanks to the compactness of Σ ω , we expect this to allow extraction of uniform bounds, possibly with translations to stronger constructive logics than LMSO.

A Proofs of §2 (Preliminaries)

We decompose Prop. 2 as follows.

Proposition 9 (Prop. 2).

(1) If F : Σ → E Γ is eager and G : Γ → S ∆ is causal then G • F : Σ → E ∆ is eager. (2) If F : Σ → E Γ is eager and G : ∆ → S Σ is causal then F • G : ∆ → E Γ is eager. Proof. Assume that F : Σ → E Γ is induced by f : Σ * → Γ . (a) Assume that G : Γ → S ∆ is induced by g : Γ + → ∆. Then (F •G)(B)(n) = F (G(B))(n) = f (G(B)(0)•. . .•G(B)(n-1)) = f (g(B(0))•. . .•g(B n)) So (F • G)(n) only depends on B(0), . . . , B(n -1). (b) Assume that G : ∆ → S Σ is induced by g : ∆ * → Γ . Then (G•F )(B)(n) = G(F (B))(n) = g(F (B)(0)•. . .•F (B)(n)) = g(f (ε)•. . .•f (B n)) So (G • F )(n) only depends on B(0), . . . , B(n -1).

A.1 Proof of Proposition 3 (Fixpoints for Eager Functions)

We split Proposition 3 into two statments.

Proposition 10. For each F : Σ × Γ → E Σ Γ there is a fix(F ) : Γ → E Σ Γ such that fix(F )(C) = F e(fix(F ))(C) , C) (for all C ∈ Γ ω )
Consider an eager function

F : Σ × Γ -→ E Σ Γ
We are going to define a causal function

fix(F ) : Γ -→ E Σ Γ such that for all C ∈ Γ ω , fix(F )(C) = F e(fix(F ))(C) , C) = F @(fix(F )(C), C) , C) ∈ Σ Γ ω Intuitivelly, fix(F )(C) is the fixpoint of the map B → F (B, C) . Assume first that F is induced by f : n∈N Σ n × Γ n+1 -→ Σ (Σ × Γ ) * -→ Σ Γ
and let us look at how fix(F ) :

Γ -→ M Σ Γ -→ E Σ Γ
can be induced induced by a function h : Γ + → Σ defined from f . We should have

h(b 1 ) = f (ε, b 1 ) = a 1 h(b 1 b 2 ) = f ( f (b 1 , ε), b 1 b 2 ) = f (a 1 , b 1 b 2 ) = a 2 h(b 1 b 2 b 3 ) = f ( f (b 1 , ε) • f ( f (ε, b 1 ), b 1 b 2 ) , b 1 b 2 b 3 ) = f (a 1 a 2 , b 1 b 2 b 3 ) = a 3 . . . h(b 1 . . . b n b n+1 ) = f (a 1 . . . a n , b 1 . . . b n b n+1 ) = a n+1 That is, for n > 0, h(b 1 . . . b n ) = a n
, where the a k 's are given by the recurrence:

a 1 := f (ε, b 1 ) and a k+1 := f (a 1 . . . a k , b 1 . . . b k b k+1 )
In terms of

f : (Σ × Γ ) * -→ Σ Γ such that F (B, C)(n) = f (B n, C n)
this amounts to define

h : Γ * -→ Σ Γ such that fix(F )(C)(n) = h(C n)
as follows:

h(ε) := f (ε) = g 1 ∈ Σ Γ h(b 1 ) := f (a 1 , b 1 ) = g 2 ∈ Σ Γ h(b 1 b 2 ) := f (a 1 a 2 , b 1 b 2 ) = g 3 ∈ Σ Γ . . . h(b 1 . . . b n ) := f (a 1 . . . a n , b 1 . . . b n ) = g n+1 ∈ Σ Γ where a k = g k (b k ), that is a 1 := @(f (ε), b 1 ) and a k+1 := @(f (a 1 . . . a k , b 1 . . . b k ), b k+1 )
This easily gives an eager machine for fix(F ) given an eager machine for F .

Lemma 3. Consider a f.s. eager function

F : Σ × Γ -→ EM Σ Γ
induced by an eager machine

(E : Σ × Γ → Σ Γ ) = (Q, q ı , ∂, λ) Then fix(F ) : Γ -→ EM Σ Γ
is induced by the eager machine

(H : Γ → Σ Γ ) = (Q, q ı , ∂ H , λ)
where

∂ H : Q × Γ -→ Q (q , b) -→ ∂(q , (@(λ(q), b), b))
Proposition 10 will mostly be used in the following context. Consider a Mealy term u(z, y) of sort (ς, σ; τ ) and an eager term t(x, y) of sort (τ, σ; ς). Intuitivelly, the term u(t(x, y), y) is "eager in x", in the sense that it can be seen as an eager Moore function

τ × σ -→ EM τ σ Lemma 4. Given F : Σ × Γ -→ E Θ and G : Θ × Σ × Γ -→ E (∆ Γ ) Θ
there is an eager H : Σ × Γ → E ∆ Γ such that such that for all B ∈ Σ ω and all C ∈ Γ ω , we have

@ H(B, C), C = @ G F (B, C), B, C , F (B, C) , C
Moreover H is finite-state whenever F and G are finite-state.

Proof. Assume that F and G are induced respectivelly by

f : (Σ × Γ ) * -→ Θ g : (Θ × Σ × Γ ) * -→ (∆ Γ ) Θ
Then for all B ∈ Σ ω , all C ∈ Γ ω and all n ∈ N we have

@ G F (B, C), B, C , F (B, C) , C (n) = @ G F (B, C), B, C (n) , F (B, C)(n) , C(n) = @ g F (B, C) n, B n, C n , f (B n, C n) , C(n) Let h : (Σ × Γ ) * → ∆ Γ take (a, b) ∈ (Σ × Γ ) * to b -→ @ g f (ε) • • • f (a, b), a, b , f (a, b) , b ∈ ∆ Γ and let H : Σ × Γ → E ∆ Γ be the eager function induced by h. Then we are done since @(H(B, C), C)(n) = @(h(B n, C n), C(n))
In particular, given F as in Lemma 4 and given G :

Θ × Γ → S ∆, since ΛG : Θ × Γ → E ∆ Γ Θ we obtain H such that @ H(B, C), C = @ ΛG F (B, C), C , F (B, C) , C = G(F (B, C), C) Corollary 4. If G : Θ × Γ → S ∆ is causal and F : Σ × Γ → E Θ is eager, then there is an eager H : Σ × Γ → E ∆ Γ such that for all B ∈ Σ ω and all C ∈ Γ ω , we have @(H(B, C), C) = G(F (B, C), C)
Moreover, H is finite-state whenever so are F and G.

Returning to u(z, y) and t(x, y), consider H defined from G := u and F := t as in Corollary 4. Note that H is finite state since so are u and t . By applying Proposition 10 to In particular, ϕ(a) -→ ψ(a) stands for -→ w.r.t. the system FS without further axioms.

H : Σ × Γ -→ EM Σ Γ we thus obtain a fixpoint of x -→ u(t(x, y), y) since fix(H) : Γ -→ EM Σ Γ
We will prove Theorem 2 with the following inductive invariant. Let Proof. We have

ϕ D (a υ ) = (∃u τ )(∀x σ )ϕ D (u, x, a)
and we have to provide eager terms u(u, x, a) of sort (τ, σ, υ; (τ )υτ ) and

x(u, y, a) of sort (τ, σ, υ; (σ)υστ ) such that ϕ D u , @(x(u, x, a), u, x, a) , a FS+Ax ϕ D @(u(u, x, a), u, a) , x , a

For x(u, x, a), consider the M-projection

[π] : τ × σ × υ -→ M σ
We obtain x(u, x, a) by composising the eager term for

Λ([π]) : τ × σ × υ -→ EM σ τ × σ × υ with the M-iso σ τ × σ × υ (( σ υ ) σ ) τ
For u(u, x, a), we take the eager term obtained by composing the eager function

τ × υ Λ([π]) -→ EM σ τ × υ -→ M ( σ υ ) τ
(where π is a suitable projection) with the Mealy projection

τ × σ × υ -→ M τ × υ
Then we are done since FS proves @(u(u, x, a), u, a) . = σ u and @(x(u, x, a), u, x, a) . = σ x Proposition 11.

ϕ 0 (a) -→ Ax ϕ 1 (a) =⇒ ϕ 1 (a) -→ Ax ϕ 2 (a) =⇒ ϕ 0 (a) -→ Ax ϕ 2 (a)
The proof of Proposition 11 relies on the fixpoints of (finite-state) eager functions given by Proposition 3 (see also §A.1). For legibility reasons, we may refrain from writing free variables of terms explicitely and manipulate explicit substitutions.

In such a case, given a term t(. . . , x, . . . ) with free variable x and a term u of the appropriate sort, we write t[u/x] for the substitution of x by u in t. Let

ϕ D 0 (a υ ) = (∃u τ0 0 )(∀x σ0 0 )(ϕ 0 ) D (u 0 , x 0 , a) ϕ D 1 (a υ ) = (∃u τ1 1 )(∀x σ1 1 )(ϕ 1 ) D (u 1 , x 1 , a) ϕ D 2 (a υ ) = (∃u τ2 2 )(∀x σ2 2 )(ϕ 2 ) D (u 2 , x 2 , a)
By assumption, there are eager terms

u 1 (u 0 , x 1 , a) of sort (τ 0 , σ 1 , υ; (τ 1 )υτ 0 ) x 0 (u 0 , x 1 , a) of sort (τ 0 , σ 1 , υ; (σ 0 )υσ 1 τ 0 ) u 2 (u 1 , x 2 , a) of sort (τ 1 , σ 2 , υ; (τ 2 )υτ 1 ) and x 1 (u 1 , x 2 , a) of sort (τ 1 , σ 2 , υ; (σ 1 )υσ 2 τ 1 ) such that (ϕ 0 ) D u 0 , (x 0 )u 0 x 1 a , a FS+Ax (ϕ 1 ) D (u 1 )u 0 a , x 1 , a and (ϕ 1 ) D u 1 , (x 1 )u 1 x 2 a , a FS+Ax (ϕ 2 ) D (u 2 )u 1 a , x 2 , a
From this data, our goal is to produce eager terms v(u 0 , x 2 , a) of sort (τ 0 , σ 2 , υ; (τ 2 )υτ 0 ) and y(u 0 , x 2 , a) of sort (τ 0 , σ 2 , υ;

(σ 0 )υσ 2 τ 0 ) such that (ϕ 0 ) D u 0 , (y)u 0 x 2 a , a FS+Ax (ϕ 2 ) D (v)u 0 a , x 2 , a
We would like v and y to satisfy the following equations in FS:

(y)u 0 x 2 a . = (x 0 )u 0 x 1 a (v)u 0 a . = (u 2 )u 1 a where u 1 := (u 1 )u 0 a x 1 := (x 1 )u 1 x 2 a
But the variables x σ1 1 and u τ1 1 , which are free in u 1 and x 1 , should not occur in the terms y, v. We are thus lead to solve the following equations in FS

(y)u 0 x 2 a . = (x 0 [y 1 /x 1 ])u 0 y 1 a (v)u 0 a . = (u 2 [v 1 /u 1 ])v 1 a where v 1 . = (u 1 [y 1 /x 1 ])u 0 a y 1 . = (x 1 [v 1 /u 1 ])v 1 x 2 a (11)
with terms y 1 (u 0 , x 2 , a) of sort (τ 0 , σ 2 , υ; σ 1 ) v 1 (u 0 , x 2 , a) of sort (τ 0 , σ 2 , υ; τ 1 ) Assuming ( 11) satisfied, we are done since

(ϕ 0 ) D u 0 , (y)u 0 x 2 a , a FS (ϕ 0 ) D u 0 , (x 0 [y 1 /x 1 ])u 0 y 1 a , a FS+Ax (ϕ 1 ) D (u 1 [y 1 /x 1 ])u 0 a , y 1 , a FS (ϕ 1 ) D v 1 , (x 1 [v 1 /u 1 ])v 1 x 2 a , a FS+Ax (ϕ 2 ) D (u 2 )v 1 a , x 2 , a FS (ϕ 2 ) D (v)u 0 a , x 2 , a
We now turn to the resolution of [START_REF] Filiot | Antichains and compositional algorithms for LTL synthesis[END_REF]. We first discuss the construction of y 1 and v 1 and then turn to y and v.

Definition of y 1 (u 0 , x 2 , a) and v 1 (u 0 , x 2 , a). Note that if y 1 satisfies

FS y 1 . = x 1 [(u 1 [y 1 /x 1 ])u 0 a/u 1 ] (u 1 [y 1 /x 1 ])u 0 a x 2 a ( 12
)
then a by taking v 1 := (u 1 [y 1 /x 1 ])u 0 a one obtains a term satisfying the corresponding equation in [START_REF] Filiot | Antichains and compositional algorithms for LTL synthesis[END_REF]. The Mealy term

t(u, u 0 , x 2 , a) := x 1 [(u)u 0 a/u 1 ] (u)u 0 a x 2 a
induces a finite-state causal function

G : (τ 1 )υτ 0 × τ 0 × σ 2 × υ -→ E σ 1
while the eager term u 1 (u 0 , x 1 , a) induces (via Prop. 9) a f.s. eager function

F : σ 1 × τ 0 × σ 2 × υ -→ EM (τ 1 )υτ 0
By Corollary 4, there is a (f.s.) eager function

H : σ 1 × τ 0 × σ 2 × υ -→ EM σ 1 τ0 × σ2 × υ such that, for all X 1 ∈ σ 1 ω , U 0 ∈ τ 0 ω , X 2 ∈ σ 2 ω and B ∈ υ ω , e(H)(X 1 , U 0 , X 2 , B) = G F (X 1 , U 0 , X 2 , B) , U 0 , X 2 , B
Take the fixpoint fix(H) :

τ 0 × σ 2 × υ -→ EM σ 1 τ0 × σ2 × υ
of H given by Proposition 10. We thus get

fix(H)(U 0 , X 2 , B) = H e(fix(H))(U 0 , X 2 , B) , U 0 , X 2 , B
Note that fix(H) is finite-sate by Lemma 3. Let y 1 be the Mealy term of sort (τ 0 , σ 2 , υ; σ 1 ) for e(fix(H))(-, -, -). It follows that y 1 satisfies (12) since

FS y 1 (u 0 , x 2 , a) . = t u 1 u 0 , y 1 (u 0 , x 2 , a) , a , u 0 , x 2 , a
Definition of y(u 0 , x 2 , a). We have to provide a term y(u 0 , x 2 , a) (τ 0 , σ 2 , υ; (σ 0 )υσ 2 τ 0 ) of sort First, since x 0 is eager it follows from Prop. 9 that the term

x 0 (u 0 , y 1 (u 0 , x 2 , a) , a)
is eager. Let

F 0 := x 0 (u 0 , y 1 (u 0 , x 2 , a) , a) : τ 0 × σ 2 × υ -→ EM (σ 0 )υσ 1 τ 0 and G 0 := (f )u 0 y 1 a : (σ 0 )υσ 1 τ 0 × τ 0 × σ 2 × υ -→ M σ 0
By Corollary 4 there is a finite-state eager function

H 0 : τ 0 × σ 2 × υ -→ EM σ 0 τ0 × σ2 × υ such that for U 0 ∈ τ 0 ω , X 2 ∈ σ 2 ω and B ∈ υ ω , e(H 0 )(U 0 , X 2 , B) = G 0 (F 0 (U 0 , X 2 , B), U 0 , X 2 , B)
Letting y(u 0 , x 2 , a) be the term for e(H 0 ), we thus get

FS (y)u 0 x 2 a . = (x 0 [y 1 /x 1 ])u 0 y 1 a
Definition of v(u 0 , x 2 , a). Our goal is to find a finite-state eager

V : τ 0 × σ 2 × υ -→ EM ( τ 2 υ ) τ0
with term v(u 0 , x 2 , a) such that @(v(u 0 , x 2 , a) , u 0 , a) = @ u 2 v 1 (u 0 , x 2 , a), x 2 , a , v 1 (u 0 , x 2 , a), a

Let Σ := σ 2 , Γ := τ 0 × υ and Θ := τ 1 . We apply Lemma 4 to

F := v 1 (u 0 , x 2 , a) : Σ × Γ -→ EM Θ and G := u 2 (u 1 , x 2 , a) : Θ × Σ × Γ -→ EM (∆ Γ ) Θ
Then we are done since we obtain obtain a finite-state eager

V : Σ × Γ -→ EM ∆ Γ with term v(u 0 , x 2 , a) such that FS @ v(u 0 , x 2 , a), u 0 , a . = @ u 2 v 1 (u 0 , x 2 , a), x 2 , a , v 1 (u 0 , x 2 , a), a
This concludes the proof of Proposition 11.

Monoidal Structure.

Lemma 6.

( The cases of !(ϕ -) and ?(ϕ + ) are easy. The cases of !(ϕ + ) and ?(ϕ -) amount to the corresponding rules in PF and follow by taking terms similar to those of Lemma 5. We only detail some cases. We first consider cases of !(ϕ -) and ?(ϕ + ).

(1) We have

(∀a) !ϕ -(a) - ϕ -(a) D = (∀x 1 )(∀a) !(∀x 0 )ϕ D (-, x 0 , a) - ϕ D (-, x 1 , a)
and the result follows from

ϕ D (-, x 1 , a) ϕ D (-, x 1 , a) (∀x 0 )ϕ D (-, x 0 , a) ϕ D (-, x 1 , a) !(∀x 0 )ϕ D (-, x 0 , a) ϕ D (-, x 1 , a) (2) We have (∀a) !ϕ -(a) - I D = (∀a) !(∀x)ϕ D (-, x, a) - I
and the result follows from the that FS proves !ψ I for all ψ.

(3) We have

(∀a) !ϕ -(a) - !ϕ -(a) ⊗ !ϕ -(a) D = (∀a) !(∀x)ϕ D (-, x, a) - !(∀x)ϕ D (-, x, a) ⊗ !(∀x)ϕ D (-, x, a)
and the result follows from the that FS proves !ψ -!ψ ⊗ !ψ for all ψ.

We now turn to cases of !(ϕ + ) and ?(ϕ -).

(1) We have

(∀a υ ) !ϕ + (a) - ϕ + (a) D = (∃u (τ )υτ 1 )(∀u τ 0 )(∀a υ ) !ϕ D (u 0 , -, a) - ϕ D ((u 1 )u 0 a, -, a)
and we conclude as in Lemma 5, using that FS proves !ψ ψ for all ψ. and we conclude as in Lemma 5, using that FS proves !ψ -!ψ ⊗ !ψ for all ψ.

Lemma 8.

(

γ D , ϕ D ψ D γ D ϕ D ψ D and γ D ϕ D ψ D ϕ D ϕ D ψ D ψ D ϕ D ψ D , ϕ D ψ D γ D , ϕ D ψ D γ D ⊗ ϕ D ψ D
(2) Note that !ϕ is positive and that ?γ is negative, so that Quantifiers.

Lemma 10.

(1) ϕ(a, t(a)) -→ Ax (∃z)ϕ(a, z).

(

) (∀z)ϕ(a, z) -→ Ax ϕ(a, t(a)). Proof. Let ϕ D (a, z) = (∃u τ )(∀x σ )ϕ D (u, x, a, z) 2
We thus have (∃z.ϕ(a, z)) D = (∃u)(∃z)(∀x)ϕ D (u, x, a, z) and (∀z.ϕ(a, z)) D = (∃u (τ )κ )(∀x)(∀z)ϕ D ((u)z, x, a, z)

In both cases we assume a υ , z κ and t(a) to be of sort (υ; κ)

(1) We have to find eager terms u(u, x, a), z(u, x, a) and x(u, x, a) such that ϕ D (u, @(x(u, x, a), u, x, a), a, t(a)) -ϕ D (@(u(u, x, a), u, a), x, a, @(z(u, x, a), a))

We let u and x be given as in Lemma 5. As for z(u, x, a), we take the eager term obtained from the composite

τ × σ × υ [π] -→ M υ Λ(t) -→ EM κ υ
where [π] is a suitable Mealy projection. (2) Note that the variable u now has type (τ )κ. We have to find eager terms u(u, x, a), z(u, x, a) and x(u, x, a) such that ϕ D (u)(@(z(u, x, a), z)), @(x(u, x, a), u, x, a), a, @(z(u, x, a), a)ϕ D (@(u(u, x, a), u, x, a), x, a, t(a))

First, for z(u, x, a), we take as above the eager term obtained from the composite

τ κ × σ × υ [π] -→ M υ Λ(t) -→ EM κ υ
It thus remains to find u and x such that ϕ D @(u, t(a)), @(x(u, x, a), u, x, a), a, t(a)ϕ D (@(u(u, x, a), u, x, a), x, a, t(a))

We then take for x the same term as in Lemma 5. It remains to deal with u. Consider the Mealy term ũ for

τ κ × σ × υ [π] -→ M τ κ × υ @(u,t(a)) -→ M τ
Then we take for u the eager term

τ κ × σ × υ Λ(ũ) -→ EM τ τ κ × σ × υ -→ M (( τ υ ) σ ) τ κ Lemma 11.
( The Equality Axioms [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF]. Realization of the equality axioms [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF], follows from the fact that atomic formulae are interpreted by themselves, so these axioms are interpreted by instances of themselves. This concludes the proof of Theorem 8.

B.2 Realization of Additional Axioms (Proposition 4)

We decompose Proposition 4 as follows.

Lemma 12. The axioms (LSIP) are realized in FS:

(1) (∀a)(ϕ -(a) ⊗ ψ -) -→ (∀a)ϕ -(a) ⊗ ψ - (2) (∀a)(ϕ -(a) `ψ-) -→ (∀a)ϕ -(a) `ψ- (3) (∃a)ϕ -(a) `ψ -→ (∃a)(ϕ -(a) `ψ) (4) ψ - (∃a)ϕ -(a) -→ (∃a)(ψ - ϕ -(a)) (5) ((∀a)ϕ ± (a) ψ ± ) -→ (∃a)(ϕ ± (a) ψ ± ) Proof. Let ϕ D (a) = (∃u)(∀x)ϕ D (u, x, a) and ψ D (a) = (∃v)(∀y)ψ D (v, y, a)
In each case we are done by taking terms similar to those of Lemma 5:

(1) We have

(∀a) ϕ -(a) ⊗ ψ - D = (∀x, y, a) ϕ D (-, x, a) ⊗ ψ D (-, y) (∀a)ϕ -(a) ⊗ ψ - D = (∀a, x, y) ϕ D (-, x, a) ⊗ ψ D (-, y) (2)
(∃a) ϕ -(a) `ψ D = (∃a, v)(∀x, y) ϕ D (-, x, a) `ψD (v, y) (4) We have ψ - (∃a)ϕ -(a) D = (∃a, y)(∀x) ψ D (-, (y)x) ϕ D (-, x, a) (∃a) ψ - ϕ -(a) D = (∃a, y)(∀x) ψ D (-, (y)x) ϕ D (-, x, a) (5) We have (∀a)ϕ ± (a) ψ ± D = (∃a) ϕ D (-, -, a) ψ D (-, -) (∃a) ϕ ± (a) ψ ± D = (∃a) ϕ D (-, -, a) ψ D (-, -)
Lemma 13. The axiom (LAC) is realized in FS: Theorem 3 can be split in two statments, one for polarized formulae and one for all FS-formulae.

(∀a σ )(∃b τ )ϕ(a, b, c) -→ (∃f (τ )σ )(∀a σ )ϕ(a, (f )a, c) Proof. Let ϕ D (a, b, c) = (∃u)(∀x)ϕ D (u, x,
Characterization for The Full System FS. We begin by the full system. We show by induction on formulae that • Case of ϕ ⊗ ψ. We first show

(ϕ ⊗ ψ) D - ϕ D ⊗ ψ D using the axiom (∀a)(ϕ -(a) ⊗ ψ -) - (∀a)ϕ -(a) ⊗ ψ - (∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∀x)ϕ D (u, x) ⊗ (∀y)ψ D (v, y) . . . D (∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∃u)(∀x)ϕ D (u, x) ⊗ (∃v)(∀y)ψ D (v, y) (∃v)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∃u)(∀x)ϕ D (u, x) ⊗ (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∃u)(∀x)ϕ D (u, x) ⊗ (∃v)(∀y)ψ D (v, y) where D is (∀x)ϕ D (u, x) (∀x)ϕ D (u, x) (∀x)ϕ D (u, x) (∃u)(∀x)ϕ D (u, x) (∀y)ψ D (v, y) (∀y)ψ D (v, y) (∀y)ψ D (v, y) (∃v)(∀y)ψ D (v, y) ∀x.ϕ D (u, x), ∀y.ψ D (v, y) ∃u.∀x.ϕ D (u, x) ⊗ ∃v.∀y.ψ D (v, y) ∀x.ϕ D (u, x) ⊗ ∀y.ψ D (v, y) ∃u.∀x.ϕ D (u, x) ⊗ ∃v.∀y.ψ D (v, y)
The other direction is trivial:

ϕ D (u, x), ψ D (v, y) ϕ D (u, x) ⊗ ψ D (v, y) ϕ D (u, x), (∀y)ψ D (v, y) ϕ D (u, x) ⊗ ψ D (v, y) (∀x)ϕ D (u, x), (∀y)ψ D (v, y) ϕ D (u, x) ⊗ ψ D (v, y) (∀x)ϕ D (u, x), (∀y)ψ D (v, y) (∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∀x)ϕ D (u, x), (∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∃u)(∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) (∃u)(∀x)ϕ D (u, x) ⊗ (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) ⊗ ψ D (v, y)) • Case of ϕ `ψ. We first show (ϕ `ψ) D - ϕ D `ψD using axiom (∀a)(ϕ -(a) `ψ-) - (∀a)ϕ -(a) `ψ- (∀xy)(ϕ D (u, x) `ψD (v, y)) (∀x)ϕ D (u, x) `(∀y)ψ D (v, y) . . . D (∀xy)(ϕ D (u, x) `ψD (v, y)) (∀x)ϕ D (u, x), (∀y)ψ D (v, y) (∀xy)(ϕ D (u, x) `ψD (v, y)) (∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∀xy)(ϕ D (u, x) `ψD (v, y)) (∃u)(∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) `ψD (v, y)) (∃u)(∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) `ψD (v, y)) (∃u)(∀x)ϕ D (u, x) `(∃v)(∀y)ψ D (v, y) where D is (∀x)ϕ D (u, x) `(∀y)ψ D (v, y) (∀x)ϕ D (u, x), (∀y)ψ D (v, y) (∀x)ϕ D (u, x) `(∀y)ψ D (v, y) (∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y) (∀x)ϕ D (u, x) `(∀y)ψ D (v, y) (∃u)(∀x)ϕ D (u, x), (∃v)(∀y)ψ D (v, y)
For the converse implication, we use the axiom

(∃a)ϕ -(a) `ψ - (∃a)(ϕ -(a) `ψ) ∃u.∀x.ϕ D (u, x) `∃v.∀y.ψ D (v, y) ∃u.∀x.ϕ D (u, x) `∃v.∀y.ψ D (v, y) . . . D (∃u)(∀x)ϕ D (u, x) `(∃v)(∀y)ψ D (v, y) (∃uv)((∀x)ϕ D (u, x) `(∀y)ψ D (v, y)) . . . D (∃u)(∀x)ϕ D (u, x) `(∃v)(∀y)ψ D (v, y) (∃uv)(∀xy)(ϕ D (u, x) `ψD (v, y))
where D is obtained by proceeding as in

(∀a)ϕ(a) `ψ ϕ(a), ψ (∀a)ϕ(a) `ψ ϕ(a) `ψ (∀a)ϕ(a) `ψ ∀a(ϕ(a) `ψ)
and where D is obtained using the axiom

(∃a)ϕ -(a) `ψ - (∃a)(ϕ -(a) `ψ) • Case of ϕ ψ. We first show (ϕ ψ) D - ϕ D ψ D ϕ D (u, (F )uy) ψ D ((f )u, y), ϕ D (u, (F )uy) ϕ D ((f )u, y) ϕ D (u, (F )uy) ψ D ((f )u, y), (∀x)ϕ D (u, x) ϕ D ((f )u, y) (∀uy) ϕ D (u, (F )uy) ψ D ((f )u, y) , (∀x)ϕ D (u, x) ϕ D ((f )u, y) (∀uy) ϕ D (u, (F )uy) ψ D ((f )u, y) , (∀x)ϕ D (u, x) (∀y)ϕ D ((f )u, y) (∀uy) ϕ D (u, (F )uy) ψ D ((f )u, y) , (∀x)ϕ D (u, x) (∃v)(∀y)ϕ D (v, y) (∃f, F )(∀uy) ϕ D (u, (F )uy) ψ D ((f )u, y) , (∃u)(∀x)ϕ D (u, x) (∃v)(∀y)ϕ D (v, y) (∃f, F )(∀uy) ϕ D (u, (F )uy) ψ D ((f )u, y) (∃u)(∀x)ϕ D (u, x) (∃v)(∀y)ϕ D (v, y)
For the converse direction, we use the axioms (LAC) as well as

* ψ - (∃a)ϕ -(a) - ∃a.(ψ - ϕ -(a)) * ((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± )
We have to show

(∃u)(∀x)ϕ D (u, x) (∃v)(∀y)ψ D (v, y) (∃f, F )(∀uy) ϕ D (u, (F )uy)) ψ D ((f )u, y) Since ϕ(a) (∃a)ϕ(a) ψ ψ (∃a)ϕ(a) ψ, ϕ(a) ψ (∃a)ϕ(a) ψ ϕ(a) ψ (∃a)ϕ(a) ψ (∀a) ϕ(a) ψ and ψ ψ ϕ(a) ϕ(a) (∀a)ϕ(a) ϕ(a) ψ (∀a)ϕ(a), ψ ϕ(a) ψ (∀a)ϕ(a) ψ ϕ(a) ψ (∀a)ϕ(a) (∀a) ψ ϕ(a)
and using the axioms

* ψ - (∃a)ϕ -(a) - ∃a.(ψ - ϕ -(a)) * ((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± ) we derive (∃u)(∀x)ϕ D (u, x) (∃v)(∀y)ψ D (v, y) (∀u)(∃v)(∀y)(∃x) ϕ D (u, x) ψ D (v, y)
We can then conclude with (LAC). -Case of (∃a)ϕ(a). Let We have to show

ϕ D (a) = (∃u)(∀x)ϕ D (u, x
(∃u)(∀x)(∀a)ϕ D ((u)a, x, a) ˛(∀a)ϕ D (a)
The right-to-left implication is given by (LAC) and the left-to-right implication follows from

ϕ D ((u)a, x, a) ϕ D ((u)a, x, a) (∀a)ϕ D ((u)a, x, a) ϕ D ((u)a, x, a) (∀xa)ϕ D ((u)a, x, a) ϕ D ((u)a, x, a) (∀xa)ϕ D ((u)a, x, a) (∀x)ϕ D ((u)a, x, a) (∀xa)ϕ D ((u)a, x, a) (∃u)(∀x)ϕ D (u, x, a) (∃u)(∀xa)ϕ D ((u)a, x, a) (∃u)(∀x)ϕ D (u, x, a) (∃u)(∀xa)ϕ D ((u)a, x, a) (∀a)(∃u)(∀x)ϕ D (u, x, a)
-We finally deal with the exponentials. By induction hypothesis, assume

ϕ(a) ˛(∃u)(∀x)ϕ D (u, x, a)
In each relevant case we show

(!ϕ) D ˛!ϕ D and (?ϕ) D ˛?ϕ D
• Cases of !(ϕ -) and ?(ϕ + ). Both cases are trivial since

(!(ϕ -)) D = !(∀x)ϕ D (-, x, a) = !(ϕ -) D and (?(ϕ + )) D = ?(∃u)ϕ D (u, -, a) = ?(ϕ + ) D
• Cases of !(ϕ + ) and ?(ϕ + ). We have

(!(ϕ + )) D = (∃u)!ϕ D (u, -, a) and (?(ϕ -)) D = (∀x)?ϕ D (-, x, a)
We first have

ϕ D (u, -, a) ϕ D (u, -, a) !ϕ D (u, -, a) ϕ D (u, -, a) !ϕ D (u, -, a) (∃u)ϕ D (u, -, a) !ϕ D (u, -, a) !(∃u)ϕ D (u, -, a) (∃u)!ϕ D (u, -, a) !(∃u)ϕ D (u, -, a)
and

ϕ D (-, x, a) ϕ D (-, x, a) ϕ D (-, x, a) ?ϕ D (-, x, a) (∀x)ϕ D (-, x, a) ?ϕ D (-, x, a) ?(∀x)ϕ D (-, x, a) ?ϕ D (-, x, a) ?(∀x)ϕ D (-, x, a) (∀x)?ϕ D (-, x, a)
For the converse implications, we use the exponential axioms (DEXP):

ϕ D (u, -, a) !ϕ D (u, -, a) ϕ D (u, -, a) (∃u)!ϕ D (u, -, a) (∃u)ϕ D (u, -, a) (∃u)!ϕ D (u, -, a) !(∃u)ϕ D (u, -, a) (∃u)!ϕ D (u, -, a) and ?ϕ D (-, x, a) ϕ D (-, x, a) (∀x)?ϕ D (-, x, a) ϕ D (-, x, a) (∀x)?ϕ D (-, x, a) (∀x)ϕ D (-, x, a) (∀x)?ϕ D (-, x, a) ?(∀x)ϕ D (-, x, a)
Characterization for Polarized Formulae. There are two ways to see characterization for polarized formulae. The first one, stated in Theorem 3,

FS+(LSIP)+(DEXP) ϕ(a) ˛ϕD (a) (ϕ PF-formula)
amounts to the following.

Lemma 15. FS + (LSIP) proves ϕ ˛ϕD , ψ ˛ψD (ϕ ψ) ˛(ϕ ψ) D (ϕ(a) ψ(a) polarized) ϕ(a, b) ˛ϕD (a, b) (∀b.ϕ(a, b)) ˛(∀b.ϕ(a, b)) D ((∀b)ϕ(a, b) negative)
The second one is to notice that characterization for polarized formulae is provable within the polarized fragment PF augmented with the following polarized weakening of (LSIP) (with polarities as displayed):

(∀a)(ϕ ± (a) ⊗ ψ -) - (∀a)ϕ ± (a) ⊗ ψ - (∀a)(ϕ ± (a) `ψ-) - (∀a)ϕ ± (a) `ψ- (∃a)ϕ ± (a) `ψ+ - (∃a)(ϕ ± (a) `ψ+ ) ψ - (∃a)ϕ ± (a) - (∃a)(ψ - ϕ ± (a)) ((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± ) (PLSIP)
We only detail Lemma 15, as it corresponds to the statment of Theorem 3.

Proof of Lemma 15. Consider first the case of ϕ(a) ψ(a). By assumption, for θ either ϕ or ψ, we have

θ + (a) ˛∃u.θ D (u, -, a) θ -(a) ˛∀x.θ D (-, x, a) θ ± (a) ˛θD (-, -, a)
The case of ϕ ± (a)

ψ ± (a) is trivial. The other cases are given by the following derviations (where we did not display the free variable a).

-Case of (ϕ - ψ + ) D . We first show

(ϕ - ψ + ) D - (ϕ -) D (ψ + ) D ϕ D (x) ϕ D (x) (∀x)ϕ D (x) ϕ D (x) ψ D (v) ψ D (v) ψ D (v) (∃v)ψ D (v) ϕ D (x) ψ D (v), (∀x)ϕ D (x) (∃v)ψ D (v) ϕ D (x) ψ D (v) (∀x)ϕ D (x) (∃v)ψ D (v) (∃v, x) ϕ D (x) ψ D (v) (∀x)ϕ D (x) (∃v)ψ D (v)
For the converse implication, we use the axioms

• ψ - (∃a)ϕ ± (a) - (∃a)(ψ - ϕ ± (a)) • ((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± ) D D (∃v, x) ϕ D (x) ψ D (v) (∃v, x) ϕ D (x) ψ D (v) (∃v) (∀x)ϕ D (x) ψ D (v) (∃v, x) ϕ D (x) ψ D (v) (∀x)ϕ D (x) (∃v)ψ D (v) (∃v, x) ϕ D (x) ψ D (v)
where D is obtained from the axiom

((∀a)ϕ ± (a) ψ ± ) - (∃a)(ϕ ± (a) ψ ± )
and D is obtained from the axiom

ψ - (∃a)ϕ ± (a) - (∃a)(ψ - ϕ ± (a)) -Case of (ϕ + ψ -) D . We first show (ϕ + ψ -) D - (ϕ + ) D (ψ -) D ϕ D (u) ϕ D (u) ψ D (y) ψ D (y) ϕ D (u) ψ D (y), ϕ D (u) ψ D (y) (∀y, u) ϕ D (u) ψ D (y) , ϕ D (u) ψ D (y) (∀y, u) ϕ D (u) ψ D (y) , (∃u)ϕ D (u) (∀y)ψ D (y) (∀y, u) ϕ D (x) ψ D (u) (∃u)ϕ D (u) (∀y)ψ D (y)
The converse direction is given by

ϕ D (u) ϕ D (u) ϕ D (u) (∃u)ϕ D (u) ψ D (y) ψ D (y) (∀y)ψ D (y) ψ D (y) (∃u)ϕ D (u) (∀y)ψ D (y), ϕ D (u) ψ D (y) (∃u)ϕ D (u) (∀y)ψ D (y) ϕ D (u) ψ D (y) (∃u)ϕ D (u) (∀y)ψ D (y) (∀u, y) ϕ D (u) ψ D (y)
Consider now the case of (∀a)ϕ -(a). Let

ϕ D (a) = (∀x)ϕ D (-, x, a)
and by assumption ϕ D (a) ˛ϕ(a)

We have to show

(∀x)(∀a)ϕ D (-, x, a) ˛(∀a)ϕ D (a)
But this is trivial since for negative ϕ -, we have (∀a.ϕ(a)) D = (∀a)ϕ D (a) by definition.

B.4 Extraction (Corollary 1)

Let recall the statment of Corollary 1

Corollary 5 (Extraction (Cor. 1)). Consider a closed formula ϕ := (∀x σ )(∃u τ )δ(u, x) with δ deterministic. From a proof of ϕ in FS + (LAC) + (LSIP) + (DEXP) one can extract a term t(x) such that |= (∀x σ ) δ(t(x), x) .

Proof. Note that

ϕ D = (∃f (τ )σ )(∀x σ )δ D (-, -, (f )x, x )
By Theorem 2 (Thm. 8) and Proposition 4 (Lem. 12 & 13), from a proof of ϕ in FS + (LAC) + (LSIP) + (DEXP) we get an eager term u (τ )σ (x σ ) such that

FS+(DEXP) δ D (-, -, e(u)(x), x )
Since δ deterministic, we have

δ D (a) = δ D (-, -, a)
and from Characterization for polarized formulae (Theorem 3) we get

FS+(DEXP)+(PEXP)
δ(e(u)(x), x)

We thus obtain

|= (∀x σ ) δ (t(x), x) (where t τ (x) := e(u)(x))
B.5 Proofs of §3.4 (Translations of Classical Logic)

While the usual (-)

T and (-) Q translations target resp. negative and positive formulae [9] (see also [16]), one can consider the following deterministic variants:

T ± := ?I ⊥ T ± := ?⊥ (t . = u) T ± := ?(t . = u) (ϕ → ψ) T ± := ?(!ϕ T ± ψ T ± ) (ϕ ∧ ψ) T ± := ?(!ϕ T ± ⊗ !ψ T ± ) (ϕ ∨ ψ) T ± := ?(ϕ T ± `ψT ± ) (∃x.ϕ) T ± := ?(∃x)!ϕ T ± (∀x.ϕ) T ± := ?!(∀x)ϕ T ±
and

Q± := !I ⊥ Q± := !⊥ (t . = u) Q± := !(t . = u) (ϕ → ψ) Q± := !(ϕ Q± ?ψ Q± ) (ϕ ∧ ψ) Q± := !(ϕ Q± ⊗ ψ Q± ) (ϕ ∨ ψ) Q± := !(?ϕ Q± `?ψ Q± ) (∃x.ϕ) Q± := !?(∃x)ϕ Q± (∀x.ϕ) Q± := !(∀x)?ϕ Q±
Soundness (Proposition 6). The soundness of (-) T ± and (-) Q± proceeds as that of (-)

T and (-) Q . We then easily deduce the soundness of (-) L .

Proposition Proof. The proof goes on as in the case of (-)

T and (-) Q . We obtain sequents provable in FS because both translations produce sequents of the form !(-) ?(-), so that the right and ∀ rules of FS ϕ, !ϕ ψ, ?ψ ϕ !ϕ ψ, ?ψ ϕ ϕ, ?ψ ϕ (∀z)ϕ, ?ψ can be used for the right → and ∀ rules of classical logic

ϕ, ϕ ψ, ψ ϕ ϕ ψ, ψ ϕ ϕ, ψ ϕ (∀z)ϕ, ψ
We only detail the cases which differs from [16]. As usual we write ϕ T ± = ?ϕ T ± and ϕ Q± = ?ϕ Q± -Case of the (-) T ± translation of the rule

ϕ, ϕ 0 , ϕ 1 ψ ϕ, ϕ 0 ∧ ϕ 1 ψ
The result follows from . . . !?ϕ T ± , !?(ϕ 0 ) T ± , !?(ϕ 1 ) T ± ?ψ T ± !?ϕ T ± , !?(ϕ 0 ) T ± ⊗ !?(ϕ 1 ) T ± ?ψ T ± !?ϕ T ± , ?(!?(ϕ 0 ) T ± ⊗ !?(ϕ 1 ) T ± ) ?ψ T ± !?ϕ T ± , !?(!?(ϕ 0 ) T ± ⊗ !?(ϕ 1 ) T ± ) ?ψ T ± -Case of the (-) T ± translation of the rule ϕ ϕ, ϕ ψ ψ, ψ ϕ, ψ ϕ ∧ ψ, ϕ , ψ The result follows from . . .

!?ϕ T ± ?ϕ T ± , ?ϕ T ± !?ϕ T ± !?ϕ T ± , ?ϕ T ± . . . !?ψ T ± ?ψ T ± , ?ψ T ± !?ψ T ± !?ψ T ± , ?ψ T ± !?ϕ T ± , !?ψ T ± !?ϕ T ± ⊗ !?ψ T ± , ?ϕ T ± , ?ψ T ± !?ϕ T ± , !?ψ T ± ?(!?ϕ T ± ⊗ !?ψ T ± ), ?ϕ T ± , ?ψ T ± -Case of the (-)
T ± translation of the rule ϕ, ϕ[t/x] ψ ϕ, (∀x)ϕ ψ The result follows by cutting ?ϕ T ± ?ϕ T ± (∀x)?ϕ T ± ?ϕ T ± !(∀x)?ϕ T ± ?ϕ T ± ?!(∀x)?ϕ T ± ?ϕ T ± !?!(∀x)?ϕ T ± ?ϕ T ± !?!(∀x)?ϕ T ± !?ϕ T ± !?!(∀x)?ϕ T ± (∀x)!?ϕ T ± !?!(∀x)?ϕ T ± ?(∀x)!?ϕ T ± !?!(∀x)?ϕ T ± !?(∀x)!?ϕ T ± with . . . !?ϕ T ± , !?ϕ T ± [t/x] ?ψ T ± !?ϕ T ± , (∀x)!?ϕ T ± ?ψ T ± !?ϕ T ± , ?(∀x)!?ϕ T ± ?ψ T ± !?ϕ T ± , !?(∀x)!?ϕ T ± ?ψ T ± -Case of the (-) T ± translation of the rule ϕ ϕ, ψ ϕ (∀z)ϕ, ψ

The result follows from . . . !?ϕ T ± ?ϕ T ± , ?ψ T ± !?ϕ T ± (∀z)?ϕ T ± , ?ψ T ± !?ϕ T ± !(∀z)?ϕ T ± , ?ψ T ± !?ϕ T ± ?!(∀z)?ϕ T ± , ?ψ Proof. It remains to deal with the equality axioms [START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF]. But they follow from the fact that α L = α for each atomic formula α ∈ At.

Proof of Proposition 5. We now turn to Prop. 5, namely the equivalence of (DEXP) + (PEXP) with

?ϕ + ˛ ϕ + L δ ± ˛ δ ± L !ψ -˛ ψ -L
First, notice that So we can as well prove Proposition 5 with (-) T ± instead of (-) L . We split this into two statments.

I T ± = ?I ⊥ T ± = ?⊥ (t . = u) T ± = ?(t . = u) ϕ ψ T ± = ?(! ϕ T ± ψ T ± ) ϕ ⊗ ψ T ± = ?(! ϕ T ± ⊗ ! ψ T ± ) ϕ `ψ T ± = ?( ϕ T ± ` ψ T ± ) !ϕ T ± = ϕ T ± ?ϕ T ± = ϕ T ± ∃x.ϕ T ± = ?(∃x)! ϕ T ± ∀x.ϕ T ± = ?!(∀x) ϕ T ± I Q± = !I ⊥ Q± = !⊥ (t . = u) Q± = !(t . = u) ϕ ψ Q± = !( ϕ Q± ? ψ Q± ) ϕ ⊗ ψ Q± = !( ϕ Q± ⊗ ψ Q± ) ϕ `ψ Q± = !(? ϕ Q± `? ψ Q± ) !ϕ Q± =
Lemma 17. FS augmented with the axioms

?ϕ + ˛ ϕ + T ± δ ± ˛ δ ± T ± !ψ -˛ ψ -T ±
(for formulae ϕ + , ψ -, δ ± with the displayed equalities), proves all instances of (DEXP) and (PEXP).

Proof. We show that FS augmented with the axioms 7) ?(ϕ + ) ⊗ ?(ψ + ) ?(ϕ + ⊗ ψ + ). ( 8) !(ϕ -⊗ ψ -) !(ϕ -) ⊗ !(ψ -). ( 9) ?(ϕ + ) `?(ψ + ) ?(ϕ + `ψ+ ). ( 10) !(ϕ -`ψ-) !(ϕ -) `!(ψ -).

?ϕ + ˛ ϕ + T ± δ ± ˛ δ ± T ± !ψ -˛ ψ -T ± proves (1) δ ± !δ ± . (2) ?δ ± δ ± . (3) ?(ϕ + ) ?!(ϕ + ). (4) !?(ψ -) !(ψ -). (5) (!(ϕ -) ?(ψ + )) ?(ϕ - ψ + ). (6) (?(ϕ + ) !(ψ -)) !(ϕ + ψ -). (
(1) We have !δ T ± = δ T ± and we obtain the result by following the chain of implications δ ± δ ± T ± = !δ ± T ± !δ ± (2) Similar.

(3) We have !ϕ T ± = ϕ T ± and we obtain the result by following the chain of implications

?(ϕ + ) ϕ + T ± = (!ϕ) + T ± ?(!ϕ) + (4) Similar.
(5) We have

!(ϕ -) ˛ ϕ -T ± ?(ψ + ) ˛ ψ + T ± and ?(ϕ - ψ + ) ˛ ϕ - ψ + T ±
Using the ! and ?-properties of determinisitic formulae, it follows that we have the following chain of implications:

(!(ϕ -) ?(ψ + )) ( ϕ -T ± ψ + T ± ) ?(! ϕ -T ± ψ + T ± ) = ϕ - ψ + T ± ?(ϕ - ψ + ) (6) Similar. ( 7
)
We have

?(ϕ + ) ˛ ϕ + T ± ?(ψ + ) ˛ ψ + T ± and ?(ϕ + ⊗ψ + ) ˛ ϕ + ⊗ ψ + T ±
Using the ! and ?-properties of determinisitic formulae, it follows that we have the following chain of implications:

(?(ϕ + ) ⊗ ?(ψ + )) ( ϕ + T ± ⊗ ψ + T ± ) ?(! ϕ + T ± ⊗ ! ψ + T ± ) = ϕ + ⊗ ψ + T ± ?(ϕ + ⊗ ψ + ) (8) Similar.
(9) We have ?(ϕ + ) ˛ ϕ + T ± ?(ψ + ) ˛ ψ + T ± and ?(ϕ + `ψ+ ) ˛ ϕ + `ψ+ T ± Using the ?-property of determinisitic formulae, it follows that we have the following chain of implications:

(?(ϕ + ) `?(ψ + )) ( ϕ + T ± ` ψ + T ± ) ?( ϕ + T ± ` ψ + T ± ) = ϕ + `ψ+ T ± ?(ϕ + `ψ+ ) (10) Similar.
Lemma 18. The equivalences

?ϕ + ˛ ϕ + T ± δ ± ˛ δ ± T ± !ψ -˛ ψ -T ±
(where ϕ + , δ ± and ψ -have the displayed polarities) are provable in FS + (DEXP) + (PEXP).

Proof. First note that using the ! and ?-axioms on deterministic formulae, for a deterministic δ ± , the equivalence

δ ˛ δ T ±
follows from the series of equivalences

δ + T ± ˛?(δ + ) ˛δ± ˛!(δ -) ˛ δ -T ± Conversely, the equivalence δ ˛ δ T ± entails ?(δ + ) ˛ δ + T ± and !(δ -) ˛ δ -T ±
We proceed by simulateneous induction on formulae.

-Case of ϕ and atomic formula α. Since α T ± = ?α, we have to show ?α + ˛?α and !α -˛?α and we are done by the ! and ?-axioms on deterministic formulae. -Case of (ϕ - ψ + ) + . We have

ϕ ψ T ± = ?(! ϕ T ± ψ T ± )
so that we have to show

?(ϕ - ψ + ) ˛?(! ϕ T ± ψ T ± )
By induction hypothesis we have !(ϕ -) ˛ ϕ -T ± and ?(ψ

+ ) ˛ ψ + T ±
We are thus left with showing ?(ϕ - ψ + ) ˛?(!!(ϕ -) ?(ψ + ))

The left-to-right implication follows from

ϕ -ϕ - ψ + ψ + ϕ - ψ + , ϕ -ψ + ϕ - ψ + , !(ϕ -) ψ + ϕ - ψ + , !!(ϕ -) ψ + ϕ - ψ + , !!(ϕ -) ?(ψ + ) ϕ - ψ + !!(ϕ -) ?(ψ + ) ϕ - ψ + ?(!!(ϕ -) ?(ψ + )) ?(ϕ - ψ + ) ?(!!(ϕ -) ?(ψ + ))
The right-to-left implication follows from the ?/ -axiom for positive implications:

!(ϕ -) !(ϕ -) !(ϕ -) !!(ϕ -) ?(ψ + ) ?(ψ + ) !!(ϕ -) ?(ψ + ), !(ϕ -) ?(ψ + ) !!(ϕ -) ?(ψ + ) !(ϕ -) ?(ψ + ) !(ϕ -) ?(ψ + ) ?(ϕ - ψ + ) !!(ϕ -) ?(ψ + ) ?(ϕ - ψ + ) ?(!!(ϕ -) ?(ψ + )) ?(ϕ - ψ + ) -Case of (ϕ + ψ -) -. We have ϕ ψ T ± = ?(! ϕ T ± ψ T ± )
so that we have to show

!(ϕ + ψ -) ˛?(! ϕ T ± ψ T ± )
By induction hypothesis we have

?(ϕ + ) ˛ ϕ + T ± and !(ψ -) ˛ ψ -T ±
We are thus left with showing

!(ϕ + ψ -) ˛?(!?(ϕ + ) !(ψ -))
The left-to-right implication follows from the !-axiom for deterministic formulae. We cut

ϕ + ϕ + ϕ + ?(ϕ + ) ψ -ψ - !(ψ -) ψ - ?(ϕ + ) !(ψ -), ϕ + ψ - ?(ϕ + ) !(ψ -) ϕ + ψ - !(?(ϕ + ) !(ψ -)) ϕ + ψ - !(?(ϕ + ) !(ψ -)) !(ϕ + ψ -) ?(ϕ + ) !(ψ -) !(?(ϕ + ) !(ψ -)) ?(ϕ + ) !(ψ -) !(ϕ + ψ -) with ?(ϕ + ) !?(ϕ + ) !(ψ -) !(ψ -) !?(ϕ + ) !(ψ -), ?(ϕ + ) !(ψ -) !?(ϕ + ) !(ψ -) ?(ϕ + ) !(ψ -) ?(ϕ + ) !(ψ -) !(ϕ + ψ -) !?(ϕ + ) !(ψ -) !(ϕ + ψ -) ?(!?(ϕ + ) !(ψ -)) !(ϕ + ψ -)
The right-to-left implication follows from the !/ -axiom for negative implications:

!(ϕ + ψ -) ?(ϕ + ) !(ψ -) ?(ϕ + ) ?(ϕ + ) !(ψ -) !(ψ -) ?(ϕ + ) !(ψ -), ?(ϕ + ) !(ψ -) ?(ϕ + ) !(ψ -), !?(ϕ + ) !(ψ -) ?(ϕ + ) !(ψ -) !?(ϕ + ) !(ψ -) !(ϕ + ψ -) ?(!?(ϕ + ) !(ψ -)) -Case of ϕ + ⊗ ψ + . We have ϕ ⊗ ψ T ± = ?(! ϕ T ± ⊗ ! ψ T ± )
so that we have to show

?(ϕ + ⊗ ψ + ) ˛?(! ϕ + T ± ⊗ ! ψ + T ± )
The induction hypothesis gives ?(ϕ + ) ˛ ϕ + T ± and ?(ψ

+ ) ˛ ψ + T ±
We are thus left with showing ?(ϕ + ⊗ ψ + ) ˛?(!?(ϕ + ) ⊗ !?(ψ + ))

The left-to-right implication follows from the !-axiom on deterministic formulae:

ϕ + ϕ + ϕ + ?(ϕ + ) ?(ϕ + ) !?(ϕ + ) ϕ + !?(ϕ + ) ψ + ψ + ψ + ?(ψ + ) ?(ψ + ) !?(ψ + ) ψ + !?(ψ + ) ϕ + , ψ + !?(ϕ + ) ⊗ !?(ψ + ) ϕ + , ψ + ?(!?(ϕ + ) ⊗ !?(ψ + )) ϕ + ⊗ ψ + ?(!?(ϕ + ) ⊗ !?(ψ + )) ?(ϕ + ⊗ ψ + ) ?(!?(ϕ + ) ⊗ !?(ψ + ))
The right-to-left implication follows from the ?/⊗-axiom for positive formulae: ?(ϕ + ), ?(ψ + ) ?(ϕ + ⊗ ψ + ) !?(ϕ + ), !?(ψ + ) ?(ϕ

+ ⊗ ψ + ) !?(ϕ + ) ⊗ !?(ψ + ) ?(ϕ + ⊗ ψ + ) ?(!?(ϕ + ) ⊗ !?(ψ + )) ?(ϕ + ⊗ ψ + ) -Case of ϕ -⊗ ψ -. We have ϕ ⊗ ψ T ± = ?(! ϕ T ± ⊗ ! ψ T ± )
so that we have to show

!(ϕ -⊗ ψ -) ˛?(! ϕ -T ± ⊗ ! ψ -T ± )
The induction hypothesis gives

!(ϕ -) ˛ ϕ -T ± and !(ψ -) ˛ ψ -T ±
We are thus left with showing

!(ϕ -⊗ ψ -) ˛!(!!(ϕ -) ⊗ !!(ψ -))
The left-to-right implication follows from the !/⊗-axiom for negative formulae:

!(ϕ -⊗ ψ -) !(ϕ -) ⊗ !(ψ -) !(ϕ -) !(ϕ -) !(ϕ -) !!(ϕ -) !(ψ -) !(ψ -) !(ψ -) !!(ψ -) !(ϕ -), !(ψ -) !!(ϕ -) ⊗ !!(ψ -) !(ϕ -) ⊗ !(ψ -) !!(ϕ -) ⊗ !!(ψ -) !(ϕ -⊗ ψ -) !!(ϕ -) ⊗ !!(ψ -) !(ϕ -⊗ ψ -) !(!!(ϕ -) ⊗ !!(ψ -))
The right-to-left implication is given as follows:

ϕ -ϕ - !(ϕ -) ϕ - !!(ϕ -) ϕ - ψ -ψ - !(ψ -) ψ - !!(ψ -) ψ - !!(ϕ -), !!(ψ -) ϕ -⊗ ψ - !!(ϕ -) ⊗ !!(ψ -) ϕ -⊗ ψ - !(!!(ϕ -) ⊗ !!(ψ -)) ϕ -⊗ ψ - !(!!(ϕ -) ⊗ !!(ψ -)) !(ϕ -⊗ ψ -) -Case of ϕ + `ψ+ . We have ϕ `ψ T ± = ?( ϕ T ± ` ψ T ± )
so that we have to show

?(ϕ + `ψ+ ) ˛?( ϕ + T ± ` ψ + T ± )
The induction hypothesis gives ?(ϕ + ) ˛ ϕ + T ± and ?(ψ

+ ) ˛ ψ + T ±
We are thus left with showing ?(ϕ + `ψ+ ) ˛?(?(ϕ + ) `?(ψ + ))

The left-to-right implication is given by

ϕ + ϕ + ϕ + ?(ϕ + ) ψ + ψ + ψ + ?(ψ + )
ϕ + `ψ+ ?(ϕ + ), ?(ψ + ) ϕ + `ψ+ ?(ϕ + ) `?(ψ + ) ϕ + `ψ+ ?(?(ϕ + ) `?(ψ + ))

?(ϕ + `ψ+ ) ?(?(ϕ + ) `?(ψ + ))

The right-to-left implication follows from the ?/`-axiom on positive formulae: ?(ϕ + ) `?(ψ + ) ?(ϕ + `ψ+ ) ?(?(ϕ + ) `?(ψ + )) ?(ϕ + `ψ+ )

-Case of ϕ -`ψ-. We have ϕ `ψ T ± = ?( ϕ T ± ` ψ T ± ) so that we have to show !(ϕ -`ψ-) ˛?( ϕ -T ± ` ψ -T ± )
The induction hypothesis gives

!(ϕ -) ˛ ϕ -T ± and !(ψ -) ˛ ψ -T ±
We are thus left with showing !(ϕ -`ψ-) ˛?(!(ϕ -) `!(ψ -))

The left-to-right implication follows from the !/`-axiom for negative formulae:

!(ϕ -`ψ-) !(ϕ -) `!(ψ -) !(ϕ -`ψ-) ?(!(ϕ -) `!(ψ -
)) The right-to-left implication follows form the ! and ?-axioms on deterministic formulae:

?(!(ϕ -) `!(ψ -)) !(ϕ -) `!(ψ -) ϕ -ϕ - !(ϕ -) ϕ - ψ -ψ - !(ψ -) ψ - !(ϕ -) `!(ψ -) ϕ -, ψ - !(ϕ -) `!(ψ -) ϕ -`ψ- ϕ -`ψ-!(ϕ -`ψ-) !(ϕ -) `!(ψ -) !(ϕ -`ψ-) ?(!(ϕ -) `!(ψ -)) !(ϕ -`ψ-) -Case of (!(ϕ + )) + . Since !ϕ T ± = ϕ T ± we have to show ?!ϕ ˛ ϕ T ±
We have ϕ + T ± ˛?(ϕ + ) by induction hypothesis. We are thus left with ?!(ϕ + ) ˛?(ϕ + ) and the result follows from the !-axiom on positive formulae.

-Case of (!(ϕ -)) ± . Since !ϕ T ± = ϕ T ± we have to show !ϕ ˛ ϕ T ±
We have ϕ -T ± ˛!(ϕ -) by induction hypothesis. We are thus left with !ϕ ˛!ϕ and we are done. -Case of (?(ϕ -)) -. Since ?ϕ T ± = ϕ T ± we have to show

!?ϕ ˛ ϕ T ±
We have ϕ -T ± ˛!(ϕ -) by induction hypothesis. We are thus left with showing !?ϕ ˛!ϕ and the result follows from the ?-axiom on negative formulae.

-Case of (?(ϕ + )) ± . Since ?ϕ

T ± = ϕ T ± we have to show ?ϕ ˛ ϕ T ±
We have ϕ + T ± ˛?(ϕ + ) by induction hypothesis. We are thus left with ?ϕ ˛?ϕ and we are done. -Case of ((∃x)ϕ) + . Since (∃x)ϕ

T ± = ?(∃x)! ϕ T ± we have to show ?(∃x)ϕ ˛?(∃x)! ϕ T ±
The induction hypothesis gives

?(ϕ + ) ˛ ϕ + T ±
and it follows from the !-axioms on deterministic formulae that we have the sequence of equivalences ?(∃x)! ϕ T ± ˛?(∃x) ϕ T ± ˛?(∃x)?ϕ

We are thus left with showing ?(∃x)ϕ ˛?(∃x)?ϕ and the result follows from ϕ ϕ ϕ (∃x)ϕ ϕ ?(∃x)ϕ ?ϕ ?(∃x)ϕ (∃x)?ϕ ?(∃x)ϕ ?(∃x)?ϕ ?(∃x)ϕ and ϕ ϕ ϕ ?ϕ ϕ (∃x)?ϕ ϕ ?(∃x)?ϕ (∃x)ϕ ?(∃x)?ϕ ?(∃x)ϕ ?(∃x)?ϕ

-Case of ((∀x)ϕ) -. Since (∀x)ϕ T ± = ?!(∀x) ϕ T ± we have to show !(∀x)ϕ ˛?!(∀x) ϕ T ±
The induction hypothesis gives

!(ϕ -) ˛ ϕ -T ±
and it follows from the ?-axioms on deterministic formulae that we have the sequence of equivalences

?!(∀x) ϕ T ± ˛!(∀x) ϕ T ± ˛!(∀x)!ϕ
We are thus left with showing !(∀x)ϕ ˛!(∀x)!ϕ and the result follows from

ϕ ϕ (∀x)ϕ ϕ !(∀x)ϕ ϕ !(∀x)ϕ !ϕ !(∀x)ϕ (∀x)!ϕ !(∀x)ϕ !(∀x)!ϕ and ϕ ϕ !ϕ ϕ (∀x)!ϕ ϕ !(∀x)!ϕ ϕ !(∀x)!ϕ (∀x)ϕ !(∀x)!ϕ !(∀x)ϕ
Proof of Proposition 7 (Extraction from FS + (DEXP) + (PEXP)). We first show that FS + (LSIP) + (DEXP) + (PEXP) realises all instances of (PEXP). (1) ?

(ϕ + ) - ?!(ϕ + ) (2) !?(ψ -) - !(ψ -) (3) !(ϕ -) ?(ψ + ) - ?(ϕ - ψ + ) (4) ?(ϕ + ) !(ψ -) - !(ϕ + ψ -) (5) ?(ϕ + ) ⊗ ?(ψ + ) - ?(ϕ + ⊗ ψ + ) (6) !(ϕ -⊗ ψ -) - !(ϕ -) ⊗ !(ψ -) (7) ?(ϕ + ) `?(ψ + ) - ?(ϕ + `ψ+ ) (8) !(ϕ -`ψ-) - !(ϕ -) `!(ψ -) Proof. Let ϕ D = (∃u)(∀x)ϕ D and ψ D = (∃v)(∀y)ψ D (v, y) (1)
We have to show

?(∃u)ϕ D (u, -) - ?(∃u)!ϕ D (u, -)
This follows from (DEXP):

ϕ D (u) !ϕ D (u) ϕ D (u) (∃u)!ϕ D (u) ϕ D (u) (∃u)!ϕ D (u) ϕ D (u) ?(∃u)!ϕ D (u) (∃u)ϕ D (u) ?(∃u)!ϕ D (u) ?(∃u)ϕ D (u) ?(∃u)!ϕ D (u)
(∀x)ϕ D (-, x) ?(∃v)ψ D (v, -) - ?(∃v)(∃x) ϕ D (-, x) ψ D (v, -) With (LSIP) we have (∀x)ϕ D (x) (∃v)ψ D (v) (∃v)(∃x) ϕ D (x) ψ D (v)
and we conclude with (PEXP). Proof. The result directly follows from Proposition 6 (Cor. 6) and the fact that LMSO proves the (-) L translation of all the axioms of MSO(M). They are dealt with exactly as in [START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF].

-The arithmetic rules of Fig. 5 follow from the fact that α L = α for each atomic formula α ∈ At. -The induction scheme of LMSO requires one hypothesis to be under an exponential modality !(-) to accomodate arbitrary negative formulae; the situation is resolved by cutting with the LMSO axiom enabling to remove exponentials over deterministic formulae. By the induction hypothesis (and since (-) L commutes over substitution), we have proofs of

(∀X o )(∀x ι ) x ∈ f M (X) ←→ δ M (x, X)
Clearly, it is equivalent to the following scheme where we make the universal quantification implicit by using formulae with free variables

N(x) → x ∈ f M (X) ←→ δ M (x, X)
which translate to the following, which is then clearly derivable from the corresonding scheme in LMSO by instantiating the universal quantifiers by the free variables

N(x)

x ∈ f M (X) ˛δM (x, X) L Proposition 14. Given a realizable instance of Church's synthesis (∀x σ )(∃u τ )ϕ(u, x), we have LMSO (∀x σ )(∃u τ )ϕ L (u, x).

Proof. Assume that there is a Mealy term u τ (x σ ) such that |= (∀x σ )ϕ(u(x), x)

It then follows from the completeness of MSO(M) (Theorem 4) that MSO(M) (∀x σ )ϕ(u(x), x) so that Proposition 8 (Proposition 13) gives LMSO !(∀x σ )ϕ L (u(x), x)

We then easily derive LMSO ϕ L (u(x), x) whence the result.

Theorem 10 (Soundness of (-) D (Theorem 5)). Let ϕ be closed with ϕ D = (∃u τ )(∀x σ )ϕ D (u, x). From a proof of ϕ in LMSO(C) one can extract an eager term u(x) such that LMSO proves (∀x σ )ϕ D (u(x), x).

Proof. The result follows from the soundness of (-) D in FS + (LAC) + (LSIP) + (DEXP) + (PEXP) given by Theorem 2 (Thm. 8), Proposition 4 (Lem. 12 & 13) and Lemma 19, and the fact that the axioms of LMSO are realized.

-For the arithmetic rules of Fig. 5, this follow from the fact that atomic formulae are interpreted by themselves, so these axioms are interpreted by instances of themselves. -For comprehension, this follows from the fact that the axiom is a deterministic formula, so its realizers are trivial, and the fact that each instance is interpreted by an instance of the axiom. -For the axiom giving definition definitions of Mealy machines, since atomic formulae are interpreted by themselves and since (-) L -formulae are deterministic, each instance is interpreted by a formula of the form

x ∈ f M (X) ˛(δ L M ) D (x, X)
The result then follows from Characterization (Theorem 3). -Consider now induction: !ϕ, 0(z) ϕ -[z/x], ?ϕ !ϕ, S(y, z), !ϕ -[y/x] ϕ -[z/x], ?ϕ !ϕ (∀x ι )ϕ -, ?ϕ First, note that the conlusion is of the form (-) + (-) -, so no realizers have to be provided and we just have to show that the axiom is interpreted by in instance of itself. Now, (-) D takes !-formulae to !-formulae and ?-formulae to ?-formulae. So we are left with showing that from a proof of

Fig. 1 .

 1 Fig. 1. A Mealy machine (left) and an equivalent eager (Moore) machine (right).

  extends MSO with ∃x τ and ∀x τ ranging over S[1, τ ] τ ω and with sorted equalities t τ . = u τ interpreted as equality over S[1, τ ] τ ω . Write |= ϕ when ϕ holds in this model, called the standard model. The full definition of MSO(M) is deferred to §4.1.

Fig. 2 .

 2 Fig. 2. Deduction for MF (where z τ is fresh).

Fig. 3 .

 3 Fig. 3. The Dialectica Interpretation of MF (where types are leaved implicit).

Example 5 .

 5 Polarized contraction ϕ + -ϕ + ⊗ ϕ + and ψ -`ψ--ψ -(ϕ + positive, ψ -negative) gives realizers of all instances of itself. Indeed, with say ϕ D (a) = (∃u)ϕ D (u, -, a) and ψ D (a) = (∀y)ψ D (-, y, a), Λ(π 1 ) (for π 1 a M-projection on suitable types) gives eager terms U(u, a) and Y(y, a) such that ϕ D (u, -, a) -ϕ D e(U)(u, a), -, a ⊗ ϕ D e(U)(u, a), -, a and ψ D -, e(Y)(y, a), a `ψD -, e(Y)(y, a), a -ψ D (-, y, a)

Fig. 4 .

 4 Fig. 4. Exponential rules of PF.

Proposition 4 .

 4 The axioms (LAC) and (LSIP) are realized in FS. The axioms (DEXP) are realized in FS + (DEXP).

Proposition 7 .

 7 in many-sorted classical logic with equality then FS + (DEXP) proves ϕ L . The axioms (PEXP) are realized in FS + (LSIP) + (DEXP) + (PEXP). Corollary 1 thus extends to FS + (LAC) + (LSIP) + (DEXP) + (PEXP).

B. 1 Notation 7 .

 17 is such that u t e(fix(H))(C), C , C = e(H)(e(fix(H))(C), C) = e(fix(H))(C) B Proofs of §3 (A Monadic Linear Dialectica-like Interpretation) Soundness of Dialectica (Theorem 2) Consider formulae ϕ(a) and ψ(a) with free variable a υ and let ϕ D (a) = (∃u τ )(∀x σ )ϕ D (u, x, a) and ψ D (a) = (∃v κ )(∀y ς )ψ D (v, y, a) We write ϕ(a) -→ Ax ψ(a) if there are eager terms v(u, y, a) of sort (τ, ς, υ; (κ)υτ ) and x(u, y, a) of sort (τ, ς, υ; (σ)υςτ ) such that ϕ D u , @(x(u, y, a), u, y, a) , a FS+Ax ψ D @(v(u, y, a), u, a) , y , a

⊗Theorem 8 .

 8 1≤i≤0 ϕ i (a) := I and `1≤j≤0 ψ j (a) := ⊥ Assume given ϕ(a) = ϕ 1 (a), . . . , ϕ n (a) and ψ(a) = ψ 1 (a), . . . , ψ m (a) with free variables among a. The we have ϕ 1 (a), . . . , ϕ n (a) FS+Ax ψ 1 (a), . . . , ψ m (a) =⇒ ⊗ i ϕ i (a) -→ Ax `j ψ j (a) Remark 1. Note that ϕ(a) -→ Ax ψ(a) ⇐⇒ ϕ (a) -→ Ax ψ (a) whenever (∀a) ϕ(a) -ψ(a) D = (∀a) ϕ (a) -ψ (a) D We first list some (expected) structure of -→ Ax and then give the proof of Theorem 8. Basic Structure. Lemma 5. ϕ(a) -→ Ax ϕ(a).

  ) If ϕ(a) -→ Ax ϕ (a) and ψ(a) -→ Ax ψ (a), then ϕ(a) ⊗ ψ(a) -→ Ax ϕ (a) ⊗ ψ (a). (2) If ϕ(a) -→ Ax ϕ (a) and ψ(a) -→ Ax ψ (a), then ϕ(a) `ψ(a) -→ Ax ϕ (a) ψ (a). (3) ϕ(a) ⊗ ψ(a) -→ Ax ψ(a) ⊗ ϕ(a). (4) ϕ(a) `ψ(a) -→ Ax ψ(a) `ϕ(a). (5) ϕ(a) ⊗ I -→ Ax ϕ(a). (6) ϕ(a) -→ Ax ⊥ `ϕ(a). (7) (ϕ(a) `ψ(a)) ⊗ γ(a) -→ Ax ϕ(a) `(ψ(a) ⊗ γ(a)) Exponential Structure. Lemma 7. (1) !ϕ(a) -→ Ax ϕ(a). (2) !ϕ(a) -→ Ax I. (3) !ϕ(a) -→ Ax !ϕ(a) ⊗ !ϕ(a).

( 4 )

 4 ϕ(a) -→ Ax ?ϕ(a).(5) ⊥ -→ Ax ?ϕ(a). (6) ?ϕ(a) `?ϕ(a) -→ Ax ?ϕ(a).Proof. Letϕ D (a υ ) = (∃u τ )(∀x σ )ϕ D (u, x, a)

( 2 )

 2 We have (∀a) !ϕ + (a) -I D = (∀u)(∀a) !ϕ D (u, -, a) -I and we conclude from the fact that FS proves !ψ I for all ψ. (3) We have (∀a) !ϕ + (a) -!ϕ + (a) ⊗ !ϕ + (a) D = (∃u 1 )(∃u 2 )(∀u 0 )(∀a) !ϕ D (u 0 , -, a) -!ϕ D ((u 1 )u 0 a, -, a)⊗!ϕ D ((u 2 )u 0 a, -, a)

( 1 )( 2 )( 1 )

 121 ) If !γ(a) -→ Ax ϕ(a) `?ψ(a) then !γ(a) -→ Ax !ϕ(a) `?ψ(a).(2) If !γ(a) ⊗ ϕ(a) -→ Ax ?ψ(a) then !γ(a) ⊗ ?ϕ(a) -→ Ax ?ψ(a).Proof. First, note that !γ(a) is positive and that ?ψ(a) is negative. We thus have(!γ) D (a) = (∃w)(!γ) D (w, -,a) and (?ψ) D (a) = (∀y)(?ψ) D (-, y, a) where (!γ) D (resp. (?ψ) D ) is an !-formula (resp. a ?-formula). Consider first the case of ϕ negative. We have (!ϕ) D (a) = (!ϕ) D (-, -, a) = !(∀x)ϕ D (-, x, a) By assumption, FS + Ax proves (!γ) D (w, -, a) ϕ D (-, x, a) `(?ψ) D (-, y, a) and the result follows from (!γ) D (w, -, a) ϕ D (-, x, a), (?ψ) D (-, y, a) (!γ) D (w, -, a) (∀x)ϕ D (-, x, a), (?ψ) D (-, y, a) (!γ) D (w, -, a) !(∀x)ϕ D (-, x, a), (?ψ) D (-, y, a)Consider now the case of ϕ positive. We have(!ϕ) D (a) = (∃u)(!ϕ) D (u, -, a) = (∃u)!ϕ D (u, -, a)By assumption there is an eager term u(w, y, a) such that (!γ) D (w, -, a) FS+Ax ϕ D (@(u(w, y, a), w, a), -, a) `(?ψ) D (-, y, a) and the result follows from (!γ) D (w, -, a) ϕ D (@(u(w, y, a), w, a), -, a), (?ψ) D (-, y, a) (!γ) D (w, -, a) !ϕ D (@(u(w, y, a), w, a), -, a), (?ψ) D (-, y, a) Consider first the case of ϕ positive. We have (?ϕ) D (a) = (?ϕ) D (-, -, a) = ?(∃u)ϕ D (u, -, a) By assumption, FS + Ax proves (!γ) D (w, -, a) ⊗ ϕ D (u, -, a) (?ψ) D (-, y, a) and the result follows from (!γ) D (w, -, a), ϕ D (u, -, a) (?ψ) D (-, y, a) (!γ) D (w, -, a), (∃u)ϕ D (u, -, a) (?ψ) D (-, y, a) (!γ) D (w, -, a), ?(∃u)ϕ D (u, -, a) (?ψ) D (-, y, a) Consider now the case of ϕ negative. We have (?ϕ) D (a) = (∀x)(?ϕ) D (-, x, a) = (∀x)?ϕ D (-, x, a) By assumption there is an eager term u(w, y, a) such that (!γ) D (w, -, a) ⊗ ϕ D (-, @(x(w, y, a), w, y, a), a) FS+Ax (?ψ) D (-, y, a) and the result follows from (!γ) D (w, -, a), ϕ D (-, @(x(w, y, a), w, y, a), a) (?ψ) D (-, y, a) (!γ) D (w, -, a), ?ϕ D (-, @(x(w, y, a), w, y, a), a) (?ψ) D (-, y, a) We have γ(a) ⊗ ϕ(a) -→ Ax ψ(a) if and only if γ(a) -→ Ax ϕ(a) ψ(a). (2) If γ(a) ⊗ !ϕ(a) -→ Ax ψ(a) `?γ (a) then γ(a) -→ Ax (!ϕ(a) ψ(a)) `?γ (a). Proof. Let ϕ D (a) = (∃u)(∀x)ϕ D (u, x, a) ψ D (a) = (∃v)(∀y)ψ D (v, y, a) γ D (a) = (∃w)(∀z)γ D (w, z, a) , x)(∀u, y) ϕ D u, (x)uy, a ψ D (v)u, y, a First, note that (∀a) γ ⊗ ϕ -ψ D = (∃v, z, x)(∀w, u, y, a) γ D w, (z)wuya, a ⊗ϕ D u, (x)wuya, a -ψ D (v)wua, x, z)(∀w, u, y, a) γ D w, (z)wuya, a -ϕ D u, (x)uywa, a ψ D (v)uwa, y, a So both formulae have the same realizers modulo (Σ Γ ) ∆ M (Σ ∆ ) Γ . The result then follows from

(

  !ϕ) D (a) = (∃u)(!ϕ) D (u, -, a) and (?γ ) D (a) = (∀z )(?γ ) D (-, z , a) where (!ϕ) D (resp. (?γ ) D ) is an !-formula (resp. a ?-formula). We have ψ(a) `?γ (a) D = (∃v)(∀y, z ) ψ D (v, y, a) `(?γ ) D (-, z , a) and !ϕ(a) ψ(a) D = (∃v)(∀u, y) (!ϕ) D (u, -, a) ψ D ((v)u, y, a) It follows that γ(a)⊗!ϕ(a) -→ Ax ψ(a)`?γ (a) =⇒ γ(a) -→ Ax (!ϕ(a) ψ(a))`?γ (a) since γ(a) ⊗ !ϕ(a) -ψ(a) `?γ (a) D = (∃v, z)(∀w, u, y, z ) γ D (w, (z)wuyz , a)⊗(!ϕ) D (u, -, a) -ψ D ((v)wu, y, a)`(?γ ) D (-, z , a) and γ(a) -!ϕ(a) ψ(a) `?γ (a) D = (∃v, z)(∀w, u, y, z ) γ D (w, (z)wuyz , a) -(!ϕ) D (u, -, a) ψ D ((v)wu, y, a) `(?γ ) D (-, z , a)

( 2 )

 2 ) If γ(a) ⊗ ϕ(a, b) -→ Ax ψ(a), then γ(a) ⊗ (∃b)ϕ(a, b) -→ Ax ψ(a). (2) If γ(a) -→ Ax ϕ(a, b) `?ψ(a), then γ(a) -→ Ax (∀b)ϕ(a, b) `?ψ(a). Proof. Let γ D (a) = (∃w)(∀z)γ D (w, z, a) and ϕ D (a, b) = (∃u)(∀x)ϕ D (u, x, a, b) (1) Let ψ D (a, b) = (∃v)(∀y)ψ D (v, y, a, b) We have γ(a) ⊗ ϕ(a, b) D = (∃w, u)(∀z, x) γ D (w, z, a) ⊗ ϕ D (u, x, a, b) and γ(a) ⊗ (∃b)ϕ(a, b) D = (∃w, u, b)(∀z, x) γ D (w, z, a) ⊗ ϕ D (u, x, a, b) It follows that γ(a) ⊗ ϕ(a, b) -ψ(a) D = (∃v, z, x)(∀w, u, y) γ D (w, (z)wuy, a)⊗ϕ D (u, (x)wuy, a, b) -ψ D ((v)wu, y, a) and γ(a) ⊗ (∃b)ϕ(a, b) -ψ(a) D = (∃v, z, x)(∀w, u, b, y) γ D (w, (z)wuby, a)⊗ϕ D (u, (x)wuby, a, b) -ψ D ((v)wub, y, a) We thus obtain γ(a) -→ Ax ϕ(a, b) `?ψ(a) ⇐⇒ γ(a) -→ Ax (∀b)ϕ(a, b) `?ψ(a) since (∀a, b) γ(a) ⊗ ϕ(a, b) -ψ(a) D = (∃v, z, x)(∀w, u, y, b, a) γ D (w, (z)wuyba, a)⊗ϕ D (u, (x)wuyba, a, b) -ψ D ((v)wuba, y, a) and (∀a) γ(a) ⊗ (∃b)ϕ(a, b) -ψ(a) D = (∃v, z, x)(∀w, u, b, y, a) γ D (w, (z)wubya, a)⊗ϕ D (u, (x)wubya, a, b) -ψ D ((v)wuba, y, a) Note that ?ψ is negative. We thus have (?ψ) D (a) = (∀y)(?ψ) D (-, y, a) where (?ψ) D is a ?-formula. Moreover, (∀b.ϕ(a, b)) D = (∃u)(∀x, b)ϕ D ((u)b, x, a, b) We have ϕ(a, b) `?ψ(a) D = (∃u)(∀x, y) ϕ D (u, x, a, b) `(?ψ) D (-, y, a) and (∀b)ϕ(a, b) `?ψ(a) D = (∃u)(∀x, b, y) ϕ D ((u)b, x, a, b) `(?ψ) D (-, y, a) It follows that γ(a) -ϕ(a, b) `ψ(a) D = (∃u, z)(∀w, x, y) γ D (w, (z)wxy, a) -ϕ D ((u)w, x, a, b) `ψD (-, y, a) and γ(a) -(∀b)ϕ(a, b) `ψ(a) D = (∃u, z)(∀w, x, b, y) γ D (w, (z)wxby, a) -ϕ D ((u)bw, x, a, b)`ψ D (-, y, a) We thus obtain γ(a) -→ Ax ϕ(a, b) `?ψ(a) ⇐⇒ γ(a) -→ Ax (∀b)ϕ(a, b) `?ψ(a) since (∀a, b) γ(a) -ϕ(a, b) `ψ(a) D = (∃u, z)(∀w, x, y, b, a) γ D (w, (z)wxyba, a) -ϕ D ((u)wba, x, a, b)`ψ D (-, y, a) and (∀a) γ(a) -(∀b)ϕ(a, b) `ψ(a) D = (∃u, z)(∀w, x, b, y, a) γ D (w, (z)wxbya, a) -ϕ D ((u)bwa, x, a, b)`ψ D (-, y, a)

Proof of Theorem 8 .---

 8 Assume given ϕ(a) = ϕ 1 (a), . . . , ϕ n (a) and ψ(a) = ψ 1 (a), . . . , ψ m (a) with free variables among a. We show ϕ 1 (a), . . . , ϕ n (a) FS+Ax ψ 1 (a), . . . , ψ m (a) =⇒ ⊗ i ϕ i (a) -→ Ax `j ψ j (a) with, as expected, ⊗ 1≤i≤0 ϕ i (a) = I and `1≤j≤0 ψ j (a) = ⊥ We reason by induction on derivations. -The cases of ϕ ϕ ϕ, ϕ, ψ, ψ ϕ ϕ, ψ, ϕ, ψ ϕ ϕ ϕ , ϕ, ψ, ψ ϕ ϕ , ψ, ϕ, ψ directly follow from Lemmas 5 and 6. -Case of ϕ γ, ϕ ψ, γ ψ ϕ, ψ ϕ , ψ We show that if ϕ(a) -→ Ax γ(a) `ϕ (a) and ψ(a) ⊗ γ(a) -→ Ax ψ (a) then ϕ(a) ⊗ ψ(a) -→ Ax ϕ (a) `ψ (a) Proof. Assuming ϕ(a) -→ Ax γ(a) `ϕ (a), Lemma 6 gives ϕ(a) ⊗ ψ(a) -→ Ax (γ(a) `ϕ (a)) ⊗ ψ(a) from which Lemma 6 together with Proposition 11 implies ϕ(a) ⊗ ψ(a) -→ Ax ϕ (a) `(ψ(a) ⊗ γ(a)) Since ψ(a) ⊗ γ(a) -→ Ax ψ (a), Lemma 6 together with Proposition 11 give the result. The cases of ϕ, ϕ 0 , ϕ 1 ϕ ϕ, ϕ 0 ⊗ ϕ 1 ϕ ϕ ϕ 0 , ϕ 1 , ϕ ϕ ϕ 0 `ϕ1 , ϕ are tautological. -Case of ϕ ϕ, ϕ ψ ψ, ψ ϕ, ψ ϕ ⊗ ψ, ϕ , ψ We show that if ϕ(a) -→ Ax γ 0 (a) `ϕ (a) and ψ(a) -→ Ax γ 1 (a) `ψ (a) then ϕ(a) ⊗ ψ(a) -→ Ax (γ 0 (a) ⊗ γ 1 (a)) `ϕ (a) `ψ (a) Proof. By Lemma 6, we have ϕ(a) ⊗ ψ(a) -→ Ax γ 0 (a) `ϕ (a) ⊗ γ 1 (a) `ψ (a) from which we deduce by Lemma 6 and Proposition 11 ϕ(a) ⊗ ψ(a) -→ Ax γ 0 (a) ⊗ (γ 1 (a) `ψ (a)) `ϕ (a) and then ϕ(a) ⊗ ψ(a) -→ Ax (γ 0 (a) ⊗ γ 1 (a)) `ψ (a) `ϕ (a) -Case of ϕ, ϕ ϕ ψ, ψ ψ ϕ, ψ, ϕ `ψ ϕ , ψ We show that if ϕ(a) ⊗ γ 0 (a) -→ Ax ϕ (a) and ψ(a) ⊗ γ 1 (a) -→ Ax ψ (a) then ϕ(a) ⊗ ψ(a) ⊗ (γ 0 (a) `γ1 (a)) -→ Ax ϕ (a) `ψ (a) Proof. By Lemma 6 we have ϕ(a) ⊗ γ 0 (a) ` ψ(a) ⊗ γ 1 (a) -→ Ax ϕ (a) `ψ (a) On the other hand, by Lemma 6 we have ϕ(a) ⊗ ψ(a) ⊗ (γ 0 (a) `γ1 (a)) -→ Ax (ϕ(a) ⊗ γ 0 ) `γ1 (a) ⊗ ψ(a) so that Lemma 6 together with Proposition 11 give ϕ(a) ⊗ ψ(a) ⊗ (γ 0 (a) `γ1 (a)) -→ Ax (ϕ(a) ⊗ γ 0 ) `(γ 1 (a) ⊗ ψ(a)) and we conclude by Propsition 11. Lemma 7 (together with Lemma 6 and Proposition 11) handles the rules: Lemma 8 handles the rules !ϕ ϕ, ?ψ !ϕ !ϕ, ?ψ !ϕ, ϕ ?ψ !ϕ, ?ϕ ?ψ -The rules ϕ ϕ[t/x], ϕ ϕ (∃x)ϕ, ϕ ϕ, ϕ[t/x] ϕ ϕ, (∀x)ϕ ϕ follow from Lemma 10 (together with Lemma 6 and Proposition 11). -The cases of ϕ, ϕ ϕ ϕ, (∃z)ϕ ϕ ϕ ϕ, ?ψ ϕ (∀z)ϕ, ?ψ are tautological (Lemma 11). -Lemma 9 handles the rules ϕWe are left with showing γ(a) -→ Ax ϕ(a) ψ(a) and γ (a) -→ Ax ϕ(a) imply γ⊗γ -→ Ax ψ(a) Proof. Assume γ(a) -→ Ax ϕ(a) ψ(a) and γ (a) -→ Ax ϕ(a). Lemma 9 gives γ(a) ⊗ ϕ(a) -→ Ax ψ(a) while Lemma 6 gives γ(a) ⊗ γ (a) -→ Ax γ(a) ⊗ ϕ(a) and we conclude by Proposition 11.

  We have (∀a) ϕ -(a) `ψ-D = (∀x, y, a) ϕ D (-, x, a) `ψD (-, y) (∀a)ϕ -(a) `ψ-D = (∀a, x, y) ϕ D (-, x, a) `ψD (-, y) (3) We have (∃a)ϕ -(a) `ψ D = (∃a, v)(∀x, y) ϕ D (-, x, a) `ψD (v, y)

  a, b, c ) We thus have (∀c)(∀a)(∃b)ϕ(a, b, c) D = (∃b, u)(∀x, a, c)ϕ D ((u)ac, x, a, (b)ac, c ) and (∀c)(∃f )(∀a)ϕ(a, (f )a, c) D = (∃f, u)(∀x, a, c)ϕ D ((u)ac, x, a, (f )ac, c ) Hence we are done by taking terms similar to those of Lemma 5. Lemma 14. The axioms (DEXP) are realized in Ax + (DEXP), in the sense that for all deterministic δ we have δ -→ (DEXP) !δ and ?δ -→ (DEXP) δ Proof. If δ(a) is deterministic, then δ D (a) = δ D (-, -, a) with δ D deterministic. It follows that the axioms reduce to themselves: δ D (-, -, a) FS+(DEXP) !δ D (-, -, a) and ?δ D (-, -, a) FS+(DEXP) δ D (-, -, a) B.3 The Characterization Theorem (Theorem 3)

FS+-

  (LAC)+(LSIP)+(DEXP) ϕ(a) ˛ϕD (a) If ϕ is atomic, then the result is trivial since ϕ D = ϕ. -Consider the case of ϕ(a) ψ(a) with is either ⊗, `or . By induction hypothesis, we have ϕ(a) ˛(∃u)(∀x)ϕ D (u, x, a) ψ(a) ˛(∃v)(∀y)ψ D (v, y, a) and in each case we are left with showing (ϕ(a) ψ(a)) D ˛ϕD (a) ψ D (a)

  , a) and by induction hypothesis assume ϕ D (a) ˛ϕ(a) Hence we are done if we show (∃a.ϕ(a)) D ˛(∃a)ϕ D (a) But this is trivial since (∃a.ϕ(a)) D = (∃a)ϕ D (a) by definition. -Case of (∀a)ϕ(a). Let ϕ D (a) = (∃u)(∀x)ϕ D (u, x, a) and by induction hypothesis assume ϕ D (a) ˛ϕ(a)

  DEXP) follows from the equivalence δ L ˛δ (δ deterministic)

Lemma 19 .

 19 The axioms (PEXP) are realized in FS+(LSIP)+(DEXP)+(PEXP):

( 2 )

 2 We have to show !(∀y)?ψ D (-, y) -!(∀y)ψ D This follows from (DEXP): ?ψ D (y) ψ D (y) (∀y)?ψ D (y) ψ D (y) !(∀y)?ψ D (y) ψ D (y) !(∀y)?ψ D (y) (∀y)ψ D (y) !(∀y)?ψ D (y) !(∀y)ψ D (y) (3) We have to show !

( 4 )

 4 We have to show ?(∃u)ϕ D (u, -) !(∀y)ψ D (-, x) -!(∀u)(∀y) ϕ D (u, -) ψ D (-, y) First, with (PEXP) we have ?(∃u)ϕ D (u, -) !(∀y)ψ D (-, x) -! (∃u)ϕ D (u, -) (∀y)ψ D (-, y) We the conclude from (∃u)ϕ D (u, -) (∀y)ψ D (-, y) -(∀u)(∀y) ϕ D (u, -) ψ D (-, y) (see the case of (-) D (-) D -(--) D in the proof of Theorem 3, §B.3.) (5) We have to show?(∃u)ϕ D (u, -) ⊗ ?(∃v)ψ D (v, -) -?(∃u, v) ϕ D (u, -) ⊗ ψ D (v, -)First, with (PEXP) we have?(∃u)ϕ D (u, -) ⊗ ?(∃v)ψ D (v, -) -? (∃u)ϕ D (u, -) ⊗ (∃v)ψ D (v, -)We then conclude as follows:ϕ D (u), ψ D (v) ϕ D (u) ⊗ ψ D (v) ϕ D (u), ψ D (v) ∃u, v. ϕ D (u) ⊗ ψ D (v) (∃u)ϕ D (u), (∃v)ψ D (v) ∃u, v. ϕ D (u) ⊗ ψ D (v) (∃u)ϕ D (u) ⊗ (∃v)ψ D (v) ∃u, v. ϕ D (u) ⊗ ψ D (v) (6) We have to show !(∀x, y) ϕ D (-, x) ⊗ ψ D (-, y) -!(∀x)ϕ D (-, x) ⊗ !(∀y)ψ D (-, y)First, by (LSIP) we have(∀x, y) ϕ D (-, x) ⊗ ψ D (-, y) -(∀x)ϕ D (-, x) ⊗ (∀y)ψ D (-, y)and we conclude with (PEXP).[START_REF] Büchi | Solving Sequential Conditions by Finite-State Strategies[END_REF] We have to show?(∃u)ϕ D (u, -) `?(∃v)ψ D (v, -) -?(∃u, v) ϕ D (u, -) `ψD (v, -)First, by (PEXP) we have?(∃u)ϕ D (u, -) `?(∃v)ψ D (v, -) -? (∃u)ϕ D (u, -) `(∃v)ψ D (v, -)and we conclude with (LSIP). (8) We have to show!(∀x, y) ϕ D (-, x) `ψD (-, y) -!(∀x)ϕ D (-, x) `!(∀y)ψ D (-, y)First, by (LSIP) we have(∀x, y) ϕ D (-, x) `ψD (-, y) -(∀x)ϕ D (-, x) `(∀y)ψ D (-, y)and we conclude with (PEXP).The corresponding extension of Corollary 1 (Cor. 5) is the following. The proof is exactly that of Cor. 5, but invoking Lemma 19 in addition to Theorem 2 (Thm. 8) and Proposition 4 (Lem. 12 & 13). Corollary 7. Consider a closed formula ϕ := (∀x σ )(∃u τ )δ(u, x) with δ deterministic. From a proof of ϕ in FS + (LAC) + (LSIP) + (DEXP) + (PEXP) one can extract a term t(x) such that |= (∀x σ ) δ(t(x), x) . C Proofs of §4 (Completeness) C.1 Completeness of MSO(M) (Theorem 4) Thanks to the equational theory of MSO(M), we reduce Theorem. 4 to the completeness of MSO + [24, Thm. 2.11]: Theorem 9 (Completeness of MSO + ). For each closed formula ϕ of MSO + , |= ϕ ⇐⇒ MSO + ϕ First, recall that Proposition 1 implies that MSO(M) proves (3

(where σ i = 2

 2 mi ) and such that 1≤i≤nx σi . = x o i,1 , . . . , x o i,ni MSO(M )(ω)ϕ ←→ ϕ Theorem 4 then follows from Theorem 9.C.2 Proof of §4.2 (The Logic LMSO)We split Proposition 8 into two statments.Proposition 13. If MSO(M) ϕ then LMSO ϕ L .

ϕL-

  L , 0(z) ϕ L [z/x], ψ L and ϕ L , S(y, z), ϕ L [y/x] ϕ L [z/x], ψ L Using (DEXP) we thus derive !ϕ L , 0(z) ϕ L [z/x], ?ψ L and !ϕ L , S(y, z), !ϕ L [y/x] ϕ L [z/x], ?ψ L from which the induction scheme of LMSO gives !ϕ L (∀x ι )ϕ L , ?ψ L and we directly get !ϕ L !(∀x ι )ϕ L , ?ψ The translation of each instance of the comprehension scheme of MSO(M) is an instance of the comprehension scheme of LMSO. -The axiom scheme defining terms in MSO(M) is as follows

(

  !ϕ) D , S(y, z), (!ϕ -) D [y/x] ϕ D (-, x, z)(?ϕ D ) D one can get a proof of (!ϕ) D , S(y, z), !ϕ D (-, x, [y/z]) ϕ D (-, x, z)(?ϕ D ) D But this is trivial since(!ϕ -) D (a) = !(∀x)ϕ D (-, x, a) -!ϕ D (-, x, a) C.3 Proofs of §4.3 (Completeness of LMSO(C))Lemma 20 (Lem. 1). For each LMSO-formula ϕ, we have(ϕ(a) ⊥) ⊥ LMSO(C) ϕ(a)Lemma 20 relies on a combinatorial property already used in[START_REF] Pradic | LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic[END_REF].Lemma 21. Let P and O be sets such that O may be well-ordered. Then the following is true∀F ∈ P O P .∃p ∈ P.∀o ∈ O.∃f ∈ O P . [F (f ) = p and f (p) = o]Proof. Fix F ∈ P O P . The negation of our statement is equivalent to∀p ∈ P.∃o ∈ O.¬ ∃f ∈ O P . [F (f ) = p ∧ f (p) = o]Using an instance of choice available thanks to the fact that O may be wellordered, this is in turn equivalent to∃õ ∈ O P .∀p ∈ P.¬ ∃f ∈ O P . [F (f ) = p ∧ f (p) = õ(p)]It follows that we only need to prove∀F ∈ P O P .∀õ ∈ O P .∃p ∈ P.∃f ∈ O P . [F (f ) = p and f (p) = õ(p)]But this is now easy: given F ∈ P O P and õ ∈ O P , we can take f := õ and p := F (õ) to conclude.In particular, given alphabets Σ and Γ , there are functionsu : (Γ )((Σ)Γ ) -→ Γ and g : (Γ )((Σ)Γ ) × Σ -→ (Σ)Γsuch that for all F : (Σ)Γ → Γ and all x ∈ Σ, @(F , g(F, x)) = u(F ) and @(g(F, x) , u(F )) = xWe can now prove Lemma 20. Recall that LMSO Thanks to the Characterization Theorem 3, we are done if we show ψ D (a) LMSO(C) ϕ D (a) Assume ϕ D (a) = (∃u τ )(∀x σ )ϕ D (u, x, a) We thus have (ϕ(a) ⊥) D = (∃g (σ)τ )(∀u τ ) ϕ D (u, (g)u, a)

  σ1×

  [START_REF] Finkbeiner | Synthesis of Reactive Systems[END_REF]. If many-sorted first-order logic proves a sequent ϕ 1 , . . . , ϕ n ψ 1 , . . . , ψ m

	then
		!ϕ 1	T ± , . . . , !ϕ n	T ±	FS	ψ 1	T ± , . . . , ψ m	T ±
	and	ϕ 1	Q± , . . . , ϕ n	Q±	FS	?ψ 1	Q± , . . . , ?ψ m	Q±

  Q± , !ψ Q± ?!ψ Q± !ψ Q± , ?!ψ Q± ?!ψ Q± !ϕ Q± , !ψ Q± , ?!ϕ Q± `?!ψ Q± ?!ϕ Q± , ?!ψ Q± !ϕ Q± , !ψ Q± , !(?!ϕ Q± `?!ψ Q± ) ?!ϕ Q± , ?!ψ Q±

	The result follows from Corollary 6 (Prop. 6). If many-sorted first-order logic proves a sequent
			. . . ϕ 1 , . . . , ϕ n ψ 1 , . . . , ψ m
	then		!ϕ Q± , !ϕ Q± ?!ψ Q±
		!ϕ Q± , (∃z)!ϕ Q± ?!ψ Q± 1 , . . . , ϕ L ϕ L n FS+(DEXP) ψ L 1 , . . . , ψ L m
			!ϕ Q± , ?(∃z)!ϕ Q± ?!ψ Q±
			!ϕ Q± , !?(∃z)!ϕ Q± ?!ψ Q±
	-Case of the (-)	Q± translation of the rule
			ϕ ϕ[t/x], ψ ϕ (∃x)ϕ, ψ	T ±
	-Case of the (-)	Q± translation of the rule
	The result follows by cutting
			ϕ, ϕ ϕ	ψ, ψ ψ
			ϕ, ψ, ϕ ∨ ψ ϕ , ψ !ϕ Q± !ϕ Q±
			!ϕ Q± (∃x)!ϕ Q±
	The result follows from	!ϕ Q± !(∃x)!ϕ Q±
	. . . !ϕ Q± , !ϕ Q± ?!ϕ Q± !ϕ Q± , ?!ϕ Q± ?!ϕ Q± !ϕ Q± !?(∃x)!ϕ Q± !ϕ Q± ?!?(∃x)!ϕ Q± ?!ϕ Q± ?!?(∃x)!ϕ Q± (∃x)?!ϕ Q± ?!?(∃x)!ϕ Q± !(∃x)?!ϕ Q± ?!?(∃x)!ϕ Q± ?!(∃x)?!ϕ Q± ?!?(∃x)!ϕ Q± . . . !ψ -Case of the (-) with Q± translation of the rule . . .
			ϕ ϕ 0 , ϕ 1 , ϕ !ϕ Q± ?!ϕ Q± [t/x], ?!ψ Q± ϕ ϕ 0 ∨ ϕ 1 , ϕ !ϕ Q± (∃x)?!ϕ Q± , ?!ψ Q±
	The result follows from	!ϕ Q± !(∃x)?!ϕ Q± , ?!ψ Q±
			. . . !ϕ Q± ?!(∃x)?!ϕ Q± , ?!ψ Q±
		!ϕ Q± ?!ϕ 0Q± , ?!ϕ 1Q± , ?!ϕ Q±
	!ϕ Q± ?!ϕ 0Q± `?!ϕ 1Q± , ?!ϕ Q± The soudness of (-) L (Proposition 6) then follows by noticing that FS + (DEXP) !ϕ Q± ?(?!ϕ 0Q± `?!ϕ 1Q± ), ?!ϕ Q± proves that (-) T ± , (-) Q± and (-) L are all equivalent.
	-Case of the (-) Lemma 16. For all formula ϕ of classical logic with equality, we have Q± translation of the rule
		FS+(DEXP)	ϕ, ϕ ψ ϕ, (∃z)ϕ ψ ϕ T ± ˛ϕL ˛ϕQ±

  ). In particular, MSO(M) proves t . = π 1 t, . . . , π 2 p t ( σ = 2 p ) Hence each term t of sort (σ 1 , . . . , σ n ; τ ) with τ = 2 p is provably equal to a tuple of terms (t i ) 1≤i≤2 p with each t i of sort (σ 1 , . . . , σ n ; o). Now, we turn terms t of sort (σ 1 , . . . , σ n ; o) withσ 1 × • • • × σ n = 2 qMoreover, we replace each such term t with the MSO + -term t representing the Mealy machine 2 q → 2 for t. To summarize, we have

	to terms t of sort
			(2, . . . , 2
	MSO(M )(ω)	t	. = σ u ←→	t i	. = o u
			1≤i≤2 p

q

; 2) i (t, u of sort (σ 1 , . . . , σ n ; τ ))

Consider now an MSO(M)-formula ϕ with free variables among x σ1 , . . . , x σn . To ϕ we can associate an MSO + -formula ϕ with free variables among x o 1,1 , . . . , x o 1,m1 , . . . , x o n,1 , . . . , x o n,mn

This work was partially supported by the ANR-14-CE25-0007 -RAPIDO and Polish National Science Centre grant no. 2014/13/B/ST6/03595. UMR 5668 CNRS ENS Lyon UCBL INRIA

D

˛(∃F (τ )((σ)τ ) )(∀g (σ)τ )ϕ D ((F )g , (g)((F )g) , a)

Then we are done if we show that LMSO proves (∀F (τ )((σ)τ ) )(∃u τ )(∀x σ )(∃g (σ)τ ) ϕ D ((F )g , (g)((F )g) , a) -ϕ D (u, x, a)

Consider the functions u : (τ )((σ)τ ) -→ τ and g : (τ )((σ)τ ) × σ -→ (σ)τ

given by Lemma 21. Let u(F ) and g(F, x) be terms representing their pointwise lift to M. We then have, in LMSO u(F ) . = @ F , g(F, x) and @ g(F, x) , u(F ) . = x and we conclude as follows:

Lemma 22 (Lemma 2).

Proof. Thanks to Corollary 3 we are done if we show

We use fixpoints for finite-state eager functions (Proposition 3 and §A.1). Let

We apply Corollary 4 to

We thus obtain a f.s. eager

We now apply Proposition 3 and obtain a finite-state fixpoint of H, that is a finite-state eager fix(H) :

Let v(f (σ)τ ) be the (Mealy) term for e(fix(H)) : (σ)τ → M σ . We thus have

and it follows that Proof. Let ϕ be a closed LMSO-formula and ϕ D (u τ , x σ ) be the body of its Dialectica interpretation. We apply Büchi-Landweber Theorem 1 to the MSO(M)formula ϕ D (u τ , x σ ) . There are two cases.

-Either there exists an eager term u(x) of sort (σ, τ ) such that (∀x σ ) ϕ D (t(x), x) holds. We then proceed as follows.

-Otherwise, there exists a term x(u) of sort (τ ; σ) such that (∀u τ )¬ ϕ D (x(u), u) holds. Note that

We then conclude as follows.

By definition (see Fig. 3)

Table of Contents