Thierry Coquand
email: coquand@cse.gu.se

Henri Lombardi
email: lombardi@univ-fcomte.fr

Hidden constructions in abstract algebra Krull Dimension of distributive lattices and commutative rings

Keywords: MSC 2000: 13C15, 03F65, 13A15, 13E05 Krull dimension, distributive lattices, Constructive Mathematics

We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors. We show that the notion of Krull dimension has an explicit computational content in the form of existence (or lack of existence) of some algebraic identities. We can then get an explicit computational content where abstract results about dimensions are used to show the existence of concrete elements. This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.

This paper has been published as: Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. p. 477-499 in Commutative ring theory and applications (Fez, 2001), Lecture Notes in Pure and Applied Mathematics, volume 231. Dekker, New-York (2003).

Here we have updated the bibliography. Notice also that for entailment relations and from a constructive viewpoint it is simpler to take P f (S) as the set of finitely enumerated subsets of S (rather than finite subsets).

Introduction

We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors. We show that the notion of Krull dimension has an explicit computational content in the form of existence (or lack of existence) of some algebraic identities. This confirms the feeling that commutative algebra can be seen computationally as a machine that produces algebraic identities (the most famous of which being called Nullstellensatz). This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.

Our presentation follows Bishop's style (cf. in algebra [START_REF] Mines | A Course in Constructive Algebra[END_REF]). As much as possible, we kept minimum any explicit mention to logical notions. When we say that we have a constructive version of an abstract algebraic theorem, this means that we have a theorem the proof of which is constructive, which has a clear computational content, and from which we can recover the usual version of the abstract theorem by an immediate application of a well classified non-constructive principle. An abstract classical theorem can have several distinct interesting constructive versions.

In the case of abstract theorem in commutative algebra, such a non-constructive principle is the completeness theorem, which claims the existence of a model of a formally consistent propositional theory. We recall the exact formulation of this theorem in the appendix, as well as its derivation from the compactness theorem When this is used for algebraic structures of enumerable presentation (in a suitable sense) the compactness and completeness theorem can be seen as a reformulation of Bishop LLPO (a real number is ≥ 0 or ≤ 0).

To avoid the use of completeness theorem is not motivated by philosophical but by practical considerations. The use of this principle leads indeed to replace quite direct (but usually hidden) arguments by indirect ones which are nothing else than a double contraposition of the direct proofs, with a corresponding lack of computational content. For instance [START_REF] Coste | Dynamical method in algebra: Effective Nullstellensätze[END_REF] the abstract proof of 17 th Hilbert's problem claims : if the polynomial P is not a sum of rational fractions there is a field K in which one can find an absurdity by reading the (constructive) proof that the polynomial is everywhere positive or zero. The direct version of this abstract proof is: from the (constructive) proof that the polynomial is everywhere positive or zero, one can show (using arguments of the abstract proofs) that any attempt to build K will fail. This gives explicitly the sum of squares we are looking for. In the meantime, one has to replace the abstract result: "any real field can be ordered" by the constructive theorem: "in a field in which any attempt to build an ordering fails -1 is a sum of squares". One can go from this explicit version to the abstract one by completeness theorem, while the proof of the explicit version is hidden in the algebraic manipulations that appear in the usual classical proof of the abstract version.

Here is the content of the paper.

Distributive lattices

In this section, we present basic theorems on distributive lattices. An important simplification of proofs and computations is obtained via the systematic use of the notion of entailment relation, which has its origin in the cut rule in Gentzen's sequent calculus, with the fundamental theorem 1.7.

Dimension of distributive lattices

In this section, we develop the theory of Krull dimension of distributive lattices, explaining briefly the connection with Español's developments of Joyal' s theory. We show that the property to have a Krull dimension ≤ can be formulated as the existence of concrete equalities in the distributive lattice.

Zariski and Krull lattice

In section 3 we define the Zariski lattice of a commutative ring (whose elements are radicals of finitely generated ideals), which is the constructive counterpart of Zariski spectrum : the points of Zariski spectrum are the prime ideals of Zariski lattice, and the constructible subsets of Zariski spectrum are the elements of the Boolean algebra generated by the Zariski lattice. Joyal's idea is to define Krull dimension of a commutative ring as the dimension of its Zariski lattice. This avoids any mention of prime ideals. We show the equivalence between this (constructive) point of view and the (constructive) presentation given in [START_REF] Lombardi | Dimension de Krull, Nullstellensätze et Évaluation dynamique[END_REF], showing that the property to have a Krull dimension ≤ can be formulated as the existence of concrete equalities in the ring.

Conclusion

This article confirms the actual realisation of Hilbert's program for a large part of abstract commutative algebra. (cf. [START_REF] Coste | Dynamical method in algebra: Effective Nullstellensätze[END_REF][START_REF] Coquand | Valuations and Dedekind's Prague Theorem[END_REF][START_REF] Kuhlmann | Construction du hensélisé d'un corps valué[END_REF]11,[START_REF] Lombardi | Le contenu constructif d'un principe local-global avec une application à la structure d'un module projectif de type fini[END_REF][START_REF] Lombardi | Relecture constructive de la théorie d'Artin-Schreier[END_REF][START_REF] Lombardi | Dimension de Krull, Nullstellensätze et Évaluation dynamique[END_REF][START_REF] Lombardi | localisation et anneaux de Prüfer: une approche constructive[END_REF]16,17]). The general idea is to replace ideal abstract structures by partial specifications of these structures. The very short elegant abstract proof which uses these ideal objects has then a corresponding computational version at the level of the partial specifications of these objects. Most of classical results in abstract commutative algebra, the proof of which seem to require in an essential way excluded middle and Zorn's lemma, seem to have in this way a corresponding constructive version. Most importantly, the abstract proof of the classical theorem always contains, more or less implicitly, the constructive proof of the corresponding constructive version. Finally, we should note that the explicit characterisations of Krull dimension of distributive lattices, Theorem 2.9, of spectral spaces, Theorem 2.14, and of rings, Corollary 3.6, are new.

Distributive lattice, Entailment relations

Elementary though it has become after successive presentations and simplifications, the theory of distributive lattices is the ideal instance of a mathematical theory, where a syntax is specified together with a complete description of all models, and what is more, a table of semantic concepts and syntactic concepts is given, together with a translation algorithm between the two kinds of concepts. Such an algorithm is a "completeness theorem" (G. C. Rota [START_REF] Rota | Indiscrete Thoughts Birkhauser[END_REF]).

Distributive lattices, filters and spectrum

As indicated by the quotation above, the structure of distributive lattices is fundamental in mathematics, and G.C. Rota has pointed out repeatedly its potential relevance to commutative algebra and algebraic geometry. A distributive lattice is an ordered set with finite sups and infs, a minimum element (written 0) and a maximum element (written 1). The operations sup and inf are supposed to be distributive w.r.t. the other. We write these operations ∨ and ∧ . The relation a ≤ b can then be defined by a ∨ b = b or, equivalently, a ∧ b = a. The theory of distributive lattices is then purely equational. It makes sense then to talk of distributive lattices defined by generators and relations.

A quite important rule, the cut rule, is the following

(((x ∧ a) ≤ b) & (a ≤ (x ∨ b))) =⇒ a ≤ b.
In order to prove this, write

x ∧ a ∧ b = x ∧ a and a = a ∧ (x ∨ b) hence a = (a ∧ x) ∨ (a ∧ b) = (a ∧ x ∧ b) ∨ (a ∧ b) = a ∧ b.
A totally ordered set is a distributive lattice as soon as it has a maximum and a minimum element. We write n for the totally ordered set with n elements (this is a distributive lattice for n = 0.) A product of distributive lattices is a distributive lattice. Natural numbers with the divisibility relation form a distributive lattice (with minimum element 1 and maximum element 0). If L and L are two distributive lattices, the set Hom(L, L ) of all morphisms (i.e., maps preserving sup, inf, 0 and 1) from L to L has a natural order given by

ϕ ≤ ψ def ⇐⇒ ∀x ∈ L ϕ(x) ≤ ψ(x).
A map between two totally ordered distributive lattices L and S is a morphism if, and only if, it is nondecreasing and 0 L and 1 L are mapped into 0 S and 1 S .

The following proposition is direct.

Proposition 1.1 Let L be a distributive lattice and J a subset of L. We consider the distributive lattice L generated by L and the relations x = 0 for x ∈ J (L is a quotient of L). Then

• the equivalence class of 0 is the set of a such that for some finite subset J 0 of J:

a ≤ x∈J0 x in L
• the equivalence class of 1 is the set of b such that for some finite subset J 0 of J:

1 = b ∨ x∈J0 x in L
• More generally a ≤ L b if, and only if, for some finite subset J 0 of J:

a ≤ b ∨ x∈J0 x
In the previous proposition, the equivalence class of 0 is called an ideal of the lattice; it is the ideal generated by J. We write it J L . We can easily check that an ideal I is a subset such that:

0 ∈ I x, y ∈ I =⇒ x ∨ y ∈ I x ∈ I, z ∈ L =⇒ x ∧ z ∈ I (the last condition can be written (x ∈ I, y ≤ x) ⇒ y ∈ I).
Furthermore, for any morphim ϕ :

L 1 → L 2 , ϕ -1 (0) is an ideal of L 1 .
A principal ideal is an ideal generated by one element a. We have a L = {x ∈ L ; x ≤ a}. Any finitely generated ideal is principal.

The dual notion of ideal is the one of filter. A filter F is the inverse image of 1 by a morphism. This is a subset such that: [START_REF] Coste | Dynamical method in algebra: Effective Nullstellensätze[END_REF] We write P f (X) for the set of all finite subsets of the set X. If A is a finite subset of a distributive lattice L we define

1 ∈ F x, y ∈ F =⇒ x ∧ y ∈ F x ∈ F, z ∈ T =⇒ x ∨ z ∈ F Notation 1.
A := x∈A x and A := x∈A x
We write A B or A L B for the relation defined on the set P f (L):

A B def ⇐⇒ A ≤ B
Note the relation A B is well defined on finite subsets because of associativity commutativity and idempotence of the operations ∧ and ∨ . Note also ∅ {x} ⇒ x = 1 and {y} ∅ ⇒ y = 0. This relation satisfies the following axioms, where we write x for {x} and A, B for

A ∪ B. a a (R) (A B) & (A ⊆ A ) & (B ⊆ B ) =⇒ A B (M ) (A, x B) & (A B, x) =⇒ A B (T )
we say that the relation is reflexive, monotone and transitive. The last rule is also called cut rule.

Let us also mention the two following rules of "distributivity":

(A, x B) & (A, y B) ⇐⇒ A, x ∨ y B (A B, x) & (A B, y) ⇐⇒ A B, x ∧ y
The following is proved in the same way as Proposition 1.1.

1 Distributive lattice, Entailment relations Proposition 1.3 Let L be a distributive lattice and (J, U ) a pair of subsets of L. We consider the distributive lattice L generated by L and by the relations x = 0 for x ∈ J and y = 1 for y ∈ U (L is a quotient of L). We have that:

• the equivalence class of 0 is the set of elements a such that:

