Guillaume Geoffroy
email: guillaume.geoffroy@univ-amu.fr

Classical realizability as a classifier for nondeterminism

come

Classical realizability as a classifier for nondeterminism

Introduction

Classical realizability Realizability is an instance of the formulasas-types/proofs-as-programs correspondence in which each formula is interpreted as the specification of a certain computational behaviour. Initially, this correspondence (and hence realizability) was limited to intuitionistic reasoning, until Griffin noted a connection between control operators and classical reasoning [START_REF] Griffin | A Formulae-as-type Notion of Control[END_REF], which lifted this limitation. Classical realizability is an extension of Kleene's realizability to accommodate classical reasoning: using control operators, Krivine developed a theory capable of interpreting all classical reasoning within second-order arithmetic ( [START_REF] Krivine | Dependent Choice, 'Quote' and the Clock[END_REF][START_REF] Krivine | Realizability in classical logic[END_REF]) and Zermelo-Fraenkel set theory with dependent choice ([6-9, 13]). Subsequently, Miquel adapted this framework to higher-order arithmetic [START_REF] Miquel | Forcing as a Program Transformation[END_REF].

Following intuitionistic realizability, Krivine's framework is made of three ingredients:

• A computational model (in Krivine's setting, it is called a realizability algebra). In general, it is a set of programs (with an operational semantics); • A logical language (for arithmetic, higher-order arithmetic or set theory), together with a realizability relation expressing the fact that a given program realizes a given formula. The essential result is the adequacy lemma which states that classical realizability is compatible with deduction rules; • A realizability model (in the usual sense of model theory), which satisfies all formulas that are realized. Such a model must exist by the completeness theorem. Krivine noted that this construction may be seen as an extension of Cohen's forcing construction [START_REF] Cohen | Set theory and the continuum hypothesis[END_REF]. Here, we will not look at it directly, nor even define it explicitly: we will look at realizability theories (i.e. consistent sets of realized formulas) rather than realizability models. In Krivine's framework, each realizability model comes with a characteristic Boolean algebra 2ג ("gimel 2") [START_REF] Krivine | Realizability algebras II : new models of ZF + DC[END_REF] whose structure encodes interesting properties of the model. In particular, forcing models correspond to the degenerate case where 2ג = {0, 1}.

In order to emphasise the central role of the characteristic Boolean algebra, let us recall that classical realizability gives rise to surprising models of set theory (such as the model of threads [START_REF] Krivine | Realizability algebras II : new models of ZF + DC[END_REF]), whose strange set-theoretic properties are mostly direct consequences of the structure of their characteristic Boolean algebras.

As noted above, classical realizability can be seen as an extension of forcing. However, while there are plenty of theoretical results connecting the properties of a forcing model to the structure of the underlying forcing set, there is currently a severe lack of general results connecting the properties of a classical realizability model to the properties of the underlying computational model. The goal of this paper is to start addressing this state of affairs by two means. First, by proving new results of this kind (namely, results which connect the presence of nondeterminism in the computational model with the size of the characteristic Boolean algebra in the realizability model), and second, by introducing a new framework which should make it easier, in the future, to find such results.

Nondeterminism The logical language can be extended by adding realizability connectives (such as union "∪" and intersection "∩"), which may in particular be used to express various forms of nondeterminism in the computational model.

For example, we will see that the formula ∀X ∀Y X → Y → X ∩ Y specifies the may-nondeterministic choice operator "fork", which takes two programs as arguments and does whatever either does. Dually the formula ∀X ∀Y X → Y → X ∪ Y specifies the must-nondeterministic choice operator "choose", which takes two programs as arguments and only does what both do.

It is known that adding a must-nondeterministic choice operator does not change the realizability model (no new formulas are realized), and that adding a may-nondeterministic choice operator collapses it into a forcing model.

However, we show that adding more subtle nondeterministic instructions corresponding to different mixes of may and must has the effect of altering the properties of .2ג To this end, we define an abstract notion of multi-evaluation relation which can express arbitrary mixes of may-and must-nondeterminism such as Kleene's "parallel or" [START_REF] Kleene | Introduction to Metamathematics[END_REF], Berry's "Gustave's function" [START_REF] Berry | Bottom-up computation of recursive programs[END_REF], and Trakhtenbrot's "voting function" [START_REF] Mark B Trakhtenbrot | Russian version 1974. On representation of sequential and parallel functions[END_REF], as well as generalisations thereof.

Outline We recall Krivine's formalisation of classical realizability -in the context of second-order arithmetic -(sections 2 and 3). Our presentation follows closely those given by Krivine and Miquel, except that, instead of individual poles, we consider sets of poles (which we call realizability structures), a formula being realized if it has a common realizer for all the poles in the structure. The rationale behind this is that realizability structures are a notion dual to multi-evaluation relations.

Then, we define the notion of multi-evaluation relation (section 4) and show that each multi-evaluation relation defines a unique realizability structure.

Next, we analyse in detail particular examples of such mixes, to notice that they are organised in a hierarchy, in terms of both their computational expressiveness and the properties of 2ג to which they correspond (sections 6 and 5). This hierarchy is reminiscent of Sazonov's degrees of parallelism [START_REF] Yu | Degrees of parallelism in computations[END_REF].

Finally, we prove that this hierarchy does not collapse: each level is indeed strictly more expressive than the levels below (section 7). To this end, we prove that 2ג can be made elementarily equivalent to any finite Boolean algebra with at least two elements. The case of Boolean algebras with 4 elements was stated and proved by Krivine [START_REF] Krivine | Realizability algebras III: some examples[END_REF], but the method used here is new.

The contributions of this paper are:

• The dual notions of realizability structures and multi-evaluation relations, • The results connecting the size of 2ג to voting functions, parallel or and Gustave's function (the result about fork is due to Krivine), • The method presented in section 7, which fits nicely in the framework developed here, and will be used in some future work to prove the same result about all Boolean algebras, not just the finite ones.

Classical realizability semantics

Following Krivine [START_REF] Krivine | Realizability algebras II : new models of ZF + DC[END_REF], we define the model of computation and the logical language which will be used throughout this paper, and we connect them through the classical realizability interpretation.

The computational model: the λ c -calculus

The λ c -calculus is a model of computation which extends pure λcalculus (with a specific evaluation strategy, namely: weak head βreduction) by the addition of a control operator cc (call-with-currentcontinuation). It is made up of three kinds of syntactic entities: λ c -terms, stacks and processes.

Definition 1. Let us fix a countably infinite set of variables. The sets of λ c -terms, stacks and processes are defined by the following grammars, modulo α-equivalence (free and bound variables are defined as usual, abstraction being the only binding construction):

λ c -terms: t, u ::= x (x variable) | tu (t, u λ c -terms -application) | λx .t (x variable, t λ c -term -abstraction) | cc (call-with-current-continuation) | k π (π stack -continuation constants) | ξ n (n ∈ N -nonrestricted instructions) | η n (n ∈ N -restricted instructions), Stacks: π ::= ω n (n ∈ N -stack bottoms) | t • π (t closed λ c -term, π stack),
Processes:

p ::= t ⋆ π (t closed λ c -term, π stack).
The additional instructions (i.e. ξ n and η n ) will serve as customizable instructions: the evaluation relation of the λ c -calculus, which we will define in this section, gives no evaluation rule for them, and therefore treats them as inert constants. On the other hand, in section 4, we will define multi-evaluation relations, which can specify evaluation rules for these instructions: thus, the meaning of a given additional instruction will depend on the particular evaluation relation which we are considering at the moment. Typically, they will represent nondeterministic choice operators.

Intuitively, restricted instructions correspond to privileged instructions of real-world processors (which cannot be called directly be the user), while unrestricted instructions correspond to system calls (through which the user can access privileged instructions, in a controlled fashion).

From now on, closed λ c -terms will be simply called terms.

The set of terms is denoted by Λ, the set of stacks by Π and the set of processes by Λ ⋆ Π.

If t ⋆ π is a process, we call t its head term and π its stack.

Application is left-associative (so tuvw means ((tu)v)w) and has higher priority than abstraction (so λx .tu means λx .(tu)). We write t n u for t applied n times to u.

Substitutions [START_REF] Krivine | Lambda-calculus types and models[END_REF]. Given any list of λ c -terms t, u 1 , . . . , u n and any list of distinct variables x 1 , . . . , x n , we will denote by t[x 1 := u 1 , . . . , x n := u n ] the λ c -term obtained by replacing simultaneously each free occurrence of x i by u i in t for i = 1, . . . , n. Definition 2. The evaluation relation of the λ c -calculus, denoted by ≻ K , is the smallest preorder on Λ ⋆ Π satisfying the following rules:

tu ⋆ π ≻ K t ⋆ u • π (push) λx .t ⋆ u • π ≻ K t[x := u] ⋆ π (grab) cc ⋆ t • π ≻ K t ⋆ k π • π (save) k π ′ ⋆ t • π ≻ K t ⋆ π ′ (restore)
The one-step evaluation relation of λ c -calculus, denoted by ≻ 1 K , is the smallest binary relation on Λ ⋆ Π satisfying these rules.

The push and grab rules simulate weak head β-reduction; they will make the realizability interpretation compatible with intuitionistic logic. The save and restore rules allow a program (i.e. a term) to save its evaluation context (i.e. the stack), and restore it later; they will make the realizability interpretation compatible with classical logic.

Remark. The one-step evaluation relation is deterministic: for all p, q, q ′ , if p ≻ 1 K q and p ≻ 1 K q ′ , then q = q ′ .

The realizability language

The realizability language is a second-order logical language, whose first-order terms are intended to represent integers.

Definition 3. We fix a set of first-order variables, and for each natural number n, we fix a set of n-ary propositional variables. Those sets are taken pairwise disjoint and countably infinite. The sets of first-order terms and of formulas are described by the following grammars, modulo α-equivalence (the binding constructions being first-and second-order universal quantifications). First order terms: a, b

::= x (x first-order variable) | f (a 1 , . . . , a n ) (f : N n → N), Formulas: A, B ::= X (a 1 , . . . , a n ) (X n-ary relational variable) | ⊤ | ⊥ | A → B | ∀x A | ∀X A | (a = b) → A | A ∩ B | A ∪ B | F (a 1 , . . . , a n ) (F : N n → P (Π)).
All formulas can be interpreted as describing program behaviours. In addition, formulas which only contain first-order terms, propositional variables, ⊤, ⊥, → and ∀ also have a logical meaning: they can be interpreted in N (or any model of second-order arithmetic). These formulas are called arithmetic formulas.

The construction (a = b) → A is called equational implcation. As we will see later, it is logically equivalent to regular implication ((a = b) → A), and its interest lies in the fact that realizers of (a = b) → A are easier to read, write and understand than realizers of (a = b) → A (they involve less "red tape").

We write a b for (a = b) → ⊥. Caution: we use the same letters for first-order variables and variables of λ c -calculus. It will always be clear from context which is which. Additional connectives. Equality and additional logical connectives are defined by the usual second-order encodings:

• a = b means ∀Z , Z (a) → Z (b); • A ∧ B means ∀Z , (A → B → Z ) → Z ; • A ∨ B means ∀Z , (A → Z ) → (B → Z ) → Z ; • ¬A means A → ⊥; • A ↔ B means (A → B) ∧ (B → A); • ∃x A means ∀Z , (∀x, A → Z ) → Z ; • ∃X A means ∀Z , (∀X , A → Z ) → Z .
Connectives are, from highest to lowest precedence: ¬, , =, ∩, ∪, ∧, ∨, →, →, ↔, ∃ and ∀. In addition, ∧ ∨, ∩ and ∪ are leftassociative, and → is right-associative. First-order substitutions. Given any formula or first-order term α, any list of first-order terms b 1 , . . . , b n and any list of distinct first-order variables x 1 , . . . , x n we denote by α[x 1 := u 1 , . . . , x n := u n ] the formula or the first-order term obtained by replacing simultaneously each free occurrence of x i by b i in α for i = 1, . . . , n. Second-order substitutions. Given any two formulas A, B, any nary propositional variable X and any list of distinct first-order variables y 1 , . . . , y n , we denote by A[X (y 1 , . . . , y n ) := B] the formula obtained by replacing X by B in A. Specifically, each free occurence of X of the form X (a 1 , . . . , a n ), is replaced by B[y 1 := a 1 , . . . , y n := a n ]. Formulas and terms with parameters. Given any formula or first-order term α and any list of distinct first-order variables x 1 , . . . ,

x n containing at least all the free variables of α, we will sometimes denote α by α (x 1 , . . . , x n ) (the point of this notation is to order the free variables of α). In that case, given any list of first-order terms a 1 , . . . , a n we will write α (a 1 , . . . ,

a n ) for α[x 1 := a 1 , . . . , x n := a n ].
When writing first-order terms, we will use all sorts of abuses of notation, such as writing a +b instead of +(a, b), or n i=1 a i instead of +(a 1 , . . . , a n ), etc.

In addition, if A 1 , . . . A n are formulas and ⊙ is ∧, ∨, ∩ or ∪, we will write n i=1 A i for A 1 ⊙ . . . ⊙ A n .

Classical realizability

Definition 4. A pole is a set of processes which is closed by antievaluation, that is to say, a set ⊥ ⊥ ⊆ Λ ⋆ Π such that for all p, q ∈ Λ ⋆ Π, if p ≻ K q and q ∈ ⊥ ⊥, then p ∈ ⊥ ⊥. The set of all poles is denoted by S 0 .

Definition 5. Let a be a closed first-order term. The value of a, written v (a) is the integer defined (inductively

) by v ( f (a 1 , . . . , a n )) = f (v (a 1 ), . . . , v (a n )).
Definition 6. Let ⊥ ⊥ be a pole and X a subset of Π. The dual of X with respect to ⊥ ⊥, denoted by

X ⊥ ⊥ , is the set {t ∈ Λ; ∀π ∈ X , t ⋆ π ∈ ⊥ ⊥}.
Definition 7. Let ⊥ ⊥ be a pole and A a closed formula. The falsity value of A with respect to ⊥ ⊥, denoted by ∥A∥ ⊥ ⊥ , is the subset of P (Π) defined below, and the truth value of A with respect to ⊥ ⊥, denoted by |A| ⊥ ⊥ , is defined as

(∥A∥ ⊥ ⊥ ) ⊥ ⊥ .
Falsity values of closed formulas are defined as follows:

• ∥⊤∥ ⊥ ⊥ = ∅, ∥⊥∥ ⊥ ⊥ = P (Π); • ∥A → B∥ ⊥ ⊥ = {t • π ; t ∈ |A| ⊥ ⊥ , π ∈ ∥B∥ ⊥ ⊥ }; • ∥∀x A∥ ⊥ ⊥ = n ∈N ∥A[x := n]∥ ⊥ ⊥ ; • ∥∀X A∥ ⊥ ⊥ = F :N n →P (Π) A[X (y 1 , . . . , y n ) := F (y 1 , . . . , y n )] ⊥ ⊥ • ∥(a = b) → A∥ ⊥ ⊥ = ∥A∥ ⊥ ⊥ if v (a) = v (b) ∥⊤∥ ⊥ ⊥ otherwise; • ∥A ∩ B∥ ⊥ ⊥ = ∥A∥ ⊥ ⊥ ∪ ∥B∥ ⊥ ⊥ ; • ∥A ∪ B∥ ⊥ ⊥ = ∥A∥ ⊥ ⊥ ∩ ∥B∥ ⊥ ⊥ ; • ∥F (a 1 , . . . , a n )∥ ⊥ ⊥ = F (v (a 1 ), . . . , v (a n )).
Notation. Let A be a closed formula. We denote by ∥A∥ the function which maps ⊥ ⊥ to ∥A∥ ⊥ ⊥ , and by |A| the function which maps ⊥ ⊥ to |A| ⊥ ⊥ . Definition 8. Let A be a closed formula, t a term and ⊥ ⊥ a pole. If t ∈ |A| ⊥ ⊥ , we say that t realizes A with respect to ⊥ ⊥, and we write t ⊩ ⊥ ⊥ A. Definition 9. Let A be a closed formula and t a term. We say that t realizes A universally if t realizes A with respect to every pole.

Remark. Let ⊥ ⊥ be a pole. For all X , Y ⊆ P (Π), if X ⊆ Y , then X ⊥ ⊥ ⊇ Y ⊥ ⊥ . Therefore, for all closed formulas A and B, if ∥A∥ ⊥ ⊥ ⊆ ∥B∥ ⊥ ⊥ , then |A| ⊥ ⊥ ⊇ |B| ⊥ ⊥ -in particular, the identity term λx .x realizes B → A.
Semantic equivalence and semantic subtyping [START_REF] Rieg | On Forcing and Classical Realizability[END_REF]. Let A and B be two closed formulas. If ⊥ ⊥ is a pole, we write

A ≈ ⊥ ⊥ B if ∥A∥ ⊥ ⊥ = ∥B∥ ⊥ ⊥ and A ≲ ⊥ ⊥ B if ∥A∥ ⊥ ⊥ ⊇ ∥B∥ ⊥ ⊥ . Moreover, we write A ≈ B if A ≈ ⊥ ⊥ B for all ⊥ ⊥, and A ≲ B if A ≲ ⊥ ⊥ B for all ⊥ ⊥.

Adequacy

Typing λ c -terms

We type λ c -terms with (non-necessarily closed) formulas of the realizability language.

A context is a finite set of hypotheses of the form x : B (with x a variable of the λ c -calculus and B a formula) such that no variable of the λ c -calculus appears more than once. Variables of the λ ccalculus which appear on the left of an hypothesis are said to be declared in the context, and variables of the realizability language which appear freely on the right of at least one hypothesis are said to be free in the context.

Typing judgments are sequents of the form Γ ⊢ t : A, where Γ is a context, t is a λ c -term whose free variables are all declared in Γ, and A is a formula.

Γ ⊢ t : ∀X A (∀ 2 -elim) Γ ⊢ t : A[X (y 1 , . . . , y n ) := B]
These are the usual rules of intuitionistic natural deduction, plus the rule that cc is typed by Peirce's law.

A sequent is said to be derivable if it is the conclusion of some derivation.

The following lemma states the compatibility of classical realizability with respect to deduction rules:

Proposition 10 (Adequacy lemma). Let ⊥ ⊥ be a pole, x 1 : A 1 , . . . , x n : A n ⊢ t : B a derivable sequent with A 1 , . . . A n , B closed, and u 1 , . . . , u n terms such that u i realizes A i w.r.t. ⊥ ⊥ for all i. The term t[x 1 := u 1 , . . . , x n := u n ] realizes B w.r.t. ⊥ ⊥.
The proof can be found in [START_REF] Krivine | Realizability algebras II : new models of ZF + DC[END_REF] (although in a set-theoretical rather than second-order-arithmetical setting).

Realizability structures

So far, we have considered realizability with respect to a fixed pole and uniform realizability across all poles (i.e. universal realizablity). However, in order to state the results of this paper, we will need to consider uniform realizability across arbitrary sets of poles: Definition 11. A realizability structure is a set of poles. Definition 12. Let A be a closed formula, t a term and S a realizability structure. If t ⊩ ⊥ ⊥ A for all ⊥ ⊥ ∈ S, we say that t realizes A with respect to S, and we write t ⊩ S A.

Remark. To simplify notation, when we have fixed a realizability structure S but no individual pole, we shall say that t realizes A and write t ⊩ A to mean t ⊩ S A, and when we have fixed a pole ⊥ ⊥, we shall say that t realizes A and write t ⊩ A to mean t ⊩ ⊥ ⊥ A. Now, we might be tempted to define the theory of a realizability structure as the set of all formulas which have a realizer with respect to this structure. However, an important feature of classical (as opposed to intuitionistic) realizability is that, given any nonempty pole ⊥ ⊥, there are terms which realize ⊥ with respect to ⊥ ⊥. Indeed, take t ⋆ π ∈ ⊥ ⊥ and form the term k π t: when evaluated, this term ignores its context and replaces it with the "winning" context π , therefore it realises ⊥ with respect to ⊥ ⊥. As a result, to avoid getting inconsistent theories, we will consider the following restriction: Definition 13. The set of proof-like terms, denoted by PL, is the set of all terms which do not contain any continuation constant (k π ) nor any restricted instruction (η n ).

We also exclude restricted instructions because in some cases (e.g. in section 7), it will be convenient to require some of them to realize ⊥ (or other inconsistent formulas), and we want to do so without breaking the logic. Definition 14. Let S be a realizability structure. The theory generated by S, denoted by Th (S), is the set of all closed formulas A such that there exists a proof-like term t which realizes A with respect to S.

Intuitively, the adequacy lemma means that Th (S) is closed by the rules of classical deduction. Therefore, we will write Th (S) |= A for A ∈ Th (S), and we will say that Th (S) is inconsistent if it contains ⊥, and consistent if it does not. Likewise, we will say that the structure S is consistent (respectively, inconsistent) if Th (S) is.

From now on, we will say that a formula is universally realized if it is universally realized by a proof-like term. Definition 15. Two formulas A(X 1 , . . . , X m , y 1 , . . . , y n ) and B(X 1 , . . . , X m , y 1 , . . . , y n ) are universally equivalent if the formula ∀X 1 . . . X m ∀y 1 . . . y n A ↔ B is universally realized.

Remark.

A realizability structure S is consistent if and only if there is no proof-like term t such that t ⋆ π ∈ ⊥ ⊥ for all ⊥ ⊥ ∈ S and all π ∈ Π.

Remark. It is well-known that if ⊥ ⊥ = ∅, then the truth value of an arithmetic formula A is Λ if A is true in N, and ∅ else [START_REF] Miquel | Relating Classical Realizability and Negative Translation for Existential Witness Extraction[END_REF]. In particular, an arithmetic formula which is universally realized must be true in N. However, the converse is false, as we will shortly see.

Theories of the form Th (S), which we will call realizability theories, will be our main object of study: what are their properties, and how do these relate to the properties of the generating realizability structures?

Equations, inequations and equational implications

Equations and inequations are preserved by classical realizability, in the following sense: Lemma 16. Let a and b be closed first-order terms.

• ∥a b ∥ = ∥⊤∥ if v (a) v (b), ∥⊥∥ otherwise. • ∥a = b ∥ = ∥∀X X → X ∥ if v (a) = v (b), ∥⊤ → ⊥∥ otherwise.
Proof. Both facts can be checked by expanding the definitions on either side of the equality. □

Moreover, as mentioned above, equational implication is equivalent to regular implication: In particular, formulas which contain the construction → can also be read as arithmetic formulas.

Horn clauses

An other important class of formulas which are preserved by classical realizability is the class of Horn clauses: Proposition 18. Let H be a Horn clause, i.e. a closed formula of the form ∀x 1 . . . x m E 1 → . . . → E n → G, with E i of the form a i = b i for all i, and G of the form either c = d (definite clause) or ⊥ (goal clause). In particular, H is arithmetic. If H is true in N, then H is universally realized, and if not, then ¬H is universally realized.

Proof. Let us first assume that H is false in N. Let p 1 , . . . , p m be values for x 1 , . . . , x m which invalidate it (i.e. the E i (p 1 , . . . , p m ) are true and G (p 1 , . . . , p m ) is false). Then I = λy.y universally realizes E i (p 1 , . . . , p m ) for all i, so λ f .f I . . . I universally realizes either

H → ⊥ (if H is a goal clause) or H → ⊤ → ⊥ (if H is a definite clause).
Now, let us assume that H is true, and let us fix a pole ⊥ ⊥ and some p 1 , . . . , p m ∈ N. To simplify notation, we will write E i for E i (p 1 , . . . , p m ), etc. Let t 1 , . . . , t n be terms such that t i realizes E i for all i. If all the E i are true, then G is true (and therefore, of the form c = d), so u = λy.t 1 (. . . (t n (y)) . . .) realizes G ≈ ∀X X → X . If any of the E i is false, then u realizes ⊤ → ⊥, therefore, if G is of the form c = d, it is realized by u, and if it is ⊥, then it is realized by u (λy.y). □

However, as we will see in section 7, a universal (Π 0 1 ) formula which is not a Horn clause (i.e. which is not of the form described in proposition 18) is generally not universally realized, even if it is true in N.

The axioms of arithmetics in the realizability model

Let s denote the successor function: s (n) = n + 1 for all n ∈ N. The first two axioms of Peano, which can be written as ∀x s (x ) 0 and ∀x∀y s (x ) = s (y) → x = y, are universally realized (by proposition 18). However, the axiom of induction, which can be written as ∀x ∀Z (∀y Z (y) → Z (s (y))) → Z (0) → Z (x ), is not, as we will see later.

Notwithstanding, we can define a predicate Nat (x ) such that all three axioms are realized when relativized to Nat: let Nat (x ) denote the formula ∀Z (∀y Z (y) → Z (s (y))) → Z (0) → Z (x ) Intuitively, Nat (x ) says "x is a natural number".

Proposition 19. The following formulas are universally realized:

• Nat (0); • ∀x Nat (x ) → Nat (s (x )); • ∀x Nat (x ) → s (x ) 0; • ∀x∀y Nat (x ) → Nat (y) → s (x ) = s (y) → x = y; • ∀x Nat (x ) → ∀Z (∀y Z (y) → Z (s (y))) → Z (0) → Z (x ).
Proof. The third and fourth are consequences of their non-relativized versions, and the other three are provable in second-order logic (and therefore realized, by the adequacy lemma). □

3 The characteristic Boolean algebra 2ג

In this section, we define the characteristic Boolean algebra 2ג and prove some general properties about it. Intuitively, 2ג is a unary predicate (i.e. a set of individuals) present in each realizability model. Since we are dealing with models of second-order logic, 2ג must be thought of as a "first-class" object in the realizability model. However, for simplicity, we will define it as a formula with one parameter, i.e. a purely syntactic object.

The predicate (2גx ) is designed so that )0(2ג and )1(2ג are both true (i.e. universally realized) and ,)2(2ג ,)3(2ג . . . are all false. Moreover, and crucially, it is designed so that )0(2ג and )1(2ג are true in the same way, i.e. ∥)0(2ג∥ = .∥)1(2ג∥ In that respect, it is very different from the predicate (x = 0 ∨ x = 1), which represents the set {0, 1}.

In fact, we can define a predicate גn for all n, although only 2ג is a Boolean algebra:

Notation. For all integers m and n, we denote by max(m, n) the greater of the two, and by min(m, n) the lesser. For all first order terms a and b, we write a ≤ b for min(a, b) = a.

Definition 20. Let n be a natural number and a a first-order term: we denote by גn(a) the formula a + 1 ≤ n.

By lemma 16, גn(k ) is universally realized if k < n, and ¬ גn(k ) is universally realized otherwise.

However, whenever n > 1, the formula ∀x גn(x ) → (x = 0) ∨ . . . ∨ (x = n -1) is not universally realized, even though it is true in N. This means that the predicate גn does not represent the set {0, . . . , n -1}. We will prove this for n = 2 in section 7. Relativized quantifiers. Let n be an integer, x a first-order variable and A a formula. We write ∀x גn A for ∀x גn(x ) → A. Now, we show how to equip 2ג with the structure of a Boolean algebra, inherited from the set {0, 1}:

Notation. For all natural numbers m and n, let

• m ∨ n = 1 if m > 0 or n > 0, m ∨ n = 0 otherwise, • m ∧ n = 1 if m > 0 and n > 0, m ∧ n = 0 otherwise, • ¬m = 1 if m = 0, ¬m = 0 otherwise,
Definition 21. The language of Boolean algebras is the subset of the realizability language defined by the following grammar:

Terms: a, b ::

= x | 0 | 1 | a ∨ b | a ∧ b | ¬a Formulas: A, B ::= ⊤ | ⊥ | a b | a = b | A → B | A ∨ B | A ∧ B | ∀x A
Terms and formulas of this language can be interpreted in any Boolean algebra. In particular, they can be interpreted in the Boolean algebra {0, 1}.

Note that we use the same notations ∨, ∧ and ¬ for operations in Boolean algebras and for logical connectives: the context will always make it clear which is which.

Notation. If A is a formula of the language of Boolean algebras, we denote by 2ג |= A the formula A relativized to 2ג (i.e., A with all ∀x turned into ∀x 2ג ).

We choose this notation, rather than the more conventional A 2ג , in order to emphasise that we think of 2ג as a first-class object of the realizability model which, from the point of view of the realizability model, happens to be a Boolean algebra (i.e. a first-order structure on the language of Boolean algebras satisfying all the axioms of Boolean algebras).

Note that the formula

2ג |= A is true in N if and only if A is true in {0, 1}.
The following proposition establishes that 2ג is indeed a Boolean algebra (with at least two elements): Proposition 22. Let A be a closed formula of the language of Boolean algebras. If A is true in every Boolean algebra with at least two elements, then 2ג |= A is universally realized.

Proof. The theory of Boolean algebras with at least two elements can be axiomatised by a list E 1 , . . . , E n of formulas, where each E i is of the form ∀x i,1 . . .

x i,m i G i and G i is of the form a i = b i or a i b i .
For all i, denote by H i the formula ∀x i,1 . . . ∀x i,m i (2גx i,1 ) → . . . → (2גx i,m i ) → G i : it is a Horn clause, and it is universally equivalent to the formula 2ג |= E i , which is true in N (because E i is true in {0, 1}). Therefore, by proposition 18, 2ג |= E i is universally realized.

The proposition follows by the adequacy lemma and the completeness theorem of first-order logic. □

The cardinality of 2ג

An important property of a realizability model is the cardinality of its characteristic Boolean algebra. This subsection develops the basic tools that we will need in order to state and prove facts about this cardinality. If B is a Boolean algebra and n a positive integer, then formula ∀x 1 . . . x n i j (x i = x j ) is true in B if and only if B has fewer than n elements. This justifies the following notation:

Notation. Let n be a positive integer.

• We denote by |2ג| < n (or |2ג| ≤ n + 1) the formula

2ג |= ∀x 1 . . . x n i j (x i = x j ), • We denote by |2ג| ≥ n the formula |2ג|( < n) → ⊥, • We denote by |2ג| = n the formula |2ג|( ≥ n) ∧ |2ג|( < n + 1).
Remark. The cardinality of a finite Boolean algebra is always a power of two. Therefore, for all n, the formulas |2ג| ≤ 2 n |2ג| < 2 n+1 are universally equivalent, and in particular, the formula

|2ג| = 2 n is universally equivalent to |2ג| ≥ 2 n ∧ |2ג| < 2 n+1 .
In general, a Boolean algebra has at least 2 n element if and only if it contains a sequence of n pairwise-disjoint non-zero elements. Therefore, by proposition 22, the sentences 2ג" has at least 2 n elements" and 2ג" contains a sequence of n pairwise-disjoint elements" are equivalent (see [START_REF] Givant | Introduction to Boolean Algebras[END_REF], chapter 15). We will favour the latter, because because its formal statement (as a formula of the realizability language) has a better-behaved falsity value:

Notation. For all positive integers n, let us denote by A n the following formula of the language of Boolean algebras:

∀x 1 . . . x n x 1 0 → . . . → x n 0 → i j x i ∧ x j 0.
If B is a Boolean algebra and n a positive integer, then the formula A n is true in B if and only if it is not possible to find n pairwisedisjoint non-zero elements in B.

The following lemma describes the falsity value of 2ג |= A n and shows that it is indeed quite simple:

Lemma 23. Let n be a positive integer, ⊥ ⊥ a pole, t 1 , . . . , t n ∈ Λ and π ∈ Π. Then t 1 • . . . • t n • π ∈ 2ג∥ |= A n ∥ ⊥ ⊥ if
and only if at most one of the t i does not realize ⊥.

Proof. For all x 1 , . . . , x n , one can check that i j x i ∧ x j = 0 if and only if at most one of the x i is not equal to 0. Therefore,

t 1 • . . . • t n • π ∈ 2ג∥ |= A n ∥ ⊥ ⊥ if
and only there exist x 1 , . . . , x n such that t i realize x i 0 for all i and at most one of the x i is not equal to 0. □

The following notation provides a third way of expressing tha cardinality of .2ג In a way, it is the most important one, since it is the one which provides the connection with non-determinism (as we will see in section 5):

Notation. Let n be a positive integer. We denote by B n the formula

∀X                ⊤ → X → • • • → X → X (1) ∩ X → ⊤ → • • • → X → X (2) . . . . . . . . . ∩ X → X → • • • → ⊤ → X (n)
.

Its falsity value is quite similar to that of 2ג |= A n (which is why they are equivalent):

Lemma 24. Let n be a positive integer, ⊥ ⊥ a pole, t 1 , . . . , By lemmas 23 and 24,

t n ∈ Λ and π ∈ Π. Then t 1 • . . . • t n • π ∈ ∥B n ∥ ⊥ ⊥ if and only if there is at most one i such that t i ⋆ π ⊥ ⊥.
B n → 2ג( |= A n ) is universally realized by λt .t (because B n ≲ 2ג( |= A n )) and 2ג( |= A n ) → B n is universally realized by λt . λu 1 . . . . .λu n . cc (λk. t (ku 1 ) . . . (ku n )) (because for all ⊥ ⊥, π and i, u i ⋆ π ∈ ⊥ ⊥ implies k π u i ⊩ ⊥ ⊥ ⊥). □
As a side note, we would like to bring the reader's attention on the following result (which is due to Krivine, but does not seem to appear in any published work):

Proposition 26. The formulas |2ג| = 2 and ∀x Nat (x ) are universally equivalent.

Proof. By proposition 25, it suffices to realize B 2 ↔ ∀x, Nat (x ).

Let us denote by δ the λ c -term λd.x (dd ) and by Y the λ c -term δδ . For all t ∈ Λ and all π ∈ Π, Y [

x := t] ⋆ π ≻ K t ⋆ Y [x := t] • π .
Let 0 denote the term λ f .λx . x (i.e the Church numeral 0) and s the term λn.λ f .λx . n f ( f x ) (i.e. the Church successor function). Using the adequacy lemma, one can check that 0 universally realizes Nat (0) and that s universally realizes ∀n. Nat (n) → Nat (n + 1).

To simplify notation, let us denote Y [x := λy. ψ 0 (sy)] by Y ψ . We prove that the left-to-right implication is universally realized by l = λψ . Y ψ . Let us fix a pole ⊥ ⊥, and let ψ ⊩ B 2 . For all π ∈ Π,

Y ψ ⋆ π ≻ K ψ ⋆ 0 • sY ψ • π . Therefore, Y ψ ⊩ Nat (0), and for all n such that Y ψ ⊩ Nat (n), Y ψ ⊩ Nat (n + 1) (because s realizes Nat (n) → Nat (n + 1)). By induction, Y ψ realizes Nat (n) for all n.
Let us prove that the right-to-left implication is universally realized by r = λt . λu. λv. t

(λz.u) v. First, note that Nat (0) ≈ ∀Z , ⊤ → Z → Z and Nat (1) ≈ ∀Z 0 , Z 1 , (Z 0 → Z 1 ) → Z 0 → Z 1 .
Let us fix a pole ⊥ ⊥, and let t ⊩ ∀x, Nat (x ), X ∈ P (Π) and u • v • π ∈ ∥B 2 ∥ ⊥ ⊥ , which means that π ∈ X , and u or v realizes X . If v realizes X , then, since t realizes Nat (0), t (λz.u) v realizes X . If u realizes X , then λz.u realizes ⊤ → X , t realizes Nat (1) and v realizes ⊤, so again t (λz.u) v realizes X . In both cases, r ⋆ t

• u • v • π ∈ ⊥ ⊥. □ 4

Multi-evaluation relations

This section defines a correspondence between realizability structures and a certain notion of multi-evaluation relations which extend the evaluation relation of λ c -calculus: this notion is powerful enough to express arbitrary mixes of may-and must-nondeterminism.

Then, we will explore some of the connections between the properties of the theory generated by a structure and the properties of the corresponding evaluation relation.

While the evaluation relation of λ c -calculus is a relation between processes, multi-evaluation relations are relations between sets of processes which satisfy certain axioms. Using "≻" generic symbol for evaluation relations, the following intuitions should be kept in mind:

The statement "{p} ≻ {q 1 } and {p} ≻ {q 2 }" specifies that, under "≻", p reduces nondeterministically to q 1 or q 2 , according to an oracle which "favours" being in the pole: this is may-nondeterminism. One can also imagine that the program tries both branches in parallel, to find out if one eventually meets the condition for being in the pole. Meanwhile, "{p} ≻ {q 1 , q 2 }" specifies that p reduces nondeterministically to q 1 or q 2 , according to an oracle which "favours" being out of the pole: this is must-nondeterminism.

Additionally, we can mix may-and must-nondeterminism by writing, say, "{p} ≻ {q 1 , q 2 } and {p} ≻ {q 2 , q 3 } and {p} ≻ {q 3 , q 1 }". This kind of two-out-of-three nondeteministic choice will be studied in detail in the next section, under the name of 3-voting instruction.

Finally, statements like "{p 1 , p 2 } ≻ {q 1 , q 2 }" allow interaction between different branches of execution: if one branch evaluates to p 1 and another to p 2 , then they merge and evaluate must-nondeterministically to q 1 or q 2 . Definition 27. A multi-evaluation relation, or simply evaluation relation is a binary relation on

P (Λ ⋆ Π) such that • For all p, q ∈ Λ ⋆ Π such that p ≻ 1 K q, {p} ≻ {q}, • For all p ∈ Λ ⋆ Π, {p} ≻ {p} (identity), • For all P, Q, P ′ , Q ′ ∈ P (Λ ⋆ Π), for all r ∈ Λ ⋆ Π, if P ≻ Q ∪ {r } and P ′ ∪ {r } ≻ Q ′ , then P ∪ P ′ ≻ Q ∪ Q ′ (cut),
• For all P, Q, P ′ ,

Q ′ ∈ P (Λ ⋆ Π) such that P ≻ Q, if P ⊆ P ′ and Q ⊆ Q ′ , then P ′ ≻ Q ′ (weakening).
The intuition behind the cut rule is the following: if on the one hand p 1 , . . . , p m , together, evaluate to r or one of q 1 , . . . , q n , and the other hand p ′ 1 ′ , . . . , p ′ m ′ , together with r , evaluate to one of q ′ 1 ′ , . . . , q ′ n ′ , then, together, p 1 , . . . , p m and p ′ 1 ′ , . . . , p ′ m ′ must evaluate to one of q 1 , . . . , q n (directly) or one of q ′ 1 ′ , . . . , q ′ n ′ (via r ). Definition 28. Let ≻ be a binary relation on P (Λ ⋆ Π). The realizability structure generated by ≻, denoted by S ≻ , is the of set all poles ⊥ ⊥ such that, for all P, Q such that P ≻ Q, if Q ⊆ ⊥ ⊥, then P ∩ ⊥ ⊥ ∅.

Definition 29. Let S be a realizability structure. The evaluation relation associated with S, written "≻ S ", is the binary relation on P (Λ ⋆ Π) defined by the following: for all P, Q ∈ P (Λ ⋆ Π), P ≻ S Q if and only if for all ⊥ ⊥ ∈ S, if Q ⊆ ⊥ ⊥, then P ∩ ⊥ ⊥ ∅.

Proposition 30. Let S0 be a realizability structure: ≻ S0 is an evaluation relation, and S ≻ S0 = S0. This means that any realizability structure is fully described by its associated evaluation relation. Proof. The set of evaluations relations containing ≻ is stable by arbitrary intersections, so it has a smallest element. Since ≻ ⊆ ≻ * , S ≻ ⊇ S ≻ * . Moreover, ≻ S≻ is an evaluation relation which contains ≻, so it contains ≻ * . Therefore, S ≻ * ⊆ S ≻ S≻ = S ≻ , by proposition 30. □

If ≻ is an evaluation realation, it is true in general that ≻ ⊆ ≻ S≻ , but not that ≻ = ≻ S≻ . 1

Voting instructions and fork

Using the language of evaluation relations, one can state the following specification result: Definition 32. Let n be a positive integer and ≻ an evaluation relation. An n-voting instruction modulo ≻ is a term ϕ such that for all terms t 1 , . . . , t n and all stacks π , for all j ∈ {1, . . . , n}, {ϕ ⋆ t

1 • . . . • t n • π } ≻ {t i ⋆ π ; i j}.
Theorem 33. Let S be a realizability structure and n a positive integer. A term ϕ realizes B n with respect to S if and only if ϕ is an n-voting instruction modulo ≻ S .

Proof. First, we notice that, by lemma 23, for all poles ⊥ ⊥, t 1 • . . . • t n • π ∈ ∥B n ∥ ⊥ ⊥ if and only if there exists j ∈ {1, . . . , n} such that for all i j, t i ⋆ π ∈ ⊥ ⊥. Therefore, both sides of the equivalence amount to saying that for all ⊥ ⊥ ∈ S, for all, t 1 • . . . As a corollary, there is a proof-like term which computes parallel or if and ony if there is a proof-like 3-voting instruction: a similar result was stated by Sazonov in [START_REF] Yu | Degrees of parallelism in computations[END_REF], though in a very different setting.

• t n • π ∈ ∥B n ∥ ⊥ ⊥ , ϕ ⋆ t 1 • . . . • t n • π ∈ ⊥ ⊥,
Formulas of the form |2ג| ≤ 2 n create a hierarchy on realizability theories (which is included in the hierarchy of all formulas of the form 2ג |= A). Through the realizability interpretation, this gives a hierarchy on models of computation. This hierarchy compares models of computation on their ability to "try" different execution paths using nondeterminism (and, consequently, to perform computations on "partial data", the way parallel or can compute even when one of its arguments is undefined or diverges): the bigger ,2ג the more deterministic the computation model.

This hierarchy is reminiscent of the degrees of parallelism of [START_REF] Yu | Degrees of parallelism in computations[END_REF]. Indeed, the first three levels correspond to fork, parallel or and 4-voting functions respectively.

Interestingly, the third level also corresponds to Gérard Berry's "Gustave's function". More precisely, the behaviour of Gustave's function can be encoded by the formula (0

→ 1 → ⊤ → 1) ∩ (⊤ → 0 → 1 → 1) ∩ (1 → ⊤ → 0 → 1) ∩ (0 → 0 → 0 → 0) ∩ (1 → 1 → 1 → 0) (
where 0 stands for Bool(0) and 1 for Bool( 1)), and it can be proved that this formula is universally equivalent to |2ג| ≤ 8 (similar to theorem 43).

