Marcos Vinícius

Santos Issa

Americo Cunha
email: americo@ime.uerj.br

Francisco Soeiro
email: soeiro@uerj.br

Anderson Pereira
email: anderson@puc-rio.br

Marcos Vinicius
email: marcosviniciusissa@gmail.com

Francisco José Da Cunha

Pires Soeiro

Structural optimization using the cross-entropy method

Keywords: structural optimization, nonlinear optimization, cross-entropy method

Introduction

Structural optimization is an engineering discipline that deals with the minimization of a suitable performance function, seeking to improve the response of a mechanical system of interest. Frequently, the aim is to minimize the structure weight, respecting a suitable criteria of structural integrity. Due to complex geometric configurations and the use of advanced materials, whose behavior is extremely non-linear, this task can be too challenging, requiring the use of very efficient optimization algorithms [START_REF] Deaton | A survey of structural and multidisciplinary continuum topology optimization: post[END_REF][START_REF] Saitou | A Survey of Structural Optimization in Mechanical Product Development[END_REF][START_REF] Zavala | A survey of multiobjective metaheuristics applied to structural optimization[END_REF].

This work aims to test the effectiveness and robustness of the cross-entropy (CE) method [START_REF] Kroese | Cross-Entropy Method[END_REF][START_REF] Rubinstein | Simulation and the Monte Carlo Method[END_REF], a relatively new optimization technique, in the context of structural optimization. For this purpose, a structural optimization problem that seeks to minimize the weight of a two-dimensional truss, ensuring its structural integrity, is employed as benchmark.

2

The rest of the paper is organized as follows. Section 2 presents the mechanical system of interest and the model equations. In section 3 the reader is introduced to the addressed structural optimization problem and the employed optimization techniques. Numerical results are presented and discussed in section 4, while final considerations are made in section 5.

Mathematical modeling 2.1 Structural model

The structural system of interest in this work is two-dimensional truss illustrated in Figure 1, which also show the geometric dimensions of the structure and the employed coordinate system. This truss consists of 11 bars, labeled from 1 to 11, connected through 6 nodes, labeled from 1 to 6, each one with two degrees of freedom, u e for the horizontal displacement of bar e and v e for the corresponding vertical displacement, where e = 1, • • • , 11. These bars are made of a single material, with density ρ = 7900 kg and elastic modulus E = 210 GP a. The kinematic constraints are due to the fixed support on node 1 and the roller support on node 5. Three vertical loads are applied at the nodes 2, 4 and 6, with magnitudes respectively equal to 50 kN , 100 kN and 50 kN . The choice of this structural system is motivated by the fact that it is a standard finite element benchmark, which can be seen in section 4.6 of the reference [START_REF] Ferreira | MATLAB Codes for Finite Element Analysis Solids and Structures[END_REF].

Equilibrium equations

The equilibrium equations are obtained from the principle of virtual work, being written as the following matrix system

K u = f , (1)
where K is the stiffness matrix, u is the displacement vector and f is force vector, which are respectively defined by

u = u 1 v 1 u 2 v 2 u 3 v 3 u 4 v 4 u 5 v 5 u 6 v 6 T
, and f = 0 0 0 -50 0 0 0 -100 0 0 0 -50

T kN . (2)
Note that due to kinematic constraints, u 1 = v 1 = v 5 = 0. Besides that, the stiffness matrix can be written as

K = N e=1 K e , (3)
where N = 11 is the the number of bars and K e is the elementary stiffness matrix in global coordinates. In local coordinates the elementary stiffness matrix of the bar e is given by

K e = A e E e L e      cos 2 θ
where A e is the cross-sectional area, E e is the material modulus of elasticity, L e is the element length and θ e is the angle formed between the bar longitudinal axis and the horizontal axis of the reference system (x axis).

Structure mass

Each bar of the truss has a circular tubular cross-section with area is given by A e = 4 d t + t 2 π/4, where d is the external diameter and t is the section thickness. In this way, the mass of bar e is given by m e (d, t) = ρ L e 4 d t + t 2 π/4 and the total mass of the two-dimensional truss is

m(d, t) = N e=1 m e (d, t) = N e=1 ρ L e 4 d t + t 2 π/4.
(5)

Structural integrity criterion

and the local displacement u e is implicitly defined by the local equilibrium equation K e u e = f e , so that the normal stress can also be written as

σ e = E B e K -1 e f e . (7)
The structural integrity criterion employed here states that (in absolute value) the normal stress at each bar, defined by Eq.( 7), is less than or equal to the material yield stress S Y = 205 M P a. Once σ e depends on K, that depends on A e (d, t), the normal stress is a function of d and t and the integrity criterion can be written as

|σ e (d, t)| -S y ≤ 0, e = 1, • • • , N. (8)
3

Structural optimization problem

The structural optimization problem considered here aims to minimize the structure mass, Eq.( 5), using d and t as design variables, considering as constraints the inequalities in [START_REF] Zavala | A survey of multiobjective metaheuristics applied to structural optimization[END_REF], and a limited set of values for d and t, i.e.,

d min ≤ d ≤ d max and t min ≤ t ≤ t max . (9)
Note that, due to the quadratic terms in the objective function [START_REF] Kroese | Cross-Entropy Method[END_REF], and the inverse dependence of the constraints in [START_REF] Zavala | A survey of multiobjective metaheuristics applied to structural optimization[END_REF] with the design variables, this optimization problem is nonlinear.

Mathematical formulation

The optimization problem seeks to find a vector x = (d , t ) such that

γ = max S(x ), ( 10
)
where γ is the maximum value of the performance function S(x), that is a penalization of the constrained optimization problem defined by ( 5), ( 8) and (9).

Solution algorithms

Three different optimization techniques are employed in this work to deal with the nonlinear optimization problem in (10), nominally: (i) sequential quadratic programming (SQP), (ii) genetic algorithm (GA), and (iii) cross-entropy (CE) method.

SQP [START_REF] Bonnans | Numerical Optimization: Theoretical and Practical Aspects[END_REF] and GA [START_REF] Kramer | Genetic Algorithm Essentials[END_REF] are well-known methods in the structural optimization community. For this reason, and for sake of space limitation, they are not reviewed here.

On the other hand, CE method [START_REF] Kroese | Cross-Entropy Method[END_REF], although being widely used by the combinatorial optimization community, is still little used in continuous optimization problems, such as the one defined by (10). To the best of the authors' knowledge, this is the first time the CE method is used in the context of structural optimization.

The CE method is a heuristic optimization technique based on the minimization of Kullback-Leibler divergence, where the vector x is randomized following a probability ---→ γ and f (x, v l ) a.s.

---→ δ (x -x ), i.e., the family of distributions f(• , v) tends towards a point mass distribution, centered on the global optimum for the optimization problem.

The algorithm can be summarized as follows: (i) Define the number of samples N s , the number of elite samples N e , a convergence tolerance tol, the maximum of levels l max , a family of probability distributions f (•, v), an initial vector of parameters v 0 for f and set the level counter l = 0; (ii

) Update level l = l +1; (iii) Generate X 1 , • • • , X N s (iid) samples from f (•, v l-1 ); (iv) Evaluate performance function S(X n ) at samples X 1 , • • • , X N s and sort the results S (1) ≤ • • • ≤ S (N s ) ; (v) Update estimators γ l and v l ; (vi) Repeat (ii) - (v)
while a stopping criterion is not met. For further details on CE method the reader is encouraged to see [START_REF] Rubinstein | Simulation and the Monte Carlo Method[END_REF].

Numerical experiments

In the numerical experiments reported below, a penalty factor p = 10 is employed and the reference results are computed with SQP5 and GA 6 . The design variables are limited to the region 50 mm ≤ d ≤ 100 mm and 5 mm ≤ t ≤ 20 mm. The CE algorithm7 uses a Gaussian distribution truncated over this region.

Finite element analysis

In order to gain some insight on the truss behavior, a finite element analysis (FEA) is conducted before the structural optimization process. For this, the design variables are assumed as equal to (d, t) = (100, 20) mm. This FEA reveals that in no bar the structural integrity criterion has been violated, as can be noted in Table 1. The mass total of the truss in this case is m = 1979 kg.

Optimization experiments

In order to evaluate CE accuracy, a comparison with the reference results obtained via SPQ and GA is done in Table 2. The reader can see that CE performed so well as the other two algorithms, converging with a tolerance of 10 -6 in only 13 levels (iterations). The same table shows that CE method is computationally efficient, once its CPU time is of the same order of magnitude as the SQP, and an order of magnitude smaller than GA. This is very impressive, since SPQ is a gradient-based method, whereas CE has no information about objective function and constraints derivatives. This result shows that CE can be a very competitive heuristic option for structural optimization. An illustration of CE sampling of the domain, at different levels (iterations), is presented in Figure 2, where the red cross is the SQP reference solution, and the magenta cross corresponds to CE solution.

Figure 1 :

 1 Figure 1: Illustration of the two-dimensional truss (adpated from reference [3]).

  By Hooke's Law the normal stress at the bar e is σ e = E B e u e , where B e = 1 L e -cos θ e -sin θ e cos θ e sin θ e ,

Figure 2 :

 2 Figure 2: Illustration of CE sampling of the domain at different levels (iterations). The red cross is the SPQ reference solution, and the magenta cross corresponds to CE solution.

Table 1 :

 1 Normal stress at each bar of the two-dimensional truss.

	bar	1	2	3	4	5	6	7	8	9	10	11
	σ e (MPa) -28.8 16.7 12.1 -6.0 -33.4 -12.1 12.1 -33.4 -6.0 16.7 -28.8
	distribution f (•, v) and the optimization problem associated the to the calculation of a
	rare-event probability. The idea behind this method is to generate a sequence of estimators ( γ l , v l ) such that γ l a.s.

6 Table 2 :

 62 Comparison between the results obtained with different optimization techniques.

	Method mass (kg) d (mm) t (mm) CPU time* (sec)
	SQP	264	54.4	5.0	0.35
	GA	264	50.2	5.4	9.20
	CE	265	50.8	5.4	0.48
		*MacBook Pro "Core i7" 2.2 GHz 16GB 1333 MHz DDR3

fmincon routine from MATLAB with default parameters.

ga routine from MATLAB with default parameters, and a population with 25 individuals.

CE control parameters are N s = 25, N e = 3, tol = 10 -6 and lmax = 100.

Acknowledgments

The authors are indebted to the Brazilian agencies CNPq, CAPES, and FAPERJ for the financial support given to this research.

Final remarks

This work addresses a numerical study evaluating the effectiveness and robustness of the cross-entropy method in the context of structural optimization. The results show that the evaluated method is very competitive, having a much better performance than genetic algorithm in terms of processing time. In comparison to the sequential quadratic programming, cross-entropy has comparable processing time, proving to be a very appealing tool for optimization problems, especially when the use of gradients is impractical.


Luck Darnière

On the model-completion of Heyting algebras

published or not. The documents may come

Introduction

It is known since [START_REF] Pitts | On an interpretation of second-order quantification in first-order intuitionistic propositional logic[END_REF] that the second-order intuitionist propositional calculus (IPC 2 ) is interpretable in the first-order one (IPC). This proof-theoretic result, after translation in model-theoretic terms, ensures that the theory of Heyting algebras has a model-completion (see [START_REF] Ghilardi | Model completions and r-Heyting categories[END_REF]). It has been followed by numerous investigations on uniform interpolation, intermediate logics and model-theory ( [START_REF] Kremer | Propositional quantification in the topological semantics for S4[END_REF], [Po l98], [START_REF] Ghilardi | Unification in intuitionistic logic[END_REF], [START_REF] Bílková | Uniform interpolation and propositional quantifiers in modal logics[END_REF], [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF], [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF], among others). In particular, it is proved in [START_REF] Ghilardi | Model completions and r-Heyting categories[END_REF] that each of the height varieties of Heyting algebras which has the amalgamation property also has a model-completion. In spite of all this work, no intuitively meaningful axiomatization was known by now for the model-completion of the theory of Heyting algebras. So the algebraic nature of its models, the existentially closed Heyting algebras, remains quite mysterious. Our goal in this paper is to fill this lacuna.