∃J 0 ∈ P f (J), U 0 ∈ P f (U ) a, U 0 L J 0
• the equivalence class of 1 is the set of elements b such that: vérifient:

∃J 0 ∈ P f (J), U 0 ∈ P f (U ) U 0 L b, J 0
• More generally a ≤ L b if, and only if, there exists a finite subset J 0 of J and a finite subset

U 0 of U such that, in L: a, U 0 L b, J 0
We shall write L/(J = 0, U = 1) for the quotient lattice L described in Proposition 1.3. Let ψ : L → L be the canonical surjection. If I is the ideal ψ -1 (0) and F the filter ψ -1 (1), we say that the ideal I and the filter F are conjugate. By the previous proposition, an ideal I and a filter F are conjugate if, and only if, we have:

[I 0 ∈ P f (I), F 0 ∈ P f (F ), (x, F 0 I 0 )] =⇒ x ∈ I and [I 0 ∈ P f (I), F 0 ∈ P f (F ), (F 0 x, I 0 )] =⇒ x ∈ F.
This can also be formulated as follows:

(f ∈ F, x ∧ f ∈ I) =⇒ x ∈ I and (j ∈ I, x ∨ j ∈ F ) =⇒ x ∈ F.
When an ideal I and a filter F are conjugate, we have

1 ∈ I ⇐⇒ 0 ∈ F ⇐⇒ (I, F ) = (L, L).
We shall also write L/(I, F ) for L = L/(J = 0, U = 1) . By Proposition 1.3, a homomorphism ϕ from L to another lattice L 1 satisfying ϕ(J) = {0} and ϕ(U ) = {1} can be factorised in an unique way through the quotient L . As shown by the example of totally ordered sets a quotient of distributive lattices is not in general characterised by the equivalence classes of 0 and 1.

Classically a prime ideal I of a lattice is an ideal whose complement F is a filter (which is then a prime filter). This can be expressed by

1 / ∈ I and (x ∧ y) ∈ I =⇒ (x ∈ I or y ∈ I) ( * )
which can also be expressed by saying that I is the kernel of a morphism from L into the lattice with two elements written 2. Constructively, at least in the case where L is discrete, it seems natural to take the definition ( * ), where "or" is used constructively. The notion of prime filter is then defined in a dual way.

Definition 1.4

Let L be a distributive lattice.

• An idealistic prime in L is given by a pair (J, U ) of finite subsets of L. We consider this as an incomplete specification for a prime ideal P satisfying J ⊆ P and U ∩ P = ∅.

• To any idealistic prime (J, U ) we can associate a pair (I, F ) as described in Proposition 1.3 where I is an ideal, F is a filter and I, F are conjugate.

Theorem 1.5 (Simultaneous collapse for idealistic primes) Let (J, U ) be an idealistic prime for a lattice L and x be an element of L. If the idealistic primes (J ∪ {x}, U ) and (J, U ∪ {x}) collapse, then so does (J, U ).

Proof.

We have two finite subsets J 0 , J 1 of J and two finite subsets

U 0 , U 1 of U such that x, U 0 J 0 and U 1 x, J 1 hence x, U 0 , U 1 J 0 , J 1 and U 0 , U 1 x, J 0 , J 1 By the cut rule U 0 , U 1 J 0 , J 1
Notice the crucial role of the cut rule.

Distributive lattices and entailment relations

An interesting way to analyse the description of distributive lattices defined by generators and relations is to consider the relation A B defined on the set P f (L) of finite subsets of a lattice L. Indeed if S ⊆ L generates the lattice L, then the relation on P f (S) is enough to characterise the lattice L, because any formula on S can be rewritten, in normal conjunctive form (inf of sups in S) and normal disjunctive form (sup of infs in S). Hence if we want to compare two elements of the lattice generated by S we write the first in normal disjunctive form, the second in normal conjunctive form, and we notice that

i∈I A i ≤ j∈J B j ⇐⇒ & (i,j)∈I×J (A i B j )
Definition 1.6 For an arbitrary set S, a relation over P f (S) which is reflexive, monotone and transitive (see page 5) is called an entailment relation.

The notion of entailment relations goes back to Gentzen sequent calculus, where the rule (T ) (the cut rule) is first explicitly stated, and plays a key role. The connection with distributive lattices has been emphasized in [START_REF] Cederquist | Entailment relations and Distributive Lattices Logic Colloquium[END_REF][START_REF] Coquand | Valuations and Dedekind's Prague Theorem[END_REF]. The following result (cf. [START_REF] Cederquist | Entailment relations and Distributive Lattices Logic Colloquium[END_REF]) is fundamental. It says that the three properties of entailment relations are exactly the ones needed in order to have a faithfull interpretation in distributive lattices. Theorem 1.7 (fundamental theorem of entailment relations) Let S be a set with an entailment relation S over P f (S). Let L be the lattice defined by generators and relations as follows: the generators are the elements of S and the relations are

A ≤ B whenever A S B.
For any finite subsets A and B of S we have

A L B ⇐⇒ A S B.

Proof.

We give an explicit possible description of the lattice L. The elements of L are represented by finite sets of finite sets of elements of

S X = {A 1 , . . . , A n } (intuitively X represents A 1 ∨ • • • ∨ A n ). We define then inductively the relation A ≺ Y with A ∈ P f (S) and Y ∈ L (intuitively A ≤ C∈Y ( C))
1 Distributive lattice, Entailment relations

• if B ∈ Y and B ⊆ A then A ≺ Y • if A S y 1 , . . . , y m and A, y j ≺ Y for j = 1, . . . , m then A ≺ Y
It is easy to show that if A ≺ Y and A ⊆ A then we have also A ≺ Y. It follows that A ≺ Z holds whenever A ≺ Y and B ≺ Z for all B ∈ Y . We can then define X ≤ Y by A ≺ Y for all A ∈ X and one can then check that L is a distributive lattice1 for the operations

0 = ∅, 1 = {∅}, X ∨ Y = X ∪ Y, X ∧ Y = {A ∪ B | A ∈ X, B ∈ Y }.
For establishing this one first show that if C ≺ X and C ≺ Y we have C ≺ X ∧ Y by induction on the proofs of C ≺ X and C ≺ Y . We notice then that if A S y 1 , . . . , y m and A, y j S B for all j then A S B using m times the cut rule. It follows that if we have

A L B, i.e., A ≺ {{b} | b ∈ B}, then we have also A S B.
As a first application, we give the description of the Boolean algebra generated by a distributive lattice. A Boolean algebra can be seen as a distributive lattice with a complement operation x → x such that x ∧ x = 0 and x ∨ x = 1. The application x → x is then a map from the lattice to its dual. Proposition 1.8 Let L be a distributive lattice. There exists a free Boolean algebra generated by L. It can be described as the distributive lattice generated by the set L 1 = L ∪ L2 with the entailment relation L1 defined as follows: if A, B, A , B are finite subsets of L we have

A, B L1 A , B def ⇐⇒ A, B A , B in L
If we write L Bool for this lattice (which is a Boolean algebra), there is a natural embedding of L 1 in L Bool and the entailment relation of L Bool induces on L 1 the relation L1 .

Proof.

See [START_REF] Cederquist | Entailment relations and Distributive Lattices Logic Colloquium[END_REF].

Notice that by Theorem 1.7 we have x L y if, and only if, x L1 y hence the canonical map L → L 1 is one-to-one and L can be identified to a subset of L 1 .

Spectrum and completeness theorem

The spectrum of the lattice L, written Spec(L) is defined as the set Hom(L, 2). It is isomorphic to the ordered set of all detachable prime ideals. The order relation is then reverse inclusion. We have Spec(2) 1, Spec(3) 2, Spec(4) 3, etc. . .

Proposition 1.9

The completeness theorem implies the following result. If (J, U ) is an idealistic prime which does not collapse then there exists ϕ ∈ Spec(L) such that J ⊆ ϕ -1 (0) and U ⊆ ϕ -1 (1).

In particular if a ≤ b, there exists ϕ ∈ Spec(L) such that ϕ(a) = 1 and ϕ(b

) = 0. Also, if L = 1, Spec(L) is nonempty.
Proof. This follows from the completeness theorem for geometric theories (see Appendix).

A corollary is the following representation theorem (Birkhoff theorem) Theorem 1.10 (Representation theorem) The completeness theorem implies the following result. The map θ L : L → P(Spec(L)) defined by a → {ϕ ∈ Spec(L) ; ϕ(a) = 1} is an injective map of distributive lattice. This means that any distributive lattice can be represented as a lattice of subsets of a set.

Another corollary is the following proposition.

Proposition 1.11

The completeness theorem implies the following result. Let ϕ : L → L a map of distributive lattices; ϕ is injective if, and only if, Spec(ϕ) : Spec(L ) → Spec(L) is surjective.

Proof.

We have the equivalence

a = b ⇐⇒ a ∧ b = a ∨ b ⇐⇒ a ∨ b ≤ a ∧ b Assume that Spec(ϕ) is surjective. If a = b in L, take a = ϕ(a), b = ϕ(b) and let ψ ∈ Spec(L) be such that ψ(a ∨ b) = 1 and ψ(a ∧ b) = 0. Since Spec(ϕ) is surjective there exists ψ ∈ Spec(L ) such that ψ = ψ ϕ hence ψ (a ∨ b ) = 1 and ψ (a ∧ b ) = 0, hence a ∨ b ≤ a ∧ b and a = b . Suppose that ϕ is injective. We identify L to a sublattice of L . If ψ ∈ Spec(L), take I = ψ -1 (0) and F = ψ -1 (1)
. By the compactness theorem (see appendix), there exists ψ ∈ Spec(L ) such that ψ (I) = 0 and

ψ (F ) = 1, which means ψ = ψ • ϕ.
Of course, these three last results are hard to interpret in a computational way. An intuitive interpretation is that we can proceed "as if" any distributive lattice is a lattice of subsets of a set. The goal of Hilbert's program is to give a precise meaning to this sentence, and explain what is meant by "as if" there.

Krull dimension of distributive lattices 2.1 Definition of Kr (L)

To develop a suitable constructive theory of the Krull dimension of a distributive lattice we have to find a constructive counterpart of the notion of increasing chains of prime ideals.

Definition 2.1

To any distributive lattice L and ∈ N we associate a distributive lattice Kr (L) which is the lattice defined by the generators ϕ i (x) for i ≤ and x ∈ L (thus we have + 1 disjoint copies of L and we let ϕ i be the bijection between L and the ith copy) and relations

• ϕ i (1) • ϕ i (0) • ϕ i (a), ϕ i (b) ϕ i (a ∧ b) • ϕ i (a ∨ b) ϕ i (a), ϕ i (b) • ϕ i (a) ϕ i (b) whenever a ≤ b in L • ϕ i+1 (a) ϕ i (a) for i <
Let S be the disjoint union ϕ i (L) and S the entailment relation generated by these relations.

From this definition, we get directly the following theorem.

Theorem 2.2

The maps ϕ i are morphisms from the lattice L to the lattice Kr (L). Furthermore the lattice Kr (L) with the maps ϕ i is then a solution of the following universal problem: to find a distributive lattice K and + 1 homomorphisms