7 Models with |2ג| = 2 n for any n > 0

In order to prove that the hierarchy described above (of formulas of the form |2ג| ≤ 2 n ) does not collapse, we have to prove the following:

Theorem 45. Let n be a positive integer. There exists a consistent realizability structure S such that Th (S) |= |2ג| = 2 n .

The cardinality of a finite Boolean algebra is always a power of two. Moreover, for all n, the theory of Boolean algebras with 2 n elements is complete, so this theorem means 2ג can be made elementarily equivalent to any finite Boolean algebra with at least two elements.

Let us fix a positive integer n.

Because of the results from section 3, it suffices to find a consistent realizability structure where both 2ג |= A n+1 and 2ג |= A n → ⊥ are realized.

Let β ⊤ and β ⊥ be two restricted instructions and ϕ and χ two nonrestricted instructions. Let ≻ 1 be the smallest binary relation on P (Λ ⋆ Π) such that:

• For all p, q ∈ Λ ⋆ Π, if p ≻ 1 K q, then {p} ≻ 1 {q}, • For all t 0 , . . . , t n ∈ Λ, π ∈ Π and j ∈ {0, . . . , n},

{ϕ ⋆ t 0 • . . . • t n • π } ≻ 1 {t i ⋆ π ; i j}, • For all π ∈ Π, u ∈ Λ and k ∈ {1, . . . , n}, {χ ⋆ u • π } ≻ 1 {u ⋆ β 1=k • . . . • β n=k • π ; 1 ≤ k ≤ n}, where β i=k means β ⊤ if i = k and β ⊥ if i k, • For all π ∈ Π, {β ⊥ ⋆ π } ≻ 1 ∅.
Let ≻ be the smallest evaluation relation which contains ≻ 1 , and let S = S ≻ .