Recently, van Gool and Reggio have given in [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF] a different proof of Pitts' result, by showing that it can easily be derived from the following "Open Mapping Theorem".

Theorem 1.1 (Open Mapping) Every continuous p-morphism between finitely co-presented Esakia spaces is an open map.

That both results are tightly connected is further illustrated by the approach in this paper: we prove that, reciprocally, the Open Mapping Theorem can easily be derived from Pitts' result.

This, and our axiomatization of the model-completion of the theory of Heyting algebras, is based on a new property of existentially closed Heyting algebras that we introduce here, the "QE property". Its name comes from the following characterisation: a Heyting algebra has the QE property if and only if its complete theory eliminates the quantifiers (Proposition 4.4). The smart reader may observe that, knowing by Pitts' result that the theory of existentially closed Heyting algebras eliminates the quantifiers, it is not an achievement to prove that all its models have the QE property! But things are a bit more complicated: given a model M of a theory T having a model-completion T * , if M |= T * then obviously the theory of M eliminates the quantifiers, however the converse is not true in general. For example every dense Boolean algebra has the QE-property (because the theory of dense Boolean algebras eliminates the quantifiers), but none of them is existentially closed in the class of all Heyting algebras. Moreover the QE-property itself is probably not first-order in general. Our strategy in the present paper is then: firstly to characterize among the Heyting algebras having the QE property, those which are existentially closed; and secondly to prove that the QE-property is first-order axiomatisable in this class. This is done by showing first that a certain Heyting algebra H 0 , obtained by amalgamating appropriately a set of representatives of all the finite Heyting algebras, is existentially closed. By Pitts' result H 0 is then a model of the model-completion of the theory of Heyting algebras, hence it has the QE property. Moreover it is locally finite by construction, and a prime model of this model-completion. Actually it is the only countable and existentially closed Heyting algebra which is locally finite. This paper is organised as follows. We recall the needed prerequisites in Section 2. In Section 3 we construct the prime model H 0 . In Section 4, after introducing the QE property, we use that H 0 is a prime model to prove that a Heyting algebra H is existentially closed if and only if it has the QE property and the "Splitting" and "Density" properties that we introduced in [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF]. In the next Section 5 we show how the Open Mapping Theorem can be derived from this. Finally we turn to explicit elimination. Indeed the elimination of quantifiers is done by Pitts in a very effective way, but it can be somewhat puzzling from an algebraic point of view. So in Section 6 it seemed to us that it could be worth showing how, given a finite system of equations t(p, q) = 1 and s k (p, q) = 1 (for 1 ≤ k ≤ κ), we can use the Open Mapping Theorem to explicitly construct a term ∆ t (p) (the "discriminant" of t) and terms ∇ t,s k (p) for 1 ≤ k ≤ κ (the "co-discriminant" of t and s k ), such that for every tuple ā in a Heyting algebra A, the above system (with parameters ā replacing p), has a solution in an extension of A if and only if ∆ t (ā) = 1 and ∇ t,s k (ā) = 1 for 1 ≤ k ≤ κ. The appendix Section 7 is devoted to the Finite Extension Property, a strengthening of the Finite Model Property of IPC which plays a key role in proving that the Heyting algebra constructed Section 3 is indeed existentially closed.

Remark 1.2 It is claimed in [START_REF] Ghilardi | Model completions and r-Heyting categories[END_REF] that the methods of Pitts, which concern the variety V 1 of all Heyting algebras, apply mutatis mutandis to the variety V 2 of the logic of the weak excluded middle (axiomatized by ¬x ∨ ¬¬x = 1). Consequently all the results presented here for V 1 remain true for V 2 . It suffices to restrict the amalgamation in Section 3 to the finite algebras in V 2 , and to replace the "Density" and "Splitting" axioms for V 1 (D1 and S1 in [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF]) by the corresponding axioms for V 2 (D2 and S2 in [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF]).

Notation and prerequisites

Posets and lattices. For every element a in a poset (E, ≤) we let a↑ = {b ∈ E : a ≤ b} For every subset S of E we let S↑ = s∈S s↑ be the set of elements of E greater than or equal to some element of S. An up-set of E is a set S ⊆ E such that S = S↑. The family of all up-sets of E forms a topology on E that we denote by O ↑ (E).

All our lattices will be assumed distributive and bounded. The language of lattices is then L lat = {0, 1, ∨, ∧}, where 0 stands for the smallest element, 1 for the greatest one, ∨ and ∧ for the join and meet operations respectively. Iterated joins and meets will be denoted ∨ ∨ and ∧ ∧. Of course the order of the lattice is definable by b ≤ a if and only if a ∨ b = a. The language of Heyting algebras is L HA = L lat ∪ {→} where the new binary operation symbol is interpreted as usually by b → a = max c : c ∧ b ≤ a .

Stone spaces and morphisms. The prime filter spectrum, or Stone space, of a distributive bounded lattice A is denoted Spec ↑ A. The Zariski topology on Spec ↑ A is generated by the sets

P ↑ (a) = x ∈ Spec ↑ A : a ∈ x
where a ranges over A. The patch topology is generated by the sets P ↑ (a) and their complements in Spec ↑ A.

Stone's duality states that a → P ↑ (a) is an embedding of bounded lattices (an L lat -embedding for short) of A into O ↑ (Spec ↑ A). If moreover A is a Heyting algebra, it is an embedding of Heyting algebras (an L HA -embedding for short). In particular, for every a, b ∈ A and every

x ∈ Spec ↑ A, a → b ∈ x ⇐⇒ ∀y ≥ x, a ∈ y ⇒ b ∈ y .
Facts 2.1 and 2.2 below are folklore. The reader may refer in particular to [START_REF] Balbes | Distributive lattices[END_REF], chapters III and IV.

Fact 2.1 Every filter is the intersection of the prime filters which contain it.

Given an L lat -morphism f : B → A we let Ker ↑ f = f -1 (1) denote its filter kernel, and f ↑ : Spec ↑ A → Spec ↑ B be the dual map defined by

f ↑ (x) := f -1 (x). Fact 2.2 If f is surjective then f ↑ induces an increasing bijection from Spec ↑ A to {y ∈ Spec ↑ B : Ker ↑ f ⊆ y}.
In Heyting algebras, every congruence comes from a filter. So the classical "Isomorphisms Theorems" of universal algebra can be expressed for morphisms of Heyting algebras (L HA -morphisms for short) in terms of filters, just as analogous statements on morphisms of rings are expressed in terms of ideals. In particular, we will make use of the next property. In that case, such an L HA -morphism g is unique. It is injective if and only if

Ker ↑ f = I.
Esakia spaces and free Heyting algebras. An Esakia space (see [START_REF] Esakia | Topological Kripke models[END_REF]) is a poset X with a compact topology such that: (i) whenever x y in (X, ≤) there is a clopen U ⊆ X that is an up-set for ≤ such that x ∈ U and y / ∈ U ; and (ii) U ↓ is clopen whenever U is a clopen subset of X. Given a Heyting algebra A, its prime filter spectrum ordered by inclusion and endowed with the patch topology is an Esakia space, called the Esakia dual of A. We denote it by X A .

Let p = {p 1 , . . . , p l } be a finite set of variables, F (p) be the free Heyting algebra on p, and X F ( p) its Esakia space. For every l-tuple ā in a Heyting algebra A we let π ā : F (p) → A denote the canonical morphism mapping p to ā. Every formula ϕ(p) in the Intuitionistic Propositional Calculus (IPC) can be read as an L HA -term in the variables p, and conversely. The degree deg ϕ is the maximum number of nested occurrences of → in ϕ. Abusing the notation, we will also consider ϕ as an element of F (p). We let

[[ϕ(p)]] = x ∈ X F ( p) : ϕ(p) ∈ x .
As a set of prime filters, [[ϕ(p)]] is nothing but P ↑ (ϕ(p)). The different notation simply reminds us to consider it as a subset of X F ( p) with the patch topology, instead of a subset of Spec ↑ F (p) with the Zariski topology.

Systems of equations and the Finite Extension Property. Every finite system of equations and negated equations in the variables (p, q), is equivalent to an L HA -formula of the form

S t,s (p, q) = t(p, q) = 1 k≤κ s k (p, q) = 1 .
The degree of S t,s (p, q), with s = (s 1 , . . . , s κ ), is the maximum of the degrees of the IPC formulas t and s k for 1 ≤ k ≤ κ. We will identify every such formula with the corresponding system of equations and negated equations in (p, q), calling S t,s (p, q) itself a system of degree d. Given a tuple ā in a Heyting algebra H, a solution of S t,s (ā, q) is then a tuple b such that H |= S t,s (ā, b).

Theorem 2.4 (Finite Extension Property) Let V be a variety of Heyting algebras having the Finite Model Property. If an existential L HA -formula with parameters in a finite V-algebra A is satisfied in a V-algebra containing A, then it is satisfied in some finite Valgebra containing A.

We will use this improvement of the classical Finite Model Property only for the variety of all Heyting algebras, and for formulas ∃q, S t,s (ā, q). The proof requires some notions of co-dimension coming from [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF]. Since this material is not needed anywhere else in this paper, we delay the proof of the Finite Extension Property to the appendix in Section 7.

Splitting and Density axioms. In [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF] we introduced for co-Heyting algebras the notion of "strong order". It corresponds in Heyting algebras to the following relation. This is a strict order on A \ {1} (not on A because 1 a for every a ∈ A, including a = 1). Above all, we introduced the next two axioms (denoted D1 and S1 in [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF]), which translate to the following ones in Heyting algebras.

[Density] For every a, c such that c a = 1 there exists an element b = 1 such that: c b a

[Splitting] For every a, b 1 , b 2 such that b 1 ∧ b 2 a = 1 there exists a 1 = 1 and a 2 = 1 such that:

a 2 → a = a 1 ≤ b 1 a 1 → a = a 2 ≤ b 2 a 1 ∨ a 2 = b 1 ∨ b 2
The Density axiom clearly says that is a dense order. The Splitting axiom implies the lack of atoms and co-atoms, but it is actually much stronger (and more subtle) than this. For a geometric interpretation of the Splitting Property, we refer the reader to [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF] and [Dar]. The two next properties are theorems 1.1 and 1.2 in [START_REF] Darnière | Model completion of varieties of co-Heyting algebras[END_REF].

Theorem 2.5 Every existentially closed Heyting algebra has the Density and Splitting Properties.

Theorem 2.6 Let H be a Heyting algebra having the Density and Splitting properties. Let A be a finite Heyting subalgebra of H, and B an extension of A. If B is finite then B embeds into H over1 A.

In particular, if H is a non-trivial Heyting algebra (that is 0 = 1 in H) having the Density and Splitting properties, then every finite non-trivial Heyting algebra embeds into H: it suffices to apply Theorem 2.6 to H, B and A = {0, 1}. Using the model-theoretic Compactness Theorem, the next property follows immediately.

Corollary 2.7 Let H be a non-trivial Heyting algebra which has the Density and Splitting properties. If H is ω-saturated then every every finitely generated non-trivial Heyting algebra embeds into H.

The Open Mapping Theorem. Following [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF], for every integer d ≥ 0 and every x, y ∈ X F ( p) we write x ∼ d y if: for every IPC formula t(p) of degree