ϕ 0 ≥ ϕ 1 ≥ • • • ≥ ϕ from L to K such that, for any lattice L and any morphism ψ 0 ≥ ψ 1 ≥ • • • ≥ ψ ∈ Hom(L, L ) we have one and only one morphism η : K → L such that ηϕ 0 = ψ 0 , ηϕ 1 = ψ 1 , . . ., ηϕ = ψ .
The next theorem is the main result of this paper, and uses crucially the notion of entailment relation.

Theorem 2.3

If U i and J i (i = 0, . . . , ) are finite subsets of L we have in Kr (L)

ϕ 0 (U 0 ) ∧ . . . ∧ ϕ (U ) ≤ ϕ 0 (J 0 ) ∨ . . . ∨ ϕ (J )
if, and only if, ϕ 0 (U 0 ), . . . , ϕ (U ) S ϕ 0 (J 0 ), . . . , ϕ (J )

if, and only if, there exist x 1 , . . . , x ∈ L such that (where is the entailment relation of L):

x 1 , U 0 J 0 x 2 , U 1 J 1 , x 1 . . . . . . . . . x , U -1 J -1 , x -1 U J , x
Proof.

The equivalence between the first and the second statement follows from Theorem 1.7.

We show next that the relation on P f (S) described in the statement of the theorem is indeed an entailment relation. The only point that needs explanation is the cut rule. To simplify notations, we take = 3. We have then 3 possible cases, and we analyse only one case, where X, ϕ 1 (z) S Y and X S Y, ϕ 1 (z), the other cases being similar. By hypothesis we have

x 1 , x 2 , x 3 , y 1 , y 2 , y 3 such that x 1 , U 0 J 0 y 1 , U 0 J 0 x 2 , U 1 , z J 1 , x 1 y 2 , U 1 J 1 , y 1 , z x 3 , U 2 J 2 , x 2 y 3 , U 2 J 2 , y 2 U 3 J 3 , x 3 U 3 J 3 , y 3
The two entailment relations on the second line give

x 2 , y 2 , U 1 , z J 1 , x 1 , y 1 x 2 , y 2 , U 1 J 1 , x 1 , y 1 , z hence by cut x 2 , y 2 , U 1 J 1 , x 1 , y 1 i.e., x 2 ∧ y 2 , U 1 J 1 , x 1 ∨ y 1
Finally, using distributivity

(x 1 ∨ y 1 ), U 0 J 0 (x 2 ∧ y 2 ), U 1 J 1 , (x 1 ∨ y 1 ) (x 3 ∧ y 3 ), U 2 J 2 , (x 2 ∧ y 2 ) U 3 J 3 , (x 3 ∧ y 3 )
and hence ϕ 0 (U 0 ), . . . , ϕ 3 (U 3 ) S ϕ 0 (J 0 ), . . . , ϕ 3 (J 3 ). Finally it is left to notice that the entailment relation we have defined is clearly the least possible relation ensuring the ϕ i to form a non-increasing chain of morphisms.

Notice that the morphisms ϕ i are injective: it is easily seen that for a, b ∈ L the relation ϕ i (a) S ϕ i (b) implies a b, and hence that ϕ i (a) = ϕ i (b) implies a = b.

Partially specified chains of prime ideals

Definition 2. [START_REF] Coquand | Valuations and Dedekind's Prague Theorem[END_REF] In a distributive lattice L, a partial specification for a chain of prime ideals (that we shall call idealistic chain) is defined as follows. An idealistic chain of length is a list of + 1 idealistic primes of L: C = ((J 0 , U 0 ), . . . , (J , U )). An idealistic chain of length 0 is nothing but an idealistic prime.

We think of an idealistic chain of length as a partial specification of an increasing chains of prime ideals P 0 , . . . , P such that J i ⊆ P i , U i ∩ P i = ∅, (i = 0, . . . , ).

Definition 2.5

We say that an idealistic chain ((J 0 , U 0 ), . . . , (J , U )) collapses if, and only if, we have in Kr (L) ϕ 0 (U 0 ), . . . , ϕ (U ) S ϕ 0 (J 0 ), . . . , ϕ (J )

Thus an idealistic chain ((J 0 , U 0 ), . . . , (J , U )) collapses in L if, and only if, the idealistic prime P = (ϕ 0 (J 0 ), . . . , ϕ (J ); ϕ 0 (U 0 ), . . . , ϕ (U )) collapses in Kr (L). From the completeness theorem we deduce the following result which justifies this idea of partial specification.

Theorem 2.6 (formal Nullstellensatz for chains of prime ideals)

The completeness theorem implies the following result. Let L be a distributive lattice and ((J 0 , U 0 ), . . . , (J , U )) be an idealistic chain in L. The following properties are equivalent:

(a) There exist + 1 prime ideals

P 0 ⊆ • • • ⊆ P such that J i ⊆ P i , U i ∩ P i = ∅, (i = 0, . . . , ).
(b) The idealistic chain does not collapse.

Proof.

If (b) holds then the idealistic prime P = (ϕ 0 (J 0 ), . . . , ϕ (J ); ϕ 0 (U 0 ), . . . , ϕ (U )) does not collapse in Kr (L). It follows then from Proposition 1.9 that there exists σ ∈ Spec( Kr (L)) such that σ is 0 on ϕ 0 (J 0 ), . . . , ϕ (J ) and 1 on ϕ 0 (U 0 ), . . . , ϕ (U )). We can then take

P i = (σ • ϕ i ) -1 (0). That (a) implies (b) is direct.

Krull dimension of a distributive lattice

Definition 2.7 1) An elementary idealistic chain in a distributive lattice L is an idealistic chain of the form ((0, x 1 ), (x 1 , x 2 ), . . . , (x , 1)) (with x i in L).

2) A distributive lattice L is of dimension ≤ -1 iff it satisfies one of the equivalent conditions

-Any elementary idealistic chain of length collapses.

-For any sequence x 1 , . . . , x ∈ L we have

ϕ 0 (x 1 ), . . . , ϕ -1 (x ) ϕ 1 (x 1 ), . . . , ϕ (x ) in Kr (L),
The following result shows that this definition coincides with the classical definition of Krull dimension for lattices.

Theorem 2.8 The completeness theorem implies that the Krull dimension of a lattice L is ≤ -1 if, and only if, there is no strictly increasing chains of prime ideals of length .

Using Theorem 2.3, we get the following characterisation.

Theorem 2.9 A distributive lattice L is of Krull dimension ≤ -1 if, and only if, for all

x 1 , . . . , x ∈ L there exist a 1 , . . . , a ∈ L such that

a 1 ∧ x 1 = 0, a 2 ∧ x 2 ≤ a 1 ∨ x 1 , , . . . , a ∧ x ≤ a -1 ∨ x -1 , 1 = a ∨ x
In this way we have given a concrete form of the statement that the distributive lattice L has a dimension ≤ -1 in the form of an existence of a sequence of inequalities.

In particular the distributive lattice L is of dimension ≤ -1 if, and only if, 1 = 0 in L, and it is of dimension ≤ 0 if, and only if, L is a Boolean algebra (any element has a complement).

We have furthermore.

Lemma 2.10 A distributive lattice L generated by a set G is of dimension ≤ -1 if, and only if, for any sequence x 1 , . . . , x ∈ G ϕ 0 (x 1 ), . . . , ϕ -1 (x ) ϕ 1 (x 1 ), . . . , ϕ (x )

in Kr (L).

Indeed using distributivity, one can deduce

a ∨ a , A b ∨ b , B a ∧ a , A b ∧ b , B
from a, A b, B and a , A b , B. Furthermore any element of L is an inf of sups of elements of G.

Implicative lattice

A lattice L is said to be an implicative lattice [START_REF] Curry | Foundations of mathematical logic McGraw[END_REF] or Heyting algebra [START_REF] Johnstone | Stone Spaces[END_REF] if, and only if, there is a binary operation → such that

a ∧ b ≤ c ⇐⇒ a ≤ b → c Theorem 2.11 If L is an implcative lattice, we have in Kr (L) ϕ 0 (U 0 ), . . . , ϕ (U ) S ϕ 0 (J 0 ), . . . , ϕ (J )
if, and only if,

1 = u → (j ∨ (u -1 → (j -1 ∨ . . . (u 0 → j 0 ))))
where u j = ∧U j and j k = ∨J k .

In the case where L is an implicative lattice, we can write explicitely that L is of dimension ≤ -1 as an identity. For instance that L is of dimension ≤ 0 is equivalent to the identity 1 = x ∨ ¬x where ¬x = x → 0 and that L is of dimension ≤ 1 is equivalent to the identity

1 = x 2 ∨ (x 2 → (x 1 ∨ ¬x 1 ))
and so on.

Corollary 2.12 An implicative lattice L is of dimension ≤ -1 if, and only if, for any sequence

x 1 , . . . , x 1 = x ∨ (x → . . . (x 2 ∨ (x 2 → (x 1 ∨ ¬x 1 ))) . . .)

Decidability

To any distributive lattice L we have associated a family of distributive lattices Kr (L) with a complete description of their ordering. A lattice is discrete if, and only if, its ordering is decidable, which means intuitively that there is an algorithm to decide the ordering (or, equivalently, the equality) in this lattice. It should be intuitively clear that we could find a discrete lattice L such that Kr 1 (L) is not discrete since, by 2.3, the ordering on Kr 1 (L) involves an existential quantification on the set L, that may be infinite (this point is discussed in [START_REF] Boileau | La logique des topos[END_REF], with another argument). However we can use the characterisation of Theorem 2.3 to give a general sufficient condition ensuring that all Kr (L) are discrete.

Theorem 2.13 Suppose that the lattice L is a discrete implicative lattice then each Kr (L) is discrete.

Proof. This is direct from Theorem 2.11.

Dimension of Spectral Spaces

This subsection is written from a classical point of view. Following [START_REF] Hochster | Prime ideal structure in commutative rings[END_REF], a topological space X is called a spectral space if it satisfies the following conditions: (a) X is a compact T 0 -space; (b) X has a compact open basis which is closed under finite intersections; (c) each irreducible closed subspace of X has a generic point. Spec(R), with the Zariski topology, is spectral for any commutative ring R with identity. Similary, if we take for basic open the sets U a = {φ ∈ Spec(L) | φ(a) = 1} then Spec(L) is spectral for any distributive lattice. The compact open subsets of a spectral space form a distributive lattice, and it is well-known [START_REF] Stone | Topological representations of distributive lattices and Brouwerian logics[END_REF][START_REF] Johnstone | Stone Spaces[END_REF] that, if L is an arbitrary distributive lattice, then L is isomorphic to the lattice of compact open subsets of the space Spec(L).

If U, V are open subsets of a topological space X we define U → V to be the largest open W such that W ∩ U ⊆ V and ¬ U = U → ∅. In a classical setting a spectral space X is said to be of dimension ≤ -1 if, and only if, there is no strictly increasing chains of length of irreducible closed subsets of X. We can reformulate Theorem 2.9 as follows.

Theorem 2.14 A spectral space X is of dimension ≤ -1 if, and only if, for any compact open subsets