Note that ϕ is an n-voting instruction with respect to ≻.

. . . • β n=k • π ∈ 2ג∥ |= A n ∥ ⊥ ⊥ (by lemma 24). Therefore, {u ⋆ β 1=k • . . . • β n=k • π ; 1 ≤ k ≤ n} ⊆ ⊥ ⊥, so χ ⋆ u • π ∈ ⊥ ⊥. □
Note that in particular, the formula ∀x 2ג ∀y 2ג x = 0 ∨ x = 1, which is universally equivalent to |2ג| = 2, is a disjunction of two positive literals which is true in N, and whose negation is realized in S if n > 1 (compare this with proposition 18). Lemma 49. For all P, Q, P ≻ Q if and only if there exists p ∈ P such that {p} ≻ Q.

Proof. Let ≻ be the binary relation defined by P ≻ Q if and only if there exists p ∈ P such that {p} ≻ Q. It is contained in ≻, it contains ≻ 1 , and it is an evaluation relation, therefore it is equal to ≻. □ Lemma 50. The evaluation relation ≻ is compact: for all P, Q such that P ≻ Q, there exist two finite sets P 0 ⊆ P and Q

0 ⊆ Q such that P 0 ≻ Q 0 .
Proof. Similar to the previous lemma. □

It remains to prove that the structure S is consistent. It suffices to find one pole ⊥ ⊥ ∈ S such that no proof-like term realizes ⊥ with respect to ⊥ ⊥.