≤ d, t(p) ∈ x ⇐⇒ t(p) ∈ y. The relations ∼ d define on X F ( p) an ultrametric distance d p(x, y) = 2 -min{d : x ∼ d y} ,
with the conventions that min ∅ = +∞ and 2 -∞ = 0. The topology induced on X F ( p) by this distance is exactly the patch topology (Lemma 8 in [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF]). We let

B p(x, 2 -d ) = y ∈ X F ( p) : d p(x, y) < 2 -d
denote the ball of center x and radius 2 -d . Note that it is clopen and that

y ∈ B p(x, 2 -d ) ⇐⇒ y ∼ d x.
So the balls of radius 2 -d in X F ( p) are the equivalence classes of ∼ d . Recall that, up to intuitionist equivalence, there are only finitely many IPC formulas in p of degree < d. In particular, for every ball B of radius 2 -d there is a pair

(ϕ B , ψ B ) of IPC formulas of degree < d such that B = [[ϕ B ]] \ [[ψ B ]].
We let B d (p) be the set of these balls, and fix for each of them a pair (ϕ B , ψ B ) as above.

Claim 2.8 Let ā be an l-tuple in some Heyting algebra A. For every ball B in

X F ( p) , there is y ∈ B such that Ker ↑ π ā ⊆ y if and only if ϕ B (ā) → ψ B (ā) = 1.
Proof: Replacing A if necessary by the Heyting algebra generated in A by ā, we can assume that π ā is surjective. Note first that for every IPC formula θ( b) and every y ∈ X F ( p) containing Ker ↑ π ā,

θ(p) ∈ y ⇐⇒ θ(ā) ∈ π ā(y).
In particular, for every ball

B = [[ϕ B ]] \ [[ψ B ]] in X F ( p)
, there is y ∈ B which contains Ker ↑ π ā if and only if there is y A ∈ X A such that ϕ B (ā) ∈ y A and ψ B (ā) / ∈ y A (here we use Fact 2.2 and the assumption that π ā is surjective). By Stone's duality, the latter is equivalent to ϕ

B (ā) ψ B (ā), that is ϕ B (ā) → ψ B (ā) = 1.
With other words, ϕ B (ā) → ψ B (ā) = 1 if and only if there is no y ∈ B containing Ker ↑ π ā, which proves our claim.

The main result of [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF] is that, for every pair of finitely presented Heyting algebras A, B and every L HA -morphism f : A → B, the dual map f ↑ : X B → X A is an open map. We will focus on the special case where f is the natural inclusion from A = F (p), to B = F (p, q), with p an l-tuple of variables an q a new variable. Then f ↑ (x) = x ∩ F (p), for every x ∈ X F ( p,q) . In that case, by compactness of X F ( p) the Open Mapping Theorem rephrases as the following property.

Theorem 2.9 (Open Mapping for X F ( p) ) For every integer d ≥ 0, there is

an integer R l,d ≥ 0 such that ∀y ∈ X F ( p) , ∀x 0 ∈ X F ( p,q) d p y, x 0 ∩ F (p) < 2 -R l,d =⇒ ∃x ∈ X F ( p,q) x ∩ F (p) = y and d p,q (x, x 0 ) < 2 -d
It is actually from this more precise statement that the Open Mapping Theorem for general finitely presented Heyting algebras is derived in [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF]. And it is this one that we will prove in Section 5.

The prime existentially closed model

We are going to amalgamate a set of representatives of all the finite Heyting algebras in a countable, locally finite Heyting algebra H 0 which will prove to be the smallest non-trivial existentially closed Heyting algebra (up to isomorphism), and the only one which is both countable and locally finite. The construction goes by induction.

Construction of H 0 . Let H be a non-trivial existentially closed Heyting algebra. Let H 0 be the two-element Heyting algebra contained in H. Assume that a finite Heyting algebra H n ⊆ H has been constructed for some n ≥ 0. Let A 1 , . . . , A α be the list of all the subalgebras of H n with ≤ n join-irreducible elements. For each i ≤ α let B i,1 , . . . , B i,βi be a set of representatives of the minimal proper finite extensions of A i (up to L HA -isomorphism over A i ). Let H n,1,1 = H n and assume that for some i 0 ≤ α and j 0 ≤ β i0 , we have constructed a finite Heyting algebra H n,i0,j0 ⊆ H containing: firstly H n ; secondly, for every i < i 0 and j ≤ j i a copy of B i,j containing A i ; and thirdly, for every j < j 0 a copy of B i0,j containing A i0 . This assumption is obviously true if i 0 = j 0 = 1. In the induction step we distinguish three cases.