x 1 , . . . , x of X X = x ∨ (x → . . . (x 2 ∨ (x 2 → (x 1 ∨ ¬x 1 ))) . . .)

Connections with Joyal's definition

Let L be a distributive lattice, Joyal [START_REF] Español | Constructive Krull dimension of lattices[END_REF] gives the following definition of dim(L) ≤ . Let ϕ i : L → Kr (L) be the + 1 universal morphisms. By universality of Kr +1 (L), we have + 1 morphisms σ i : Kr +1 (L) → Kr (L) such that

σ i • ϕ +1 j = ϕ j if j ≤ i and σ i • ϕ +1 j = ϕ j-1 if j > i.
Joyal defines then dim(L) ≤ to mean that (σ 0 , . . . , σ ) : Kr +1 (L) → Kr (L) +1 is injective. This definition can be motivated by Proposition 1.11: the elements in the image of Sp(σ i ) are the chains of prime ideals (α 0 , . . . , α ) with α i = α i+1 , and Sp(σ 0 , . . . , σ ) is surjective if, and only if, for any chain (α 0 , . . . , α ) there exists i < such that α i = α i+1 . This means exactly that there is no nontrivial chain of prime ideals of length + 1. Using the completeness theorem, one can then see the equivalence with Definition 2.7. One could check directly this equivalence using a constructive metalanguage, but for lack of space, we shall not present here this argument. Similarly, it would be possible to establish the equivalence of our definition with the one of Español [START_REF] Español | Constructive Krull dimension of lattices[END_REF] (here also, this connection is clear via the completeness theorem).

Zariski and Krull lattices of a commutative ring

Zariski lattice

of the abstract theory of the Zariski spectrum. We shall write a for a . Given a subset S of R we write S for the subset of Zar(R) the elements of which are s for s ∈ S. We have

a 1 ∨ • • • ∨ a m = a 1 , . . . , a m and a 1 ∧ • • • ∧ a m = a 1 • • • a m .
Let U and J be two finite subsets of R, we have

U Zar(R) J ⇐⇒ u∈U u ∈ J ⇐⇒ M(U ) ∩ J = ∅
This describes completely the lattice Zar(R). More precisely we have: It is clear that the relation U J defined by "M(U ) meets J " satisfies these axioms. It is also clear that the entailment relation generated by these axioms contains this relation. Let us show that this relation is an entailment relation. Only the cut rule is not obvious. Assume that M(U, a) meets J and that M(U ) meets J, a . There exist then m 1 , m 2 ∈ M(U ) and k ∈ N, x ∈ R such that a k m 1 ∈ J , m 2 + ax ∈ J . Eliminating a this implies that M(U ) intersects J .

We have a = b if, and only if, a divides a power of b and b divides a power of a. Proposition 3.2 In a commutative ring R to give an ideal of the lattice Zar(R) is the same as to give a radical ideal of R. If I is a radical ideal of R one associates the ideal

I = {J ∈ Zar(R) | J ⊆ I} of Zar(R). Conversely if I is an ideal of Zar(R) one can associate the ideal I = J∈I J = {x ∈ R | x ∈ I},
which is a radical ideal of R. In this bijection the prime ideals of the ring correspond to the prime ideals of the Zariski lattice.

Proof.

We only prove the last assertion. If I is a prime ideal of R, if J, J ∈ Zar(R) and J ∧ J ∈ I, let a 1 , . . . , a n ∈ R be some "generators" of J (i.e., J = a 1 , . . . , a n ) and let b 1 , . . . , b m ∈ R be some generators of J . We have a i b j ∈ I and hence a i ∈ I or b j ∈ I for all i, j. It follows from this (constructively) that we have a i ∈ I for all i or b j ∈ I for all j. Hence J ∈ I or J ∈ I and I is a prime ideal of Zar(R). Conversely if I is a prime ideal of Zar(R) and if we have xy ∈ I then x ∧ y ∈ I and hence x ∈ I or y ∈ I. This shows that {x ∈ R | x ∈ I} is a prime ideal of R.

Krull lattices of a commutative ring

Definition 3. [START_REF] Cederquist | Entailment relations and Distributive Lattices Logic Colloquium[END_REF] We define Kru (R) := Kr ( Zar(R)). This is called the Krull lattice of order of the ring R. We say also that R is of Krull dimension ≤ iff the distributive lattice Zar(R) is of dimension ≤ .

Theorem 3.4 The ring R is of dimension ≤ -1 if, and only if, for any

x 1 , . . . , x n ∈ R we have in Kru (R) ϕ 0 ( x 1 ), . . . , ϕ -1 ( x ) ϕ 1 ( x 1 ), . . . , ϕ ( x )
Proof. This is a direct consequence of Lemma 2.10 and the fact that the elements x generates Zar(R).

Theorem 3.5 Let C = ((J 0 , U 0 ), . . . , (J , U )) be a list of + 1 pairs of finite subsets of R, the following properties are equivalent:

1. there exist j i ∈ J i , u i ∈ M(U i ), (i = 0, . . . , ), such that

u 0 • (u 1 • (• • • (u + j ) + • • •) + j 1 ) + j 0 = 0 2. there exist L 1 , . . . , L ∈ Zar(R) such that in Zar(R): L 1 , U 0 J 0 L 2 , U 1 J 1 , L 1 . . . . . . . . . L , U -1 J -1 , L -1 U J , L
3. there exist x 1 , . . . , x ∈ R such that (for the entailment relation described in Proposition 3.1):

x 1 , U 0 J 0 x 2 , U 1 J 1 , x 1 . . . . . . . . . x , U -1 J -1 , x -1 U J , x

Proof.

It is clear that 1 entails 3: simply take

x = u + j , x -1 = x u -1 + j -1 , . . . , x 0 = x 1 u 0 + j 0
and that 3 entails 2.

Let us prove that 2 implies 3. We assume:

L 1 , U 0 I 0 L 2 , U 1 I 1 , L 1 U 2 I 2 , L 2
The last line means that M(U 2 ) intersects I 2 + L 2 and hence I 2 + x 2 for some element x 2 of L 2 . Hence we have

U 2 I 2 , x 2 . Since x 2 ≤ L 2 in Zar(R) we have x 2 , U 1 I 1 , L 1 .
We have then replaced L 2 by x 2 . Reasoning as previously one sees that one can replace as well L 1 by a suitable x 1 . One gets then 3.

Finally, let us show that 3 entails 1: if we have for instance

x 1 , U 0 I 0 x 2 , U 1 I 1 , x 1 U 2 I 2 , x 2
by the last line we know that we can find y 2 both in the monoid

M 2 = M(U 2 ) + I 2 and in x 2 . Since y 2 x 1 y 2 , U 1 I 1 , x 1
and since y 2 ∈ M 2 we can find y 1 both in the monoid M 1 = M 2 M(U 1 ) + I 1 and in x 1 . We have y 1 x 1 and hence y 1 , U 0 I 0 and since y 1 ∈ M 1 this implies 0 ∈ M 1 M(U 0 ) + I 0 as desired.

Corollary 3.6

A ring R is of Krull dimension ≤ -1 iff for any sequence x 1 , . . . , x there exist a 1 , . . . , a ∈ R and m 1 , . . . , m ∈ N such that

x m1 1 (• • • (x m (1 + a x ) + • • •) + a 1 x 1 ) = 0
Proof. By Theorem 3.4, we have in Kru (R)

ϕ 0 ( x 1 ), . . . , ϕ -1 ( x ) ϕ 1 ( x 1 ), . . . , ϕ ( x )
we can then apply Theorem 3.5 to the elementary idealistic chain ((0, x 1 ), ( x 1 , x 2 ), . . . , ( x , 1))

and we get in this way j i ∈ x i , j 0 = 0 and u i ∈ M(x i+1 ), u = 1 such that

u 0 • (u 1 • (• • • (u + j ) + • • •) + j 1 ) + j 0 = 0 as desired.
This concrete characterisation of the Krull dimension of a ring can be found in [START_REF] Lombardi | Dimension de Krull, Nullstellensätze et Évaluation dynamique[END_REF], where it is derived using dynamical methods [START_REF] Coste | Dynamical method in algebra: Effective Nullstellensätze[END_REF]. Lemma 3.7 If R is coherent and noetherian then Zar(R) is an implicative lattice.

Proof.

Let L ∈ Zar(R), radical of an ideal generated by elements y 1 , . . . , y n and x ∈ R, we show how to define an element x → L ∈ Zar(R) such that, for any M ∈ Zar(R)

M ∧ x ≤ L ⇐⇒ M ≤ x → L
For this, we consider the sequence of ideals

I k = {z ∈ R | zx k ∈ y 1 , . . . , y n }
Since R is coherent, each I k is finitely generated. Since furthermore R is noetherian and I k ⊆ I k+1 the sequence I k is stationary and k I k is finitely generated. We take for x → L the radical of this ideal.

If M ∈ Zar(R) then M is the radical of an ideal generated by finitely many elements x 1 , . . . , x m and we can take

M → L = ( x 1 → L) ∧ . . . ∧ ( x m → L).
Corollary 3.8 If R is coherent, noetherian and strongly discrete then each lattice Kr n (R) is discrete.

Proof.

Using Theorem 2.13 and Lemma 3.7 we are left to show that Zar(R) is discrete. We have M ≤ L if, and only if, 1 = M → L. But to test if an element of Zar(R) is equal to the ideal 1 is decidable since R is strongly discrete.

The hypotheses of this corollary are satisfied if R is a polynomial ring K[X 1 , . . . , X n ] over a discrete field K [START_REF] Mines | A Course in Constructive Algebra[END_REF].

Krull dimension of a polynomial ring over a discrete field

Let R be a commutative ring, let us say that a sequence x 1 , . . . , x is singular if, and only if, there exists a 1 , . . . , a ∈ R and m 1 , . . . , m ∈ N such that

x m1 1 (• • • (x m (1 + a x ) + • • •) + a 1 x 1 ) = 0
A sequence is pseudo regular if, and only if, it is not singular. Corollary 3.6 can be reformulated as: a ring R is of Krull dimension ≤ -1 if, and only if, any sequence in R of length is singular.

Proposition 3.9 Let K be a discrete field, R a commutative K-algebra, and x 1 , . . . , x in R algebraically dependent over K. The sequence x 1 , . . . , x is singular.

Proof.

Let Q(x 1 , . . . , x ) = 0 be a algebraic dependence relation over K. Let us order the nonzero monomials of Q along the lexicographic ordering. We can suppose that the coefficient of the first monomial is 1. Let x m1 1 x m2 2 • • • x m be this momial, it is clear that Q can be written on the form

Q = x m1 1 • • • x m + x m1 1 • • • x 1+m R + x m1 1 • • • x 1+m -1 -1 R -1 + • • • + x m1 1 x 1+m2 2 R 2 + x 1+m1 1 R 1
and this is the desired collapsus.

Let us say that a ring is of dimension if it is of dimension ≤ but not of dimension ≤ -1. It follows that we have: Theorem 3.10 Let K be a discrete field. The Krull dimension of the ring K[X 1 , . . . , X ] is equal to .

Proof.

Given Proposition 3.9 it is enough to check that the sequence (X 1 , . . . , X ) is pseudo regular, which is direct.