Let ⊥ ⊥ = {p ∈ Λ ⋆ Π, {p} ≻ ∅}.

Lemma 51. We have ⊥ ⊥ ∈ S, and for all ⊥ ⊥ ′ ∈ S, ⊥ ⊥ ⊆ ⊥ ⊥ ′ : in other words, ⊥ ⊥ is the smallest pole in S.

Proof. Let us prove that ⊥ ⊥ ∈ S: let Q ⊆ ⊥ ⊥ and P ≻ Q. By lemma 50, one can assume without loss of generality that P and Q are finite. By lemma 49, there exists p ∈ P such that {p} ≻ Q. Since {q} ≻ ∅ for all q ∈ Q, one can prove by repeatedly applying the cut rule (once per element of Q) that {p} ≻ ∅: in other words, p ∈ ⊥ ⊥. Now, let ⊥ ⊥ ′ ∈ S and let p ∈ ⊥ ⊥. Since {p} ≻ ∅ and ∅ ⊆ ⊥ ⊥, necessarily, {p} ∩ ⊥ ⊥ ′ ∅, so p ∈ ⊥ ⊥ ′ . □

We say that a process is sound if it can be written without the instruction β ⊥ .

Let us fix a sequence (γ i ) i ∈N of pairwise distinct restricted instructions all different from β ⊤ and β ⊥ .

Notation. Let p be a process and K a subset of N. We denote by p[K] the process p where, for all i ∈ N, each occurence of γ i has been replaced by β ⊤ if i ∈ K, and by β ⊥ if i K.

Definition 52. Let p be a process. The content of p, denoted by C(p), is the set of all K ⊆ N such that p[K] ∈ ⊥ ⊥.

Remark. Let p be a process and K ⊆ L ⊆ N. One can prove that if L ∈ C(p), then K ∈ C(p).

Proposition 53. Let p be a sound process. For all K 1 , . . . , K n ∈ C(p), K 1 ∪ . . . ∪ K n N.

In other words, whenever p is sound, it is impossible to span all of N with only n elements of C(p).

Proof of proposition 53. By induction, we let ⊥ ⊥ 0 = ∅, and for all r ∈ N, ⊥ ⊥ r +1 = {p ∈ Λ ⋆ Π; there exists Q ⊆ ⊥ ⊥ r such that {p} ≻ 1 Q }.

For all r ∈ N, let C r (p) be the set of all K ⊆ N such that p[K] ∈ ⊥ ⊥ r .

The sequences (⊥ ⊥ r ) r and (C r (p)) r are increasing. Moreover, ⊥ ⊥ = r ∈N ⊥ ⊥ r (because r ∈N ⊥ ⊥ r can also be proved to be the smallest pole in S), and for all p, C(p) = r ∈N C r (p), so we can prove the result by induction on r .

Let r ∈ N, and let us assume that for all sound p, for all K 1 , . . . , K n ∈ C r (p), K 1 ∪ . . . ∪ K n N.

Let p be a sound process and K 1 , . . . , K n ∈ C r +1 (p). By contradiction, let us assume that K 1 ∪ . . . ∪ K n = N. By definition of C r +1 (p), for all i ∈ {1, . . . , n}, there exists Q i ⊆ ⊥ ⊥ r such that p[K i ] ≻ 1 Q i . By a case analysis on the structure of the head term of p (and by considering the definition of ≻ 1 ), we must be in one of the following cases:

• p is of the form tu ⋆ π , λx .t ⋆ u • π , cc ⋆t • π or k π ′ ⋆ t • π .
In that case, there is one and only one q such that p ≻ 1 K q, and one can check that necessarily q is sound and for all i, Q i = {q[K i ]} (because {q[K i ]} is the only R such that {p[K i ]} ≻ 1 R). Therefore, for all i, q[K i ] ∈ ⊥ ⊥ r , so K i ∈ C r (q). This contradicts the induction hypothesis, because q is sound and K 1 ∪ . . . ∪ K n = N.

• p is of the form ϕ ⋆ t 0 • . . . • t n • π . In that case, for all i ∈ {1, . . . , n}, there exists j (i) ∈ {0, . . . , n} such that

Q i = {(t k ⋆ π )[K i ]; k j (i)}.
Therefore, for all i ∈ {1, . . . , n}, for all k ∈ {0, . . . , n} such that k j (i), K i ∈ C r (t k ⋆ π ).

Let l be an element of {0, . . . , n} such that for all i ∈ {1, . . . , n}, j (i) l. Then for all i, K i ∈ C r (t l ⋆ π ). This contradicts the induction hypothesis, because t l ⋆ π is sound and K 1 ∪ . . . ∪ K n = N. • p is of the form χ ⋆u • π . In that case, for all i, Q i = {(u ⋆β 1=k

• . . .

• β n=k • π )[K i ]; 1 ≤ k ≤ n}.
Let a 1 , . . . a n ∈ N such that for all i, there is no occurence of γ a i in p, let q = u ⋆ γ a 1 • . . . • γ a n • π , and for all i, let L i = (K i \ {a 1 , . . . , a n }) ∪ {a i }.

Then for all i, q[L i ] = (u ⋆ β 1=i • . . .

• β 1=k • π )[K i ] ∈ ⊥ ⊥ r .
This contradicts the induction hypothesis because q is sound and L 1 ∪ . . . ∪ L n = N. • p is of the form γ j ⋆ π , with j ∈ N. Since K 1 ∪ . . . ∪ K n = N, there exists i ∈ {1, . . . , n} such that j ∈ K i . Then the head term of p[K i ] is β ⊤ , which contradicts p[K i ] ≻ 1 Q i , since there is no evaluation rule for β ⊤ . Now, since ⊥ ⊥ 0 = ∅, for all sound p, C 0 (p) = ∅, and so for all K 1 , . . . , K n ∈ C 0 (p), K 1 ∪ . . . ∪ K n N: the result follows by induction. □ Corollary 54. If p is a sound process, then C(p) P (N).

Corollary 55. The realizability structure S is consistent.

Proof. If t is proof-like and realizes ⊥ with respect to S, then in particular, t ⋆ω 0 is sound and for all K ⊆ N, (t ⋆ ω 0 )[K] = t ⋆ω 0 ∈ ⊥ ⊥, which contradicts the previous corollary. □

Concluding remarks

We hope to have made apparent the connection between the different forms of nondeterminism and the hierarchy of "formulas about ."2ג In this paper, we only studied this connection on Π 0 1 formulas: further work would include considering more complex first-order formulas, higher-order formulas, and formulas about the whole גN. Moreover, it would be interesting to take a more serious look at the analogy with the hierarchy of parallelism: currently, little is known about it, and the methods presented here could help understand it better.

Lemma 17 .

 17 Let A be a formula and a and b two first-order terms. The formulas (a = b) → A and (a = b) → A are universally equivalent. Proof. By the previous lemma and the definition of ∥(a = b) → a∥, we see that λa.λe.ea universally realizes the left-to-right implication and λb.b (λx .x ) the right-to-left implication. □

Proposition 25 .

 25 Let n be a positive integer. The formulas |2ג| < 2 n , 2ג |= A n and B n are universally equivalent. Proof of proposition 25. The formulas |2ג| < 2 n , 2ג |= A n are universally equivalent by proposition 22.

  Proof. Let ⊥ ⊥ ∈ S. By definition of ≻ S , ⊥ ⊥ ∈ S ≻ S . Let ⊥ ⊥ ∈ S 0 \ S. Then for all ⊥ ⊥ ′ ∈ S, ⊥ ⊥ ′ ⊥ ⊥, which means that if ⊥ ⊥ ⊆ ⊥ ⊥ ′ , there exists p ∈ ⊥ ⊥ ′ such that p ⊥ ⊥. In other words, (Λ ⋆ Π \⊥ ⊥) ≻ S ⊥ ⊥, so ⊥ ⊥ S. □ Lemma 31. Let ≻ be a binary relation on P (Λ ⋆ Π). There exists a smallest evaluation relation containing ≻. Moreover, if we denote this relation by ≻ * , then S ≻ * = S ≻ .

  and so they are equivalent. □ Corollary 44. Let S be a realizability structure. We have Th (S) |= |2ג| ≤ 4 if and only if there is a proof-like term which computes parallel or modulo S.

  Lemma 46. The term β ⊥ realizes ⊥ with respect to S. Proposition 47. The term ϕ realizes 2ג |= A n+1 with respect to S. Proposition 48. The term χ realizes 2ג |= A n → ⊥ with respect to S.Proof. Let us fix a pole ⊥ ⊥ ∈ S. Let u ⊩ ⊥ ⊥ 2ג( |= A n ), π ∈ Π and k ∈ {1, . . . , n}. There is at most one i such that β i=k does not realize ⊥, so β 1=k •

	Proof. From lemma 24 and theorem 33.	□

A typing derivation is a tree formed with the following typing rules. Its root is called its conclusion:(Axiom) Γ, x : A ⊢ x : A (Peirce) Γ ⊢ cc : ((A → B) → A) → A (⊤-intro) Γ ⊢ t : ⊤ Γ ⊢ t : ⊥ (⊥-elim) Γ ⊢ t : A Γ, x : A ⊢ t : B (→-intro) Γ ⊢ λx .t : A → B Γ ⊢ t : A → B Γ ⊢ u : A (→-elim) Γ ⊢ tu : B Γ ⊢ t : A (∀ 1 -intro) (x not free in Γ) Γ ⊢ t : ∀x A Γ ⊢ t : ∀x A (∀ 1 -elim) Γ ⊢ t : A[x := a] Γ ⊢ t : A (∀ 2 -intro)(X not free in Γ) Γ ⊢ t : ∀X A

This becomes true if ≻ is compact (i.e. for all P ≻ Q , there exist two finite sets P 0 ⊆ P and Q 0 ⊆ Q such that P 0 ≻ Q 0 ) or if ≻ satisfies the following infinitary cut-rule (which is implied by compactness): if there exists R such that, for all S ⊆ R, P ∪ S ≻ (R \ S ) ∪ Q , then P ≻ Q .

Corollary 34. Let S be a realizability structure and n a positive integer. We have Th (S) |= |2ג| ≤ 2 n if and only if there is a prooflike n-voting instruction modulo ≻ S .

We use the name n-voting instruction because whenever all but one of the t i "agree on" a certain behaviour, ϕ t 1 . . . t n "chooses" it. For example, if one of the t i is the church numeral 0 and all the others are 1, then ϕ t 1 . . . t n behaves like 1. (The notion of 3-voting instruction was introduced by Trakhtenbrot [START_REF] Mark B Trakhtenbrot | Russian version 1974. On representation of sequential and parallel functions[END_REF].)