Case 1: j 0 < β i0 . It is well known that the variety of Heyting algebras has the Finite Amalgamation Property, that is every pair of finite extensions of a given Heyting algebra L amalgamate over L in a finite Heyting algebra. In particular, there is a finite Heyting algebra C containing both H n,i0,j0 and a copy B of B i0,j0+1 . By Theorem 2.5, H satisfies the Spitting and Density axioms. So by Theorem 2.6, there is an L HA -embedding ϕ : C → H which fixes H n,i0,j0 pointwise. We let H n,i0,j0+1 be the Heyting algebra generated in H by the union of H n,i0,j0 and ϕ(B). This is a finite Heyting algebra containing H n and, for every i < i 0 and j ≤ j i a copy of B i,j containing A i , and for every j < j 0 + 1 a copy of B i0,j containing A i0 (namely ϕ(B i0,j0+1 for j = j 0 + 1, the other cases being covered by the induction hypothesis because H n,i0,j0+1 contains H n,i0,j0 ).

Case 2: j 0 = β i0 and i 0 < α. By the Finite Amalgamation Property again, there is a finite Heyting algebra C containing both H n,i0,j0 and a copy B of B i0+1,1 . Theorems 2.5 and 2.6 then give an L HA -embedding ϕ : C → H which fixes H n,i0,j0 pointwise. We let H n,i0+1,1 be the Heyting algebra generated in H by the union of H n,i0,j0 and ϕ(B). This is a finite Heyting algebra containing H n and, for every i < i 0 + 1 and j ≤ j i a copy of B i,j containing A i , and a copy of B i0,1 containing A i0 .

Case 3: j 0 = β i0 and i 0 = α. We let H n+1 = H n,α,βα .

Repeating this construction, we get an increasing chain of finite Heyting algebras H n contained in H. We let H 0 = n∈N H n . Since every H n is finite, H 0 is a countable and locally finite Heyting algebra. (1)⇒(4) Both H and H 0 have the properties of item 1. We construct an L HA -isomorphism by induction. Let (a n ) n∈N be an enumeration of H, and (b n ) n∈N an enumeration of H 0 . Assume that for some integer n ≥ 0 we have constructed an L HA -isomorphism ϕ n :

A n → B n where A n (resp. B n ) is a finite subalgebra of H (resp. H 0 ) containing a k (resp. b k ) for every k < n.
This assumption is obviously true for n = 0, with ϕ 0 the empty map. Let k 0 be the first integer k ≥ n such that a k / ∈ A n . Let A n+1/2 be the Heyting algebra generated in H by A n ∪ {a k0 }. Since H is locally finite, A n+1/2 is a finite extension of A n . Composing ϕ -1 n by the inclusion map, we get an embedding of B k into A n+1 . The assumption (1) gives an embedding of A n+1 into H 0 over B n , or equivalently a subalgebra B n+1/2 of H 0 containing B n and an L HA -isomorphism ϕ n+1/2 : A n+1/2 → B n+1/2 whose restriction to A n is ϕ n . Now let l 0 be the smallest integer l ≥ n such that b l / ∈ B l+1/2 , and let B l+1 be the Heyting algebra generated in H 0 by B n+1/2 ∪ {b l0 }. A symmetric argument gives a subalgebra A n of H containing A n+1/2 and an L HA -isomorphism ψ n+1 :

B n+1 → A n+1 whose restriction to A n+1/2 is ϕ -1 n+1/2 . We then let ϕ n+1 = ψ -1 n+1
and let the induction go on. Finally we get an isomorphism ϕ : H → H 0 whose restriction to each A n is ϕ n , and we are done.

(1)⇒(3) Let ϕ(ā, q) be a quantifier-free L HA -formula with parameters ā ∈ H l 0 , such that ∃q ϕ(ā, q) is satisfied in some extension of H 0 . Let A be the Heyting algebra generated by ā. Since H 0 is locally finite, A is finite. By the Finite Extension Property, it follows that ∃q ϕ(ā, q) is satisfied in some finite extension B of A. By assumption (1), B embeds into H 0 over A. So ∃q ϕ(ā, q) is satisfied in H 0 .

(3)⇒(2)⇒(1) is just Theorem 2.5 and Theorem 2.6, which finishes the proof. We say that ā and ā are n-similar if Th n (ā) = Th n (ā ), and write it ā ≈ n ā . They are ω-similar if they are n-similar for every n, or equivalently if Ker ↑ π ā = Ker ↑ π ā . Note that ā and ā are ω-similar if and only if the function mapping a i to a i for 1 ≤ i ≤ l, extends to an L HA -isomorphism between the Heyting algebras generated by ā and ā in A.

Proposition 4.1 Let ā, ā be two l-tuples in a Heyting algebra A. For every integer n ≥ 0 the following assertions are equivalent. (3)⇒(2) Assume that Th n (ā) = Th n (ā ), for example Th ( ā) ⊆ Th n (ā ), and pick any θ(p) in Th n (ā ) \ Th n (ā). Then θ belongs to Ker ↑ π ā but not to Ker ↑ π ā. Fact 2.1 then gives y ∈ X F ( p) such that Ker ↑ π ā ⊆ y and θ / ∈ y. In particular y ∈ Y n (a), but for every y ∈ X F (ā) such that y ∼ n y , since θ(p) has degree ≤ n we have

1. Th n (ā) = Th n (ā ). 2. Y n (ā) = Y n (ā ).
θ / ∈ y =⇒ θ / ∈ y =⇒ Ker ↑ π ā ⊆ y , so y / ∈ Y n (ā ).
Remark 4.2 Item 3 of Proposition 4.1 gives that the relation ≈ n for l-tuples in A is definable by the L HA -formula with 2l free variables Equiv l,n (p, p ) =

B∈Bn( p) ϕ B (p) ≤ ψ B (p) ⇔ ϕ B (p ) ≤ ψ B (p ) .
Now we can introduce the corner stone of our axiomatization of existentially closed Heyting algebras. Given a Heyting algebra A, we let h l,d (A) be the smallest integer n such that for every ā, ā ∈ A l such that ā ≈ n ā : for every system S t,s (p, q) of degree ≤ d, S t,s (ā, q) has a solution in A if and only if S t,s (ā , q) has a solution in A. If no such integer exists we let h l,d (A) = +∞. We call h l,d (A) the (l, d)-index of A. We say that A has the QE property if h l,d (A) is finite for every (l, d). The following characterisation motivates this terminology.

Example 4.3 If T is any theory of Heyting algebras which eliminates the quantifier in L HA , then every model of T has the QE property by Proposition 4.4 below. In particular:

• Every dense Boolean algebra has the QE property.

• By Pitt's result every existentially closed Heyting algebra has the QE property.

Proposition 4.4 A Heyting algebra A has the QE property if and only if the complete theory of A in L HA eliminates the quantifiers.

Proof: Assume that the theory of A in L HA eliminates the quantifiers. There are up to intuitionist equivalence finitely many IPC formulas in l variables with degree ≤ d, hence finitely many systems in l + 1 variable of degree ≤ d. Let S i (p, q) for 1 ≤ i ≤ N an enumeration of them. For each of them, by assumption there is a quantifier-free formula χ S (p) such that the theory of A proves that ∃q, S i (p, q) is equivalent to χ i (p). Let n be the maximal degree of all the atomic formulas composing these formulas χ i . For every ā, ā ∈ A n such that ā ≈ n ā , A |= χ i (ā) if and only if A |= χ i (ā ). So the system S i (ā, q) has a solution in A if and only if the system S i (ā , q) has a solution in A, that is h l,d (A) ≤ n.

Reciprocally, assume that h l,d (A) is finite for every integers l, d. Let ϕ(p, a) be a quantifier-free formula in l + 1 variables. It is logically equivalent to a disjunction of finitely many systems S i (p, q), for 1 ≤ i ≤ N . Let d be the maximal degree of all these systems, and n = h l,d (A). Using again that there are, up to intuitionist equivalence, finitely many IPC formulas in l variables with degree ≤ n, there are also finitely many equivalence classes for ≈ n in A l . For every such equivalence class C, let ā ∈ C and let ϕ C (resp. ψ C ) be the conjunction (resp. disjunction) of the formulas t(p) = 1 (resp t(p) = 1) for t(p) ranging over a finite set of representatives of the IPC formulas which belong to Th n (ā) (resp. which don't belong to Th n (ā)). Clearly a tuple ā ∈ A l belongs to C if and only if A |= ϕ C (ā) ¬ψ C (ā). Now, for each system S i (p, q) let C i be the list of equivalence classes C for ≈ n in A l such that S i (ā, q) has a solution in A for some ā ∈ C (hence also for every ā ∈ C by definition of n = h l,d (A)).

By construction, for every ā ∈

A l A |= ∃q, S i (ā, q) ⇐⇒ ā ∈ C i ⇐⇒ A |= C∈Ci ϕ C (ā) ¬ψ C (ā) .
Let χ i (p) be the IPC formula on the right. By construction the theory of A proves that ∃q, ϕ(p, q) is equivalent to i≤N χ i (p). The latter is quantifier-free, hence the theory of A eliminates the quantifiers by an immediate induction. In particular, every Heyting algebra elementarily equivalent to A has the same (l, d)-index.

Proof: For every system S t,s (p, q) of degree ≤ d let FC n t,s (p, p ) = Equiv l,n (p, q ) ∃q , S t,s (p , q ) ⇒ ∃b, S t,s (p, q)

where Equiv l,n (p, p ) is the quantifier-free L HA -formula introduced in Remark 4.2. This is a ∀∃-formula. Clearly h l,d (A) ≤ n if and only if A |= FC n t,s (ā, ā ) for every ā, ā ∈ A l and every system S t,s (p, q) of degree ≤ d. There are only finitely many non-equivalent IPC formulas of degree ≤ d, hence finitely many non-equivalent systems of degree ≤ d. So h l,d (A) ≤ n if and only if A satisfies the conjunction of the finitely many formulas ∀p, p FC n t,s (p, p ).

Let T be the model-completion of the theory of Heyting algebras. By Pitt's result the models of T are exactly the existentially closed Heyting algebras. In particular, the Heyting algebra H 0 constructed in Section 3 is a model of T . So by Proposition 4.4 H 0 has the QE property. Once and for all, we let h l,d = h l,d (H 0 ) < +∞.

Theorem 4.6 For every Heyting algebra H the following properties are equivalent.

1. H is existentially closed.

2. H has the Density, the Splitting and the QE properties.

3. H has the Density and Splitting properties, and h l,d (H) = h l,d for every integers l, d.

In particular, the model-completion of the theory of Heyting algebras is axiomatised by the Density and Splitting axioms, and the formulas FC (3)⇒(2) is clear.

(2)⇒(1) The case of the one-point Heyting algebra being trivial, we can assume that 0 = 1 in H. By model-theoretic non-sense, we can assume that H is ω-saturated and it suffices to prove that for every ā ∈ H l and every finitely generated Heyting algebra B containing the algebra A generated by ā in H, there is an embedding of B into H over A. By an immediate induction we are reduced to the case where B is generated over A by a single element b. Replacing if necessary H by an elementary extension, thanks to Proposition 4.5 we can assume that H is ω-saturated.

Let Σ be the set of atomic or neg-atomic L HA -formulas ϕ(p, q) such that B |= ϕ(ā, b). We only have to prove that for some b ∈ H, Σ is satisfied by (ā, b ) (by which we mean that H |= ϕ(ā, b ) for every formula ϕ(p, q) in Σ). Indeed, B will then be isomorphic over A to the Heyting algebra generated in H by (ā, b ), so we are done. Since H is ω-saturated, it suffices to prove that every finite fragment of Σ is satisfied by (ā, b ) for some b ∈ H. Such a finite fragment is equivalent to a system. So we want to prove that for every system S t,s (p, q), if S t,s (ā, q) has a solution in B then it has a solution in H. Now let S t,s (p, q) be a system such that S t,s (ā, q) has a solution in B, and let d be the degree of S t,s (p, q). By Corollary 2.7 B embeds into H. So let (ā 0 , b 0 ) ∈ H l+1 be the image of (ā, b) by such an embedding. Then Th n (ā, b) = Th n (ā 0 , b 0 ) for every integer n ≥ 0. A fortiori Th n (ā) = Th n (ā 0 ) for every n, and in particular for n = h l,d (H). Now S t,s (ā 0 , q) has solution in H, namely b 0 , and ā ≈ n ā0 for n = h l,d (H). So S t,s (ā, q) has a solution in H, by definition of h l,d (H).

The Open Mapping Theorem

Our aim in this section is to derive the Open Mapping Theorem of [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF] from Theorem 4.6.

We first need a lemma. As usually we consider IPC formulas t(p, q) and s k (p, q) as elements of F (p, q). In particular, t(p, q)↑ in the next result is the principal filter generated by t(p, q) in F (p, q). Lemma 5.1 Let S t,s (p, q) be a system, with s = (s 1 , . . . , s κ ). For every l-tuple ā in a Heyting algebra A, the following assertions are equivalent.

1. S t,s (ā, q) has a solution in some extension of A.

2. Ker ↑ π ā contains t(p, q)↑ ∩ F (p), and the filter generated in F (p, q) by Ker ↑ π ā ∪ {t(p, q)} does not contain any of the s k (p, q)'s.

3. For every y ∈ X F ( p) containing Ker ↑ π ā, there is x ∈ [[t(p, q)]] such that x ∩ F (p) = y. Moreover, for each k ≤ κ, there is at least one of these y's for which x can be chosen outside of [[s k (p, q)]].

Proof: Let A 0 be the Heyting algebra generated in A by ā. If S t,s (ā, q) has a solution in some extension of A 0 , by the amalgamation property of Heyting algebras it has a solution in some extension of A, and reciprocally. Thus, replacing A by A 0 if necessary, we can assume that A is generated by ā. We let G be the filter generated in F (p, q) by Ker ↑ π ā ∪ {t}, or equivalently by Ker ↑ π ā ∪ t↑.

(1)⇒(2) In some extension

H of A, let b be such that t(ā, b) = 1 and s k (ā, b) = 1 for every k ≤ κ. There is a unique L HA -morphism π ā,b : F (p, q) → H mapping (p, q) onto (ā, b). By construction π ā is the restriction of π ā,b to F (p), hence Ker ↑ π ā = Ker ↑ π ā,b ∩ F (p). We have t ∈ Ker ↑ π ā,b ⇒ t↑ ⊆ Ker ↑ π ā,b ⇒ t↑ ∩ F (p) ⊆ Ker ↑ π ā,b ∩ F (p). So t↑ ∩ F (p) is contained in Ker ↑ π ā. Moreover G is contained in Ker ↑ π ā,b and s k / ∈ Ker ↑ π ā,b , hence s k / ∈ G, for every k ≤ κ.
(2)⇒(1) Assuming (2), we are claiming that G∩X F ( p) = Ker ↑ π ā. The rightto-left inclusion is clear. Reciprocally, if ϕ(p) ∈ G then ϕ(p) ≥ ϕ 0 (p) ∧ τ (p, q) for some ϕ 0 ∈ Ker ↑ π ā and τ ∈ t↑.

So ϕ 0 → ϕ ≥ τ , that is ϕ 0 → ϕ ∈ t↑ ∩ X F ( p) , hence ϕ 0 → ϕ ∈ Ker ↑ π ā by assumption (2). It follows that ϕ 0 ∧ (ϕ 0 → ϕ) ∈ Ker ↑ π ā, that is ϕ 0 ∧ ϕ ∈ Ker ↑ π ā. A fortiori ϕ ∈ Ker ↑ π ā which proves our claim.
Let B = X F ( p,q) /G and f : X F ( p,q) → B be the canonical projection. G ∩ X F ( p) is obviously the filter kernel of the restriction of f to X F ( p) . Since G ∩ X F ( p) = Ker ↑ π ā, by Factorisation of Morphisms we then have a commutative diagram as follows (with left arrow the natural inclusion).

F (p, q) B F (p) A f πā
We have t ∈ G by construction, and s k / ∈ G for every k ≤ κ by assumption (2). So, after identification of A with its image by the dashed arrow, B is an extension of A in which f (q) is a solution of S t,s (ā, q).

(2)⇒(3) Given y ∈ X F ( p) containing Ker ↑ π ā, assume for a contradiction that for every

x ∈ [[t]], x ∩ F (p) = y. If x ∩ F (p) ⊆ y, pick any ϕ x in (x ∩ F (p)) \ y and let U x = [[ϕ x ]]. If x ∩ F (p) ⊇ y, pick any ψ x in y \ (x ∩ F (p)) and let U x = [[ψ x ]] c . The family (U x ) x∈[[t]] is an open cover of the compact space [[t]]. A finite subcover gives ϕ 1 , . . . , ϕ α ∈ F (p) \ y and ψ 1 , . . . , ψ β ∈ y such that [[t]] ⊆ i≤α [[ϕ i ]] ∪ j≤β [[ψ j ]] c . That is [[t]] ⊆ [[ϕ]] ∪ [[ψ]] c with ϕ = ∨ ∨ i≤α ϕ i and ψ = ∧ ∧ j≤β ψ j . In particular, t ≤ ψ → ϕ so ψ → ϕ ∈ t↑ ∩ F (p) ⊆ Ker ↑ π ā ⊆ y =⇒ ψ → ϕ ∈ y.
On the other hand every ψ i ∈ y hence ψ ∈ y, and every ϕ i / ∈ y hence ϕ / ∈ y (because y is a prime filter). In particular ψ → ϕ / ∈ y, a contradiction. We have proved that the first part of (2) implies the first part of (3). Since G is the intersection of the prime filters of F (p, q) which contain G, the second part of (2) implies that for each k ≤ κ there is x ∈ X p,q containing Ker ↑ π ā and t but not s k . Letting y = x ∩ F (p), we get the second part of (3).

(

)⇒(2) Let Y = y ∈ X F ( p) : Ker ↑ π ā ⊆ y and X = {x ∩ F (p) : x ∈ [[t]]}. The first part of (3) says that Y ⊆ X , hence Y ⊇ X . Since every filter is the intersection of the prime filters which contain it, Y = Ker ↑ π ā and [[t]] = t↑ hence X = [[t]] ∩ F (p) = t↑ ∩ F (p). So Ker ↑ π ā ⊇ t↑ ∩ F (p), which is the first part of (2). Now for each k ≤ κ the second part of (3) gives x ∈ [[t]] \ [[s k ]] such that x ∩ F (p) contains Ker ↑ π ā. So G ⊆ x, in particular s k / ∈ G. 3
Theorem 5.2 (Open Mapping for X F ( p) ) For every integer d, every y ∈ X F ( p) and every x 0 ∈ X F ( p,q) , if d p(y, x 0 ∩ F (p)) < 2 -h l,d , there exists x ∈ X F ( p,q) such that y = x ∩ F (p) and d p,q (x, x 0 ) < 2 -d .

This result says that the dual of the natural embedding f : F (p) → F (p, q), is an open map f ↑ : X F ( p) → X F ( p,q) . As shown in [START_REF] Samuel | An open mapping theorem for finitely copresented Esakia spaces[END_REF], it easily follows that for every L HA -morphism f : A → B between finitely presented Heyting algebras, the dual map f ↑ : X B → X A is an open map.

Proof: Let y 0 = x 0 ∩ F (p) and B = B p(y 0 , 2 -h l,d ) = [[ϕ B ]] \ [[ψ B ]]. Let A 0 = F (
p)/y 0 , B 0 = F (p, q)/x 0 and (ā 0 , b 0 ) be the image of (p, q) by the canonical projection π ā0,b0 : F (p, q) → B 0 . By construction A 0 is the Heyting algebra generated by ā0 in B 0 , and the system S ϕ B , ψB (ā 0 , q) has a solution in B 0 , namely b 0 .

Let A = F (p)/y, and ā be the image of p by the canonical projection π ā : F (p) → A. By construction d p(y 0 , 2 -h l,d ) < 2 -h l,d , that is y ∼ h l,d y 0 . Hence for every IPC formula θ(p) of degree ≤ h l,d , θ(p) ∈ y if and only if θ(p) ∈ y 0 . But θ(p) ∈ y if and only if θ(ā) = 1, and similarly for ā0 , so Th h l,d (ā) = Th h l,d (ā 0 ). Now A and A 0 are non-trivial by construction, so they contain the twoelement Heyting algebra. By the amalgamation property, both of them embed in a common extension, which itself embeds in an existentially closed extension H. So S ϕ B , ψB (ā 0 , q) has a solution in A 0 , hence in H, and ā ≈ h l,d ā0 . Now h l,d (H) = h l,d by Theorem 4.6, so S ϕ B , ψB (ā, q) has a solution b in H. The equivalence (1)⇔(3) of Lemma 5.1 applies: since y = Ker ↑ π ā, there is x ∈

[[ϕ B ]] \ [[ψ B ]] (that is x ∈ B) such that x ∩ F (p) = y.

Discriminant and co-discriminant

Throughout this section we fix a system of degree ≤ d S t,s (p, q) = t(s, p) = 1 k≤κ s k (p, q) = 1 .

Like the usual discriminant does for polynomial equations, we want to find IPC formulas in the coefficients of the system whose values at any l-tuple ā in a Heyting algebra A decides if S t,s (ā, q) has a solution in some extension of A.

We define the discriminant of t as

∆ t (p) = ∧ ∧ B∈Dt ϕ B (p) → ψ B (p)
where D t is the set of balls B in X F ( p) of radius 2 -R l,d such that

t(p, q) ∧ ϕ B (p) ≤ ψ B (p).
For each k ≤ κ, the co-discriminant of (t, s k ) is

∇ t,s k (p) = ∧ ∧ B∈D t,s k ϕ B (p) → ψ B (p)
where D t,s k is the set of balls B in X F ( p) of radius 2 -R l,d such that t(p, q) ∧ ϕ B (p) s k (p, q) ∨ ψ B (p).

Theorem 6.1 For every l-tuple ā in a Heyting algebra A, the system

S t,s (p, q) = t(s, p) = 1 k≤κ s k (p, q) = 1 .
has a solution in some extension of A if and only if ∆ t (ā) = 1 and ∇ t,s k (ā) = 1 for every k ≤ κ.

The proof is based on Lemma 5.1 and the Open Mapping Theorem.

Proof: (of Theorem 6.1) By Lemma 5.1 the system S t,s (ā, q) has a solution in some extension of A if and only if (i) for every y ∈ X F ( p) containing Ker ↑ π ā there is x ∈ X F ( p,q) such that x ∩ X F ( p) = y and t ∈ x, and for each k ≤ κ; (ii) k there are y ∈ X F ( p) and x ∈ X F ( p,q) such that x ∩ X F ( p) = y contains Ker ↑ π ā, t ∈ x and s k / ∈ x. Now for every ball B in X F ( p) of radius 2 -R l,d such that ϕ B (ā) → ψ B (ā) = 1, by Claim 2.8 there is y ∈ B containing Ker ↑ π ā, so (i) implies that there is also x ∈ X F ( p,q) such that x ∩ X F ( p) = y and t ∈ x. In particular x and y contain the same elements of F (p), hence

ψ B ∈ x and ψ B / ∈ x since y ∈ B = [[ϕ B ]] \ [[ψ B ]]. Altogether t ∧ ϕ B ∈ x and ψ B / ∈ x, consequently t ∧ ϕ B ψ B in F (p, q), that is B / ∈ D t . Equivalently, (i) implies that ϕ B (ā) → ψ B (ā) = 1 for every ball B ∈ D t , that is ∆ t (ā) = 1.
Conversely, let us prove that ∆ t (ā) = 1 implies (i). Pick any y ∈ X F ( p) containing Ker ↑ π ā. Let B be the unique ball in X x ∈ X F ( p,q) such that x ∼ d x and x ∩ X F ( p) = y. In particular t ∈ x implies that t ∈ x, that is x ∈ [[t]], which proves (i).

F ( p) of radius 2 -R l,d containing y. Then ϕ B (ā) → ψ B (ā) = 1 by Claim 2.8, so B / ∈ D t because ∆ t (ā) = 1. By definition of D t we have t ∧ ϕ B ψ B , so there is a point x ∈ X F ( p,q) such that t ∧ ϕ B ∈ x and ψ B / ∈ x . Let y = x ∩ X F (
Fix now some k ≤; K and assume that ∇ t,s (ā) = 1, so there is a ball B in X F ( p) of radius 2 -R l,d such that: (a) k t ∧ ϕ B s k ∨ ψ B , and; (b) ϕ B (ā) → ψ B (ā) = 1. Then (a) k gives some x ∈ X F ( p,q) which contains t and ϕ B but neither s k nor ψ B . Let y = x ∩F (p), then ϕ B ∈ y and ψ B / ∈ y , because y and x contain the same elements in F (p). So y belongs to

[[ϕ B ]] \ [[ψ B ]] = B. By (b)
and Claim 2.8 there is some y ∈ B which contains Ker ↑ π ā. Since y = x ∩ F (p) and y, y ∈ B, the Open Mapping Theorem then gives x ∈ X F ( p,q) such that x ∼ n x and x ∩ F (p) = y. In particular t ∈ x and s k / ∈ x because t, s k have degree ≤ d and x ∼ d x , which proves (ii) k .

It only remains to check that (ii) k implies that ∇ t,s k (ā) = 1. By assumption (ii) k there are some y ∈ X F ( p) and x ∈ X F ( p,q) such that t ∈ x and s k / ∈ x, and such that y = x ∩ F (p) contains Ker ↑ π ā. Let B be the unique ball in X F ( p) of radius 2 -R l,d containing y. Then ϕ B ∈ x and ψ B / ∈ x because x and y contain the same elements of F (p). Altogether t ∧ ϕ B ∈ x and s k ∨ ψ B / ∈ x, so t ∧ ϕ B s k ∨ ψ B , that is B ∈ D t,s k . Moreover y belongs to B and contains Ker ↑ π ā so ϕ B (ā) → ψ B (ā) = 1, and a fortiori ∇ t,s k (ā) = 1.

Appendix: the Finite Extension Property

We collect here all the results from [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF] needed for the proof of the Finite Extension Property (Theorem 7.6 below). The classical Finite Model Property only concerns satisfiability of formulas ∃p, t(p) = 1 with t(p) an IPC-formula. The slight improvement below is Proposition 8.1 in [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF].

Proposition 7.1 Let V be a variety of Heyting algebras having the Finite Model Property. If an existential L HA -formula is satisfied in some V-algebra, then it is satisfied in a finite V-algebra.

Recall that the height of a poset (E, ≤) is the maximal integer n such that there exists a 0 < a 1 < • • • < a n in E. If no such maximum exists we say that E has infinite length. The dimension of a lattice L, denoted dim L, is the height of its prime filter spectrum (or equivalently of its prime ideal spectrum). This is also the classical Krull dimension of Spec ↑ L and of Spec ↓ L.

We introduced in [DJ11] a notion of dimension and co-dimension for the elements of a lattice, which turned out to have better properties in co-Heyting algebras. Given an element a of a Heyting algebra A, we define the dual codimension of a in A to be the co-dimension of a in A op , the co-Heyting algebra obtained by reversing the order of A. Equivalently, by Theorem 3.8 in [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF], it is the greatest integer d such that

∃x 0 , . . . , x d ∈ A, a ≥ x d • • • x 0 .
Remark 7.2 An immediate consequence of this characterisation is that if B is a Heyting algebra such that a ∈ B ⊆ A, the dual co-dimension of a in A is greater than or equal to its dual co-dimension in B.

We let dA denote2 the set of elements in A with dual co-dimension > d. Let us recall some of the properties of the dual co-dimension proved, after reversing the order, in [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF].

(CD 1 ) A Heyting algebra A has dimension ≤ d if and only if every a ∈ A \ {1} has dual co-dimension ≤ d in A, that is (d + 1)A = {1} (Remark 2.1).

(CD 2 ) There is an IPC formula ε l,d (p) such that for every Heyting algebra A generated by an l-tuple ā, dA is the filter generated in A by ε l,d (ā) (Proposition 8.2).

(CD 3 ) For every finitely generated Heyting algebra A, A/dA is finite (Corollary 5.5 and Corollary 7.5).

Remark 7.3 From (CD 1 ) and Remark 7.2 it follows that if a Heyting algebra A has finite dimension d, then every Heyting algebra contained in A has dimension ≤ d. This also follows from [START_REF] Hosoi | On intermediate logics[END_REF] and [START_REF] Ono | Kripke models and intermediate logics[END_REF], who proved mutatis mutandis, that the class of Heyting algebras of dimension ≤ d is a variety (a direct proof of this is given in [START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF], Proposition 3.12).

Lemma 7.4 Given an integer d ≥ 0 there is an integer n d ≥ 0 such that for every Heyting algebra H of dimension ≤ d, every ā ∈ H l and every l-tuple ā in a Heyting algebra H , if Th n (ā) = Th n (ā ) then Ker ↑ π ā = Ker ↑ π ā .

Proof: By Remark 7.3, for every Heyting algebra H of dimension ≤ d, and every ā ∈ H l , the Heyting algebra A generated by ā in H has dimension ≤ d. Then (d + 1)A = 1 by (CD 1 ), that is ε l,d (ā) = 1 by (CD 2 ). In particular, ε l,d (p) ∈ Ker ↑ π ā hence (d + 1)F (p) is contained in Ker ↑ π ā. By (CD 3 ), F (p)/(d + 1)F (p) is finite. Hence there exists only finitely many prime filters y in F (p) which contain (d + 1)F (p), and since the filter (d + 1)F (p) is principal, every such y is principal (here we use Fact 2.2). let ξ 1 (p), . . . , ξ α (p) be a list of IPC formulas such that every y ∈ X F ( p) containing (d + 1)F (p) is generated by ξ i (p) for some i ≤ α. Let n d be the maximum of the degrees of the ξ i (p)'s and of ε l,d (p) and assume that ā ≈ n ā. Then ε l,d (ā ) = 1, that is ε l,d (p) ∈ Ker ↑ π ā so (d + 1)F (p) is contained in Ker ↑ π ā . Thus, for every y ∈ X F ( p) , y contains Ker ↑ π ā (resp. Ker ↑ π ā ) if and only if y is generated by ξ i (p) for some i ≤ α such that ξ i (ā) = 1 (resp. ξ i (ā ) = 1). Since Th n (ā) = Th n (ā ) by assumption, ξ i (ā) = 1 if and only if ξ i (ā ) = 1. This ensures that Ker ↑ π ā and Ker ↑ π ā are contained in the same prime filters of F (p). By Fact 2.1 it follows that Ker ↑ π ā = Ker ↑ π ā .

Remark 7.5 In [START_REF] Bellissima | Finitely generated free Heyting algebras[END_REF] an explicit formula ξ(p), with degree ≤ 2d + 1, is given for every join-irreducible element of F (p) of foundation rank ≤ d (see also Theorem 3.3 in [START_REF] Darnière | On Bellissima's construction of the finitely generated free Heyting algebras, and beyond[END_REF]). A prime filter y of F (p) contains (d + 1)F (p) if and only if is generated by such a join-irreducible element ξ(p), so we can take n d = 2d + 1 in Lemma 7.4. Theorem 7.6 (Finite Extension Property) Let V be a variety of Heyting algebras having the Finite Model Property. If an existential L HA -formula with parameters in a finite V-algebra A is satisfied in a V-algebra containing A, then it is satisfied in some finite V-algebra containing A.

Proof: It suffices to prove the result for a formula ∃q S t,s (ā, q) with ā ∈ A l generating A. Let d be the degree of S t,s (p, q). Let n ∈ N be given by Lemma 7.4 applied to the integer dim A (since A is finite, A is also finite dimensional). Up to intuitionist equivalence there are finitely many IPC formulas ϕ(p) of degree ≤ n. Let u be the conjunction of those which belong to Th n (ā), and v = (v 1 , . . . , v α ) be an enumeration of the others. Now consider the system S t ,s (p, q) where t = t ∧ u and s = (s 1 , . . . , s κ , v 1 , . . . , v α ).

By assumption S t,s (ā, q) has a solution b in some extension of A. Then (ā, b) is a solution of S t ,s (p, q). By Proposition 7.1, S t ,s (p, q) then has a solution (ā , b ) in a finite Heyting algebra H in V. In particular b is a solution S t,s (ā , q). Moreover, u(ā ) = 1 and v i (ā ) = 1 for every i ≤ α, hence Th n (ā ) = Th n (ā). By assumption on n, this implies that Ker ↑ π ā = Ker ↑ π ā . So there is an isomorphism from A to the Heyting algebra A generated by ā which maps ā onto ā . By embedding A into H via this isomorphism, we get a finite V-algebra containing A in which S t,s (ā, q) has a solution.

Fact 2. 3 (

 3 Factorisation of Morphisms) Let f : B → A be an L HA -morphism. Given a filter I of B, let π I : B → B/I be the canonical projection. Then f factors through π I , that is f = g • π I for some L HA -morphism g : B/I → A, if and only if Ker ↑ f ⊆ I.

  b a ⇐⇒ b → a = a and b ≥ a

Remark 3. 2

 2 We have constructed H 0 inside a given non-trivial existentially closed Heyting algebra H. The same construction in another non-trivial existentially closed Heyting algebra H would give a Heyting algebra H 0 contained in H to which Proposition 3.1 would apply as well as to H 0 . The characterisation given there proves that H 0 and H 0 are isomorphic. As a consequence, every non-trivial existentially closed Heyting algebra contains a copy of H 0 .4 The QE propertyGiven an integer n ≥ 0 and l-tuples ā, ā in a Heyting algebra A let Th n (ā) = {ϕ(p) : deg ϕ ≤ n and ϕ(ā) = 1} and Y n (ā) = y ∈ X F ( p) : ∃y ∈ X F ( p) , y ∼ n y and Ker ↑ π ā ⊆ y .

3.

  For every ball B in X F ( p) with radius 2 -n : ϕ B (ā) ≤ ψ B (ā) if and only if ϕ B (ā ) ≤ ψ B (ā ).Proof:(2)⇔(3) Given y ∈ X F ( p) , let B the ball in X F ( p) with center y and radius 2 -n . By Claim 2.8, y ∈ Y n (ā) if and only if ϕ B (ā) → ψ B (ā) = 1, that is if and only if ϕ B (ā) ψ B (ā). The equivalence follows.(1)⇒(3) Given a ball B in X F ( p) with radius 2 -n , ϕ B and ψ B have degree < n hence ϕ b → ψ B have degree ≤ n. The assumption (1) then implies that ϕ B (ā) → ψ B (ā) = 1 if and only if ϕ B (ā ) → ψ B (ā ) = 1, and (3) follows.

Proposition 4. 5

 5 For any given l, d, n ∈ N, there is a closed ∀∃-formula FC n l,d in L HA for every Heyting algebras A h l,d (A) ≤ n ⇐⇒ A |= FC n l,d .

h

  l,d l,d for every integers l, d. Proof: (1)⇒(3) Since H is existentially closed, it has the Density and Splitting properties by Theorem 2.5. Moreover H 0 ⊆ H by Remark 3.2, and H 0 is existentially closed by Proposition 3.1, so H 0 H y Pitts' result. In particular H 0 ≡ H so h l,d (H) = h l,d (H 0 ) for every l, d by Proposition 4.5.

  p) , since y and x contain the same elements in F (p) we have ϕ B ∈ y and ψ B / ∈ y , that is y ∈ [[ϕ B ]] \ [[ψ B ]] = B. Now, since y ∈ B and B has radius 2 -R l,d , the Open Mapping Theorem gives

  Proposition 3.1 Given a Heyting algebra H, the following properties are equivalent.1. H is countable, locally finite, and every finite extension B of a subalgebraA of H embeds into H over A.2. H is countable, locally finite, and has the Density and Splitting properties.3. H is countable, locally finite and existentially closed.4. H is L HA -isomorphic to H 0 .Proof: (4)⇒(1) We have to prove that H 0 itself has the properties of item 1. We already know that H 0 is countable and locally finite. Let B be a finite extension of a subalgebra A of H. We want to embed B in H over A. By an immediate induction we can assume that B is a minimal proper finite extension of A. Now A is contained in H

n for some integer n ≥ 0, which we can assume to be greater than the number of join-irreducible elements of A. So A is one of the algebras A 1 , . . . , A α of the above construction of H 0 , and B is isomorphic over A to some B i,j as above. By construction H n+1 contains a copy of B i,j , hence of B, which contains A. So B embeds over A into H n+1 , hence a fortiori into H 0 .

With other words, there is an L HA -embedding of B into H which fixes A pointwise.

This is slightly different from our notation in[START_REF] Darnière | Codimension and pseudometric in co-Heyting algebras[END_REF], where we let dA be the set of elements of co-dimension ≥ d.

Acknowledgement I would like to thank Sam van Gool and Luca Reggio for helpful discussions during the TOLO VI conference a Tbilissi, Georgia, and to express my gratitude to the organizers of this meeting hosting these discussions.


Coralie Pasquier

Sylvie Beaufils

Antoine Bouchoux

Sophie Rigault

Bernard Cabane

Mikael Lund

Valérie Lechevalier-Datin

Cécile Le Floch-Fouéré

Maryvonne Pasco

Valérie Lechevalier

Gilles Paboeuf

Javier Pérez

Stéphane Pezennec
email: stephane.pezennec@inra.fr

Osmotic pressures of lysozyme solutions from gas-like to crystal states

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Knowledge about the interactions in very concentrated solutions of proteins, namely up to a few hundred grams per liter, is of high relevance in various fields, such as the living cell physiology, food transformation (foams, powders, membrane filtration...), pharmacology and drug delivery, or diseases implying phase transition of proteins [1][2][3][4][5][6][7] . Predictive models, relying mostly on the knowledge originated from colloidal physics, have been proposed for the behavior of concentrated proteins [8][9][10] . However, they fail to catch the complexity and the variability of the protein molecules, related to the combination of their different levels of structure with the distinct physicochemical properties of the amino-acid residues.

Osmotic pressure measurements enable to probe protein-protein, protein-ion or protein-solvent interactions. Data about globular proteins have been established in the past [11][12][13][14] , however the highest concentrations that were obtained were never high enough to enable the system to go out of a dilute or semi-dilute range. In this work we report results obtained through osmotic stress [15][16][17][18][19][20][21][22][23] as a concentration technique. This method makes it possible to control the osmotic pressure over a wide range of volume fractions (spanning from the dilute phase to phases where interactions play a prominent role, up to the solid phase) and to reach the same concentration state by different pathways, while keeping constant salt activity.

We study lysozyme, a globular protein that has been well characterized since its discovery in 1922. Numerous studies have been conducted on lysozyme, in particular its self-interaction characteristics when concentrated or submitted to changes in the physicochemical conditions 9,[24][25][26][27][28][29][30][31][32][33][34][35] . Specifically, lysozyme has been shown, as other non-protein colloids, to exhibit a combination of long-range repulsive, and short-range attractive interactions, which leads to the formation of equilibrium clusters 24,25 .

In the present work, we aim to bring answers to the following questions:

• Do the diagrams relating osmotic pressure Π to volume fraction φ enable us to identify transitions of the system during concentration?

• If we tune the interactions, do the diagrams reflect the changes? Is it in a predictable way?

• What are the positions of the (φ , Π) lines with respect to theoretical models for simple colloids?

• Are the (φ , Π) diagrams that we obtain for lysozyme the experimental reference for true equations of state (EOS)?

2 Materials and methods Sample preparation. Lysozyme hydrochloride powder (lysozyme purity higher than 98 %, as determined by reversed-phase high-performance liquid chromatography (HPLC)) was a gift from LIOT (Annezin, France). Stock solutions were prepared by solubilizing protein in 18 MΩ resistivity Milli-Q water (Merck Millipore, Darmstadt, Germany) and were kept at 4 • C.

Osmotic stress technique.

The osmotic stress experiments were performed according to the procedure described by Bouchoux et al. 20 The osmotic stress technique is based on osmosis: the disequilibrium of chemical potentials between the interior of the dialysis bag, containing the protein solution, and the surrounding medium of controlled osmotic pressure causes a water flow from the high to the low chemical potential compartments. When the high chemical potential side is the protein solution, the latter is concentrated until equilibrium is reached. We used four types of bis-tris propane-HCl buffers: pH 7 and 20 mM, 35 mM and 150 mM ionic strength, and pH 9 and 20 mM ionic strength. Lysozyme net charges of +8.3 e and +6.3 e at pH 7 and pH 9, respectively, were predicted from its three-dimensional structure (PDB ID: 2VB1 36 ) using PROPKA 37,38 (see also Fig. S1,ESI). Each buffer contained 0.2 g/L thimerosal (Sigma, Saint Louis, USA) in order to avoid bacterial development. The bis-tris propane total concentration was chosen to account for an ionic strength of 20 mM, depending on the pH: 11.3 mM at pH 7 and 40 mM at pH 9. Ionic strengths of 35 mM and 150 mM were obtained by adding NaCl. Thimerosal, bis-tris propane (1,3-Bis[tris(hydroxymethyl)methylamino]propane) and NaCl were bought from Sigma-Aldrich (Saint-Louis, USA).

Polymer solutions were prepared directly in 500 mL glass bottles, by mixing the desired amount of polyethylene glycol (PEG) 20 000 (Sigma-Aldrich, Saint-Louis, USA) and buffer at 20 • C. To relate PEG 20 000 concentrations and osmotic pressures, we used the single-parameter phenomenological equation of state of PEG established by Cohen et al. 39 , assuming a prefactor α = 0.44, a monomer mass M m = 44 Da and a specific partial volume V = 0.825 mL/g for PEG 20 000:

ΠN 9/5 = RT M m V C C * N + α C C * N 9/4 ( 1
)
where N is the number of monomers per PEG molecule. The concentration C * N is defined by:

C * N = N -4/5 V (2)
Polymer solutions were kept at 20 • C during the whole experiments. We used a SpectraPor Dialysis Membrane, with a 6-8 kDa molecular mass cutoff and a 6.4 mm diameter (SpectrumLabs, Rancho Dominguez, USA) for the dialysis bags. Such a mass cutoff allows free exchange of ions and water, but not that of proteins and PEG 20 000. For each bag, a 10 cm length of dialysis membrane was cut and rinsed in Milli Q water. The bag was then filled with a protein stock solution of low concentration (50 g/L for osmotic pressures higher than 0.39 bar, 10 g/L at pressures of 0.05 bar and 0.12 bar) and immersed in the polymer solution.

Due to the water efflux, the volume of the dialysis bags decreased. Dialysis bags were frequently taken out of the polymer solution, rinsed carefully with deionized water in order to avoid contamination of the protein solution with PEG 20 000, then opened and re-filled with the low-concentration protein solution. The already stressed, concentrated solution and the new, dilute one were then homogenized, and the bag was put back in the polymer solution.

As the rise in concentration of the solution inside the bags can be very important, especially for solutions subject to high osmotic pressures, the solutions subject to pressures higher than 1.16 bar were first equilibrated to 1.16 bar for one week. The solutions subject to pressures lower than 1.16 bar were directly put to their final osmotic pressure. After one week, all the bags were transferred into new polymer solutions, of their final osmotic pressure. They were kept in these solutions for two weeks, during which they were frequently refilled, in order to obtain a weight of protein solution that was sufficient to make a dry content analysis (more than 1 g). At the end of the two weeks, the bags were considered of sufficient volume and were no more re-filled. However, during the two weeks, some water flowed out of the bags and diluted the polymer solution, which decreased slightly the external osmotic pressure. Thus, the bags were finally transferred in new polymer solutions of the desired osmotic pressure, and kept without re-filling for one more week. At the end of these four weeks, the protein solution was considered to be in equilibrium with the surrounding polymer solution.

For decompression experiments, the protein solution was first equilibrated at the desired final osmotic pressure following the procedure described above. Then, the dialysis bag was put in a polymer solution of higher osmotic pressure for a week, without re-filling it. Finally, the bag was put back in a polymer solution inducing the same osmotic pressure as initially. In the following, we shall refer to this compressiondecompression cycle as "two-way compression".

Dry content measurement.

This technique was used to determine the concentration of protein in the concentrated solutions obtained by osmotic pressure.

We used stainless steel cupels (diameter 60 mm, height 25 mm), with a removable lid. In each cupel, we put 25 g of Fontainebleau sand. The cupels and small glass rods were put in an oven at 102 • C for 2 h minimum, with the lid open, in order to eliminate remaining water. The cupels and rods were then left to cool at room temperature in a dessicator containing recently dehydrated silica gel, under vacuum, for minimum 45 min.

After cooling, each cupel was weighed (precision of 0.1 mg) with its lid closed and a glass rod. Each bag was rinsed, then opened and the protein solution was quickly put in a cupel. The total (cupel, lid, sample and glass rod) was then weighed. The sample was mixed with the Fontainebleau sand with the glass rod, which was left inside the cupel. The cupel (lid open) was then put in an oven at 102 • C overnight.

The day after, each cupel with its glass rod (lid closed) was left to cool at room temperature in a dessicator containing recently dehydrated silica gel for minimum 45 min. After cooling, each cupel was weighed (precision of 0.1 mg) with its lid closed.

Dry content weights were corrected for sodium chloride and bis-tris propane weights. Conversion from weights to volume fractions was performed considering that lysozyme had a specific partial volume of 0.712 mL/g 40 .

Dynamic vapor sorption (DVS).

Desorption isotherm of a 50 g/L lysozyme solution was obtained with a dynamic vapor sorption analyzer DVS (Surface Measurement Systems Ltd., London, UK) equipped with a Cahn microbalance. The experiments were carried out at constant temperature (20 • C) and relative humidity values of 5 %, 60 % and 90 %, to reach water activity values of 0.05, 0.6 and 0.9, respectively, at the equilibrium.

The water activity was converted to osmotic pressure using the formula:

Π = - RT v a ln(a w ) (3)
with Π the osmotic pressure (in Pa), R the universal gas constant, T the temperature, v a the molar volume of water and a w the water activity.

Results

Osmotic pressure profiles of lysozyme in a pH 7, I = 20 mM buffer

Fig. 1 presents the measured values of the protein volume fraction (horizontal axis) according to the osmotic pressures applied to the solution of lysozyme in a buffer at pH 7, and ionic strength 20 mM. In these conditions the net charge per protein is +8.3 e (see Materials and methods). As a comparison, we plotted the van't Hoff law of ideal gases, Π = ρk B T , where ρ is the number density and k B the Boltzmann constant, and the Carnahan-Starling EOS 41 , Π = ρk B T 1+φ +φ 2 -φ 3

(1-φ ) 3 , where φ is the volume fraction, which describes a hard sphere gas 15 , using the lysozyme molecular weight (14 313 Da) 42 and partial specific volume (0.712 mL/g) 40 so that the volume and mass of the equivalent spheres are equal to those of the proteins. The radius of the equivalent spheres is 1.59 nm.

The data demonstrate that osmotic stress makes it possible to cover three decades in osmotic pressures and two decades in volume fractions. At very high pressures, our data for pH 7 and ionic strength 35 mM match the results obtained by Rickard et al. through single particle sorption 29 and our own dynamic vapor sorption (DVS) results. It is noteworthy that, in contrast with osmotic stress, DVS and Rickard's microparticle technique concentrate all solutes, including salts, so that the ionic strength may vary.

The osmotic pressure profile can be divided into three parts: a dilute regime, up to φ = 0.1; a transition regime, ranging from φ = 0.1 to 0.5, where the slope of the curve decreases until a plateau, characterized experimentally by a large step in volume fraction (almost two-fold increase); then a concentrated regime, above φ = 0.5, where the pressure increases steeply with volume fraction. The use of the van't Hoff and Carnahan-Starling models is generally restricted to fluid, dilute systems 43 . In our case, in the dilute regime, the pressures of the lysozyme solutions are approximately twice as large as the Carnahan-Starling model or a van't Hoff perfect gas system. In the discussion, section 4, we shall present a model that explains the origin of this excess pressure. The 10 g/L and 50 g/L (φ = 0.0071 and 0.0356, respectively) stock solutions are clear, transparent liquids that flow easily. Samples obtained by osmotic compression have the same aspect as the stock solutions from 0.05 bar (Fig. 2A) to 0.12 bar. When the solutions are concentrated further, they become increasingly dense but remain transparent, with some white, fluffy aggregates visible at the bottom of the bag (Fig. 2B and2C). For pressures above 2.26 bar, namely above the "large volume fraction step" (see section 3.1), the samples become white and solid (Fig. 2D and2E). If a sample is compressed to 0.05 bar, then 39.75 bar, and finally de-compressed to 0.05 bar without any mechanical treatment, the solid re-dissolves spontaneously and completely, and becomes as clear and liquid as the original sample compressed at 0.05 bar, without any insoluble part remaining (Fig. 2F). This morphological reversibility needs to be confirmed from a thermodynamic point of view, as addressed in the following section.

Thermodynamic reversibility of the compression

We designed several experiments in order to verify that the same points on the osmotic pressure profile can be attained through different paths.

We performed osmotic compressions at 0.05 bar, 1.16 bar and 7.40 bar at pH 7 and I = 20 mM. After equilibrium was reached, we immersed the dialysis bags in a PEG solution at a 39.75 bar osmotic pressure.

After a new equilibrium, we brought each bag back to its initial osmotic pressure ("two-way compression").

As shown on Fig. 1, for 3 cycles with different final osmotic pressures, we found that the final volume fractions were similar for samples obtained through one-way compression and through two-way compression.

We performed additional experiments at pH 7, I = 35 mM and pH 7, I = 150 mM (see Fig. S2 andS3, ESI), and we also changed the pathways of the cycles: for pH 7 and I = 35 mM (Fig. S3, ESI), each sample was compressed to a different osmotic pressure and were then decompressed to the same osmotic pressure (0.57 bar). The results confirm that, on both sides of the "large volume fraction step", one-way and two-way compressions are equivalent.

Influence of pH and ionic strength

In another set of osmotic stress experiments, we reduced the net charge of the protein to Z = +6.3 e (see Materials and methods) by using a pH 9, I = 20 mM bis-tris propane buffer. Alternatively, we kept pH at 7 but adjusted the ionic strength to 35 mM and 150 mM by adding NaCl. Fig. 3 presents the (φ , Π) diagrams obtained for each condition, compared with the (φ , Π) diagram obtained at pH 7, I = 20 mM.

Increasing pH at constant ionic strength or increasing the ionic strength at constant pH causes a shift of the experimental curve towards lower osmotic pressures in the dilute and the transition regimes. However, in the concentrated regime, the volume fraction is the same for all the conditions. Whatever pH and ionic strength, the evolution of the solutions morphology follows the same pattern as for pH 7, I = 20 mM, showing in particular solidification for concentrations above the "large volume fraction step".

Discussion

The results presented above demonstrate that the use of osmotic stress applied through a dialysis equilibrium makes it possible to cover a vol- ume fraction / osmotic pressure range that joins, at high concentrations, the data obtained through vapor sorption 29 (Fig. 1). The lowest concentrations that we have studied match the lysozyme concentration in egg white and the highest ones reach those commonly met in industrial processes.

The first aim of this section is to show that the reported (φ , Π) diagrams, unambiguously relating the volume fraction to the osmotic pressure of lysozyme solutions at chosen ionic conditions, constitute the reference experimental counterpart of equations of state (EOS) for lysozyme solutions. We shall then address the nature of the transition regime and its relationship to the volume fractions of the concentrated regime, by considering the nature of the interactions between solutes in the ionic conditions that are imposed by the outer stressing solution.

The (φ , Π) diagrams are reference experimental data for equations of state

The first argument comes from the thermodynamic reversibility of the transformations of the system. Preliminary observations of the morphology gave us a clue about this reversibility, as the samples get back to their liquid, clear form when decompressed to low osmotic pressures, even after having been strongly compressed at 39.75 bar. Focusing on the (φ , Π) diagrams reveals that compressing a lysozyme solution to 39.75 bar and decompressing it back to a lower pressure is equivalent to a one-way compression to the lowest pressure, for ionic strengths ranging from 20 mM to 150 mM at pH 7. The analysis of the pH 7, I = 20 mM samples by Fourier transform infrared spectroscopy (FTIR) clearly showed that the system was composed of the same structural entities, regardless of the volume fraction or the pathway (Fig. S4,ESI). All these features proved that the state of the solution reversibly depends on the pressure, volume fraction and physicochemical conditions, and not on the compression history.

Considering the above, in addition to the fact that the diagrams originate from several data sets and batches of protein, we can state that we established the reference experimental data for equations of state (EOS) of lysozyme solutions, for ionic strengths up to 150 mM.

Nature of the transition regime

Since our data points identify equilibrium states of the system, the existence of a plateau, where the chemical potential of water remains nearly constant over a large range of volume fraction, must reflect the existence of a phase transition.

Small angle X-ray scattering (SAXS) data obtained in the concentrated regime reveal lysozyme crystallization, as shown by Bragg peaks, in all ionic conditions up to I = 150 mM. As an example, the structure factors of lysozyme solutions in a pH 7, I = 20 mM buffer compressed at 1.16 bar and 39.75 bar are presented on Fig. S5,ESI. We therefore propose that the phase transition evidenced by the (φ , Π) diagrams is caused by crystallization of the protein. This hypothesis is consistent with the solubilities determined by Retailleau et al. 44 for lysozyme at pH 6.5 and different NaCl concentrations (φ = 0.25, 0.15 and 0.10 for 0 mM, 50 mM and 100 mM NaCl, respectively).

We interpret the SAXS spectra as powder diffraction spectra. The major crystalline form is tetragonal, of the P 4 3 2 1 2 space group, as found in numerous crystallographic structures of lysozyme (see e.g., 1HEL 45 ). Fitting the lattice parameters allows us to estimate the volume fraction of protein in the crystal. As shown in Fig. 1, the values that result from the fit are quite consistent with the volume fractions of the samples in concentrated regime, indicating that all of the lysozyme was crystallized in these samples. The volume fraction variations between the points shown on the diagram are related to slight changes in the P 4 3 2 1 2 lattice parameters.

Rickard et al. 29 found higher osmotic pressures at volume fraction φ = 0.52 and did not mention crystallization. This is easily explained by the kinetics of concentration in that case. Indeed, the dehydration method used by Rickard et al. causes a rapid concentration of the lysozyme solution, leading to a glassy state within the compressed droplets. Therefore the crystals do not nucleate, and the (φ , Π) diagram follows a liquid-like tendency, parallel to the Carnahan-Starling model, instead of following the bend caused by crystallization in our slow equilibrium experiments. The ratio of osmotic pressures of the glassy and crystal states (×10) is comparable with the solubility ratios commonly found for amorphous and crystalline solids.

The question then arises of the smoothness of the change of slope at the beginning of the transition regime. Indeed, as soon as the nuclei of the crystal have reached the critical size, crystallization should occur without any barrier. Therefore the concentration in the liquid protein phase would remain constant as the chemical potential of lysozyme must be the same in the liquid and crystallized phases. Accordingly, the data would then show an angular profile at the leading edge of the plateau, instead of the smooth pretransition bending shown in Figs. 1 and3.

The existence of an intermediate regime of sub-critical nuclei, or equilibrium clusters 24,25 , could explain the pre-transition bending, as the concentration range where the equilibrium clusters have been observed (φ = 0.12 -0.23) is consistent with most of the transition regime of the (φ , Π) diagram, and the conditions are quite close to ours 25 : low ionic strength, pH 7.8 instead of 7, and same temperature 25 • C). In the next section, we will however show that the pre-transitional bending can also be explained quantitatively by the effects of ionic screening and van der Waals forces.

Interactions between proteins

Since the structure of lysozyme molecules remains the same through the whole range of pressures and volume fractions, it becomes interesting to compare the osmotic pressures of their solutions with those from dispersions of monodisperse spherical particles. A first observation is that the Carnahan-Starling equation of state provides a surprisingly good fit to the data over 4 decades in pressures, and even at concentrations where the virial equation of state with only 2-body interactions is not expected to hold (Fig. 1). Here we show that deviations from the Carnahan-Starling equation can be partly accounted for by taking into account the ionic interactions between proteins, and their interactions due to van der Waals forces.

To explain the impact of ionic conditions on osmotic pressures in the dilute regime, with the simple hypotheses that lysozyme molecules are spheres with a uniform surface charge density and following a meanfield approach, we developed a generalized van der Waals (GVDW) model (see the full development in Supporting Information) leading to the expression of the osmotic pressure as a function of an effective pair potential:

β Π v φ = 1 + φ + φ 2 -φ 3 (1 -φ ) 3 + 2π φ v ∞ 2a β w(r)r 2 dr (4)
where β = 1/k B T is the reciprocal of the thermal energy, Π is the osmotic pressure, v is the protein molecular volume, φ is the volume fraction, a is the molecular hard-core radius, r the intermolecular centerto-center distance and w is an effective pair potential.

In order to account for the shift of the experimental osmotic pressures upon changes in pH or ionic strength, we describe the contribution of screened ionic repulsions to the pair potential by a Debye-Hückel potential,

β w DH (r) = Z 2 L B (1 + κa) 2 e -κ(r-2a) r ( 5
)
where Z is the molecular charge, L B is the Bjerrum length. κ is the reciprocal of the screening length and, if the protein counterions are taken into account, κ is defined by:

κ 2 = 4πL B N A (2C S + ZC P ) (6)
where N A is the Avogadro constant, C S is the pair concentration of monovalent salt and C P is the protein molar concentration. The contribution of short-ranged van der Waals forces to the effective pair potential is accounted for by a Hamaker potential,

β w H (r) = - A H 6 2a 2 r 2 -4a 2 + 2a 2 r 2 + ln r 2 -4a 2 r 2 (7)
for r > 2a, infinity otherwise, where A H is the Hamaker constant (in k B T units). The total pair potential can be written as w(r) = w DH (r) + w H (r), and the expression of osmotic pressure given by Eq. 4 then can be fitted to the experimental data, through numerical integration of its interaction term, using the Hamaker constant A H as the only adjustable parameter (the lower integration limit was increased by 0.02 nm to avoid divergence).

We fit this model in the packing fraction region below the crystallization, with a global A H , common to all pH and ionic strength conditions. The protein charge Z was fixed to the theoretical net charge of the protein for the considered pH. Results are shown in Fig. 4, where the model is drawn on the experimental points used for the fitting. In spite of large approximations (lysozyme figured as a spherical molecule with uniform surface charge density, mean-field model assuming a step-shaped pair correlation function), our single-parameter GVDW model accounts strikingly well for the shape of the experimental data in the low-concentration range, as well as for their tendency to shift upon changes in the ionic conditions.

As regards the shape of the (φ , Π) diagrams, especially the downward bending observed below the crystallization plateau, it is important to point out that the counterions of the proteins strongly screen the electrostatic interactions, especially at high protein volume fractions, and that it is necessary to take this contribution into account in order to reproduce the shape of the data in the dilute and transition regime (see Fig. S6, ESI, for an example at pH 7 and ionic strength 20 mM). The increase of the concentration of these counterions, and thus of the effective ionic strength, with volume fraction may be a cause of the existence of equilibrium clusters in a concentration range that is consistent with the transition regime of the (φ , Π) curve. Indeed, the bending of the curve occurs when the counterions concentration is sufficient to decrease significantly the repulsions between proteins and thus favor the attractions, giving rise to a new balance of interactions. Moreover, the aggregation number of the equilibrium clusters has been shown to be related to changes that favor attractions over repulsions, such as a decrease of the temperature or an increase of the salt concentration, but also to the increase in volume fraction 24,25 . This latter point could be explained by the increase in counterion concentration, which has a major effect in screening ionic repulsions, as explained above. This screening of ionic repulsions may cause an increase in the size of equilibrium clusters size, until the repulsions are so low that a barrier no longer exists to lysozyme self-association. At this point the association of lysozyme into equilibrium clusters is preempted by crystallization.

The fitted model still fails to describe quantitatively the strength of ionic repulsions at low ionic strength, and also the strength of attractions at high ionic strength.

The discrepancy between the experimental data and the model could be due to the simplicity of the assumptions of our model (uniformly charged spherical particles). It could also be due to specific interactions of salt ions with protein residues, which are the subject of a very active debate [46][47][48][49][50] . In particular, deviations of the effective net charge from the predicted one may be caused by added salt due to ionic strength effects but also to specific ion effects [51][52][53] .

Conclusion

Our results show complete experimental osmotic pressures vs. volume fraction for the aqueous solutions of a protein. Each point of these curves illustrates an equilibrium state of the lysozyme solution. Relationships between osmotic pressure and concentration in solu-tions of lysozyme and a few other proteins have already been described [11][12][13][14]20,54,55 , but our experiments span much wider ranges of osmotic pressure and concentration. As a consequence, all the states classically described for protein solutions have been explored, from the ideally dilute solution to the solid state, for which the solidus line, usually extrapolated from the density of crystals, is poorly described in phase diagrams 56 . Moreover, these data highlight the crystallization transition, and its displacement towards lower volume fractions caused by the decrease of the range and strength of the electrostatic interactions. The crystallization transition shown by our data is consistent with the solubility data available in the literature 44 , and with a crystal space group well known for lysozyme 45 .

Simple colloidal models, without interactions other than steric, such as the Carnahan-Starling model, do not reproduce any of our data series. However, for all our experimental data, the low packing fraction region up to the crystallization event is correctly described by the combination of a steric repulsion (Carnahan-Starling model), van der Waals forces and a screened electrostatic repulsion as described by the classical Debye-Hückel potential, provided that the contribution from the counterions of the proteins to the screening is taken into account. Quantitative agreement between this model and the experimental data would probably require to take into account the shape and charge distribution of the molecules. The possible specific interactions between ions and protein residues 51,[57][58][START_REF] Zhang | Protein-Protein Interactions -Computational and Experimental Tools[END_REF] could also make the electrical charge of the protein deviate from theoretical predictions based of the pK a of the aminoacids.

The mechanisms involved in our description of the dilute part of the osmotic pressure vs. volume fraction of lysozyme, i.e., the balance between short-range attraction and long-range repulsion have been described for colloids [START_REF] Groenewold | [END_REF] and lysozyme 24 and may be applicable to other proteins. However, some features of our experimental data are related to specific properties of lysozyme, like its ability to crystallize in the physicochemical conditions we used. Indeed, the plateau reflecting the crystallization transition has not yet been observed for other globular proteins, such as ovalbumin 12 or BSA 11 . This may be due to the smaller range of concentration, but more likely to the experimental conditions (pH, ionic strength, nature of salts, kinetics of concentration, temperature) that, depending on the protein, favor behaviors other than crystallization when the solutions are highly concentrated. The high concentration part of the osmotic pressure vs. volume fraction curve is then probably also controlled by other protein properties, such as anisotropy of shape and charge density. The determination of the contribution of these structural specificities in the equations of state of proteins is still to be explored.

Figure 1 :

 1 Figure 1: (φ , Π) diagram of lysozyme in a pH 7, I = 20 mM bis-tris propane buffer, obtained by one-way compression (filled blue circles), or by compression to 39.75 bar followed by decompression to different pressures ("two-way compression", empty black circles): the arrows symbolize the decompression part of the two-way compression experiments. The solid line represents the Carnahan-Starling model, the dashed black line represents the van't Hoff model. Data from Rickard et al.29 obtained by bulk vapor desorption are represented by green triangles. Our data from dynamic vapor sorption (DVS, empty blue circles) were obtained using lysozyme solutions initially at pH 7 and 35 mM ionic strength, but DVS does not keep concentrations constant. Crystal densities extracted from SAXS data (see discussion, section 4.2) are represented by orange diamonds.

3. 2 Figure 2 :

 22 Figure 2: Photographs of dialysis bags containing lysozyme at pH 7 and 20 mM ionic strength, submitted to different osmotic pressures: 0.05 bar (A), 0.39 bar (B), 1.16 bar (C), 2.30 bar (D) and 39.75 bar (E). Photograph (F) shows the bag after compressing the solution from 0.05 bar to 39.75 bar, then decompressing it back to 0.05 bar.

Figure 3 :

 3 Figure 3: (φ , Π) diagrams of lysozyme for several physicochemical conditions. Conditions presented are: pH 7, ionic strength I = 20 mM (grey empty circles); pH 7, I = 35 mM (dark blue circles); pH 7, I = 150 mM (light blue circles) and pH 9, I = 20 mM (red squares). The solid line represents the Carnahan-Starling model, the dashed line represents the van't Hoff model.

Figure 4 :

 4 Figure 4: Fit of the generalized van der Waals model to the experimental osmotic pressures of lysozyme in the dilute region. The model (solid lines) was fitted simultaneously to the 4 plotted series of experimental data, using Z/e values of 8.3 and 6.3 at pH 7 (circles) and pH 9 (squares), respectively. The corresponding fitted value of the Hamaker constant is 3.76 k B T . Conditions are pH 7, I = 20 mM (dark blue), pH 7, I = 35 mM (medium blue), pH 7, I = 150 mM (light blue) and pH 9, I = 20 mM (red). The model lines are plotted only in the volume fraction range used for the fit. The dashed line represents the Carnahan-Starling model.

Acknowledgement

The authors thank Martine Meireles, Yannick Hallez, Christophe Labbez, Marie Skepö, Valérie Briard-Bion, Julien Jardin for helpful discussions.