Notice that we got this basic result quite directly from the characterisation of Corollary 3.6, and that our argument is of course also valid classically (with the usual definition of Krull dimension). This contradicts the current opinion that constructive arguments are necessarily more involved than classical proofs.

Annex: Completeness, compactness theorem, LLPO and geometric theories

A.1 Theories and models

We fix a set V of atomic propositions or propositional letters. A proposition φ, ψ, . . . is a syntactical object built from the atoms p, q, r ∈ V with the usual logical connectives 0, 1, φ ∧ ψ, φ ∨ ψ, φ → ψ, ¬φ

We let P V be the set of all propositions. Let F 2 be the Boolean algebra with two elements. A valuation is a function v ∈ F V 2 that assigns a truth value to any of the atomic propositions. Such a valuation can be extended to a map

P V → {0, 1}, φ -→ v(φ) in the expected way. A theory T is a subset of P V . A model of T is a valuation v such that v(φ) = 1 for all φ ∈ T .
More generally given a Boolean algebra B we can define B-valuation to be a function v ∈ B V . This can be extended as well to a map

P V → B, φ -→ v(φ). A B-model of T is a valuation v such that v(φ) = 1 for all φ ∈ T .
The usual notion of model is a direct special case, taking for B the Boolean algebra F 2 . For any theory there exists always a free Boolean algebra over which T is a model, the Lindenbaum algebra of T , which can be also be defined as the Boolean algebra generated by T , thinking of the elements of V as generators and the elements of T as relations. The theory T is formally consistent if, and only if, its Lindenbaum algebra is not trivial.

A.2 Completeness theorem

Theorem A.1 (Completeness theorem) Let T be a theory. If T is formally consistent then T has a model. This theorem is the completeness theorem for propositional logic. Such a theorem is strongly related to Hilbert's program, which can be seen as an attempt to replace the question of existence of model of a theory by the formal fact that this theory is not contradictory.

Let B the Lindenbaum algebra of T . To prove completeness, it is enough to find a morphism B → F 2 assuming that B is not trivial, wich is the same as finding a prime ideal (which is then automatically maximal) in B. Thus the completeness theorem is a consequence of the existence of prime ideal in nontrivial Boolean algebra. Notice that this existence is clear in the case where B is finite, hence that the completeness theorem is direct for finite theories.

A.3 Compactness theorem

The completeness theorem for an arbitrary theory can be seen as a corollary of the following fundamental result.

Theorem A.2 (Compactness theorem) Let T be a theory. If all finite subsets of T have a model then so does T .

Suppose indeed that the compactness theorem holds, and let T be a formally consistent theory. Then an arbitrary finite subset T 0 of T is also formally consistent. Furthermore, we have seen that this implies the existence of a model for T 0 . It follows then from the compactness theorem that T itself has a model.

Conversely, it is clear that the compactness theorem follows from the completeness theorem, since a theory is formally consistent as soon as all its finite subsets are.

A simple general proof of the compactness theorem is to consider the product topology on {0, 1} V and to notice that the set of models of a given subset of T is a closed subset. The theorem is then a corollary of the compactness of the space W := {0, 1} V when compactness is expressed (in classical mathematics) as: if a family of closed subsets of W has non-void finite intersections, then its intersection is non-void.

A.4 LPO and LLPO

If V is countable (i.e., discrete and enumerable) we have the following alternative argument. One writes V = {p 0 , p 1 , . . .} and builds by induction a partial valuation v n on {p i | i < n} such that any finite subset of T has a model which extends v n , and v n+1 extends v n . To define v n+1 one first tries v n+1 (p n ) = 0. If this does not work, there is a finite subset of T such that any of its model v that extends v n satisfies v(p n ) = 1 and one can take v n+1 (p n ) = 1.

The non-effective part of this argument is contained in the choice of v n+1 (p n ), which demands to give a gobal answer to an infinite set of (elementary) questions. Now let us assume also that we can enumerate the infinite set T . We can then build a sequence of finite subsets of T in a nondecreasing way K 0 ⊆ K 1 ⊆ . . . such that any finite subset of T is a subset of some K n . Assuming we have construct v n such that all K j 's have a model extending v n , in order to define v n+1 (p n ) we have to give a global answer to the questions: do all K j 's have a model extending v n+1 when we choose v n+1 (p n ) = 1 ? For each j this is an elementary question, having a clear answer. More precisely let us define g n : N → {0, 1} in the following way: g n (j) = 1 if there is a model v n,j of K j extending v n with v n,j (p n ) = 1, else g n (j) = 0. By induction hypothesis if g n (j) = 0 then all K have a model v n, extending v n with v n, (p n ) = 1, and all models v n, of K extending v n satisfy v n, (p n ) = 1 if ≥ j. So we can "construct" inductively the infinite sequence of partial models v n by using at each step the non-constructive Bishop's principle LPO (Least Principle of Omniscience): given a function f : N → {0, 1}, either f = 1 or ∃j ∈ N f (j) = 1. This principle is applied at step n to the function g n .

In fact we can slightly modify the argument and use only a combination of Dependant Choice and of Bishop's principle LLPO (Lesser Limited Principle of Omniscience), which is known to be strictly weaker than LPO: given two non-increasing functions g, h : N → {0, 1} such that, for all j g(j) = 1 ∨ h(j) = 1 then we have g = 1 or h = 1. Indeed let us define h n : N → {0, 1} in a symmetric way: h n (j) = 1 if there is a model v n,j of K j extending v n with v n,j (p n ) = 0, else h n (j) = 0. Cleraly g n and h n are non-increasing functions. By induction hypothesis, we have for all j g n (j) = 1 ∨ h n (j) = 1. So, applying LLPO, we can define v n+1 (p n ) = 1 if g n = 1 and v n+1 (p n ) = 1 if h n = 1. Nevertheless, we have to use dependant choice in order to make this choice inifnitely often since the answer "g = 1 or h = 1" given by the oracle LLPO may be ambiguous.

In a reverse way it is easy to see that the completeness theorem restricted to the countable case implies LLPO.

A.5 Geometric formulae and theories

What would have happened if topologies without points had been discovered before topologies with points, or if Grothendieck had known the theory of distributive lattices? (G. C. Rota [START_REF] Rota | Indiscrete Thoughts Birkhauser[END_REF]).

A formula is geometric if, and only if, it is built only with the connectives 0, 1, φ ∧ ψ, φ ∨ ψ from the propositional letters in V . A theory if a (propositional) geometric theory iff all the formula in T are of the form φ → ψ where φ and ψ are geometric formulae.

It is clear that the formulae of a geometric theory T can be seen as relations for generating a distributive lattice L T and that the Lindenbaum algebra of T is nothing else but the free Boolean algebra generated by the lattice L T . It follows from Proposition 1.8 that T is formally consistent if, and only if, L T is nontrivial. Also, a model of T is nothing else but an element of Spec(L T ). The general notion of geometric formula allows also existential quantification, but we restrict ourselves here to the propositional case. Even in this restricted form, the notion of geometric theory is fundamental. For instance, if R is a commutative ring, we can consider the theory with atomic propositions D(x) for each x ∈ R and with axioms This is a geometric theory T . The model of this theory are clearly the complement of the prime ideals. What is remarkable is that, while the existence of models of this theory is a nontrivial fact which may be dependent on set theoretic axioms (such as dependent axiom of choices) its formal consistency is completely elementary (as explained in the beginning of the section 3). This geometric theory, or the distributive lattice it generates, can be seen as a point-free description of the Zariski spectrum of the ring. The distributive lattice generated by this theory (called in this paper the Zariski lattice of R) is isomorphic to the lattice of compact open of the Zariski spectrum of R, while the Boolean algebra generated by this theory is isomorphic to the algebra of the constructible sets.

Theorem A. 3 (

 3 Completeness theorem for geometric theories) Let T be a geometric theory. If T generates a nontrivial distributive lattice, then T has a model.

• D( 0 R ) → 0 • 1 →

 001 D(1 R ) • D(x) ∧ D(y) → D(xy) • D(xy) → D(x) • D(x + y) → D(x) ∨ D(y)

L is actually the quotient of P f (P f (S)) by the equivalence relation: X ≤ Y and Y ≤ X.

L is a disjoint copy of L.

A monoid will always be multiplicative.

• We say that the idealistic prime (J, U ) collapses iff we have I = F = L. This means that the quotient lattice L = T /(J = 0, U = 1) is a singleton i.e., 1 ≤ L 0, which means also U J.

1.2 Distributive lattices and entailment relations


Survey of the Remains of Mammals Recovered in the Middle Bronze Age Burials at Sidon (Lebanon)

The discovery, at Sidon, of a group of burials dated to the Middle Bronze Age -most of which contained animal remains together with human burials -presents a new corpus of funerary offerings and animal sacrifices. The analysis of the animal remains was undertaken in the field at the time of the excavations at Sidon in July 2001. There is little in the way of archaeozoological data on the practices of burying animals and providing food offerings for the dead in the northern Levant and more generally in the Near East; in the southern Levant, however, a larger number of Middle Bronze Age sites have provided data on the animal remains found in burials. For a true understanding of burials and funerary rites it is essential that the animal remains are studied, in addition to and in parallel with the study of the other grave goods found in burials.

Of the three types of burials found in the part of the necropolis of Sidon that has been excavated: simple inhumations, jar burials and burials in constructed graves, it is the last which are the richest in animal remains. Very few such remains accompanied the burials in the sand and the jar burials. Altogether, fifteen burials of the twenty excavated contained skeletal material, mainly of mammals, although some fishbones, some fragments of the plastrons of turtles and tortoises and a few shells that have not yet been positively identified were recovered.

Among the species of mammals identified, only domestic animals are represented. Given the difficulty, in certain cases, of distinguishing the bones of sheep from those of goats, those remains that could not be precisely determined have been placed in the category 'ovi-caprines'. Also, the terms sheep(Ovis aries), goat (Capra hircus), cow (Bos taurus) and pig (Sus scrofa) are used generically to describe domestic ovines, caprines, bovines and suiforms.The ovi-caprines, that is the sheep and the goats, were found in quantity, whereas the bovines and the pigs were far less numerous. No wild species were found, except for one bone of a small carnivore, which can probably be attributed to a mustelid.

Cutmarks were found on some of the bones. Some were burnt.

Inventory of the animal remains in the burials.

I Simple Inhumations

Three of the four simple inhumations contained animal remains.

Inhumation 3 Only two fragments of animal bone were recovered from this burial: one fragment of the pelvis of a pig with a cutmarks on the edge of the acetabulum and a fragment of the rib of a small mammal.

Inhumation 10 Only one fish vertebra was found.

Inhumation 26 Some remains were found in the fill of the burial: a tooth, the diaphysis of a humerus, a cervical vertebra of ovi-caprines as well as one phalanx I of an adult goat and three cow bones ( frontal bone, calcaneum and phalanx I of an adult). Three ribs also probably belong to ovi-caprines (these are mentioned in the table under small mammals).In addition, parts of the plastron of a turtle were identified.

II Jar burials

Four jar burials out of eight contained some skeletal remains of animals.