Interestingly, the important point turns out to be, not the number of "votes for", but rather their proportion. Indeed, one can define a notion of (n, k )-voting instruction, which takes n arguments and requires at least nk "votes" (so that an n-voting instruction is the same thing as an (n, 1)-voting instruction). Then, using the same method, one can prove that there is a proof-like (n, k )-voting instruction if and only if Th (S) |= |2ג| < 2 ⌈ n k ⌉ . Now, let us consider the following definitions: Definition 35. Let ≻ be an evaluation relation.

• A fork instruction (or may-nondeterministic choice operator) modulo ≻ is a term ψ such that for all terms u, v and all stacks π , {ψ ⋆u

a 2-voting instruction).

• A must-nondeterministic choice operator modulo ≻ is a term χ such that for all terms u, v and all stacks π , {χ ⋆u

Proposition 36. Let S be a realizability structure and t a term. Then t is a may-nondeterministic choice operator modulo ≻ S if and only if it realizes ∀X ∀Y X → Y → X ∩ Y with respect to S, and it is a must-nondeterministic choice operator ≻ S if and only if it realizes

and similarly if π ∈ Y . Assume t is not a fork instruction. Without loss of generality, one can assume that there exist u, v and π such that {t ⋆u

The proof of the second point is similar. □ Proposition 37. Let S be a realizability structure. We have Th (S) |= |2ג| = 2 if and only if there exists a proof-like fork instruction modulo ≻ S .

Proof. Consequence of corollary 34 and proposition 22. □ 6 Parallel Or Definition 38. Let Bool(y) denote the formula ∀X X (0) → X (1) → X (y).

Lemma 39. We have

Proof. Similar to theorem 33 □

In other words, realizers of Bool(0) are terms which behave like false, and realizers of Bool(1) are terms which behave like true.

One can say that a term "computes the or function" (modulo some realizability structure S) if it realizes the formula ∀xy Bool(x ) → Bool(y) → Bool(x ∨ y), which we denote by Or. In general, there are two different ways of doing that:

• left-first: or l = λx .λy. x y true,

• right-first: or r = λx .λy. y x true.

The left-first version "returns true", i.e. behaves like true, as soon as its first argument does, even if its second argument diverges. The right-first version does the symmetric.

Let Or l denote the formula (∀x Bool(0) → Bool(x ) → Bool(x )) ∩ (Bool(1) → ⊤ → Bool(1)), and let Or r denote the formula (∀x 1)). Note that Or l ≲ Or and Or r ≲ Or.

Lemma 41. The term or l universally realizes Or l , and the term or r universally realizes Or r .

How different are or l and or r ? Can we come up with a (prooflike) term which captures the behaviour of both? That is to say, a parallel or, which returns true as soon as either of its arguments is true, even if the other diverges, and false if both arguments are false. This turns out to depend on the realizability structure and to be related to the properties of .2ג

First, let us denote by Or ∥ the formula (Bool(1)

Definition 42. Let S be a realizability structure and t a term. The term t computes parallel or modulo S if it realizes Or ∥ with respect to S.

Theorem 43. The formulas Or ∥ and |2ג| ≤ 4 are universally equivalent.

Proof. In order to realize the left-to-right implication, by proposition 25, it suffices to realize Or ∥ → 2ג( |= A 3 ). Let us prove that this formula is universally realized by l = λt .λu 1 .λu 2 .λu 3 . (t u 1 u 2 ) u 1 u 3 . Let us fix a pole ⊥ ⊥, and let t ⊩ ⊥ ⊥ Or ∥ and u 1

. By lemma 23, at least two of the u i realize ⊥. If u 1 and u 2 realize ⊥, in particular, they realize Bool(0), which means that t u 1 u 2 realizes Bool(0). Since u 1 realizes ⊥, (t

The last case (u 2 and u 3 realize ⊥) is similar tho the second.

In order to realize the right-to-left implication, by proposition 25, it suffices to realize B n → Or ∥ . Let us prove that this formula is universally realized by r = λt .λu.λv. t (or l u v) (or r u v) true. Indeed, let us fix a pole ⊥ ⊥, and let t ⊩ ⊥ ⊥ B 3 , u, v ∈ Λ and π ∈ Π.

If u realizes Bool(1) and π ∈ ∥Bool(1)∥ ⊥ ⊥ , then or l u v and true both realize Bool(1), so t (or l u v) (or r u v) true realizes Bool(1) (because t realizes ∀X X → ⊤ → X → X ), so r ⋆ t

If v realizes Bool(1) and π ∈ ∥Bool(1)∥ ⊥ ⊥ , then r ⋆ t • u • v • π ∈ ⊥ ⊥ for similar reasons.

If u and v realize Bool(0) and π ∈ ∥Bool(0)∥, then or l u v and or r u v both realize Bool(0), so t (or l u v) (or r u v) true realizes Bool(1) (because t realizes ∀X X → X → ⊤ → X ), so

□


tional [START_REF] Stauffer | The measurement of surface tension by the pendant drop technique[END_REF][START_REF] Adamson | Physical Chemistry of Surfaces[END_REF] analysis, which is the basis of the commercial measurement of surface tension.

However another way to estimate surface tension can be given by the following simple equation 10 :

(

where is the difference in density between the liquid and air, g is the gravitational constant (g = 9.81 m/s²), D E is defined in Fig. 1(a) and is the maximum diameter of the pendant drop, and is a dimensionless function of the ratio between D S and D E , which accounts for the specific shape of the drop due to gravity. D S is defined as the diameter of the drop at a distance D E from the bottom of the drop. For instance, if the drop was a perfect sphere, D S would be zero. Due to gravity, the droplet is then elongated and D S becomes strictly positive. This 1/H function can then be understood as a form factor and has been calculated numerically, [START_REF] Stauffer | The measurement of surface tension by the pendant drop technique[END_REF] but for our purpose we use the values tabulated in classic books [START_REF] Adamson | Physical Chemistry of Surfaces[END_REF] and represented in Fig. 1(c). However, it is also interesting to note that within a good approximation, this 1/H dimensionless function can be approximated by a simple analytical formula, , with a < 0.345 and b < -2.5 .

Thus, following Eq. ( 1), surface tension can be obtained by measuring diameters with a ruler directly on the screen of the smartphone using the optical and numerical zooms of the smartphone.

Experiment

Droplets of various liquids (water, olive oil, water with surfactants, ethanol) were suspended at the tip of a Pasteur pipette (diameter tip d Tube = 1.4 mm) by dipping it and pulling it out of a liquid reservoir. The experiment has also been tested with standard straws such as the tube of a pen (d Tube < 2.9 mm) or McDonald's straw (d Tube < 5.9 mm) instead of Pasteur pipette to test the generality of our approach. The smartphone used in the experiment is an iPhone 4s (camera sensor 8 MPixels, display 6403960 pixels, 3.5-in screen) and the standard camera function of the smartphone

Surface tension measurements with a smartphone

Nicolas-Alexandre Goy, Zakari Denis, Maxime Lavaud, Adrian Grolleau, Nicolas Dufour, Antoine Deblais, and Ulysse Delabre, University of Bordeaux, France S martphones are increasingly used in higher education and at university in mechanics, 1-3 acoustics, [START_REF] Hirth | Measurement of sound velocity made easy using harmonic resonant frequencies with everyday mobile technology[END_REF] and even thermodynamics [START_REF] Vieyra | Kitchen physics: Lessons in fluid pressure and error analysis[END_REF] as they offer a unique way to do simple science experiments. In this article, we show how smartphones can be used in fluid mechanics to measure surface tension of various liquids, which could help students understand the concept of surface tension through simple experiments.

Background

Interfacial tension is the energy per unit area required for a material to create an interface with a surrounding material. This surface tension exists for interfaces between solids, liquids, and gas. In the case of a liquid surrounded by air, interfacial tension is often called surface tension, which plays an essential role in many natural phenomena such as pulmonary breathing, use of detergents, and insect-walking on water. [START_REF] Hu | Meniscus climbing insects[END_REF][START_REF] Boutinguiza | Floating together on the top[END_REF][START_REF] Ondris-Crawford | It's all on the surface[END_REF] Usually surface tension is measured with quite expensive equipment (Wilhelmy plate, ring method) and long calibration procedures in order to get very accurate values, which perhaps prevents a simple understanding of the concept of surface tension. The method described here is based on the standard pendant drop method, [START_REF] Stauffer | The measurement of surface tension by the pendant drop technique[END_REF] where a drop of liquid is suspended from a tube as shown in Fig. 1(a). The shape of the drop is then governed by the balance of surface tension forces along the tube and the weight of the drop. We show here that without a specific image setup, smartphones are accurate enough to get reasonable values of surface tension for various liquids such as water, oil, and water with detergent, and can be done easily by students on their smartphones.

When a drop is hung at the tip of a tube, the shape of the drop is governed by the local Laplace equation, where the weight of the drop and surface tension forces are balanced. The complete resolution of this equation requires computa- is used. Taking advantage of the optical lens and the digital zoom (x5) of the smartphone, it is possible to measure D E , D S , and d Tube directly on the screen of the smartphone with a standard ruler. For example, a droplet with a real diameter D E = 3.3 mm [Fig. 1(a)] can be magnified using the optics and the digital zoom of the smartphone into a 2.8-cm diameter, which can easily be measured. For more accurate measurements, it is also possible to export pictures and analyze them with the free image analysis software ImageJ. [START_REF]ImageJ software[END_REF]

Results

Figure 2 shows typical pictures of various droplets at room temperature (20 °C) taken with the smartphone. Using Eq. ( 1) we get surface tension values summarized in Table I. These results show that relatively good surface tension values for various liquids are obtained with this smartphone method. Even if the values obtained for surface tension for water are scattered, the values are always larger than the surface tension of olive oil and ethanol droplets, which is consistent with literature data. Indeed, a rough estimate of surface tension is given by 12 where E is the typical energy between two molecules and a the typical size of the molecules. This explains that the surface tension of water due to hydrogen bonds is much higher than that of olive oil or ethanol.

For other measurements with standard straws, the experimental surface tension gives reasonable values but they are less accurate as explained in Ref. 13

Conclusion

We present here a simple method to measure the surface tension of various liquids with a smartphone. The simplicity of our method especially compared to force measurement methods makes this approach interesting for educational purposes. It could enable a simple characterization of surface tension.

Fig. 1 .

 1 Fig. 1. (a) Water droplet suspended at the tip of a Pasteur pipette. (b) Illustration of the measurement of the diameters directly on the screen of the smartphone with a simple ruler. (c) 1/H as a function of the ratio D S /D E . 10 Note the logarithmic scale on the axes. (a) (b) (c)

Fig. 2 .

 2 Fig. 2. (a) Water droplet, (b) oil droplet, (c) ethanol droplet hung at the tip of a Pasteur pipette. (d) Water droplet hung at the tip of a pen tube. (e) Water droplet hung at the tip of a McDonald's straw.

  because the diameter of the tube is quite large, especially compared to capillary length c which induces D S /D E ratios close to 1 [see for example Fig. 2(e)].

Table I .

 I Surface tension values obtained with the smartphone pendant drop method.

		Typical	Density	Surface	Surface
		range of	differ-	tension	tension
		D S /D E	ence	(mN/m)	tabulated
			=	(Smartphone	value
			L -air (kg/m 3 )	measure-ment at	(mN/m) at 20 o C
				20 o C)
	Water (Pasteur	0.68-0.78	999	7815	72.8
	pipette)			(6 drops)
	Olive oil	0.75	930	333	32
	Pasteur pipette)			(2 drops)
	Ethanol Pasteur	0.8	780	222	23
	pipette)			(2 drops)
	Water (pen	0.82	999	60 (2 drops)	72.8
	tube)
	Water	~1	999	67	72.8
	McDonald's
	straw)

(a) (b) (c) (d) (e)


Jean-Yves Chemin
email: chemin@ann.jussieu.fr

Isabelle Gallagher
email: isabelle.gallagher@math.jussieu.fr

LARGE, GLOBAL SOLUTIONS TO THE NAVIER-STOKES EQUATIONS, SLOWLY VARYING IN ONE DIRECTION

Keywords:

classes of initial data to the three dimensional, incompressible Navier-Stokes equations were presented, generating a global smooth solution although the norm of the initial data may be chosen arbitrarily large. The aim of this article is to provide new examples of arbitrarily large initial data giving rise to global solutions, in the whole space. Contrary to the previous examples, the initial data has no particular oscillatory properties, but varies slowly in one direction. The proof uses the special structure of the nonlinear term of the equation. def = λ 2 p(λ 2 t, λx)

Introduction

The purpose of this paper is to use the special structure of the tridimensional Navier-Stokes equations to prove the global existence of smooth solutions for a class of (large) initial data which are slowly varying in one direction. Before entering further in the details, let us recall briefly some classical facts on the global wellposedness of the incompressible Navier-Stokes equations in the whole space R 3 . The equation itself writes

(N S)    ∂ t u + u • ∇u -∆u = -∇p div u = 0 u |t=0 = u 0
where u = (u 1 , u 2 , u 3 ) = (u h , u 3 ) is a time dependent vector field on R 3 . The divergence free condition determines p through the relation

-∆p = 1≤j,k≤3 ∂ j ∂ k (u j u k ).
This relation allows to put the system (N S) under the more general form

(GN S) ∂ t u -∆u = Q(u, u) u |t=0 = u 0 where Q(v, w) def = 1≤j,k≤3
Q j,k (D)(v j w k ) and Q j,k (D) are smooth homogeneous Fourier multipliers of order 1.

Moreover, this system has the following scaling invariance: if (u, p) is a solution on the time interval [0, T ), then (u λ , p λ ) defined by u λ (t, x) def = λu(λ 2 t, λx) and p λ (t, x) is a solution on the time interval [0, λ -2 T ). Of course, any smallness condition on the initial data that ensures global solutions, must be invariant under the above scaling transformation. The search of the "best" smallness condition is a long story initiated in the seminal paper of J. Leray (see [START_REF] Leray | Essai sur le mouvement d'un liquide visqueux emplissant l'espace[END_REF]), continuated in particular by H. Fujita and T. Kato in [START_REF] Fujita | On the Navier-Stokes initial value problem I[END_REF], Y. Giga and T. Miyakawa in [START_REF] Giga | Solutions in L r of the Navier-Stokes initial value problem[END_REF], and M. Cannone, Y. Meyer and F. Planchon in [START_REF] Cannone | Solutions autosimilaires des équations de Navier-Stokes, Séminaire[END_REF]. This leads to the following theorem proved by H. Koch and D. Tataru in [START_REF] Koch | Well-posedness for the Navier-Stokes equations[END_REF]. In the statement of the theorem, P (x, R) stands for the parabolic set [0, R 2 ] × B(x, R) where B(x, R) is the ball centered at x, of radius R.

Theorem 1 ( [START_REF] Koch | Well-posedness for the Navier-Stokes equations[END_REF]). If the initial data u 0 is such that

(1.1) u 0 2 BM O -1 def = sup t>0 t e t∆ u 0 2 L ∞ + sup x∈R 3 R>0 1 R 3 P (x,R)
|(e t∆ u 0 )(t, y)| 2 dy is small enough, then there exists a global smooth solution to (GN S).

A typical example of application of this theorem is the initial data

(1.2) u ε 0 (x) def = cos x 3 ε (∂ 2 φ(x 1 , x 2 ), -∂ 1 φ(x 1 , x 2 ), 0) with φ ∈ S(R 2 ),
as soon as ε is small enough (see for example [START_REF] Chemin | Wellposedness and stability results for the Navier-Stokes equations in R 3 to appear in Annales de l'Institut Henri Poincaré[END_REF] for a proof). The above theorem is probably the end point for the following reason, as observed for instance in [START_REF] Chemin | Wellposedness and stability results for the Navier-Stokes equations in R 3 to appear in Annales de l'Institut Henri Poincaré[END_REF]. If B is a Banach space continuously included in the space S ′ of tempered distributions on R 3 , such that, for any (λ,

a) ∈ R + ⋆ × R 3 , f (λ(•-a)) B = λ -1 f B , then • B ≤ C sup t>0 t 1 2 e t∆ u 0 L ∞ .
The second condition entering in the definition of the BM O -1 norm given in (1.1) merely translates the fact that the first Picard iterate should be locally square integrable in space and time.

Those results of global existence under a smallness condition do not use the special structure of the incompressible Navier-Stokes system and are valid for the larger class of systems of the type (GN S). The purpose of this paper is to provide a class of examples of large initial data which give rise to global smooth solutions for the system (N S) itself, and not for the larger class (GN S). In all that follows, an initial data u 0 will be said "large" if

(1.3) u 0 Ḃ-1 ∞,∞ def = sup t>0 t 1 2 e t∆ u 0 L ∞ is not small.
Such initial data, in the spirit of the example provided by (1.2), are exhibited in [START_REF] Chemin | Wellposedness and stability results for the Navier-Stokes equations in R 3 to appear in Annales de l'Institut Henri Poincaré[END_REF] (see also [START_REF] Chemin | On the global wellposedness of the 3-D Navier-Stokes equations with large initial data[END_REF] for the periodic case). In particular, the following theorem is proved in [START_REF] Chemin | Wellposedness and stability results for the Navier-Stokes equations in R 3 to appear in Annales de l'Institut Henri Poincaré[END_REF].

Theorem 2 ([4]

). Let φ ∈ S(R 3 ) be a given function, and consider two real numbers ε and α in ]0, 1[. Define

ϕ ε (x) = (-log ε) 1 5 ε 1-α cos x 3 ε φ x 1 , x 2 ε α , x 3 .
Then for ε small enough, the smooth, divergence free vector field The proof of that theorem shows that the solution remains close to the solution of the free equation e t∆ u 0,ε . It is important to notice that the proof uses in a crucial way the algebraic structure of the non linear term u • ∇u, but uses neither the energy estimate, nor the fact that the two dimensional, incompressible Navier-Stokes is globally wellposed. Let us give some other results on large initial data giving rise to global solutions: In [START_REF] Mahalov | Global solvability of three-dimensional Navier-Stokes equations with uniformly high initial vorticity[END_REF], the initial data is chosen so as to transform the equation into a rotating fluid equation. In [START_REF] Iftimie | Navier-Stokes equations in thin 3D domains with Navier boundary conditions[END_REF], [START_REF] Raugel | Navier-Stokes equations on thin 3D domains. I. Global attractors and global regularity of solutions[END_REF] the equations are posed in a thin domain (in all those cases the global wellposedness of the two dimensional equation is a crucial ingredient in the proof). In [START_REF] Gallagher | The tridimensional Navier-Stokes equations with almost bidimensional data: stability, uniqueness and life span[END_REF] and [START_REF] Iftimie | The 3D Navier-Stokes equations seen as a perturbation of the 2D Navier-Stokes equations[END_REF], the case of an initial data close to bidimensional vector field is studied, in the periodic case. Finally in [START_REF] Foias | Asymptotic behavior, as t → +∞, of solutions of Navier-Stokes equations and nonlinear spectral manifolds[END_REF] (Remark 7), an arbitrary large initial data is constructed in the periodic case, generating a global solution (which is in fact a solution to the heat equation, as the special dependence on the space variables implies that the nonlinear term cancels).

u ε 0 (x) = (∂ 2 ϕ ε (x), -∂ 1 ϕ ε (x), 0) satisfies lim ε→0 u ε 0 Ḃ-1 ∞,∞ = ∞,
The class of examples we exhibit here is quite different. They are close to a two dimensional flow in the sense that they are slowly varying in the one direction (the vertical one). More precisely the aim of this paper is the proof of the following theorem.

Theorem 3. Let v h 0 = (v 1 0 , v 2
0 , 0) be a horizontal, smooth divergence free vector field on R 3 (i.e. v h 0 is in L 2 (R 3 ) as well as all its derivatives), belonging, as well as all its derivatives, to L 2 (R x 3 ; Ḣ-1 (R 2 )); let w 0 be a smooth divergence free vector field on R 3 . Then if ε is small enough, the initial data u ε 0 (x) = (v h 0 + εw h , w 3 0 )(x h , εx 3 ) generates a unique, global solution u ε of (N S).

Remarks

• A typical example of vector fields v h 0 satisfying the hypothesis is v h 0 = (-∂ 2 φ, ∂ 1 φ, 0) where φ is a function of the Schwarz class S(R 3 ).

• This class of examples of initial data corresponds to a "well prepared" case. The "ill prepared" case would correspond to the case when the horizontal divergence of the initial data is of size ε α with α less than 1, and the vertical component of the initial data is of size ε α-1 . This case is certainly very interesting to understand, but that goes probably far beyond the methods used in this paper. • We have to check that the initial data may be large. This is ensured by the following proposition.

Proposition 1.1. Let (f, g) be in S(R 3 ). Let us define h ε (x h , x 3 ) def = f (x h )g(εx 3 ). We have, if ε is small enough, h ε Ḃ-1 ∞,∞ (R 3 ) ≥ 1 4 f Ḃ-1 ∞,∞ (R 2 ) g L ∞ (R) .
Proof. By the definition of

• Ḃ-1 ∞,∞ (R 3 )
given by (1.3), we have to bound from below the quantity e t∆ h ε L ∞ (R 3 ) . Let us write that (e t∆ h ε )(t, x) = (e t∆ h f )(t, x h )(e t∂ 2 3 g)(ε 2 t, εx 3 ). Let us consider a positive time t 0 such that

t 1 2 0 e t 0 ∆ h f L ∞ (R 2 ) ≥ 1 2 f Ḃ-1 ∞,∞ (R 2 ) .
Then we have

t 1 2 0 e t 0 ∆ h ε L ∞ (R 3 ) = t 1 2 0 e t 0 ∆ h f L ∞ (R 2 ) (e t 0 ∂ 2 3 g)(ε 2 t 0 , ε•) L ∞ (R) ≥ 1 2 f Ḃ-1 ∞,∞ (R 2 ) e ε 2 t 0 ∂ 2 3 g L ∞ (R) .
As lim ε→0 e ε 2 t 0 ∂ 2 3 g = g in L ∞ (R), the proposition is proved.

Structure of the paper: The proof of Theorem 3 is achieved in the next section, assuming two crucial lemmas. The proof of those lemmas is postponed to Sections 3 and 4 respectively.

Notation: If A and B are two real numbers, we shall write A B if there is a universal constant C, which does not depend on varying parameters of the problem, such that A ≤ CB. If A B and B A, then we shall write A ∼ B.

If v 0 is a vector field, then we shall denote by C v 0 a constant depending only on norms of v 0 . Similarly we shall use the notation C v 0 ,w 0 if the constant depends on norms of two vector fields v 0 and w 0 , etc.

A function space with a subscript "h" (for "horizontal") will denote a space defined on R 2 , while the subscript "v" (for "vertical") will denote a space defined on R. For instance

L p h def = L p (R 2 ), L q v def = L q (R
), and similarly for Sobolev spaces or for mixed spaces such as

L p v L q h or L p v Ḣσ h .

Proof of the theorem

The proof of Theorem 3 consists in constructing an approximate solution to (N S) as a perturbation to the 2D Navier-Stokes system. Following the idea that we are close to the two dimensional, periodic incompressible Navier-Stokes system, let us define v h as the solution of the following system, where y 3 ∈ R is a parameter:

(N S2D 3 )    ∂ t v h + v h • ∇ h v h -∆ h v h = -∇ h p 0 in R + × R 2 div h v h = 0 v h |t=0 = v h 0 (•, y 3
). This system is globally wellposed for any y 3 ∈ R, and the solution is smooth in (two dimensional) space, and in time. Let us consider the solution w ε of the linear equation

(T ε v )    ∂ t w ε + v h • ∇ h w ε -∆ h w ε -ε 2 ∂ 2 3 w ε = -(∇ h p 1 , ε 2 ∂ 3 p 1 ) in R + × R 3 div w ε = 0 w ε |t=0 = w 0 , and let us define the approximate solution v ε app (t, x) = ((v h , 0) + ε(w ε,h , ε -1 w ε,3 ))(t, x h , εx 3 ) and (2.1) p ε app (t, x) = (p 0 + εp 1 )(t, x h , εx 3
). Finally let us consider the unique smooth solution u ε of (N S) associated with the initial data u ε 0 on its maximal time interval of existence [0, T ε ). The proof of Theorem 3 consists in proving global in time estimates on v ε app , in order to prove that R ε def = u ε -v ε app remains small, globally in time; this ensures the global regularity for (N S).

More precisely, the proof of Theorem 3 relies on the following two lemmas, whose proofs are postponed to Sections 3 and 4 respectively.

Lemma 2.1. The vector field v ε app defined in (2.1) satisfies the following estimate:

v ε app L 2 (R + ;L ∞ (R 3 )) + ∇v ε app L 2 (R + ;L ∞ v L 2 h ) ≤ C v 0 ,w 0 . Lemma 2.2. The vector field R ε def = u ε -v ε app satisfies the equation (E ε )    ∂ t R ε + R ε • ∇R ε -∆R ε + v ε app • ∇R ε + R ε • ∇v ε app = F ε -∇q ε div R ε = 0 R ε |t=0 = 0 with F ε L 2 (R + ; Ḣ-1 2 (R 3 )) ≤ C v 0 ,w 0 ε 1 3 .
Let us postpone the proof of those lemmas and conclude the proof of Theorem 3. We denote, for any positive λ,

V ε (t) def = v ε app (t, •) 2 L ∞ (R 3 ) + ∇v ε app (t, •) 2 L ∞ v L 2 h and R ε λ (t) def = exp -λ t 0 V ε (t ′ )dt ′ R ε (t). Lemma 2.1 implies that I 0 def = ∞ 0 V ε (t)dt is finite. By an Ḣ 1 2 energy estimate in R 3 , we get 1 2 d dt R ε λ (t) 2 Ḣ 1 2 + ∇R ε λ (t) 2 Ḣ 1 2 ≤ -2λV ε (t) R ε λ (t) 2 Ḣ 1 2 + e λI 0 (R ε λ (t) • ∇R ε λ (t)|R ε λ (t)) Ḣ 1 2 + (R ε λ (t) • ∇v ε app (t)|R ε λ (t)) Ḣ 1 2 + (v ε app (t) • R ε λ (t)|R ε λ (t)) Ḣ 1 2 + (F ε (t)|R ε λ (t)) Ḣ 1 2 .
The estimate (i) of Lemma 1.1 of [START_REF] Chemin | Remarques sur l'existence pour le système de Navier-Stokes incompressible[END_REF] claims in particular that, for any s ∈] -d/2, d/2[, for any divergence free vector field a in d space dimensions and any function b, we have

(2.2) (a • ∇b|b) Ḣs ≤ C ∇a Ḣ d 2 -1 b Ḣs ∇b Ḣs . Applying with d = 3 and s = 1/2, this implies that (2.3) (R ε λ (t) • ∇R ε λ (t)|R ε λ (t)) Ḣ 1 2 R ε λ (t) Ḣ 1 2 ∇R ε λ (t) 2 Ḣ 1 2 .
In order to estimate the other non linear terms, let us establish the following lemma.

Lemma 2.3. Let a and b be two vector fields. We have

(a • ∇b|b) Ḣ 1 2 + (b • ∇a|b) Ḣ 1 2 a L ∞ + ∇a L ∞ v (L 2 h ) b Ḣ 1 2 ∇b Ḣ 1 2 .
Proof. By definition of the Ḣ 1 2 scalar product, we have

(a • ∇b|b) Ḣ 1 2 ≤ a • ∇b L 2 ∇b L 2 ≤ a L ∞ ∇b 2 L 2 . The interpolation inequality between Sobolev norm gives (a • ∇b|b) Ḣ 1 2 ≤ a L ∞ b Ḣ 1 2 ∇b Ḣ 1 2 . Now let us estimate (b • ∇a|b) Ḣ 1 2 . Again we use that (b • ∇a|b) Ḣ 1 2 ≤ b • ∇a L 2 ∇b L 2 . Then let us write that b • ∇a 2 L 2 = R 3 |b(x h , x 3 )∇a(x h , x 3 )| 2 dx h dx 3 .
Gagliardo-Nirenberg's inequality in the horizontal variable implies that

∀x 3 ∈ R, |b(x h , x 3 )| 2 b(•, x 3 ) Ḣ 1 2 h ∇ h b(•, x 3 ) Ḣ 1 2 h .
Let us use the Cauchy-Schwarz inequality; this gives

b • ∇a 2 L 2 ≤ R b(•, x 3 ) Ḣ 1 2 h ∇ h b(•, x 3 ) Ḣ 1 2 h ∇a(•, x 3 ) 2 L 2 h dx 3 ≤ ∇a 2 L ∞ v (L 2 h ) R b(•, x 3 ) Ḣ 1 2 h ∇ h b(•, x 3 ) Ḣ 1 2 h dx 3 ≤ ∇a 2 L ∞ v L 2 h b L 2 v Ḣ 1 2 h ∇ h b L 2 v Ḣ 1 2 h .
When s is positive, we have, thanks to Fourier-Plancherel in the vertical variable,

b L 2 v ( Ḣs h ) = R R 2 |ξ h | 2s |F h b(ξ h , x 3 )| 2 dξ h dx 3 ∼ R R 2 |ξ h | 2s | b(ξ h , ξ 3 )| 2 dξ h dξ 3 R 3 |ξ| 2s | b(ξ)| 2 dξ b 2
Ḣs . This concludes the proof of Lemma 2.3.

Conclusion of the proof of Theorem 3. We infer from the above lemma that

(R ε λ (t) • ∇v ε app (t)|R ε λ (t)) Ḣ 1 2 + (v ε app (t) • R ε λ (t)|R ε λ (t)) Ḣ 1 2 ≤ 1 4 ∇R ε λ (t) 2 Ḣ 1 2 + CV ε (t) R ε λ (t) 2 Ḣ .
Together with (2.3), this gives 1 2

d dt R ε λ (t) 2 Ḣ 1 2 + ∇R ε λ (t) 2 Ḣ 1 2 ≤ (C -2λ)V ε (t) R ε λ (t) 2 Ḣ 1 2 + Ce λI 0 R ε λ (t) Ḣ 1 2 ∇R ε λ (t) 2 Ḣ 1 2 + C F ε (t) 2 Ḣ .
Choosing λ such that C -2λ is negative, we infer that

d dt R ε λ (t) 2 Ḣ 1 2 + (1 -Ce λI 0 ) ∇R ε λ (t) 2 Ḣ 1 2 ≤ C F ε (t) 2 Ḣ 1 2 .
Since R ε (0) = 0, we get, as long as R ε λ (t) Ḣ 1 2 is less or equal to 1/2Ce -λI 0 , that

R ε λ (t) 2 Ḣ 1 2 + 1 2 t 0 ∇R ε λ (t ′ ) 2 Ḣ 1 2 dt ′ ≤ C v 0 ,w 0 ε 1 3 .
We therefore obtain that R ε goes to zero in 2 ). That implies that u ε remains close for all times to v ε app , which in particular implies Theorem 3.

L ∞ (R + ; Ḣ 1 2 ) ∩ L 2 (R + ; Ḣ 3

Estimates on the approximate solution

In this section we shall prove Lemma 2.1 stated in the previous section. The proof of the lemma is achieved by obtaining estimates on v, stated in the next lemma, as well as on w ε (see Lemma 3.2 below).

Lemma 3.1. Let v h be a solution of the system (N S2D 3 ). Then, for any s greater than -1 and any α ∈ N 3 , we have, for any y 3 in R and for any positive t,

∂ α v h (t, •, y 3 ) 2 Ḣs h + t 0 ∂ α ∇ h v h (t ′ , •, y 3 ) 2 Ḣs h dt ′ ≤ C v 0 (y 3 ),
where

C v 0 (•) belongs to L 1 ∩ L ∞ (R)
and its norm is controled by a constant C v 0 .

Proof. For s = 0 and α = 0, the estimate is simply the classical L 2 -energy estimate with y 3 as a parameter: writing v = (v h , 0) we have

(3.1) v(t, •, y 3 ) 2 L 2 h + 2 t 0 ∇ h v(t ′ , •, y 3 ) 2 L 2 h dt ′ = v 0 (•, y 3 ) 2 L 2 h .
In the case when α = 0, the estimate (i) in Lemma 1.1 of [START_REF] Chemin | Remarques sur l'existence pour le système de Navier-Stokes incompressible[END_REF] gives, for any s greater than -1,

1 2 d dt v(t, •, y 3 ) 2 Ḣs h + ∇ h v(t, •, y 3 ) 2 Ḣs h ≤ C ∇ h v(t, •, y 3 ) L 2 h v(t, •, y 3 ) Ḣs h ∇ h v(t, •, y 3 ) Ḣs h . We infer that d dt v(t, •, y 3 ) 2 Ḣs h + ∇ h v(t, •, y 3 ) 2 Ḣs h ≤ C ∇ h v(t, •, y 3 ) 2 L 2 h v(t, •, y 3 ) 2 Ḣs h .
Gronwall's lemma ensures that

v(t, •, y 3 ) 2 Ḣs h + t 0 ∇ h v(t ′ , •, y 3 ) 2 Ḣs h dt ′ ≤ v 0 (•, y 3 ) 2 Ḣs h exp C t 0 ∇ h v(t ′ , •, y 3 ) 2 L 2 h dt ′ .
The energy estimate (3.1) implies that

v(t, •, y 3 ) 2 Ḣs h + t 0 ∇ h v(t ′ , •, y 3 ) 2 Ḣs h dt ′ ≤ v 0 (•, y 3 ) 2 Ḣs h exp C v 0 2 L ∞ v L 2 h .
This proves the lemma in the case when α = 0. Let us now turn to the general case, by induction on the length of α. It is clear that in the proof, we can restrict ourselves to the case when s ∈] -1, 1[. Let us assume that, for some k ∈ N,

(3.2) ∀s ∈] -1, 1[, |α|≤k ∂ α v(t, •, y 3 ) 2 Ḣs h + t 0 ∂ α ∇ h v(t ′ , •, y 3 ) 2 Ḣs h dt ′ ≤ C k,v 0 (y 3 ), with C k,v 0 (•) ∈ L 1 ∩ L ∞ (R).
Thanks to the Leibnitz formula we have, for |α| ≤ k + 1,

∂ t ∂ α v h + v h • ∇ h ∂ α v h -∆ h ∂ α v h = -∇ h p α - β≤α β =α C β α ∂ α-β v h • ∇ h ∂ β v h .
Performing a Ḣs h energy estimate in the horizontal variable and using the estimate (2.2) in the case when d = 2 gives 1 2

d dt ∂ α v(t, •, y 3 ) 2 Ḣs h + ∇ h ∂ α v(t, •, y 3 ) 2 Ḣs h ≤ C ∇ h v(t, •, y 3 ) L 2 h ∂ α v(t, •, y 3 ) Ḣs h ∇ h ∂ α v(t, •, y 3 ) Ḣs h +C α β≤α β =α ∂ α-β v h (t, •, y 3 ) • ∇ h ∂ β v h (t, •, y 3 ) ∂ α vh(t, •, y 3 ) Ḣs h .
To estimate the last term, we shall treat differently the case |β| = 0 and |β| = 0. In the first case, we notice first that when s = 0, laws of product for Sobolev spaces in R 2 give

∂ α v h (t, •, y 3 ) • ∇ h v h (t, •, y 3 ) ∂ α v h (t, •, y 3 ) L 2 h ∂ α v h (t, •, y 3 ) 2 Ḣ 1 2 ∇ h v h (t, •, y 3 ) L 2 ∂ α v h (t, •, y 3 ) L 2 h ∇ h ∂ α v h (t, •, y 3 ) L 2 h ∇ h v h (t, •, y 3 ) L 2 h .
If s > 0, then again laws of product for Sobolev spaces in R 2 give, for s ∈]0, 1[,

∂ α v h (t, •, y 3 ) • ∇ h v h (t, •, y 3 ) ∂ α v(t, •, y 3 ) Ḣs h ∂ α v h Ḣs h ∇ h v h L 2 h ∇ h ∂ α v h Ḣs h , whereas if -1 < s < 0, ∂ α v h (t, •, y 3 ) • ∇ h v h (t, •, y 3 ) ∂ α v(t, •, y 3 ) Ḣs h ∇ h ∂ α v h Ḣs h ∇ h v h L 2 h ∂ α v h Ḣs h .
So in any case we have

∂ α v h (t, •, y 3 ) • ∇ h v h (t, •, y 3 ) ∂ α v(t, •, y 3 ) Ḣs h ≤ 1 4 ∇ h ∂ α v h 2 Ḣs h + C ∇ h v h 2 L 2 h ∂ α v h 2 Ḣs h .
Now let us consider the case when |β| = 0. As the horizontal divergence of v is identically 0, we have

∂ α-β v h • ∇ h ∂ β v h ∂ α v(t, •, y 3 ) Ḣs h ≤ ∂ α-β v h (t, •, y 3 )⊗∂ β v h (t, •, y 3 ) Ḣs h ∇ h ∂ α v(t, •, y 3 ) Ḣs h .
Laws of product for Sobolev spaces in R 2 give, for s ∈] -1, 1[,

∂ α-β v h ⊗ ∂ β v h Ḣs h ≤ C ∂ α-β v h Ḣs ′ h ∂ β ∇ h v h Ḣs-s ′ h ,
where s ′ is chosen so that s < s ′ < 1.

Finally we deduce that

d dt ∂ α v(t, •, y 3 ) 2 Ḣs h + ∇ h ∂ α v(t, •, y 3 ) 2 Ḣs h ≤ C ∇ h v 2 L 2 h ∂ α v 2 Ḣs h + C α β≤α β / ∈{0,α} ∂ α-β v(t, •, y 3 ) Ḣs ′ h ∂ β ∇ h v(t, •, y 3 ) Ḣs-s ′ h ∇ h ∂ α v(t, •, y 3 ) Ḣs h .
Gronwall's lemma together with the induction hypothesis (3.2) implies that

|α|=k+1 ∂ α v(t, •, y 3 ) 2 Ḣs h + t 0 ∂ α ∇ h v(t ′ , •, y 3 ) 2 Ḣs h dt ′ |α|=k+1 ∂ α v 0 (•, y 3 ) 2 Ḣs h + C k,v 0 (y 3 ) exp C k t 0 ∇ h v(t ′ , •, y 3 ) 2 L 2 h dt ′ .
The L 2 energy estimate (3.1) allows to conclude the proof of Lemma 3.1.

From this lemma, we deduce the following corollary.

Corollary 3.1. Let v h be a solution of the system (N S2D 3 ). Then, for any non negative σ, we have

v h L 2 (R + ; Ḣσ (R 3 )) ≤ C v 0 and ∂ α v h L 2 (R + ;L ∞ v Ḣσ h ) ≤ C v 0 .
Proof. To start with, let us assume σ > 0. Lemma 3.1 applied with s = σ -1 implies that

(3.3) ∀σ > 0 , ∀α ∈ N , ∂ α v h L 2 (R + ;L 2 v Ḣσ h ) ≤ C v 0 .
Then, for any non negative σ, we have

∂ α v(t, •, y 3 ) 2 Ḣσ h = 2 y 3 -∞ (∂ 3 ∂ α v(t, •, y ′ 3 )|∂ α v(t, •, y ′ 3 ) Ḣσ h dy ′ 3 ≤ 2 ∂ 3 ∂ α v h (t, •) L 2 v Ḣσ h ∂ α v h (t, •) L 2 v Ḣσ h
By the Cauchy-Schwarz inequality, we have

∀σ ≥ 0 , ∀α ∈ N , ∂ α v h L 2 (R + ;L ∞ v Ḣσ h ) ≤ ∂ 3 ∂ α v h 1 2 L 2 (R + ;L ∞ v Ḣσ h ) ∂ α v h 1 2 L 2 (R + ;L ∞ v Ḣσ h ) . From (3.3), we infer (3.4) ∀σ > 0 , ∀α ∈ N , ∂ α v h L 2 (R + ;L ∞ v Ḣσ h ) ≤ C v 0 . Now,
by interpolation, it is enough to prove the first inequality with σ = 0. The system (N S2D 3 ) can be written

∂ t v -∆ h v = f v |t=0 = v 0 (•, y 3 ) with f def = 1≤j,k≤2 Q j,k (D)(v j v k ).
where Q j,k are homogenenous smooth Fourier multipliers of order 1. By Sobolev embeddings in R 2 , we get, for any

y 3 in R, v(•, y 3 ) L 2 (R + × R 2 ) ≤ v 0 (•, y 3 ) Ḣ-1 h + f (•, y 3 ) L 1 (R + ; Ḣ-1 h ) ≤ v 0 (•, y 3 ) Ḣ-1 h + C v(•, y 3 ) 2 L 2 (R + ; Ḣ 1 2 h ) ≤ v 0 (•, y 3 ) Ḣ-1 h + C v(•, y 3 ) L 2 (R + ; Ḣ 1 2 h ) sup y 3 v(•, y 3 ) L 2 (R + ; Ḣ 1 2 h )
.

As sup y 3 v(•, y 3 )

L 2 (R + ; Ḣ 1 2 h ) ≤ v L 2 (R + ;L ∞ v Ḣ 1 2 h )
, we infer from (3.4)

v 2 L 2 (R + × R 3 ) v 0 2 L 2 v Ḣ-1 h + C v 0 v 2 L 2 (R + ;L 2 v Ḣ 1 2 h ) ≤ C v 0 .
The corollary is proved.

Finally we have the following estimate on w ε . Lemma 3.2. Let w ε be a solution of the system (T ε v ). Then, for any s greater than -1 and any α ∈ N 3 and for any positive t, we have

∂ α w ε (t, •) 2 L 2 v Ḣs h + t 0 ∂ α ∇ h w ε (t ′ , •) 2 L 2 v Ḣs h dt ′ ≤ C v 0 ,w 0 .
Proof. We shall only sketch the proof, as it is very close to the proof of Lemma 3.1 which was carried out above. The only difference is that the horizontal divergence of w does not vanish identically, but that will not change very much the estimates. We shall only write the proof in the case when α = 0 and -1 < s < 1, and leave the general case to the reader. Using Lemma 1.1 of [START_REF] Chemin | Remarques sur l'existence pour le système de Navier-Stokes incompressible[END_REF] we have, for any y 3 in R,

v h (t, •, y 3 ) • ∇ h w ε (t, •, y 3 )|w ε (t, •, y 3 ) Ḣs h ≤ C ∇ h v(t, •, y 3 ) L 2 h ∇ h w ε (t, •, y 3 ) Ḣs h w ε (t, •, y 3 ) Ḣs h . Thus we get 1 2 d dt w ε (t) 2 L 2 v Ḣs h + ∇ h w ε (t) 2 L 2 v Ḣs h ≤ 1 4 ∇ h w ε (t) 2 L 2 v Ḣs h + C ∇ h v h (t) 2 L ∞ v L 2 h w ε (t) 2 L 2 v Ḣs h -ε 2 R (∂ 3 p 1 (t, •, y 3 )|w ε,3 (t, •, y 3 )) Ḣs h dy 3 - R (∇ h p 1 (t, •, y 3 )|w ε,h (t, •, y 3 )) Ḣs h dy 3 .
By integration by parts we have, thanks to the divergence free condition on w ε , -

R (∂ 3 p 1 (t, •, y 3 )|w ε,3 (t, •, y 3 )) Ḣs h dy 3 = R (p 1 (t, •, y 3 )|∂ 3 w ε,3 (t, •, y 3 )) Ḣs h dy 3 = - R (p 1 (t, •, y 3 )| div h w ε,h (t, •, y 3 )) Ḣs h dy 3 .

By definition of the inner product of Ḣs

h , we get - R (∂ 3 p 1 (t, •, y 3 )|w ε,3 (t, •, y 3 )) Ḣs h dy 3 = R (∇ h p 1 (t, •, y 3 )|w ε,h (t, •, y 3 )) Ḣs h dy 3 .
Thus we have 1 2

d dt w ε (t) 2 L 2 v Ḣs h + ∇ h w ε (t) 2 L 2 v Ḣs h ≤ 1 4 ∇ h w ε (t) 2 L 2 v Ḣs h + C ∇ h v h (t) 2 L ∞ v L 2 h w ε (t) 2 L 2 v Ḣs h -(1 -ε 2 ) R (∇ h p 1 (t, •, y 3 )|w ε,h (t, •, y 3 )) Ḣs h dy 3 .

Now we notice that

-(ε 2 ∂ 2 3 + ∆ h )p 1 = div(v h • ∇ h w ε ) = div 2 j=1 ∂ j (v j w ε ),
which can be written in the simpler way

-(ε 2 ∂ 2 3 + ∆ h )p 1 = div h N h with N h = v h • ∇ h w ε,h + ∂ 3 (w ε,3 v h ).
It is easy to check that for any σ ∈ R,

(3.5) ∇ h p 1 L 2 v Ḣσ h N h L 2 v Ḣσ h ,
simply by noticing that

∇ h p 1 2 L 2 v Ḣσ h ∼ |ξ h | 2σ+2 | p 1 (ξ)| 2 dξ ∼ |ξ h | 2σ+4 | N h (ξ)| 2 dξ (|ξ h | 2 + ε 2 |ξ 3 | 2 ) 2 N h 2 L 2 v Ḣσ h .
We infer from (3.5) that

∇ h p 1 L 2 v Ḣσ h ≤ v h • ∇ h w ε,h L 2 v Ḣσ h + ∂ 3 (w ε,3 v h ) L 2 v Ḣσ h ≤ v h • ∇ h w ε L 2 v Ḣσ h + w ε,3 ∂ 3 v L 2 v Ḣσ h + v div h w ε,h L 2 v Ḣσ h .
We claim that for all -1 < s < 1,

I h def = R |(∇ h p 1 (t, •, y 3 )|w ε (t, •, y 3 ))| Ḣs h dy 3 ≤ 1 4 ∇ h w ε 2 L 2 v Ḣs h + C w ε 2 L 2 v Ḣs h ∇v h 2 L ∞ v L 2 h (1 + v h 2 L ∞ v L 2 h
). (3.6) Let us prove the claim. Suppose first that s = 0. Then a product law gives

I h ≤ w ε L 2 v Ḣ 1 2 h ∇ h p 1 L 2 v Ḣ-1 2 h w ε L 2 v Ḣ 1 2 h v h L ∞ v Ḣ 1 2 h ∇ h w ε L 2 (R 3 ) + w ε 2 L 2 v Ḣ 1 2 h ∂ 3 v L ∞ v L 2 h .
By interpolation, we get

I h ≤ ∇ h w ε 3 2 L 2 (R 3 ) w ε 1 2 L 2 (R 3 ) v h 1 2 L ∞ v L 2 h ∇ h v h 1 2 L ∞ v L 2 h + w ε L 2 (R 3 ) ∇ h w ε L 2 (R 3 ) ∂ 3 v L ∞ v L 2 h .
The claim in the case s = 0 follows from a convexity inequality, which gives

I h ≤ 1 4 ∇ h w ε 2 L 2 (R 3 ) + C w ε 2 L 2 (R 3 ) (1 + v 2 L ∞ v L 2 h ) ∇v 2 L ∞ v L 2 h .
In the case when 0 < s < 1, then we use the product rule

∇ h p 1 L 2 v Ḣs-1 h v h L ∞ v Ḣ 1 2 h ∇ h w ε L 2 v Ḣs-1 2 h + w ε L 2 v Ḣs h ∇v L ∞ v L 2 h along with the fact that I h ≤ ∇ h p 1 L 2 v Ḣs-1 h ∇ h w ε L 2 v Ḣs h .
Finally in the case when -1 < s < 0, we write

I h ≤ w ε • ∇v h L 2 v Ḣs h w ε L 2 v Ḣs h + w ε • v h L 2 v Ḣs h ∇ h w ε L 2 v Ḣs h ∇v h L ∞ v L 2 h w ε L 2 v Ḣs h ∇ h w ε L 2 v Ḣs h + v h L ∞ v Ḣ 1 2 h w ε L 2 v Ḣs+ 1 2 h ∇ h w ε L 2 v Ḣs h .
The claim (3.6) follows by interpolation.

Using that result we obtain that

d dt w ε (t) 2 L 2 v Ḣs h + ∇ h w ε (t) 2 L 2 v Ḣs h ∇v h (t) 2 L ∞ v L 2 h w ε (t) 2 L 2 v Ḣs h (1 + v h (t) 2 L ∞ v L 2 h )
and we conclude by a Gronwall lemma. Indeed we get that

w ε (t) 2 L 2 v Ḣs h + t 0 ∇ h w ε (t ′ ) 2 L 2 v Ḣs h dt ′ ≤ w 0 2 L 2 v Ḣs h × exp C t 0 ∇v h (t ′ ) 2 L ∞ v L 2 h (1 + v h (t ′ ) 2 L ∞ v L 2 h ) dt ′ .
But by the basic energy estimate (3.1), we have

v h (t) L ∞ v L 2 h ≤ v 0 L ∞ v L 2 h .
Moreover, Corollary 3.1 implies that

∇v h ∈ L 2 (R + ; L ∞ v L 2 h
), so Lemma 3.2 is proved in the case when α = 0. The case when α is positive is an easy adaptation of the proof of Lemma 3.1; it is left to the reader.

Clearly Lemmas 3.1 and 3.2 allow to obtain Lemma 2.1 stated in the previous section.

The estimate of the error term

In this section we shall prove Lemma 2.2 stated above. We need to write down precisely the equation satisfied by the remainder term R ε , and to check that the forcing terms appearing in the equation can be made small. Let us recall that v ε app (t, x) = ((v h , 0) + ε(w ε,h , ε -1 w ε,3 ))(t, x h , εx 3 ) and p ε app (t, x) = (p 0 + εp 1 )(t, x h , εx 3 ). It is an easy computation to see that

∂ t v ε app + v ε app • ∇v ε app -∆v ε app (t, x h , x 3 ) = (∂ t v h + v h • ∇ h v h -∆ h v h , 0)(t, x h , εx 3 ) + ε ∂ t w ε,h + v h • ∇ h w ε,h -∆ h w ε,h -ε 2 ∂ 2 3 w ε,h , 0 (t, x h , εx 3 ) + 0, ∂ t w ε,3 + v h • ∇ h w ε,3 -∆ h w ε,3 -ε 2 ∂ 2 3 w ε,3 (t, x h , εx 3 ) + ε F ε (t, x h , εx 3 )
where

F ε (t, x h , y 3 ) def = (εw ε • ∇w ε,h , w ε • ∇w ε,3 ) + (w ε • ∇v h , 0) + ε(∂ 2 3 v h , 0) (t, x h , y 3 ).
In order to simplify the notation, let us write

F ε = F ε,1 + F ε,2 with F ε,1 def = (εw ε • ∇w ε,h , w ε • ∇w ε,3 ) + (w ε • ∇v h , 0) and F ε,2 def = ε(∂ 2 3 v h , 0
). Recalling the equations satisfied by v h and w ε , we infer that

∂ t v ε app + v ε app • ∇v ε app -∆v ε app (t, x h , x 3 ) = -∇p ε app + εG ε (t, x h , εx 3 ) with G ε (t, x h , y 3 ) def = F ε + (0, ∂ 3 p 0 ) (t, x h , y 3 ) and F ε (t, x h , x 3 ) def = εG ε (t, x h , εx 3 ). Denot- ing q ε = p ε -p ε app , we infer that ∂ t R ε + R ε • ∇R ε + v ε app • ∇R ε + R ε • ∇v ε app -∆R ε = -∇q ε + F ε .
So Lemma 2.2 will be established as soon as we prove that

F ε L 2 (R + ; Ḣ-1 2 (R 3 )) ≤ C v 0 ,w 0 ε 1 3 .
The forcing term F ε consists in three different types of terms: a pressure term involving p 0 , a linear term ε 2 ∂ 2 3 v h (t, x h , εx 3 ), and finally a number of nonlinear terms, defined as ε F ε,1 (t, x h , εx 3 ) above. Each of these contributions will be dealt with separately. Let us start by the pressure term.

Lemma 4.1. The following estimate holds:

ε (∂ 3 p 0 )(t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ≤ C v 0 ,w 0 ε 1 3 .
Proof. We define P ε 0 (t, x h , x 3 ) def = (∂ 3 p 0 )(t, x h , εx 3 ). Sobolev embeddings enable us to write

P ε 0 L 2 (R + ; Ḣ-1 2 (R 3 )) P ε 0 L 2 (R + ;L 3 2 (R 3 )) ε -2 3 ∂ 3 p 0 L 2 (R + ;L 3 2 (R 3 ))
.

Recalling that

p 0 = (-∆ h ) -1 2 j,k=1 ∂ j ∂ k (v j v k ),
we have by Sobolev embeddings,

∂ 3 p 0 L 2 (R + ;L 3 2 (R 3 )) 2 j,k=1 v j ∂ 3 v k L 2 (R + ;L 3 2 (R 3 )) v L ∞ (R + ;L 3 (R 3 )) ∂ 3 v L 2 (R + ;L 3 (R 3 )) v L 2 (R + ;H 1 2 (R 3 )) ∂ 3 v L ∞ (R + ;H 1 2 (R 3 ))
, so we can conclude by Lemma 3.1. This proves Lemma 4.1. Now let us consider the linear term ε 2 ∂ 2 3 v h (t, x h , εx 3 ). The statement is the following.

Lemma 4.2. The following estimate holds:

ε 2 (∂ 2 3 v h )(t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ≤ C v 0 ε 1 2 .
Proof. We have

ε 2 (∂ 2 3 v h )(t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ε ∂ 3 ∂ 3 v h (t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ε (∂ 3 v h )(t, x h , x 3 ) L 2 (R + ; Ḣ 1 2 (R 3 )) ,
A computation in Fourier variables shows that, for any function a on R 3 , we have

a(x h , εx 3 ) 2 Ḣ 1 2 (R 3 ) = 1 ε 2 R 3 a ξ h , ξ 3 ε 2 |ξ| dξ ≤ 1 ε R 3 a ξ h , ξ 3 ε 2 |ξ h | dξ h dξ 3 ε + R 3 a ξ h , ξ 3 ε 2 |ξ 3 | ε dξ h dξ 3 ε •
By interpolation, we deduce that

a(x h , εx 3 ) 2 Ḣ 1 2 (R 3 ) ≤ 1 ε a L 2 (R 3 ) ∇ h a L 2 (R 3 ) + a L 2 (R 3 ) ∂ 3 a L 2 (R 3 ) .
Applying this inequality with a = ∂ 3 v, we get

ε 2 (∂ 2 3 v h )(t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ε 1 2 ∂ 3 v(t) 1 2 L 2 (R + ;L 2 (R 3 )) ∂ 3 ∇ h v(t) 1 2
L 2 (R + ;L 2 (R 3 ))

+ ε ∂ 3 v(t) 1 2 L 2 (R + ;L 2 (R 3 )) ∂ 2 3 v(t) 1 2
L 2 (R + ;L 2 (R 3 ))

≤ C v 0 ε 1 2
by Lemma 3.1. This proves Lemma 4.2. Now let us turn to the nonlinear terms composing F ε , which we denoted above ε F ε,1 .

Lemma 4.3. The following estimate holds:

ε F ε,1 (t, x h , εx 3 ) L 2 (R + ; Ḣ-1 2 (R 3 )) ≤ C v 0 ,w 0 ε 1 3 .
Proof. We recall that F ε,1 = (εw ε • ∇w ε,h , w ε • ∇w ε,3 ) + (w ε • ∇v h , 0).

Notice that for all functions a and b and any 1 ≤ j ≤ 3,

a∂ j b L 2 (R + ; Ḣ-1 2 (R 3 )) a∂ j b L 2 (R + ;L 3 2 (R 3 )) a L ∞ (R + ;L 3 (R 3 )) ∂ j b L 2 (R + ;L 3 (R 3 )) .
Defining c ε (t, x h , x 3 ) = (a∂ j b)(t, x h , εx 3 ) this implies that

c ε L 2 (R + ; Ḣ-1 2 (R 3 )) ε -2 3 a L ∞ (R + ; Ḣ 1 2 (R 3 )) ∂ j b L 2 (R + ; Ḣ 1 2 (R 3 ))
.

We can apply that inequality to a and b equal to v or w ε , due to the results proved in Section 3, and the lemma follows.

  and generates a unique global solution to (N S).