Jar Burial 1 In this inhumation jar, the finds include: bovines -fragments of skull (premaxilla) and hindlimb (patella and metarsal) as well as a thoracic vertebra and a rib; ovi-caprines -a tooth, some radius and metapodial diaphyses, fragments of tibia (from an individual less than two years old), a phalanx with fused epiphyses (from an individual more than two years old), as well as a vetebra and a rib. The phalanx could be identified as belonging to an adult goat. In addition, a fragment of a bivalve was present. Jar Burial 2 A fragment of bovine mandible; a tooth and a fragment of zygomatic bone of ovicaprines, two goat scapulae -one right and one left from the same individual, a juvenile less than a year old -as well as some elements of tortoise plastron were present in this jar. Many fragments of long bones of ovi-caprines have remained undetermined.

Jar Burial 8 One sole root of a tooth of an ovi-caprine was recovered from within this jar.

Jar Burial 15

The animal remains in this jar consisted of one fish vertebra only.

III Inhumations in Constructed Graves.

All of the eight constructed graves excavated yielded animal remains.

Constructed Grave 4

The most numerous remains are those of ovi-caprines. The only bones whose articulation could be determined with certainty are those of the right forelimb of a sheep two to four years old. Cutmarks are visible near the proximal head and on the distal trochlea of the humerus and on the medial side of the proximal end of the diaphysis of the radius. Elements of a left hindlimb of a sheep and of the pelvis, as well as a metatarsal, were also recovered. An axis (2nd cervical vertebra) belongs to a sheep, as does a horn-core, which may be attributed to an ewe. Two lower molars, attributable specifically to sheep, indicate ages of one and two years respectively. An axis with cutmarks under the odontoid process and on the ventral side of the vertebra, a fragment of mandible as well as some elements of hind extremity have been attributed to goat. Among the other very fragmentary ovi-caprine remains that could not be precisely determined, are fragments of skulls, elements of the right forelimb of one juvenile (less than one year old) and fragments of left forelimbs: two left scapulae and some fragments of radius of which one, proximal, bears a cutmark on its medial side. Elements of two left hindlimbs (pelvis, femurs, tibia), from one individual less than four years old and from another more than four years old are present; a fragment of pelvis has a cutmark on the ramus of the ilium. One atlas (1st cervical vertebra) among the four present had been cut in two transversally. The vertebral column is represented by numerous cervical, thoracic and lumbar vertebrae. One lumbar vertebra has a cutmark on its ventral face. To conclude, skeletal elements of at least four ovi-caprines are represented in this burial: one sheep two to four years old (one forelimb interred complete; one hindlimb? one atlas), one goat of indeterminate age (axis, atlas, one hind extremity, one mandible?), one juvenile ovi-caprine under a year old (one complete forelimb placed in the burial? one atlas), one ovi-caprine more than four years old (one hindlimb? one atlas). Some remains of bovines were recovered: elements of a skull of which the left maxilla with its deciduous teeth and molar 1 with no signs of wear belongs to a juvenile; this maxilla has fine cutmarks above the deciduous molars; an axis, as well as parts of a hindlimb were recovered along with some fragments of hind extremity and a lumbar vertebra. The remains of the hindlimb have their epiphyses fused and belong to an adult. There are thus vestiges of at least two individuals in this burial, one juvenile and one adult. Elements of a skull, an axis and a fragment of femur are attributable to pig. The axis and the femur are burnt.

Finally, the presence in this burial of a fragment of bivalve and fragments of twelve small gasteropods should be noted.

Constructed Grave 5

The only animal remains found in Burial 5 are of ovi-caprines: none of these remains could be positively attributed to sheep, although a certain number have the osteological characteristics of goat. These last include elements of a skull, of right and left forelimbs, of left hindlimb and of vertebral column. These remains belong to one sole individual. According to estimates of the age of the living animal by the degree of ossification of the epiphyses and by the degree of wear on the teeth, this goat was between two and four years old at the time of its death. Cutmarks are visible on the supraglenoid tubercle of the left scapula, on the antero-proximal part of the left radius and on the trochlea of the right humerus. There is not a single element that attests to the presence of the right hindlimb. Moreover, the absence of any foot bones (metapodials and phalanges) no doubt indicates that the lower parts of the limbs were cut off below the tarsus and the carpus. It seems that the goat was not interred complete: probably only three limbs were placed in the burial together with the head and the vertebral column.

Constructed Grave 7

Two goat bones -one tibia and one phalanx -were recovered from Burial 7 as well as some bones from the extremities of bovines: a metacarpal, a talus and two phalanges. Butchering marks are visible on one phalanx and on the bovine talus, on which last the marks of a knife and an axe can be distinguished.

Constructed Grave 9

In Burial 9 some remains of ovi-caprines were found: parts of fore-and hindlimbs as well as some teeth (of an individual two to four years old) and some vertebrae, of which an atlas could be identified. A fragment of tibia and a vertebra of bovines were also recovered. The presence of a cuttlefish bone should also be noted.

Constructed Grave 12

The complete skeleton of a goat had been interred in Burial 12: all parts of the skeleton are present, the skull, the vertebral column, the limbs and their extremities. Judging by the degree of fusion of the epiphyses, the goat was one to two years old. No cutmarks are visible on the surface of the bones. Also found were: one diaphysis of a radius, apparently of a bovine, as well as the distal end of a sheep humerus which has traces of a circular cut round the diaphysis.

Constructed Grave13

Aside from one upper molar of a bovine, the animal remains in this burial are of ovicaprines. Two half mandibles, elements of fore-and hindlimb as well as thoracic vertebrae all belong to an ovi-caprine nine to twelve months old.

Constructed Grave 16

One metacarpal of a pig (adult), a phalanx I and an axis of ovi-caprine, as well as one fish vertebra were found in this burial.

Constructed Grave 19

One mandible of a pig (adult) and a mandible of a fish were recovered from this burial.

Species of Animals Selected for Offering in the Burials at Sidon

Among the species of animals which were found in the burials, it is useful to distinguish between those species that were common locally and that were intentionally placed in the burials and those which were accidentally buried in the sediment, such as rare or exotic imported species. These distinctions have been categorized by Liora K. Horwitz (2001, 79). It is also useful to make a distinction between partial offerings and an 'integral' offering of a complete animal (Vila, forthcoming).

The mammals found in funerary contexts consist entirely of domesticated species. Those that occur most frequently are the ovi-caprines, which are present in eleven burials out of fifteen. Bovines are represented in eight burials and pigs in four. Fish remains occur in four contexts, in two of which they appear on their own (Simple Inhumation 10 and Jar Burial 15).

All four domesticated species are found together only once, in Constructed Grave 4, which is particularly well supplied with animal remains. Except for Constructed Graves 5 and 12, in which only ovi-caprines -goats to be precise -were placed, the commonest combination is that of bovines with ovi-caprines. Pigs appears only twice (in Simple Inhumation 3 and in Consructed Grave 19).

The abundance of animal remains is clearly dependent on the type of inhumation. All the species are found in all three types of burials; however, the richest deposits are found in the constructed graves, all of which contain animal remains. It is also in the constructed graves that complete animals were placed (Constructed Grave 12: a goat), or complete limbs as indicated by associations between bones that attest to the presence of complete parts of skeletons (one goat in Constructed Grave 5; some ovi-caprines and one bovine in Constructed Grave 4). These deposits consist first and foremost of ovi-caprines; no complete bovines or pigs were recovered. The only complete limb of a bovine, a forelimb, was placed with other offerings in Constructed Grave 4.

The lack of coherence sometimes found among the recovered remains could indicate that in certain interments one is contending with a mixture of remains buried accidentally and those buried intentionally, difficult to distinguish from one another or separate.

There does not appear to have been a strict selection by age of the sacrificed animals. Juveniles, sub-adults and adults are all found as readily among the ovi-caprines as they are among the bovines.

Funerary Butchering, Jointing and Carving

The cutmarks noted on some of the bones suggest that butchering had taken place before they were interred. Although the purpose of the cuts is not always easy to determine, the marks on the respective parts of the skeleton generally accord with the disarticulation of the limbs, or with the removal of the flesh, or, lastly, with the removal of the skin.

In the category 'disarticulation of the limbs', a number of examples may be considered. In Simple Inhumation 3, the cutmarks on the pelvic bone of a pig is the result of the disarticulation of the femur. In Constructed Grave 4, the cutmark on on the ventral side of a lumbar vertebra of an ovi-caprine, and in Constructed Grave 9, the mark on the centrum of a bovine vertebra are no doubt the result of the disarticulation of the vertebral column; nonetheless, these marks could also attest to the removal of flesh or even to evisceration. In Multiple Burial 7 the cutmark and axemark on the talus of a bovine indicate the disarticulation of the hind extremity from the limb (fig. 1a).

In the category 'removal of flesh' there are several examples of cutmarks of a particular kind: in Constructed Grave 4, the knifemarks on the forelimb of a sheep -on the proximal and on the distal parts of the humerus and on the proximal part of the radius; in the same grave, the cutmarks on the ramus of the ilium from the pelvis of an ovi-caprine and on the proximal part of another radius of an ovi-caprine; in Constructed Grave 5, this same type of cut is attested on the trochlea of the humerus and on the proximal part of the radius of the goat, as well as on the supraglenoid tubercle of the scapula; in Consructed Grave 12, the cut encircles the diaphysis of the humerus of a sheep (fig. 1c).

In the category 'removal of the skin' there are two examples: one in Group Burial 7, a cutmark on a bovine phalanx II, the other in Constructed Grave 4, some cutmarks on a bovine maxilla (fig. 1b).

On the other hand, the cutmarks on the ventral side of the neural spine and centrum of the axis of a goat from Constructed Grave 4 may attest to the slitting of its throat (fig. 1d).

Finally, the marks of burning on a proximal metacarpal of a sheep and on a femur and an axis of pig in Constructed Grave 4 are somewhat enigmatic. Are these indications of cooking and evidence of roasting?

The presence of marks of butchering raises the question of the form in which the parts of the skeletons were placed in the burials. It is certain, in at least two examples, that the entire animal, or very nearly the entire animal, was deposited as a sacrifice to the deceased, as in Constructed Graves 5 and 12. On the other hand, in other cases, when it is a matter of limbs that were placed in the graves still articulated but bearing cutmarks, as in Constructed Graves 4 and 5, one may well wonder whether some flesh had not been removed. In that case the remains could as well represent the residue of a funeral repast eaten by the living as food offerings for the dead. To return to isolated bones and fragments, they probably represent offerings of small portions of meat.

It should be noted that in the burials at Sidon, the goat is the only animal to have been placed in a burial in its entirety. The other species are represented only by quarters or by isolated bones or fragments. There would thus have been two different funerary rites. The first involves the sacrifice of an animal to the deceased, the goat being preferentially selected and its meat not eaten by the living: this rite was evidently uncommon. In the second the animals were sacrificed, cut into quarters and into portions of which some were placed in the burial and others apparently consumed elsewhere: this rite occurs more frequently, is more complex and is more difficult to understand.

Funerary Offerings of Animals in Middle Bronze Age Burials in the Levant

As yet there have not been very many archaeozoological studies of the funerary assemblages of the Middle Bronze Age in the Levant. Most of the comparative data are from the southern Levant, where recent work on excavated material has taken into account the skeletal remains of animals found in burials, cf. [START_REF] Horwitz | The Animal Bone Assemblage from the Middle Bronze II Tomb (T1181, Area L) at Hazor[END_REF].

The site nearest to Sidon, Tel Dan, has provided an assemblage of animals from infant burials in jars and from constructed graves [START_REF] Horwitz | Animal Bones from the Middle Bronze Age Tombs at Tel Dan[END_REF]. The jar burials, like those at Sidon, are the poorest in animal remains, whereas the constructed graves contain larger numbers of remains and above all a greater variety of species. At Tel Dan, in fact, the range of fauna recovered from the burials is greater than that at Sidon. Wild species such as fallow deer, red deer, gazelles, lions and birds appear in addition to the domesticated species sheep, goat, pig and cow. In the burials at Tel Dan none of the skeletal remains are articulated with one exception, the post-cranial skeleton of a young goat found in a jar (burial 8096). In all the other examples, the skeletal remains are of isolated bones and come from all parts of the skeleton. A few bear cutmarks, mainly on the bones of the hind extremities, but also on the proximal part of a humerus and on the diaphysis of an ovicaprine ulna. Juvenile and adult ovi-caprines and bovines appear to be represented in equal numbers. Most of the remains of pigs, on the other hand, are of immature animals.

At Sasa, two Middle Bronze Age burials (BM II A/B and BM II A/C) have provided animal remains [START_REF] Horwitz | Animal Offerings from Two Middle Bronze Age Tombs[END_REF]. These consist entirely of domesticated species: sheep, goat, cow and pig; there are also some fish. No complete skeletons were found within the burials. Some of the bones, however, display articular associations and it is probable that complete limbs were placed in the burials. At Djebel Qa'aqir, the animal remains found in nine burials out of sixteen are mostly of sheep and goats; one sole bovine bone was identified, and a fragment of the antler of a fallow deer [START_REF] Horwitz | Animal Offerings from Two Middle Bronze Age Tombs[END_REF]. No remains of pig were found in these burials.

At Hazor, the bones of ovi-caprines, and particularly those of sheep, predominate among the remains recovered from a Middle Bronze Age burial (BM II) [START_REF] Horwitz | The Animal Bone Assemblage from the Middle Bronze II Tomb (T1181, Area L) at Hazor[END_REF]. All the remains are from individuals sacrificed when they were two to three years old. The parts of the skeleton that occur most frequently are the bones of the forelimb and the vertebrae. The extremities, the hindlimb and the skull are considerably less well represented. It seems that the fleshiest parts were preferentially selected.

At Jericho, the twenty-three Middle Bronze Age burials contained animal remains consisting mainly of ovi-caprines, probably mainly sheep, as well as remains of birds and equids [START_REF] Grosvenor-Ellis | Excavations at Jericho II[END_REF]. Pigs appear to be absent. It is thus in the Middle Bronze Age that equids, which appear to be absent in Early Bronze Age burials, emerge in funerary contexts. Fifteen individuals in all were found in nine burials dated to Middle Bronze II (Grosvenor-Ellis 1960). As only one individual has been described (burial J3), it is impossible to say whether the other skeletons were preserved in their entirety.

Instances of the interment of equids -horses or asses -in association with human burials are fairly numerous in the southern Levant in the Middle Bronze Age, cf. Wapnish (1977). In general the complete animals were placed in the burials. This represents a type of funerary rite different from that in which food offerings were deposited when, with a few exceptions, only parts of the skeletons are found. Ó Archaeozoological studies have shown that, in the Middle Bronze Age, it is deposits and sacrifices of ovi-caprines that are found most frequently in burials. The ovi-caprines, the sheep and the goats, are thus par excellence the species connected with funerary rites [START_REF] Horwitz | Animal Bones from the Middle Bronze Age Tombs at Tel Dan[END_REF][START_REF] Horwitz | The Animal Bone Assemblage from the Middle Bronze II Tomb (T1181, Area L) at Hazor[END_REF].

Conclusion

Very little is known about funerary rites in the Ancient Near East. Although sacrifices of animals on the occasion of important events, very often religious ones, or as offerings to the gods are sometimes described in ancient texts [START_REF] Borowski | Animals in the Religions of Syria-Palestine[END_REF], sacrificial rites relating to death have rarely been touched on in the textual sources. The occasional Mesopotamian text does nonetheless provide some food for thought on the subject. Zarins (1986, 180-81) and Limet (2000, 46-7 and n. 18), have published several Mesopotamian texts that relate equids to human burials. One text that accords with a passage on the death of Gilgamesh -cf. Kramer (1944), cited by [START_REF] Zarins | Equids Associated with Human Burials in Third Millenium B.C. Mesopotamia: Two Complementary Facets[END_REF] indicates that the deceased is accompanied by a certain number of people (sacrifices?), offerings and presents, the latter two categories not being elucidated. Another text on the death of the king Ur Nammu, killed in battle (Kramer (1967) mentions that the dead king offers gifts to the deities of the Netherworld, including offerings of bovines, lambs and fatted sheep; in addition, the text alludes to the fact that his main gift for a warrior called Ningiszida seems to consist of an assortment of asses. Yet another text -cf. [START_REF] Gelb | Household and Family in Early Mesopotamia[END_REF] -contains a list of produce and objects for the funeral rites of a certain Bilalla and his wife Lalla, which largely coincides with the actual finds from the burials at Ur, Kish and in the Hamrin basin, as remarked by [START_REF] Zarins | Equids Associated with Human Burials in Third Millenium B.C. Mesopotamia: Two Complementary Facets[END_REF]. This text also mentions equids harnessed to a chariot. Likewise, equids (four mules?) are alluded to in a Girsu text that lists objects and other equipment for the funeral of a certain Nin-e-ni-se -cf. Steinkeller (1980), cited by [START_REF] Zarins | Equids Associated with Human Burials in Third Millenium B.C. Mesopotamia: Two Complementary Facets[END_REF]. These texts are important in that they attest to the interment of equids much as they were recovered from burials of the end of the third millennium BC. Moreover, they give a reason for this practice: they would have been offerings to the divinities who lived in the earth. On the other hand, there is no explicit mention in the texts, so far as is known, of food offerings -that is of the fleshy parts of animals -nor is anything said about the selection of animals or the disjointing and further subdivision of their carcasses. Animal sacrifice is not attested at Mari in the context of burial rites or mourning rituals (Lafont 1999, 66). At Lagash, on the other hand, there were sacrifices of sheep, lambs and bovines in the rituals connected to repasts for the dead (Rosengarten 1960, 305 ff). However, these sacrifices do not, according to this study, appear to have taken place at the time of the funeral, but rather to have been connected to ritual (commemmorative?) feasts. Two practices that seem to me to be of particular interest can be extracted from the Mesopotamian example: first, at Lagash one animal -in this case a sheep -may be sacrificed for several people (Rosengarten 1960, 311-312); second, in one instance some of the offerings would have been made in the vicinity of the body of the deceased, while others would have been made elsewhere (Rosengarten 1960, 313). This alludes to to the existence of a practice of apportioning the carcasses as has been observed among the funerary offerings from the archaeological contexts; the details of the rituals connected with the latter remain completely unknown.

For all that, the absence in the Levant -so far as is known -of textual sources on funerary rites places severe limits on the interpretation of the archaeological data, while endowing them with enormous significance: for our knowledge of these practices rests entirely on the archaeological evidence. One of the Ugaritic rituals interpreted by [START_REF] Pardee | Marzihu, Kispu, and the Ugaritic Funerary Cult: A Minimalist View[END_REF] as a funerary rite for the king, a bird on this occasion being sacrificed to the ancestors, should nonetheless be mentioned. Thus, offerings of animals or of parts of animals should not be omitted from the inventory of the contents of burials, even if these offerings are far from systematic. Indeed, they have an aspect that recurs in the practices linked to the death of individuals of the second millennium along the entire Levantine littoral.

Mustelid ?

1 complete right tibia

Figure 1 :

 1 Figure 1: Sidon, examples of cutmarks on bones recovered from the burials.

Table Jar

 Jar

	Burial 1
				right	left fragments epiphyses		Total Number of Finds
						unfused OC Ovis Capra Bos Sus
	OVIS/CAPRA
	skull	teeth	upper	1			1
	frontlimb	radius	diaphysis		1		1
	hindlimb	tibia	proximal		1	1	1
		tibia	distal	1		1	1
	hind extremity	metapodial	diaphysis		1		1
		phalanx I			1			1
	axial skeleton	thoracic vertebra		1		1
	BOS/Large Mammals
	skull	premaxilla			1			1
	hindlimb	patella			1			1
	hind extremity	metatarsal	proximal	1				1
	axial skeleton	thoracic vertebra		1			1
		rib			2			2
	Total Number of Finds						6	1	6
	indeterminate fragments small mammals		1
		rib			2
	Shells	1 bivalve
	Jar Burial 2
				right	left fragments epiphyses		Total Number of Finds
						unfused OC Ovis Capra Bos Sus
	OVIS/CAPRA
	skull	tooth			1		1
		zygomatic bone		1		1
	frontlimb	scapula		1	1	2	1	1
	BOS/Large Mammals
	skull	mandible	bar					1
	Total Number of Finds						2	1	1
	indeterminate fragments small mammals		31
	Turtle	4 framents of plastron


Artur Pessoa
email: pessoa@producao.uff.br

Ruslan Sadykov
email: ruslan.sadykov@inria.fr

Eduardo Uchoa
email: uchoa@producao.uff.br

Improved Branch-Cut-and-Price algorithm for the Heterogeneous Vehicle Routing Problem

Introduction

In this problem, a fleet of heterogeneous vehicles of different capacity is available to serve a set of customers with different demands. Each vehicle has to start and end its tour at the same depot. The cost of a tour of a vehicle is the sum of the fixed cost of the vehicle and the total distance of this tour multiplied by the "weight" of the vehicle. The problem consists in finding a set of vehicle routes that serve all the customers such that the sum of the quantities delivered in each tour does not exceed the capacity of the vehicle used in the tour and the total cost is minimized. The problem has several different variants depending of whether 1) there are fixed vehicle costs or not, 2) there are different vehicle "weights" or they are the same, 3) there are upper bounds of the number of available vehicles of the same type of not.

To our knowledge, the best exact approaches for the problem are proposed in [START_REF] Pessoa | A robust branch-cut-and-price algorithm for the heterogeneous fleet vehicle routing problem[END_REF] and in [START_REF] Baldacci | A unified exact method for solving different classes of vehicle routing problems[END_REF]. The later considers five variants of the problem and presents computational results on the instances of Taillard [START_REF] Taillard | A heuristic column generation method for the heterogeneous fleet vrp[END_REF], with up to 100 customers. All but five instances were solved to optimality. The best published heuristic for the problem was proposed in [START_REF] Subramanian | A hybrid algorithm for the heterogeneous fleet vehicle routing problem[END_REF] and provides the current best known solutions for all Taillard instances and also for a set of Brandão instances [START_REF] Brand | A tabu search algorithm for the heterogeneous fixed fleet vehicle routing problem[END_REF] with up to 199 customers.

Branch-Cut-and-Price Algorithm

In the work, we present an extension of the branch-cut-and-price algorithm of [START_REF] Pecin | Improved branch-cut-andprice for capacitated vehicle routing[END_REF] to the case of heterogeneous vehicles. It uses a state-of-the-art bi-directional labeling algorithm to solve the pricing problem which decomposes to a set of non-elementary resource-constrained shortest path problems, one for each vehicle type. The labeling algorithm supports ng-routes and limited memory rank-1 cuts, which are used to strengthen the relaxation of the problem. Additionally we use reduced cost fixing and enumeration of elementary routes techniques to speed-up pricing problem resolution. We branch first on the number of vehicles of a same type and then on the arcs of the graph of customers. Multi-phase strong-branching with pseudo-costs is used to improve the selection of branching candidates.

The original contributions of this work in comparison with [START_REF] Pecin | Improved branch-cut-andprice for capacitated vehicle routing[END_REF] are : 1) the use of cuts over the extended variables introduced in [START_REF] Pessoa | A robust branch-cut-and-price algorithm for the heterogeneous fleet vehicle routing problem[END_REF], even with the rank-1 cuts they are shown to be still important for solving some instances ; 2) the concept of subproblem dependent memory for rank-1 cuts, that sharper memory definitions allows more cuts to be added without making the pricing too expensive ; 3) We propose a way of lifting the coefficients of columns-routes in rank-1 cuts that takes advantage of the fact that the enumeration of routes is subproblem dependent.

Our branch-cut-and-price algorithm was able to solve all Taillard instances considered in [START_REF] Baldacci | A unified exact method for solving different classes of vehicle routing problems[END_REF] to optimality. The maximum instance solution time is 1 hour and 35 minutes (all instances except one were solved in less than 30 minutes). Improved feasible solutions were found for two instances.

Our algorithm was able to solve seven out of ten Brandão instances to optimality. The largest solved instance has 199 customers and took 12 hours. The smallest unsolved instance has 120 customers. Improved feasible solutions were found for four instances.

We have also tested our algorithm with a time limit of 24 hours on 96 DLP instances [START_REF] Duhamel | Efficient frameworks for greedy split and new depth first search split procedures for routing problems[END_REF] which have from 20 to 256 customers. Each instance is based on the map of one of departments of France. Our algorithm solved to optimality 14 (out of 15) instances up to 100 customers, 25 (out of 38) instances with 101-150 customers, 9 (out of 30) instances with 151-200 customers. Improved feasible solutions were found for 23 instances.


Artur Alves Pessoa

Ruslan Sadykov

Eduardo Uchoa

An improved Branch-Cut

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

Heterogeneous Vehicle Routing

Set I of n customers, each i ∈ I with demand d i .

Set U of vehicle types, each u ∈ U has a depot with K u vehicles of capacity Q u , with fixed cost f u and travel costs c u a for each edge a.

Objective: minimize the total fixed and travel cost. Set partitioning (master) formulation R u -set of q-routes feasible for a vehicle of type u a r i -number of times that customer i appears in route r . c r -cost of route r .

Binary variable λ r u = 1 if and only if a vehicle of type u uses route r

min u∈U r ∈Ru c r λ r u∈U r ∈Ru a r i λ r = 1, ∀i ∈ I, r ∈Ru λ r ≤ K u , ∀u ∈ U, λ r ∈ {0, 1}, ∀r ∈ R u , ∀u ∈ U.
Pricing subproblem for a vehicle type Arc memory [Pecin et al., 2017a] Subproblem dependent memory (this work) Extended Capacity Cuts Definition An Extended Capacity Cut (ECC) [START_REF] Pessoa | A robust branch-cut-and-price algorithm for the heterogeneous fleet vehicle routing problem[END_REF] over subset C of customers is any inequality valid for P(C), the polyhedron given by the convex hull of the 0 -1 solutions of Homogeneous Extended Capacity Cuts

u∈U   a∈δ - u (C) Q q=1 dx q a - a∈δ + u (C) Q-1 q=0 dx q a   = d(C)
y m,q = a q ∈δ - u (C)
x q a , z q = a q ∈δ + u (C)

x m,q a , (q = 0, . . . , Q).

Definition

A Homogeneous Extended Capacity Cut (HECC) over set C of customers is any inequality valid for the polyhedron given by the convex hull of the integral solutions of

u∈U   Q q=1 dy m,q - Q-1 q=0 dz m,q   = d(C). (1)

Separation

Cuts obtained by applying integer rounding of (1).

Heuristic separation of [START_REF] Pessoa | A robust branch-cut-and-price algorithm for the heterogeneous fleet vehicle routing problem[END_REF] is used.

Lifting of cuts in enumerated state

Rank-1 cuts Limited memory is extended to full memory

Homogeneous Extended Capacity Cuts

Integer rounding of

u∈EU r ∈Ru d r (C)λ r + u∈U\EU   Q q=1 dy m,q - Q-1 q=0 dz m,q   = d(C).
For a particular rounding multiplier and EU = U (all subproblems are in the enumerated state), equivalent to Strong Capacity Cuts [START_REF] Baldacci | An exact algorithm for the vehicle routing problem based on the set partitioning formulation with additional cuts[END_REF].

Other enhancements

Heuristic pricing (keeping one label per bucket)

Automatic dual price smoothing stabilization [START_REF] Pessoa | Automation and combination of linear-programming based stabilization techniques in column generation[END_REF].

Rollback mechanism [START_REF] Pecin | Improved branch-cut-and-price for capacitated vehicle routing[END_REF] Pessoa, A., Sadykov, R., [START_REF] Pessoa | Automation and combination of linear-programming based stabilization techniques in column generation[END_REF].

Automation and combination of linear-programming based stabilization techniques in column generation.

INFORMS Journal on Computing, (Forthcoming).

Results for classic Heterogeneous VRP instances 40 instances with 50-100 customers by [START_REF] Taillard | A heuristic column generation method for the heterogeneous fleet vrp[END_REF] 10 instances with 100-200 customers [START_REF] Brandao | A tabu search algorithm for the heterogeneous fixed fleet vehicle routing problem[END_REF] Instances with 27-324 customers by [Cordeau and Laporte, 2001] 10s 1m 10m 1h 10h 36h 9/13 21/23 solved to optimality in at most X time (log scale) Number of instances Our algorithm [START_REF] Baldacci | A unified exact method for solving different classes of vehicle routing problems[END_REF] Largest solved instance has 216 customers [START_REF] Baldacci | A unified exact method for solving different classes of vehicle routing problems[END_REF] solved only 1 of 5 instances with 100 customers and more Results for standard Multi-Depot VRP instances Instances with 50-360 customers [Cordeau et al., 1997]

Figure :

 : Figure: |I| = Q = 5, d 1 = d 3 = d 4 = 2, d 2 = d 5 = 3; routes 0-1-5-0, 0-2-0, 0-3-4-0 are shown

  = 0.5, λ 2 = 0.5, and λ 3 = 0.5, cut C = {1, 2, 3} is violated. memory[Pecin et al., 2017a] Pecin, D., Contardo, C., Desaulniers, G., and Uchoa, E. (2017a). New enhancements for the exact solution of the vehicle routing problem with time windows. INFORMS Journal on Computing, 29(3

  . and Mingozzi, A. (2009). A unified exact method for solving different classes of vehicle routing problems. Mathematical Programming, 120(2):347-380.

  in at most X time (log scale) Number of instances Our algorithm Brandao, J. (2011). A tabu search algorithm for the heterogeneous fixed fleet vehicle routing problem. Computers and Operations Research, 38(1):140 -151.

Bucket Graph Based Labelling Algorithm for the RCSPP with Applications to Vehicle Routing

	Impact of Extended Capacity Cuts Improved Best Known Solutions
	10s solved to optimality in at most X time (log scale) 1m 10m 1h 10h 7/9 10/10 11/11 [Baldacci and Mingozzi, 2009] [Contardo and Martinelli, 2014] A new exact algorithm for the multi-depot vehicle routing problem under capacity Our algorithm 10 ECC and rank-1 cuts with arc memory Contardo, C. and Martinelli, R. (2014). R1C+ECC arc, sp.dep 0.105% 113 29.6 88/90 170 1 2 5 10 20 20 30 40 50 60 70 80 90 Rank-1 cuts only with arc memory ECC and rank-1 cuts with node memory Number of instances Number of instances Rank-1 cuts Root Root Nodes Total Cuts memory gap time num. Solved time R1C only arc, sp.dep 0.323% 93 67.8 87/90 181 R1C+ECC node, sp.dep 0.133% 106 38.7 86/90 178 Previous Improved Problem Instance Size BKS A
	and route length constraints.
	Discrete Optimization, 12:129 -146. for which variant is at most X times slower than the best

Université Bordeaux, France

Universidade Federal Fluminense, Brazil Verolog 2017 Amsterdam, July 11

The labeling algorithm

Arbitrary cuts of Rank 1 Rounding using a vector p instead of single value: u∈U r ∈Ru i∈C p i a r i λ r ≤ i∈C p i

All facet-defining vectors p for cuts up to 5 rows [START_REF] Pecin | Limited memory rank-1 cuts for vehicle routing problems[END_REF]:

Pecin, D., Pessoa, A., Poggi, M., Uchoa, E., and Santos, H. (2017).

Limited memory rank-1 cuts for vehicle routing problems.

Operations Research Letters, 45(3):206 -209.

Elementary routes enumeration

We try to enumerate all elementary routes whose reduced cost is smaller than the current gap [START_REF] Baldacci | An exact algorithm for the vehicle routing problem based on the set partitioning formulation with additional cuts[END_REF], possibly to a pool [Contardo and Martinelli, 2014].

This work contributions

Subproblem dependent enumeration

If succeeded, a subproblem passes to the enumerated state:

Pricing is performed by inspection Cut coefficients of columns in the master are lifted [START_REF] Baldacci | An exact algorithm for the vehicle routing problem based on the set partitioning formulation with additional cuts[END_REF].

An exact algorithm for the vehicle routing problem based on the set partitioning formulation with additional cuts. Mathematical Programming, 115:351-385.

Branching

Strong branching [START_REF] Pecin | Improved branch-cut-and-price for capacitated vehicle routing[END_REF] Multi-strategy

A glimpse of the results

Solved 5/9 open VRPTW instances of [START_REF] Gehring | Parallelization of a two-phase metaheuristic for routing problems with time windows[END_REF] with 200 customers Solved 6/7 distance-constrained CVRP instances of [START_REF] Ii Christofides | Combinatorial Optimization, chapter The vehicle routing problem[END_REF] (CMT) with up to 200 customers Solved all 22 distance-constrained MDVRP instances of [Cordeau et al., 1997] with up to 288 customers Solved 7/10 distance-constrained SDVRP instances of [Cordeau and Laporte, 2001] with up to 216 customers Solved 56/96 "nightmare" HFVRP instances of [START_REF] Duhamel | Efficient frameworks for greedy split and new depth first search split procedures for routing problems[END_REF] with up to 186 customers.