arXiv:1701.05115v2 [math.LO] 19 Jan 20

Lattice-ordered groups generated by an
ordered group and regular systems of ideals
Thierry Coquand

Henri Lombardi

Stefan Neuwirth

23rd January 2018

Abstract
Unbounded entailment relations, introduced by Paul Lorenzen (1951), are
a slight variant of a notion which plays a fundamental rôle in logic (see Scott
1974) and in algebra (see Lombardi and Quitté 2015). We propose to define
systems of ideals for a commutative ordered monoid G as unbounded singleconclusion entailment relations that preserve its order and are equivariant:
they describe all morphisms from G to meet-semilattice-ordered monoids generated by (the image of) G. Taking an article by Lorenzen (1953) as a starting
point, we also describe all morphisms from a commutative ordered group G
to lattice-ordered groups generated by G through unbounded entailment relations that preserve its order, are equivariant, and satisfy a “regularity” property invented by Lorenzen (1950); we call them regular systems of ideals. In
particular, the free lattice-ordered group generated by G is described through
the finest regular system of ideals for G, and we provide an explicit description for it; it is order-reflecting if and only if the morphism is injective, so
that the Lorenzen-Clifford-Dieudonné theorem fits into our framework. Lorenzen’s research in algebra is motivated by the system of Dedekind ideals
for the divisibility group of an integral domain R; we provide an explicit
description of the lattice-ordered group granted by Wolfgang Krull’s “Fundamentalsatz” if (and only if) R is integrally closed through the “regularisation”
of the Dedekind system of ideals.

Keywords: ordered monoid; unbounded single-conclusion entailment relation;
system of ideals; morphism from an ordered monoid to a meet-semilattice-ordered
monoid; ordered group; regular system of ideals; unbounded entailment relation;
morphism from an ordered group to a lattice-ordered group; Lorenzen-CliﬀordDieudonné theorem; Fundamentalsatz for integral domains; Grothendieck ℓ-group.
MSC 2010: Primary 06F20; Secondary 06F05, 13A15, 13B22.
1

1

Introduction and historical background

In this article, all monoids and groups are supposed to be commutative.
The idea of generating an unbounded semilattice by an unbounded single-conclusion entailment relation, and an unbounded distributive lattice by an unbounded
entailment relation, dates back to Lorenzen (1951, §2) and is motivated there as
capturing how ideal theory provides formal gcds and lcms, i.e. formal meets and
joins, for elements of an integral domain.

1.1

The meet-semilattice-ordered monoid generated by a
system of ideals

Let us deﬁne an unbounded meet-semilattice as a purely equational algebraic structure with just one law ∧ that is idempotent, commutative, and associative. We
are dropping the axiom of meet-semilattices providing a greatest element because
it does not suit monoid theory: meets are only supposed to exist for nonempty
ﬁnitely enumerated sets.
Let Pfe∗ (G) be the set of nonempty ﬁnitely enumerated subsets of an arbitrary
set G. For an unbounded meet-semilattice S, let us denote1 by A ⊲ b the relation
deﬁned between the sets Pfe∗ (S) and S in the following way (see Lorenzen 1951,
Satz 1):
⋀
⋀
⋀
def
def
A.
A ⊲ b ⇐⇒
A 6S b ⇐⇒ b ∧ A =S
This relation is reﬂexive, monotone (a property also called “thinning”), and
transitive (a property also called “cut” because it “cuts” x) in the following sense,
which may be expressed without the law ∧:
a⊲a
if A ⊲ b, then A, A′ ⊲ b
if A ⊲ x and A, x ⊲ b, then

A⊲b

(reﬂexivity);
(monotonicity);
(transitivity);

note that in the context of relations, we shall make the following abuses of notation
for ﬁnitely enumerated sets: we write a for the singleton consisting of a, and A, A′
for the union of the sets A and A′ .
These three properties correspond respectively to the “tautologic assertions”,
the “immediate deductions”, and to an elementary form of the “syllogisms” of the
systems of axioms introduced by Paul Hertz (1923, § 1), so that the following
notion may be attributed to him2 ; see also Gerhard Gentzen (1933, § 2), who
1 The

sign ⊲ has been introduced with this meaning by Rinaldi, Schuster, and Wessel (2017).
Béziau (2006, § 6) discusses the relationship of single-conclusion entailment relations with Alfred Tarski’s consequence operation, which may be compared to the relationship
of our Definition 1.3 of a system of ideals with the set-theoretic star-operation: see Item (2 ) of
Remarks 1.4.
2 Jean-Yves

2

coined the terms “thinning” and “cut”. The deﬁnition below has been introduced
as description of an unbounded meet-semilattice (see Theorem 2.1) in Lorenzen
(1951, § 2).
Definition 1.1. Let G be an arbitrary set.
1. A relation ⊲ between Pfe∗ (G) and G which is reﬂexive, monotone, and transitive is called an unbounded single-conclusion entailment relation for G.
2. The unbounded single-conclusion entailment relation ⊲2 is coarser than the
unbounded single-conclusion entailment relation ⊲1 if A ⊲1 y implies A ⊲2 y. One
says also that ⊲1 is finer than ⊲2 .
Remarks 1.2.
1. If instead of nonempty subsets, we had considered nonempty
multisets, we would have had to add a contraction rule, and if we had considered
nonempty lists, we would have had to add also a permutation rule.
2. The terminology “coarser than” has the following explanation. The nonempty ﬁnitely enumerated set A to the left of ⊲ represents a formal meet of A for
the preorder 6⊲ on Pfe∗ (G) associated to the unbounded single-conclusion entailment relation ⊲, deﬁned by
def

A 6⊲ B ⇐⇒ A ⊲ b for all b ∈ B.

(∗)

To say that the relation ⊲2 is coarser than the relation ⊲1 is to say this for the
associated preorders, i.e. that A 6⊲1 B implies A 6⊲2 B, and this corresponds
to the usual meaning of “coarser than” for preorders, since A =⊲1 B implies
accordingly A =⊲2 B, i.e. the equivalence relation =⊲2 is coarser than =⊲1 .
⋄
Now suppose that (G, 6G ) is an ordered monoid3 , (M, 6M ) a meet-semilatticeordered monoid4 , a meet-monoid for short, and ψ : G → M a morphism of ordered
monoids. The relation
def

a1 , . . . , an ⊲ b ⇐⇒ ψ(a1 ) ∧ · · · ∧ ψ(an ) 6M ψ(b)
deﬁnes an unbounded single-conclusion entailment relation for G that satisﬁes furthermore the following properties:
S1 if a 6G b, then a ⊲ b

(preservation of order);

S2 if A ⊲ b, then x + A ⊲ x + b

(x ∈ G)

(equivariance).

We propose to introduce systems of ideals in a purely logical way (i.e. as entailment
relations that require only a naive set theory for ﬁnitely enumerated sets): the
following deﬁnition has been extracted from Lorenzen (1939, Deﬁnition 1) (compare
Jaﬀard 1960, I, § 3, 1).
3 I.e. a monoid (G, +, 0) endowed with an order relation 6
G compatible with addition: x 6G
y =⇒ x + z 6G y + z.
4 I.e. a monoid endowed with an unbounded meet-semilattice law ∧ inducing 6
M and compatible with addition: the equality x + (y ∧ z) = (x + y) ∧ (x + z) holds.

3

Definition 1.3. A system of ideals for an ordered monoid G is an unbounded
single-conclusion entailment relation ⊲ for G satisfying Properties S1 and S2.
Remarks 1.4.
1. We ﬁnd that it is more natural to state a direct implication
rather than an equivalence in Item S1 ; we deviate here from Lorenzen and Paul
Jaﬀard (1960, page 16). The reverse implication expresses the supplementary property that the system of ideals is order-reﬂecting.
2. Lorenzen (1939), following Heinz Prüfer (1932, § 2) and David Hilbert in
subordinating algebra to set theory, is describing a (ﬁnite) “r-system” of ideals
through a set-theoretic map (called ′ -operation by Krull 1935, 43., and rather
called star-operation today)
Pfe∗ (G) −→ P(G),

def

A 7−→ { x ∈ G | A ⊲ x } = Ar

(here P(G) stands for all subsets of G, and r is just a variable name for distinguishing diﬀerent systems) that satisﬁes the following properties:
I1

Ar ⊇ A;

I2

Ar ⊇ B

I3

{a}r = { x ∈ G | a 6G x }

I4

(x + A)r = x + Ar

=⇒

Ar ⊇ Br ;
(preservation and reﬂection of order);
(equivariance).

Let us note that the containment Ar ⊇ Br corresponds to the inequality A 6⊲ B
for the preorder associated to the single-conclusion entailment relation ⊲ by the
equivalence (∗) above.
As previously indicated, in contradistinction to Lorenzen and Jaﬀard, we ﬁnd it
more natural to relax the equality in I3 to a containment: if we do so, the reader
can prove that the deﬁnition of star-operation is equivalent to Deﬁnition 1.3. Items
I1 and I2 correspond to the deﬁnition of a single-conclusion entailment relation,5
and Items I3 (relaxed) and I4 correspond to Items S1 and S2 in Deﬁnition 1.3.
Compare Lorenzen (1950, pages 504–505).
3. In the set-theoretic framework of the previous item, the r2 -system is coarser
than the r1 -system exactly if Ar2 ⊇ Ar1 holds for all A ∈ Pfe∗ (G) (see Jaﬀard 1960,
I, § 3, Proposition 2).
⋄
Comment 1.5. Lorenzen unveiled the lattice theory hiding behind multiplicative
ideal theory step by step, the decisive one being dated back by him to 1940. In
a footnote to his deﬁnition, Lorenzen (1939, page 536) writes: “If one understood
hence by a system of ideals every lattice that contains the principal ideals and
satisﬁes Property [I4 ], then this deﬁnition would be only unessentially broader”.
In a letter to Krull6 dated 13th March 1944, he writes: “For example, the insight
5 They

can also be read as a finite version of Tarski’s consequence operation (see Footnote 2).
Archiv, Universität Konstanz, PL 1-1-131.

6 Philosophisches

4

that a system of ideals is actually nothing more than a supersemilattice, and a
valuation nothing more than a linear order, strikes me as the most essential result
of my eﬀort”.
⋄
The eﬀectiveness of Deﬁnition 1.3 is shown by the following theorem.
Theorem I. Let ⊲ be a system of ideals for an ordered monoid G. Let S be the unbounded meet-semilattice generated by the unbounded single-conclusion entailment
relation ⊲. Then there is a (unique) monoid law on S which is compatible with its
semilattice structure and such that the natural morphism (of ordered sets) G → S
is a monoid morphism.
Comment 1.6. Lorenzen (1950, page 486) emphasises the transparency of this
approach as compared to the set-theoretic ideals: “But if one removes this settheoretic clothing, then the concept of ideal may be deﬁned quite simply: a system
of ideals of a preordered set is nothing other than an embedding into a semilattice.”
⋄

1.2

The lattice-ordered group generated by a regular system
of ideals

Let us deﬁne an unbounded distributive lattice as a purely equational algebraic
structure with two laws ∧ and ∨ satisfying the axioms of distributive lattices,
except the two axioms providing a greatest and a least element, because they do
not suit group theory.
For an unbounded distributive lattice L, let us denote by A ⊢ B the relation
deﬁned on the set Pfe∗ (L) in the following way (see Lorenzen 1951, Satz 5):
def

A ⊢ B ⇐⇒

⋀

A 6L

⋁

B.

This relation is reﬂexive, monotone, and transitive in the following sense, which
may be expressed without the laws ∧ and ∨:
(reﬂexivity);

a⊢a
′

if A ⊢ B, then A, A ⊢ B, B
if A ⊢ B, x and A, x ⊢ B, then
A⊢B

′

(monotonicity);
(transitivity);

we insist on the fact that A and B must be nonempty.
The following deﬁnition is a variant of a notion whose name has been coined
by Dana Scott (1974, page 417). It is introduced as description of an unbounded
distributive lattice (see Theorem 3.1) in Lorenzen (1951, § 2).
Definition 1.7.
1. For an arbitrary set G, a binary relation ⊢ on Pfe∗ (G) which
is reﬂexive, monotone, and transitive is called an unbounded entailment relation.
5

2. The unbounded entailment relation ⊢2 is coarser than the unbounded entailment relation ⊢1 if A ⊢1 B implies A ⊢2 B. One says also that ⊢1 is finer
than ⊢2 .
Item (1 ) of Remarks 1.2 applies again verbatim for Deﬁnition 1.7.
Now suppose that (G, 6G ) is an ordered group7 , (H, 6H ) a lattice-ordered
group8 , an ℓ-group for short, and ϕ : G → H a morphism of ordered groups. The
laws ∧ and ∨ on an ℓ-group provide an unbounded distributive lattice structure,
and the relation
def

a1 , . . . , an ⊢ b1 , . . . bm ⇐⇒ ϕ(a1 ) ∧ · · · ∧ ϕ(an ) 6H ϕ(b1 ) ∨ · · · ∨ ϕ(bm )
deﬁnes an unbounded entailment relation for G that satisﬁes furthermore the following properties:
R1 if a 6G b, then a ⊢ b

(preservation of order);

R2 x + a, y + b ⊢ x + b, y + a
R3 if A ⊢ B, then x + A ⊢ x + B

(regularity);
(x ∈ G)

(equivariance).

Properties R1 and R3 are straightforward, and the property R2 of regularity follows from the observation that if x′ , a′ , y ′ , b′ are elements of H, then the inequality
(x′ + a′ ) ∧ (y ′ + b′ ) 6H (x′ + b′ ) ∨ (y ′ + a′ )

(†)

reduces successively to


0 6H (−x′ − a′ ) ∨ (−y ′ − b′ ) + (x′ + b′ ) ∨ (y ′ + a′ )

0 6H (b′ − a′ ) ∨ (y ′ − x′ ) ∨ (x′ − y ′ ) ∨ (a′ − b′ )
0 6H |b′ − a′ | ∨ |y ′ − x′ |.

We assemble these observations into the following new purely logical deﬁnition
(compare Lorenzen 1953, § 1).
Definition 1.8. Let G be an ordered group.
1. A regular system of ideals for G is an unbounded entailment relation ⊢ for G
satisfying Properties R1, R2, and R3.
2. A system of ideals for G is regular if it is the restriction of a regular system
of ideals to Pfe∗ (G) × G.
The ambiguity introduced by these two deﬁnitions is harmless because it turns
out that a regular system of ideals is determined by its restriction to Pfe∗ (G) × G
(see Theorem 3.9).
7 I.e.

a group that is an ordered monoid.
an ordered group that is a semilattice: this is enough to ensure that it is a meet-monoid,
that any two elements have a join, and that the distributivity laws hold.
8 I.e.

6

Comment 1.9. The property of regularity arises in Lorenzen’s analysis of the rôle
played by the commutativity of the group: he isolates Inequality (†), which is
trivially veriﬁed in a commutative ℓ-group, but not in a noncommutative one. Lorenzen (1950, Satz 13) proves by a well-ordering argument that a (noncommutative)
ℓ-group that is regular in this sense is a subdirect product of linearly preordered
groups. In the commutative setting, this corresponds to the theorem (in classical
mathematics) stating that any commutative ℓ-group is a subdirect product of linearly preordered commutative groups.
⋄
A system of ideals gives rise to a regular system of ideals if one supposes that,
i.e. one does as if, elements occurring in a computation are comparable. More
precisely, this gives the following deﬁnition.
Definition 1.10 (see Lorenzen 1953, (2.2) and page 23). Let ⊲ be a system of
ideals for an ordered group G.
1. For every element x of G, consider the system of ideals ⊲x coarser than ⊲
obtained by forcing the property 0 ⊲ x. The regularisation of ⊲ is the relation
on Pfe∗ (G) deﬁned by
def

A ⊢⊲ B ⇐⇒ there are x1 , . . . , xℓ such that for every choice
of signs ± holds A − B ⊲±x1 ,...,±xℓ 0.
2. The group G is ⊲-closed if ⊢⊲ reﬂects the order on G, i.e. if a ⊢⊲ b =⇒
a 6G b holds for all a, b ∈ G.
The basic idea of this construction is described in the introduction of Lorenzen
1950, pages 488–489. Let us go through a simple example that illustrates a relevant
feature of regularisation (compare Corollary 3.4).
Example 1.11. Let us apply a case-by-case reasoning in order to prove that in a
linearly ordered group, if n1 u1 + · · · + nk uk 6 0 for some integers ni > 0 not all
zero, then uj 6 0 for some j. If uj 6 0 for some j, everything is all right. If uj > 0
for all j, take i such that ni > 1: then ui 6 ni ui 6 n1 u1 + · · · + nk uk 6 0. The
conclusion holds in each case.
Similarly, assume that n1 u1 + · · · + nk uk ⊲ 0 with ni > 0 not all zero. We have
uj ⊲ −uj 0 for each j. By monotonicity,
u1 , . . . , uk ⊲ǫ1 u1 ,...,ǫk uk 0
if at least one ǫj is equal to −1. If 0 ⊲ uj for all j, take i such that ni > 1: then
ui 6⊲ ni ui 6⊲ n1 u1 + · · · + nk uk 6⊲ 0. This proves that u1 , . . . , uk ⊲+u1 ,...,+uk 0.
We conclude that
u1 , . . . , uk ⊢⊲ 0.
⋄
Comment 1.12. Lorenzen (1950, 1952, 1953) considers a preordered commutative or
noncommutative group (G, 4G ) and a meet-monoid Hr (“H ” for “Halbverband”,
7

semilattice, r a variable name for distinguishing diﬀerent monoids) given by a
system of ideals ⊲ for G. The meet-monoid Hr gives rise to another meet-monoid,
Hra (“a” for “algebraically representable”), given by a system of ideals ⊲a that is
not deﬁned as in Theorem 6.7 by forcing cancellativity, but so as to capture the
classical deﬁnition of integral dependence of an element b over a nonempty ﬁnitely
enumerated set A, i.e.
def

A ⊲a b ⇐⇒ for every linear order 6 which is coarser than ⊲,
there is an a ∈ A with a 6 b.
Lorenzen’s analysis of the constructive content of this deﬁnition results in the system of ideals ⊢⊲ of Deﬁnition 1.10 with B a single conclusion, i.e. in the system ⊲
supplemented with the hypothesis that elements occurring in a computation are
comparable. Lorenzen (1950, Satz 24) proves that A ⊢⊲ b holds if and only if
A ⊲a b holds: more precisely, it is straightforward that every linear order coarser
than ⊲ is also coarser than ⊢⊲ , so that A ⊢⊲ b =⇒ A ⊲a b; conversely, he
considers a maximal order without A ⊢⊲ b holding (granted by a well-ordering
argument) and shows that it cannot be other than linear.
⋄
Theorem II (see Lorenzen 1953, § 1). Let ⊲ be a system of ideals for an ordered
group G. The regularisation A ⊢⊲ B given in Definition 1.10 is the finest regular
system of ideals for G whose restriction to Pfe∗ (G) × G is coarser than ⊲.
Remark 1.13. This enhances the ﬁrst part of the proof of the remarkable Satz 1 of
Lorenzen (1953). In our analysis of Lorenzen’s proof, we separate the construction
of the regularisation from the investigation of its relationship with the group law.
In doing so, we make the regularity property (Property R2 ) the lever for sending G
homomorphically into an ℓ-group. In place of its second part, we propose the new
Theorem IV below, stating that regular systems of ideals provide a description
of all morphisms from an ordered group G to ℓ-groups generated by (the image
of) G.
⋄
Underway, we provide the following constructive version of a key observation
concerning the ℓ-group freely generated by an ordered group.
Theorem III. Let ı be the morphism from an ordered group G to the ℓ-group H
⋁k
that it freely generates. Let u1 , . . . , uk ∈ G. We have j=1 ı(uj ) >H 0 if and only
Pk
if there exist integers mj > 0 not all zero such that j=1 mj uj >G 0.

Theorem III may be seen as a generalisation of the following corollary, i.e. the
classical Lorenzen-Clifford-Dieudonné theorem.

Corollary 1.14 (Lorenzen-Cliﬀord-Dieudonné, see Lorenzen 1939, Satz 14 for the
s-system of ideals; Cliﬀord 1940, Theorem 1; Dieudonné 1941, Section 1). The
ordered group (G, 6G ) is embeddable into an ℓ-group if and only if
nx >G 0 implies x >G 0
8

( x ∈ G, n > 1).

(‡)

Proof. The condition is clearly necessary. Theorem III shows that it yields the
injectivity of the morphism ı : G → H as well as the fact that ı(x) 6H ı(y) implies
x 6G y.
Comments 1.15.
1. In fact, in his Ph.D. thesis (1939), Lorenzen proves Corollary 1.14 as a side-product of his enterprise of generalising the concepts of multiplicative ideal theory to the framework of preordered groups. See Comment 3.17.
2. In each of the three references given in Corollary 1.14, the authors invoke
a maximality argument for showing that G embeds in fact into a direct product
of linearly ordered groups. The goal of Lorenzen (1950, § 4; 1953) is to avoid the
necessarily nonconstructive reference to linear orders in conceiving embeddings into
an ℓ-group, and this endeavour culminates in the Corollary to Theorem IV below.
But this goal may also be achieved through the Prüfer approach of Lorenzen (1939),
and the sought-after ℓ-group may be constructed via Item (2 ) of Theorem 6.7. ⋄
Theorem IV. Let ⊢ be a regular system of ideals for an ordered group G. Let H
be the unbounded distributive lattice generated by the unbounded entailment relation ⊢. Then there is a (unique) group law on H which is compatible with its lattice
structure and such that the natural morphism (of ordered sets) G → H is a group
morphism.
Theorem IV is new and replaces the second step of the proof of Satz 1 in
Lorenzen (1953). Our approach reveals the rôle of regularity and allows for more
conceptual arguments, with the price of an appeal to Theorem III, avoided by
Lorenzen (see Comment 5.1).
These results give rise to the following construction and corollary, that one can
ﬁnd in Lorenzen (1953, § 2 and page 23).
Definition 1.16. Let ⊲ be a system of ideals for an ordered group G. The
Lorenzen group associated to ⊲ is the ℓ-group provided by Theorems II and IV.
Comment 1.17. Lorenzen (1939, § 4) and Jaﬀard (1960, II, § 2, 2) deﬁne the Lorenzen group associated to a system of ideals according to the Prüfer approach
(see Deﬁnition 6.9). The present approach leading to Deﬁnition 1.16 dates back
to Lorenzen (1950, § 6). The two deﬁnitions are equivalent according to Proposi⋄
tion 6.10.
Corollary to Theorem IV. Let ⊲ be a system of ideals for an ordered group G.
If G is ⊲-closed, then G embeds into the Lorenzen group associated to ⊲.
In this article, our aim is to give a precise account of the approach by regular
systems of ideals; we are directly inspired by Lorenzen (1953). The literature
on ℓ-groups seems not to have taken notice of these results. In Lorenzen’s work,
this approach supersedes another, based on the Grothendieck ℓ-group of the meetmonoid obtained by forcing cancellativity of the system of ideals, ideated by Prüfer
9

(1932) and generalised to the setting of ordered monoids in Lorenzen’s Ph.D. thesis
(1939). In Section 6, we also provide an account for that approach, which yields
a construction of an ℓ-group from a system of ideals which turns out to be the
associated Lorenzen group.

1.3

The Fundamentalsatz for integral domains

The motivating example for Lorenzen’s analysis of the concept of ideal is Wolfgang
Krull’s “Fundamentalsatz”, which states that an integral domain is an intersection
of valuation rings if and only if it is integrally closed. As Krull (1935, page 111)
himself emphasises, “Its main defect, that one must not overlook, lies in that it is
a purely existential theorem”, resulting from a well-ordering argument. In a letter
to Heinrich Scholz9 dated 18th April 1953, Krull writes: “At working with the
uncountable, in particular with the well-ordering theorem, I always had the feeling
that one uses ﬁctions there that need to be replaced some day by more reasonable
concepts. But I was not getting upset over it, because I was convinced that at a
careful application of the common ‘ﬁctions’ nothing false comes out, and because
I was ﬁrmly counting on the man who would some day put all in order. Lorenzen
has now found according to my conviction the right way [. . . ]”.
Lorenzen’s goal is to unveil the constructive content of Krull’s Fundamentalsatz,
i.e. to express it without reference to valuations. He shows that the well-ordering
argument may be replaced by the right to compute as if the divisibility group was
linearly ordered (see Deﬁnition 1.10 above), that integral closedness guarantees
that such computations do not add new relations of divisibility to the integral
domain, and that this generates an ℓ-group. The corollary to Theorem IV is in
fact an abstract version of the following theorem (see Theorem 5.4).
Theorem. Let R be an integral domain, K its field of fractions, and G = K × /R×
its divisibility group. Consider the Dedekind system of ideals for G defined by
def

A ⊲d b ⇐⇒ b ∈ hAiR ,
where hAiR is the fractional ideal generated by A over R in K. Then G embeds
into an ℓ-group that contains the Dedekind system of ideals if and only if R is
integrally closed.

1.4

Outline of the article

Let us now brieﬂy describe the structure of this article.
Section 2 deals with unbounded meet-semilattices as generated by unbounded
single-conclusion entailment relations, discusses systems of ideals for an ordered
9 Scholz-Archiv, Westfälische Wilhelms-Universität Münster, http://www.uni-muenster.de/
IVV5WS/ScholzWiki/doku.php?id=scans:blogs:ko-05-0647, accessed 21st September 2016.

10

monoid and the meet-monoid they generate (Theorem I), and describes the case
in which the system of ideals for an ordered group is in fact a group: then G is a
divisorial group, a notion tightly connected with Weil divisor groups.
Section 3 deals with unbounded distributive lattices as generated by unbounded
entailment relations, discusses regular systems of ideals and provides the proof of
Theorem II. It also proposes two applications: a description of the ﬁnest regular
system of ideals and Lorenzen’s theory of divisibility for integral domains.
Section 4 provides a constructive proof of Theorem III based on the Positivstellensatz for ordered groups.
Section 5 proves the main theorem of the article, Theorem IV, stating that
regular systems of ideals for an ordered group generate in fact an ℓ-group. Some
consequences for Lorenzen’s theory of divisibility for integral domains are stated.
Section 6 reminds us of an important theorem by Prüfer which leads to the
historically ﬁrst approach to the Lorenzen group associated to a system of ideals.
A more elaborate study of Lorenzen’s work will be the subject of another article that will provide a detailed analysis of Lorenzen (1950, 1952, 1953). These
works have been written with careful attention to the possibility of constructive
formulations for abstract existence theorems.
This article is written in Errett Bishop’s style of constructive mathematics
(Bishop 1967; Bridges and Richman 1987; Mines, Richman, and Ruitenburg 1988;
Lombardi and Quitté 2015): all theorems can be viewed as providing an algorithm
that constructs the conclusion from the hypotheses.

2
2.1

Unbounded meet-monoids and systems of ideals
Unbounded meet-semilattices and single-conclusion entailment relations

A fundamental theorem holds for an unbounded single-conclusion entailment relation for a given set G: it states that the relation generates an unbounded meet-semilattice S whose order reﬂects the relation. This is the single-conclusion analogue
of the better known Theorem 3.1.
Theorem 2.1 (fundamental theorem of unbounded single-conclusion entailment
relations, see Lorenzen 1951, Satz 3).10 Let G be a set and ⊲ an unbounded singleconclusion entailment relation between Pfe∗ (G) and G. Let us consider the unbounded meet-semilattice S defined by generators and relations in the following way:
the generators are the elements of G and the relations are the
⋀
A 6S b whenever A ⊲ b.
10 Our statement is the natural counterpart to Lorenzen’s when using basic notions of universal
algebra, and follows readily from his sketch of proof.

11

Then, for all (A, b) in Pfe∗ (G) × G, we have the reflection of entailment
⋀
if
A 6S b, then A ⊲ b.
In fact, S can be defined as the ordered set obtained by descending to the quotient
of (Pfe∗ (G), 6⊲ ), where 6⊲ is the preorder defined by
def

A 6⊲ B ⇐⇒ A ⊲ b for all b ∈ B.

(∗)

Pfe∗ (G)

Proof. One sees easily that 6⊲ is a preorder on
that endows its quotient
by =⊲ with a meet-semilattice structure, where the law ∧⊲ is obtained by descending the law (A, B) 7→ A ∪ B to the quotient. The reader will prove that S can also
be deﬁned by generators and relations as in the statement.
Note that the preorder x ⊲ y on G makes its quotient a subobject of S in the
category of ordered sets.
Remarks 2.2.
1. Suppose that (G, 6G ) is an ordered set. The “ﬁnite DedekindMacNeille completion” that adds formal ﬁnite meets to G in a minimal way is the
unbounded semilattice generated by the coarsest order-reﬂecting unbounded singleconclusion entailment relation for G, denoted by ⊲v :
def

A ⊲v b ⇐⇒ ∀z ∈ G if z 6G A, then z 6G b,

(§)

where z 6G A means z 6G a for all a ∈ A.
2. The relation a ⊲ b is a priori just a preorder relation for G, not an order
relation. Let us denote the element a viewed in the ordered set G associated to this
preorder by a, and let A = { a | a ∈ A } for a subset A of G. In Theorem 2.1, we
construct a meet-semilattice S endowed with an order 6S that coincides with ⊲
on Pfe∗ (G) × G; for the sake of rigour, we should have written A 6S b rather than
A 6S b in order to deal with the fact that the equality of S is coarser than the
equality of G. In particular, it is G rather than G which can be identiﬁed with a
subset of S.
⋄

2.2

Systems of ideals for an ordered monoid

Let us now discuss the deﬁnition of a system of ideals à la Lorenzen for an ordered
monoid, Deﬁnition 1.3, given in the language of single-conclusion entailment relations.
In the case that G is an ordered group, we may state an apparently simpler
deﬁnition for systems of ideals.
Proposition 2.3 (a variant for the deﬁnition of a system of ideals for an ordered
group). Let us consider a predicate · ⊲ 0 on Pfe∗ (G) for an ordered group G and
let us define a relation between the sets Pfe∗ (G) and G by
def

A ⊲ b ⇐⇒ A − b ⊲ 0.
12

In order for this relation to be a system of ideals, it is necessary and sufficient that
the following properties be fulfilled:
T1

if a 6G 0, then a ⊲ 0

(preservation of order);

′

T2

if A ⊲ 0, then A, A ⊲ 0

T3

if A − x ⊲ 0 and A, x ⊲ 0, then A ⊲ 0

(monotonicity);
(transitivity).

Proof. Left to the reader.
The ﬁnest and the coarsest system of ideals admit the following descriptions.
Proposition 2.4 (Lorenzen 1950, Satz 14, Satz 15, Footnote 26). Let G be an
ordered monoid.
1. The finest system of ideals for G is defined by
def

A ⊲s b ⇐⇒ a 6G b for some a ∈ A.
Note that ⊲s is order-reflecting: x ⊲s y iff x 6G y.
2. The coarsest order-reflecting system of ideals for G is defined by
def

A ⊲v b ⇐⇒ ∀z, w ∈ G if z 6G A + w, then z 6G b + w,
where z 6G A + w means z 6G a + w for all a ∈ A.
3. If G is an ordered group, this may be simplified into the definitional equivalence (§) on page 12.
Remark 2.5. As noted in Item (3 ) for ⊲v , the deﬁnition of ⊲s could be stated
verbatim in the framework of ordered sets and single-conclusion entailment relations.
⋄
Comment 2.6. The system of ideals ⊲v was introduced independently by Bartel
Leendert van der Waerden (see van der Waerden 1931, § 103, or the translation
van der Waerden 1950, § 105, of its second edition) and Prüfer (1932) (“v” like
“Vielfache”, “multiples” of gcds). The system of ideals ⊲s appears ﬁrst in Lorenzen
(1939) (“s” standing perhaps for “sum”).
⋄
Proof.
1. Left to the reader.
2. It is straightforward to check that ⊲v is a single-conclusion entailment relation for G. Let us check the remaining properties.
• S1. Let y ∈ G. Suppose a 6G b: then a + y 6G b + y, i.e. if x 6G a + y,
then x 6G b + y; hence a ⊲v b.
• Reflection of order. Conversely, suppose a ⊲v b: taking z = a and w = 0 in
the deﬁnition of a ⊲v b, we get a 6G b.
13

• S2. Let us suppose A ⊲v b and prove A + x ⊲v b + x for x ∈ G. Let z, w ∈ G;
if z 6G (A + x) + w, then z 6G A + (x + w), and by hypothesis z 6G b + (x + w),
i.e. z 6G (b + x) + w.
Now let ⊲ be an order-reﬂecting system of ideals for G and suppose that A ⊲ b.
Let us prove that A ⊲v b. Let z, w ∈ G and suppose that z 6G A + w; by the
deﬁnition of 6⊲ and because A + w ⊲ b + w, we have z 6⊲ A + w 6⊲ b + w. Since
6⊲ reﬂects the order on G, z 6G b + w.

2.3

Proof of Theorem I

Proof of Theorem I. We deﬁne A + B = { a + b | a ∈ A, b ∈ B } in Pfe∗ (G). We have
to check that this law descends to the quotient S. It suﬃces to show that B 6⊲ C
implies A + B 6⊲ A + C: in fact, B 6⊲ C implies x + B 6⊲ x + C by equivariance,
and A + B 6⊲ x + C for every x ∈ A by monotonicity. Finally, let us verify
the compatibility of ∧⊲ with addition: we note that already in Pfe∗ (G) we have
A + (B ∪ C) = (A + B) ∪ (A + C).

2.4

The classical (Weil) divisor group in commutative algebra

Prüfer (1932, § 3) introduces a property for a system of ideals, “Property B”,
expressing that the associated meet-monoid is in fact a group (and hence an ℓgroup). The next proposition shows that this is essentially a property of the ordered
monoid itself.
Proposition 2.7 (Lorenzen 1950, Satz 16). Let G be an ordered monoid and ⊲ an
order-reflecting system of ideals for G. If the associated meet-monoid is a group,
then ⊲ coincides with the coarsest system of ideals ⊲v for G.
Proof. Suppose that A ⊲v b, i.e. that A 6⊲v b. We need to prove that A ⊲ b, i.e.
that A 6⊲ b. Since 6⊲v and 6⊲ reﬂect 6G , we know that
0 6⊲v B

⇐⇒

0 6⊲ B

⇐⇒

0 6G B.

Let C ∈ Pfe∗ (G) such that A + C =⊲ 0. We have 0 6⊲ A + C and hence 0 6⊲v
A + C. We get 0 6⊲v A + C 6⊲v b + C. Therefore 0 6⊲ b + C and A 6⊲
b + C + A =⊲ b.
In the rest of this section, we shall only consider the case where G is a group
because of the lack of applications, and because it avoids a more involved deﬁnition
of divisorial opposites below.
Proposition 2.10 below will show that Property B may be caught by the following deﬁnitions.
14

Definitions 2.8. Let G be an ordered group.
1. Two nonempty ﬁnitely enumerated subsets A, B of G are divisorially opposite if 0 is a meet for A + B in G.
2. The group G is divisorial if every nonempty ﬁnitely enumerated subset admits a divisorial opposite.
Remarks 2.9.
1. The notion of divisorially opposite sets coincides with the notion of divisorially inverse lists in (the multiplicative notation of) Coquand and
Lombardi (2016).
⋀
⋁
2. Formally, in Item (1 ), we think of an equality B = −A as of the equality
⋀
(A + B) = 0, so that the join of −A is given by the meet of B. It remains to
show that this intuition works.
⋄
Proposition 2.10. Let G be an ordered group. T.f.a.e.
1. The meet-monoid associated to the system of ideals ⊲v is a group.
2. The group G is divisorial.
Proof.
(1) =⇒ (2). Consider A ∈ Pfe∗ (G). Then the opposite of A in the meetmonoid associated to ⊲v may be written B for some B ∈ Pfe∗ (G), i.e. A + B =⊲v 0.
But A + B 6⊲v 0 means that if x 6G A + B, then x 6G 0; and 0 6⊲v A + B means
that every element of A + B is >G 0.
(2) =⇒ (1). It suﬃces to check that if A ∈ Pfe∗ (G), then a divisorial opposite B
of A satisﬁes A + B =⊲v 0. First 0 6G A + B, so that 0 6⊲v A + B. Second,
A + B ⊲v 0 holds because z 6G A + B =⇒ z 6G 0.
Divisorial groups will provide natural examples of the Lorenzen group associated to a system of ideals, i.e. the meet-monoid associated to ⊲v .
Remarks 2.11.
1. Proposition 2.10 can be seen as a variant of Jaﬀard (1960, II,
§ 3, Corollaire du théorème 3, page 55).
2. Divisorial groups are tightly connected to Weil divisor groups in commutative algebra. Coquand and Lombardi (2016) give a constructive presentation of
“rings with divisors” (in French, “anneaux à diviseurs”), which they deﬁne as integral domains whose divisibility group is divisorial. Rings with divisors with an
additional condition of noetherianity are called Krull domains. H. M. Edwards
(1990) describes in his Divisor theory an approach à la Kronecker to rings with
divisors in the case where they are constructed as integral closures of ﬁnite extensions of “Kronecker natural rings”. See also in the same spirit Hermann Weyl
(1940, Chapter II, § 11). Rings with divisors are called “pseudo-Prüferian integral
domains” by Nicolas Bourbaki (1972, VII.2.Ex.19), and “Prüfer-v-multiplication
domains (PvMD)” in the English literature (one can also ﬁnd the terminology
“rings with a theory of divisors”). The main examples are the gcd domains (for
which the divisor group coincides with the divisibility group) and the coherent normal domains (especially in algebraic geometry). In the case of noetherian coherent
15

normal domains, the divisor group is usually called the Weil divisor group. For a
ring with divisors R, the Weil divisor group Div(R) is a quotient of the Lorenzen
group Lor(R) as deﬁned in Deﬁnition 5.3, with equality in the case of Prüfer domains. We expand on this topic in Remark 5.7; see also Díaz-Toca, Lombardi, and
Quitté (2014, Chapter IX).
⋄

3

Unbounded distributive lattices and regular systems of ideals

3.1

Unbounded distributive lattices

References: Lorenzen 1951; Cederquist and Coquand 2000; Lombardi and Quitté
2015.
The counterpart of Theorem 2.1 for unbounded entailment relations is Theorem 3.1, an unbounded variant of the fundamental theorem of entailment relations
(Cederquist and Coquand 2000, Theorem 1, obtained independently), which may
in fact be traced back to Lorenzen (1951, Satz 7). It states that an unbounded
entailment relation for a set G generates an unbounded distributive lattice L whose
order reﬂects the relation. The proof is essentially the same as in Cederquist and
Coquand (2000) or in Lombardi and Quitté (2015, Theorem XI-5.3).
Theorem 3.1 (fundamental theorem of unbounded entailment relations, see Lorenzen 1951, Satz 7). 11 Let G be a set and ⊢ an unbounded entailment relation
on Pfe∗ (G). Let us consider the unbounded distributive lattice L defined by generators and relations in the following way: the generators are the elements of G and
the relations are the
⋀
⋁
A 6L
B whenever A ⊢ B.
Then, for all A, B in Pfe∗ (G), we have the reflection of entailment
⋀
⋁
if
A 6L
B, then A ⊢ B.
Item (2 ) of Remark 2.2 applies again mutatis mutandis.

3.2

Regular systems of ideals for an ordered group

Let us now undertake an investigation of the deﬁnition of a regular system of ideals,
Deﬁnition 1.8.
When we assume Property R1, the following fact concerning entailment relations takes a ﬂavour of “monotonicity for the order relation of G”.
11 Footnote 10 applies verbatim. Lorenzen’s Satz 7 yields directly that if for every distributive
⋀
⋁
⋀
⋁
lattice L and every f : G → L with X ⊢ Y =⇒
f (X) 6L
f (Y ) one has f (A) 6L
f (B),
then A ⊢ B. This may be considered as a result of completeness for the semantics of distributive
lattices.

16

Lemma 3.2 (a banal fact concerning entailment relations). Assume that c ⊢ d.
1. If A ⊢ B, c, then A ⊢ B, d.
2. If A, d ⊢ B, then A, c ⊢ B.
Proof. By monotonicity, c ⊢ d gives A, c ⊢ B, d.
1. A ⊢ B, c gives A ⊢ B, c, d. Cutting c, we get A ⊢ B, d.
2. Symmetric argument.
Proposition 3.3. Let ⊢ be a regular system of ideals for an ordered group G. The
following properties (of which R2 is a particular case) are valid for each integer n >
1:
if x1 + · · · + xn =G y1 + · · · + yn , then x1 , . . . , xn ⊢ y1 , . . . , yn .
Note that if we have x1 + · · · + xn =G y1 + · · · + ym with m 6= n, we may add 0s
to the shorter list in order to apply the lemma. E.g. if a =G b + c, then 0, a ⊢ b, c.
In this way, we get 0, 0 ⊢ a, −a, which contracts to 0 ⊢ a, −a, and a, −a ⊢ 0.
Proof. Case n = 2. By Property R2, we have y1 + (y2 − x2 ), x2 ⊢ y1 , x2 + (y2 − x2 )
and if x1 + x2 =G y1 + y2 , then y1 + (y2 − x2 ) =G x1 .
Case n > 2. By induction. Assume that x1 + · · · + xn =G y1 + · · · + yn . By the
induction hypothesis we have on the one hand
x1 + x2 − y1 , x3 , . . . , xn ⊢ y2 , . . . , yn
which gives by monotonicity
x1 + x2 − y1 , x1 , . . . , xn ⊢ y1 , . . . , yn .

(‖)

On the other hand, because x1 + x2 = y1 + (x1 + x2 − y1 ), we have
x1 , x2 ⊢ y1 , x1 + x2 − y1
which gives by monotonicity
x1 , . . . , xn ⊢ y1 , . . . , yn , x1 + x2 − y1 .

(◦)

Cutting x1 + x2 − y1 in (‖) and ( ◦ ), we get the sought-after entailment.
When x1 +· · ·+xn 6G y1 +· · ·+yn , we have x1 +· · ·+xn =G y1 +· · ·+yn−1 +yn′
for some yn′ 6G yn . So yn′ ⊢ yn and x1 , . . . , xn ⊢ y1 , . . . , yn−1 , yn′ , and Lemma 3.2
yields again x1 , . . . , xn ⊢ y1 , . . . , yn . In particular, the following holds.
Corollary 3.4. Let ni be integers > 0 not all zero. If 0 6G n1 u1 +· · ·+np up , then
we have 0 ⊢ u1 , . . . , up . Similarly, if n1 u1 + · · · + np up 6G 0, then u1 , . . . , up ⊢ 0.
17

Proof. Assume e.g. that 0 6G 2u1 + 3u2 ; then
0 + 0 + 0 + 0 + 0 6G u1 + u1 + u2 + u2 + u2 .
Proposition 3.3 gives 0, 0, 0, 0, 0 ⊢ u1 , u1 , u2 , u2 , u2 . By contraction and monotonicity 0 ⊢ u1 , u2 , . . . , up holds.
The following scholion states the ℓ-group equality and inequality behind the
entailments of Lemma 3.6.
⋁⋀
Scholion 3.5. In an ℓ-group (H, 6H ), the equality i j (xj − xi ) =H 0 and the
⋀ ⋁
⋁
inequality i j (yi + xi − xj ) 6H j yj hold.
⋁
⋀
Proof. The equality follows from (−xi ) = − xi . For the inequality, note that
⋁
⋀
⋁
because yi 6H j yj , we have yi + xi 6L j yj + xi and therefore i (yi + xi ) 6H
⋁
⋀
j yj +
i xi .
Lemma 3.6. Let ⊢ be a regular system of ideals for an ordered group G, x1 ,
. . . , xn , ∈ G, and σ a map ⟦1..n⟧ → ⟦1..n⟧. Then
0 ⊢ xσ1 − x1 , . . . , xσn − xn .
Let y1 , . . . , yn , ∈ G. Then
y1 + x1 − xσ1 , . . . , yn + xn − xσn ⊢ y1 , . . . , yn .
Proof. Consider the sequence deﬁned by λ1 = 1 and λk+1 = σλk . Then this
sequence “contains a cycle”: there are i 6 j such that λi = λj+1 . Therefore
(xλi − xσλi ) + · · · + (xλj − xσλj ) =G 0
because it is a telescopic sum and
(yλi + xλi − xσλi ) + · · · + (yλj + xλj − xσλj ) =G yλi + · · · + yλj .
By Corollary 3.4 and Proposition 3.3, we get respectively
0 ⊢ xσλi − xλi , . . . , xσλj − xλj
yλi , . . . , yλj ⊢ yλi + xλi − xσλi , . . . , yλj + xλj − xσλj .
The conclusion follows by monotonicity.
Comment 3.7. Lorenzen (1953) proceeds in the following way for the proof of his
Satz 1: he starts by proving the key facts that (for a noncommutative group, in
multiplicative notation)
if c, c1 , . . . , cn ⊢ 1, then xcx−1 , c1 , . . . , cn ⊢ 1
−1
−1
−1
c1 c−1
2 , c2 c3 , . . . , cn−1 cn , cn c1 ⊢ 1

18

(the second of which corresponds to Corollary 3.4) and deduces from these Property R2 only as the basic ingredient for proving that the distributive lattice generated by ⊢ is regular. The main use of these facts is for establishing an inequality
akin to Lemma 3.6 as a tool for endowing the distributive lattice with a compatible
group operation as in our Theorem IV.
⋄
The following scholion explains why Theorem 3.9 below is decisive.
Scholion 3.8. In an ℓ-group (H, 6H ), the inequality x1 ∧ · · · ∧ xn 6H y1 ∨ · · · ∨ ym
is equivalent to
⋀
(xi − yj ) 6H 0.
i∈⟦1..n⟧,j∈⟦1..m⟧

Proof. The inequality x1 ∧ · · · ∧ xn 6H y1 ∨ · · · ∨ ym is equivalent to
(x1 ∧ · · · ∧ xn ) − (y1 ∨ · · · ∨ ym ) 6H 0
and also, by distributivity, to the stated inequality.
Theorem 3.9. Let ⊢ be a regular system of ideals. We have
x1 , . . . , xn ⊢ y1 , . . . , ym

(♭)

0 ⊢ (yj − xi )i∈⟦1..n⟧,j∈⟦1..m⟧

(♮)

(xi − yj )i∈⟦1..n⟧,j∈⟦1..m⟧ ⊢ 0.

(♯)

if and only if
if and only if
Proof. (♭) =⇒ (♮). The hypothesis gives by equivariance for each k ∈ ⟦1..n⟧
x1 − xk , . . . , xn − xk ⊢ y1 − xk , . . . , ym − xk ,
By Theorem 3.1 we may compute in the distributive lattice L generated by ⊢: we
have successively
(x1 − xk ) ∧ · · · ∧ (xn − xk ) 6L (y1 − xk ) ∨ · · · ∨ (ym − xk )
⋁
⋀
⋁
⋁
(xi − xk ) 6L
(yj − xk )
k∈⟦1..n⟧ i∈⟦1..n⟧

⋁

⋀

k∈⟦1..n⟧ j∈⟦1..m⟧

⋀

(xi − xk ) =L

⋁

(xσk − xk ).

σ : ⟦1..n⟧→⟦1..n⟧ k∈⟦1..n⟧

k∈⟦1..n⟧ i∈⟦1..n⟧

By Lemma 3.6, 0 ⊢ xσ1 − x1 , . . . , xσn − xn for all σ : ⟦1..n⟧ → ⟦1..n⟧. We have
therefore successively in L
⋁
0 6L
(xσk − xk )
k∈⟦1..n⟧

0 6L

⋀

⋁

σ : ⟦1..n⟧→⟦1..n⟧ k∈⟦1..n⟧

19

(xσk − xk ).

We obtain (♮) by transitivity and reﬂection of entailment.
(♮) =⇒ (♭). The hypothesis gives by equivariance for each k ∈ ⟦1..n⟧ that
xk ⊢ (yj − xi + xk )i∈⟦1..n⟧,j∈⟦1..m⟧ . By Theorem 3.1 we may compute in the
distributive lattice L: we have successively
⋁
xk 6L
(yj − xi + xk )
i∈⟦1..n⟧,j∈⟦1..m⟧

⋀
k∈⟦1..n⟧

xk 6L

⋀

⋁

(yj − xi + xk )

k∈⟦1..n⟧ i∈⟦1..n⟧,j∈⟦1..m⟧

=L

⋁

⋀

(yτk − xσk + xk )

σ : ⟦1..n⟧→⟦1..n⟧,τ : ⟦1..m⟧→⟦1..m⟧ k∈⟦1..n⟧

Lemma 3.6 yields yτ1 − xσ1 + x1 , . . . , yτn − xσn + xn ⊢ yτ1 , . . . , yτn . Using monotonicity, we have therefore successively in L
(yτ1 − xσ1 + x1 ) ∧ · · · ∧ (yτn − xσn + xn ) 6L y1 ∨ · · · ∨ ym
⋁
⋀
⋁
(yτk − xσk + xk ) 6L
yj .
σ : ⟦1..n⟧→⟦1..n⟧,τ : ⟦1..m⟧→⟦1..m⟧ k∈⟦1..n⟧

j∈⟦1..m⟧

We obtain (♮) by transitivity and reﬂection of entailment.
Finally (♭) ⇐⇒ (♮) shows that u1 , . . . , uℓ ⊢ 0 is equivalent to 0 ⊢ −u1 , . . . , −uℓ ,
and this yields (♮) ⇐⇒ (♯).
In particular, this theorem asserts that a regular system of ideals is determined
by its restriction to Pfe∗ (G) × G. However, given an unbounded single-conclusion
entailment relation ⊲, there are several unbounded entailment relations that reﬂect ⊲, and the coarsest one admits a simple description, given in Lorenzen (1952,
§ 3):
def
A ⊢v⊲ B ⇐⇒ ∀C ∈ Pfe (G) ∀z ∈ G
(※)
if C, b ⊲ z for all b in B, then C, A ⊲ z
(here Pfe(G) stands for the set of ﬁnitely enumerated subsets of the set G; see Scott
1974, Theorem 1.2, for a proof; ⊢v⊲ is ⊢max
in Rinaldi, Schuster, and Wessel 2017,
⊲
§ 3.1). This deﬁnition is “dual” to the deﬁnitional equivalence (§) on page 12 for
the coarsest single-conclusion entailment relation; the presence of the C in (※) is
needed for proving the transitivity of ⊢v⊲ . The following corollary tells us that if a
system of ideals ⊲ is regular, then the unique regular system of ideals extending it
coincides with the coarsest unbounded entailment relation ⊢v⊲ (see Lorenzen 1950,
page 509).
Corollary 3.10. Let G be an ordered group and ⊢ a regular system of ideals
for G. Let ⊲ be the system of ideals given as the restriction of the relation ⊢
to Pfe∗ (G)×G. Then ⊢ coincides with the coarsest unbounded entailment relation ⊢v⊲
that reflects ⊲, defined in (※).
20

Proof. It suﬃces to prove that ⊢v⊲ is a regular system of ideals, because then
Theorem 3.9 yields that it is determined by its restriction to Pfe∗ (G) × G.
R1. Suppose that a 6G b, so that a ⊲ b. If C, b ⊲ z, then C, a ⊲ z by
transitivity. Therefore a ⊢v⊲ b.
R2. As ⊢ is regular, we have x + a, y + b ⊢ x + b, y + a. As ⊢v⊲ is coarser than ⊢,
we have x + a, y + b ⊢v⊲ x + b, y + a.
R3. Just note that if C, b + x ⊲ z, then C − x, b ⊲ z − x, and that if C − x, A ⊲
z − x, then C, A + x ⊲ z.
Now we are also able to give the analogue of Proposition 2.3 for regular systems
of ideals.
Corollary 3.11 (a variant for the deﬁnition of a regular system of ideals). Let us
consider a predicate · ⊲ 0 on Pfe∗ (G) for an ordered group G and let us define a
binary relation on Pfe∗ (G) by
def

x1 , . . . , xn ⊢ y1 , . . . , ym ⇐⇒ (xi − yj )i∈⟦1..n⟧,j∈⟦1..m⟧ ⊲ 0

(¶)

( n, m > 1). In order for this relation to be a regular system of ideals, it is necessary
and sufficient that the following properties be fulfilled:
Pn
G1 if
(preservation of order);
i=1 xi 6G 0, then x1 , . . . , xn ⊲ 0
G2
G3

if A ⊲ 0, then A, A′ ⊲ 0
(monotonicity);
if B + C, B ⊲ 0 and B + C, C ⊲ 0, then B + C ⊲ 0 (transitivity).

Proof. Using the deﬁnitional equivalence (¶), Property G3 is a direct translation of
cutting 0 in B ⊢ 0, −C and B, 0 ⊢ −C. For the other properties, use Theorem 3.9
and Corollary 3.4. The details are left to the reader.

3.3

Forcing the positivity of an element in a system of ideals

The precise description of the system ⊲x obtained by forcing the property 0 ⊲ x
given in Proposition 3.12 below is the counterpart for single-conclusion entailment
relations of the cone generated by adding an element to a cone in an ordered
monoid (see Lorenzen 1950, page 518).
Proposition 3.12. Let ⊲ be a system of ideals for an ordered monoid G. Let us
denote by ⊲x the finest system of ideals coarser than ⊲ and satisfying the property x > 0. Then we have the equivalence
A ⊲x b

⇐⇒

there exists a p > 0 such that A, A + x, . . . , A + px ⊲ b.

Proof. Let us denote by A ⊲ ′ b the right-hand side in the equivalence above. In
⋀
⋀
any meet-monoid, x > 0 implies (A, A + x, . . . , A + px) = A, so that A ⊲ ′ b
e b for any system of ideals ⊲
e coarser than ⊲ and satisfying 0 ⊲
e x.
implies A ⊲
21

It remains to prove that A ⊲ ′ b deﬁnes a system of ideals for G (clearly 0 ⊲ ′ x
and ⊲ ′ is coarser than ⊲). Reﬂexivity, preservation of order, equivariance, and
monotonicity are straightforward. It remains to prove transitivity. Assume e.g.
that A ⊲ ′ z and A, z ⊲ ′ y. We have to show that A ⊲ ′ y. E.g. we have
A, A + x, A + 2x, A + 3x ⊲ z,

(#)

A, A + x, A + 2x, z, z + x, z + 2x ⊲ y.

(%)

(#) gives by a translation A + 2x, A + 3x, A + 4x, A + 5x ⊲ z + 2x, and by monotonicity
A, A + x, A + 2x, A + 3x, A + 4x, A + 5x, z, z + x ⊲ z + 2x.

(##)

(%) gives by monotonicity
A, A + x, A + 2x, A + 3x, A + 4x, A + 5x, z, z + x, z + 2x ⊲ y.

(%%)

By transitivity we get from (##) and (%%)
A, A + x, A + 2x, A + 3x, A + 4x, A + 5x, z, z + x ⊲ y.
So we have cancelled z + 2x out of the left-hand side of (%). Similar entailments
allow us to cancel out successively z + x and z.

3.4

The regularisation of a system of ideals for an ordered
group

Let us now state and prove two lemmas on regularisation, introduced in Deﬁnition 1.10. Lemma 3.13 corresponds to the ﬁrst part of the proof of Satz 1 in
Lorenzen (1953): see Remark 1.13.
Lemma 3.13. Let ⊲ be a system of ideals for an ordered group G. Its regularisation ⊢⊲ is a regular system of ideals for G.
Proof. The regularisation is clearly reﬂexive and monotone, and satisﬁes Properties R1 and R3.
Let us prove that the regularisation is transitive. Suppose that A, 0 ⊢⊲ B and
A ⊢⊲ 0, B with A = {a1 , . . . , am } and B = {b1 , . . . , bn }: there are x1 , . . . , xk , y1 ,
. . . , yℓ such that for every choice of signs ± holds
A − B, −B ⊲±x1 ,...,±xk 0

and A, A − B ⊲±y1 ,...,±yℓ 0.

If ai ⊲ 0 for some i, then A 6⊲ A, 0 and A − B 6⊲ A − B, −B. Therefore
A − B 6⊲−ai ,±x1 ,...,±xk A − B, −B 6⊲−ai ,±x1 ,...,±xk 0
22

for i = 1, . . . , m.

If 0 ⊲ bj for some j, then −bj ⊲ 0 and −B 6⊲ 0, −B and A − B 6⊲ A, A − B.
Therefore
A − B 6⊲bj ,±y1 ,...,±yℓ A, A − B 6⊲bj ,±y1 ,...,±yℓ 0 for j = 1, . . . , n.
If 0 ⊲ a1 , . . . , 0 ⊲ am , then we have 0 6⊲ A, 0 and −B 6⊲ A − B, −B. Therefore
−B 6⊲a1 ,...,am ,±x1 ,...,±xk 0.
If b1 ⊲ 0, . . . , bn ⊲ 0, then 0 ⊲ −b1 , . . . , 0 ⊲ −bn , and we have 0 6⊲ 0, −B and
A 6⊲ A, A − B. Therefore successively
A 6⊲−b1 ,...,−bn ,±y1 ,...,±yℓ 0,
A − B 6⊲−b1 ,...,−bn ,±y1 ,...,±yℓ −B,
and A − B 6⊲a1 ,...,am ,−b1 ,...,−bn ,±x1 ,...,±xk ,±y1 ,...,±yℓ 0.
We conclude that
A − B ⊲±a1 ,...,±am ,±b1 ,...,±bn ,±x1 ,...,±xk ,±y1 ,...,±yℓ 0.
Let us prove that the regularisation is regular, i.e. that x+ a, y + b ⊢⊲ x+ b, y + a
holds for all a, b, x, y ∈ G: it suﬃces to note that
if a − b ⊲ 0, then a − b, x − y, y − x, b − a ⊲ 0;
if b − a ⊲ 0, then a − b, x − y, y − x, b − a ⊲ 0.
The following lemma justiﬁes the terminology of Deﬁnition 1.10. With the
ambiguity introduced by the two items of Deﬁnition 1.8, one may formulate it as
follows: “regularisation leaves a regular system of ideals unchanged”.
Lemma 3.14. Let G be an ordered group and ⊢ a regular system of ideals for G.
Let ⊲⊢ be the system of ideals given as the restriction of ⊢ to Pfe∗ (G)×G. Then ⊢ coincides with the regularisation of ⊲⊢ .
Proof. Let p, q > 0 be integers. It suﬃces to prove that if A, A + x, . . . , A + px ⊲⊢
0 and A, A − x, . . . , A − qx ⊲⊢ 0, then A ⊲⊢ 0. By Theorem 3.9, the hypotheses
are
A ⊢ 0, −x, . . . , −px and A ⊢ 0, x, . . . , qx.
If p = 0 or q = 0, we are done. Otherwise, since q × (−p) + p × q = 0, Corollary 3.4
gives −px, qx ⊢ 0. Cutting −px yields A, qx ⊢ 0, −x, . . . , −(p − 1)x; cutting qx
yields
A ⊢ −(p − 1)x, . . . , −x, 0, x, . . . , (q − 1)x.
If p = 1, we may iterate this and obtain that A ⊢ 0. Otherwise, ﬁrst acknowledge that A′ ⊢ 0, −x and A′ ⊢ 0, x, . . . , (q − 1)x imply A′ ⊢ 0; with A′ equal to
A, A + x, . . . , A + (p − 1)x these hypotheses turn out to be
A ⊢ 0, −x, . . . , −px and A ⊢ −(p − 1)x, . . . , −x, 0, x, . . . , (q − 1)x,
and do therefore hold. We may iterate this and obtain that A ⊢ 0.
23

3.5

Proof of Theorem II

Proof of Theorem II. Lemma 3.13 tells that ⊢⊲ is a regular system of ideals, and it
is clear from the deﬁnition that its restriction to Pfe∗ (G) × G is coarser than ⊲. Now
let ⊢ be a regular system of ideals whose restriction ⊲⊢ to Pfe∗ (G) × G is coarser
than ⊲. Then the same holds for their regularisation, i.e., by Lemma 3.14, ⊢ is
coarser than ⊢⊲ .

3.6

The finest regular system of ideals

We shall now give a precise description of the regularisation ⊢⊲s of the ﬁnest system
of ideals, introduced in Proposition 2.4.
Lemma 3.15. Let G be an ordered group. For u1 , . . . , uk ∈ G, t.f.a.e.
1. u1 , . . . , uk ⊢⊲s 0.
2. There exist integers ni > 0 not all zero such that we have
n1 u1 + · · · + nk uk 6G 0.
Proof. Let us denote Item (2 ) by ̺(u1 , . . . , uk ).
(1) =⇒ (2). First it is clear that u1 , . . . , uk ⊲s 0 implies that ̺(u1 , . . . , uk )
holds. Thus it is enough to prove that if one supposes that for some x ∈ G and
some integers p and q,
̺(u1 , . . . , uk , u1 + x, . . . , uk + x, . . . , u1 + px, . . . , uk + px) and
̺(u1 , . . . , uk , u1 − x, . . . , uk − x, . . . , u1 − qx, . . . , uk − qx),
then ̺(u1 , . . . , uk ). The hypothesis implies that there are integers ni , n > 0, at least
one ni nonzero, such that n1 u1 + · · · + nk uk + nx 6G 0, and integers mj , m > 0,
at least one mj nonzero, such that m1 u1 + · · · + mk uk − mx 6G 0. If n = 0 or if
m = 0, then we are done; otherwise, (mn1 + nm1 )u1 + · · · + (mnk + nmk )uk 6G 0
with at least one mni + nmi > 0.
(2) =⇒ (1). Consequence of Lemma 3.13 and Corollary 3.4.
Theorem 3.16. Let (G, 6G ) be an ordered group.
1. The finest regular system of ideals for G is the regularisation ⊢⊲s of the
finest system of ideals ⊲s .
2. The group G is ⊲s -closed if and only if
nx >G 0 implies x >G 0

( x ∈ G, n > 1).

(‡)

Proof. Theorem 3.9 shows that a regular system of ideals for G is determined by
the unbounded single-conclusion entailment relation that it deﬁnes by restriction
to Pfe∗ (G) × G. Thus every regular system of ideals for G is coarser than ⊢⊲s by
Lemma 3.15 and Corollary 3.4.
24

Comment 3.17. The reader will recognise Condition (‡) of Corollary 1.14 in the
condition of ⊲s -closedness established here. In his proof of Corollary 1.14, Lorenzen is following the Prüfer approach of Section 6, in which ⊲s -closedness is being
introduced according to Deﬁnition 6.5 and the equivalence with Condition (‡) is
easy to check (see Lorenzen 1939, page 358 or Jaﬀard 1960, I, § 4, Théorème 2). ⋄

3.7

The regularisation of the Dedekind system of ideals

Let R be an integral domain, K its ﬁeld of fractions and G = K × /R× its divisibility
group (where, in multiplicative notation, 1 6G x when x ∈ R). One deﬁnes the
Dedekind system of ideals ⊲d for G by letting
def

A ⊲d b ⇐⇒ b ∈ hAiR ,
where hAiR is the (fractional) ideal generated by A over R in K: if a1 , . . . , an are
the elements of A, then hAiR = a1 R+· · ·+an R. Note that if A contains nonintegral
2
elements, i.e. elements not in R, then hAiR may or may not be contained in hAiR :
y
consider respectively e.g. the ideal h1, x i in k[X, Y ]/(X 3 − Y 2 ) = k[x, y] and ideals
in a Prüfer domain.
Forcing 1 ⊲d x for an x ∈ K × amounts to replacing R by R[x] since Proposition 3.12 tells that the resulting system of ideals satisﬁes
A (⊲d )x b

⇐⇒

there is a p > 0 such that A, Ax, . . . , Axp ⊲d b,

which means that b ∈ hAiR[x] (where A and b are in K × ).
An element b ∈ K is said to be integral over the ideal hAiR when an integral
Pm
k
dependence relation bm = k=1 ck bm−k with ck ∈ hAiR holds. If A = {1}, then
this reduces to the same integral dependence relation with ck ∈ R, i.e. to b being
integral over R.
Lemma 3.18. One has A ⊢⊲d 1 if and only if 1 ∈ hAiR[A] .
Proof. Suppose that A ⊢⊲d 1, i.e. that there are elements x1 , . . . , xℓ ∈ G such
that 1 ∈ hAiR[x±1 ,...,x±1 ] . It suﬃces to prove the following fact and to use it in
1
ℓ
an induction argument: suppose that 1 ∈ hAiR[A,x] and 1 ∈ hAiR[A,x−1 ] ; then
1 ∈ hAiR[A] . In fact, the hypothesis means that 1 ∈ hA, Ax, . . . , Axp iR[A] and
1 ∈ hA, Ax−1 , . . . , Ax−p iR[A] for some p, which implies that
∀i ∈ ⟦−p..p⟧ xi ∈ Ax−p , . . . , Ax−1 , A, Ax, . . . , Axp

R[A]

,

i.e. that there is a matrix M with coeﬃcients in hAiR[A] such that (xi )p−p =
M (xi )p−p , i.e. (1 − M )(xi )p−p = 0. Let us now apply the determinant trick: multiplying 1 − M by the matrix of its cofactors and expanding yields that 1 ∈ hAiR[A] .
25

Conversely, let a1 , . . . , an be the elements of A. For each j, 1 = aj a−1
j , so
that 1 ∈ hAiR[a−1 ] and A (⊲d )a±1 ,...,a±1
1
for
every
choice
of
signs
with
at
least
n
1
j
one negative sign: the only missing choice of signs consists in the hypothesis 1 ∈
hAiR[A] .
Theorem 3.19 (Lorenzen 1953, Satz 2). Let R be an integral domain and ⊲d the
Dedekind system of ideals.
1. One has A ⊢⊲d b, i.e. there are x1 , . . . , xℓ such that for every choice of signs
holds b ∈ hAiR[x±1 ,...,x±1 ] , if and only if b is integral over the ideal hAiR .
1
ℓ
2. One has A ⊢⊲d B, i.e. there are x1 , . . . , xℓ such that for every choice of
P
k
−1
signs holds 1 ∈ hAB −1 iR[x±1 ,...,x±1 ] , if and only if 1 ∈ m
iR , i.e. there
k=1 hAB
1
ℓ
Pm
is an equality 1 = k=1 fk with each fk a homogeneous polynomial of degree k in
the elements of AB −1 with coefficients in R.
3. The divisibility group G is ⊲d -closed, i.e. the equivalence
x ⊢⊲d y

⇐⇒

x divides y

holds, if and only if R is integrally closed.
Proof.

(1 –2 ) This follows from the previous lemma because

bm =

Pm

k=1 ck b

m−k

A ⊢ ⊲d b

⇐⇒

k

⇐⇒

1 ∈ hAiR[A]

⇐⇒

with ck ∈ hAiR

Ab−1 ⊢⊲d 1,
Pm
k
1 ∈ k=1 hAb−1 iR ,
Pm
k
∃m 1 ∈ k=1 hAiR .

(3 ) ⊲d -closedness is equivalent to 1 ⊢⊲d b =⇒ b ∈ R; by Item (1 ), 1 ⊢⊲d b
holds if and only if b is integral over R.

4
4.1

The lattice-ordered group freely generated by a
finitely presented ordered group
A Positivstellensatz for ordered groups

Reference: Coste, Lombardi, and Roy 2001, Section 5. In the article we refer to,
Theorem 5.7 can be seen as a generalisation of results concerning rational linear
programming (e.g. the Farkas lemma).
If G is a commutative group and x1 , . . . , xm are indeterminates, let G{x} =
G{x1 , . . . , xm } be the group of Z-aﬃne forms on G, i.e. of polynomials g + z1 x1 +
· · · + zm xm with g in G and z1 , . . . , zm in Z. We may consider G as the subgroup
of G{x} consisting of the constant forms.
26

Theorem 4.1 (Positivstellensatz: algebraic certiﬁcates for ordered groups, see
Coste, Lombardi, and Roy 2001). Let (G, · + ·, −·, 0, · = 0, · > 0, · > 0) be a discrete divisible linearly ordered group. Let x1 , . . . , xm be indeterminates and R=0 ,
R>0 , R>0 three finitely enumerated subsets of G{x1 , . . . , xm }. Consider the associated system S of sign conditions


z(ξ) = 0 if z ∈ R=0 ,
S
p(ξ) > 0 if p ∈ R>0 ,


s(ξ) > 0 if s ∈ R>0 .

There is an algorithm giving the following answer:
1. either an algebraic certificate telling that the system S is impossible in G
(and in every linearly ordered group extending G),
2. or a point ξ = (ξ1 , . . . , ξm ) ∈ Gm realising the system S.
An algebraic certiﬁcate is an algebraic identity
s + p + z = 0 in G{x1 , . . . , xm },

where s is a (nonempty) sum of elements of R>0 ∪G>0 , p is a (possibly empty) sum
of elements of R>0 ∪ G>0 , and z is a Z-linear combination of elements of R=0 .

4.2

A concrete construction

A ﬁnitely presented ordered group G is given by a ﬁnite system of generators
e1 , . . . , em with a ﬁnite set of relations R = R=0 ∪ R>0 . The relations in R=0 have
the form z = 0, and those in R>0 have the form p > 0, where z, p ∈ Ze1 ⊕ · · ·⊕ Zem .
Since a relation q = 0 is equivalent to the two relations q > 0 and −q > 0, we
may assume that the presentation of G as an ordered group is given by a ﬁnite
subset R>0 = {p1 , . . . , pℓ } only. Let us work with this new presentation.
Let LGOG(G) be the ℓ-group freely generated by the ordered group G. We shall
give a description of an ℓ-group Lgog(G), and prove that it is naturally isomorphic
to LGOG(G).
Let Z′ be the group Z with the usual linear order, and let Lo(G, Z′ ) be the
set of order morphisms from G to Z′ that are linear for the Z-module structure
of G. This is an additive monoid whose natural order relation is compatible with
addition.
We deﬁne Lgog(G) as the sub-ℓ-group of
Set(Lo(G, Z′ ), Z′ )
generated by the join-semilattice-ordered monoid (G), where  is the bidual morphism of ordered groups G → (G) ⊆ Lgog(G) ⊆ Set(Lo(G, Z′ ), Z′ ):
(z) is the map α 7→ α(z).
27

This Z-linear map is a morphism of ordered groups since, if z > 0 in G and
α ∈ Lo(G, Z′ ), then one has α(z) > 0 in Z′ . Let us denote the element (z) viewed
in Lgog(G) by z.
We shall use the following principle (Lombardi and Quitté 2015, Principle XI2.10).
Principle of covering by quotients (for ℓ-groups). In order to prove an equality
u = v or an inequality u 6 v in an ℓ-group H, we can always suppose that the (finite
number of) elements which occur in a computation for a proof are comparable.
In fact, we shall need the following easy consequence of this principle.
Pk
Lemma 4.2. In an ℓ-group H, if
i=1 ui > 0 holds (with an integer k > 0), then
⋁k
one has i=1 ui > 0.
Let us now consider the canonical morphism ı : G → LGOG(G) and the unique
(surjective) morphism ϑ : LGOG(G) → Lgog(G) factorising  (i.e. such that ϑ ◦ ı =
). In order to show that ϑ is an isomorphism, it suﬃces to show that ϑ(y) > 0
implies y > 0 for all y ∈ LGOG(G).
⋀
⋀ ⋁
Let us write the element y ∈ LGOG(G) as y =
yj = j i ı(yji ) with
⋀ ⋁
the yji s in G. The hypothesis is that j i yji > 0, i.e. that for each j one has
⋁
⋀
ϑ(yj ) = i yji > 0. In order to show that
y > 0, it is thus suﬃcient to show
⋁
⋁ j
that if ui > 0 with P
u1 , . . . , uk in G, then ı(ui ) > 0 inPLGOG(G).
m
Let us write ui = m
µ=1 uiµ eµ , i = 1, . . . , k, and pj =
µ=1 pjµ eµ , j = 1, . . . , ℓ,
and introduce indeterminates x1 , . . . , xm and linear forms
Pm
Pm
λi (x1 , . . . , xm ) = µ=1 uiµ xµ and ρj (x1 , . . . , xm ) = µ=1 pjµ xµ .

Let us consider the following system of sign conditions w.r.t. the indeterminates x1 , . . . , xm for the divisible linearly ordered group (Q, 6Q ):
(
λi (x1 , . . . , xm ) < 0 for i = 1, . . . , k;
S
ρj (x1 , . . . , xm ) > 0 for j = 1, . . . , ℓ.

Theorem 4.1 says that we are in one of the two following cases.
P
1. The system S is incompatible: this implies an algebraic identity ni λi = P
for integers ni > 0 not all zero and P in the additive monoid generated by the ρj s.
When one substitutes the xµ s with the eµ s, one gets P (eP
1 , . . . , em ) > 0 in G
because
each
ρ
(e
,
.
.
.
,
e
)
=
p
is
>
0
in
G,
and
therefore
ni ui > 0 in G and
j
1
m
j
P
P
ni ı(ui ) > 0 in LGOG(G), and
ni ui > 0 in Lgog(G). Lemma 4.2 implies that
⋁
⋁
we have ı(ui ) > 0 as well as ui > 0.
2. One can ﬁnd (ξ1 , . . . , ξm ) ∈ Qm such that the λi (ξ)s are all < 0 and the
ρj (ξ)s are all > 0. Multiplying by a convenient positive rational number, we
may assume that (ξ1 , . . . , ξm ) ∈ Zm . Let α : G → Z′ be the linear form such that
28

eµ 7→ ξµ : as α(pj ) = ρj (ξ) > 0 for j = 1, . . . , ℓ, we have that α belongs to Lo(G, Z′ );
⋁
let us note that ui (α) = α(ui ) = λi (ξ). We deduce that v = ui is not > 0, as
v > 0 implies that for all β ∈ Lo(G, Z′ ), one has v(β) > 0; however α ∈ Lo(G, Z′ )
⋁
⋁
and v(α) = ui (α) = λi (ξ) < 0.
⋁
⋁
In brief, we have proved that
ui
0 and
ı(ui ) > 0 are exclusive of each
other. The case distinction above shows more precisely the following theorem.
Theorem 4.3. Let G be a finitely presented ordered group.
1. The canonical morphism LGOG(G) → Lgog(G) is an isomorphism.
2. Let u1 , . . . , uk be elements of the ℓ-group LGOG(G). T.f.a.e.:
⋁
•
ı(ui ) > 0;
P
• there exist integers ni > 0 not all zero such that
ni ui > 0 in G.
In particular, an element x of G is > 0 in LGOG(G) if and only if one has nx > 0
in G for some integer n > 0.
3. The group LGOG(G) is discrete (the order is decidable).

4.3

Proof of Theorem III

Constructive proof of Theorem III. This theorem follows from the preceding Theorem 4.3, from the fact that every ordered group is a ﬁltered colimit of ﬁnitely
presented ordered groups, and from the fact that the functor LGOG preserves
ﬁltered colimits.

5

The lattice-ordered group generated by a regular system of ideals

Comment 5.1. Lorenzen (1953, § 2) starts with a system of ideals ⊲ for an ordered
group and uses the heuristics of Scholion 3.8 to deﬁne the regular system of
ideals ⊢⊲ of Deﬁnition 1.10. Then he applies the fundamental theorem for unbounded entailment relations, Theorem 3.1, and obtains a distributive lattice Vra
(“V ” like “Verband”, lattice). Theorem IV is new and replaces the second step
of the proof of Satz 1 in Lorenzen (1953), which establishes that Vra is in fact an
ℓ-group. Its ﬁrst step is the proof of Lemma 3.13, in which the entailment relation ⊢⊲ is constructed and shown to be regular (see Remark 1.13). Its second step
is a construction “by hand” of group laws for Vra in which the rôle of regularity is
not emphasised.
⋄

5.1

The free case

Theorem 5.2. Let (G, 6G ) be an ordered group. Let Gs be the unbounded distributive lattice generated by the finest regular system of ideals ⊢⊲s . Then Gs admits a (unique) group law that is compatible with the lattice structure and such
29

that the morphism (of ordered sets) G → Gs is a group morphism. This defines
the ℓ-group freely generated by the ordered group (G, 6G ) (in the sense of the left
adjoint functor of the forgetful functor).
Proof. Using the distributivity of + over ∧ and ∨, there is no choice in deﬁning
the group laws + and − from those of G. The problem is to show that these laws
are well-deﬁned and are in fact group laws.
Let us consider the ℓ-group LGOG(G) freely generated by G. It is generated as
an unbounded distributive lattice by (the image of) G because any term constructed
from G, +, −, ∧, ∨ can be rewritten as an ∧-∨-combination of elements of G. Let
us denote by ⊢free the entailment relation thus deﬁned for G. We know that
u1 , . . . , uk ⊢free 0 is equivalent to u1 , . . . , uk ⊢⊲s 0: this follows from Theorem III
and Lemma 3.15. Moreover LGOG(G) satisﬁes the equivalent properties given
in Theorem 3.9 simply because it is an ℓ-group. If we see it as an unbounded
distributive lattice generated by G, LGOG(G) is thus the distributive lattice which
is deﬁned by the unbounded entailment relation ⊢⊲s . Therefore the laws + and −
on Gs are well-deﬁned and Gs , endowed with these laws, becomes an ℓ-group for
which we have a canonical isomorphism LGOG(G) → Gs .

5.2

The general case: proof of Theorem IV

Proof of Theorem IV. Let Gs denote the ℓ-group freely generated by (G, 6G ) constructed in Theorem 5.2 via the entailment relation ⊢⊲s . The relation ⊢ is coarser
than the relation ⊢⊲s , so that the distributive lattice H is a quotient lattice of Gs .
It remains to see that the group law descends to the quotient.
Let G0 = { x ∈ Gs | x =H 0 }. We have to show that
(i) G0 is a subgroup of Gs ;
(ii) for x, y, z ∈ Gs with x =H y holds x + z =H y + z.
It is enough to show that
1. for x ∈ Gs , if 0 6H x, then −x 6H 0;
2. for x, y ∈ Gs , if 0 6H x and 0 6H y, then 0 6H x + y;
3. for x, y, z ∈ Gs , if x 6H y, then x + z 6H y + z.
Item (1 ) is a particular case of Item (3 ) and Item (2 ) follows easily from
Item (3 ).
⋁⋀
⋀ ⋁
(3 ) Let us write x = i j xij , y = k ℓ ykℓ with the xij s and the ykℓ s in G.
⋁
⋀
The hypothesis x 6H y means that for each i and k we have j xij 6H ℓ ykℓ , i.e.
xi1 , . . . , xip ⊢ yk1 , . . . , ykq .
Using R3 one has
xi1 + z, . . . , xip + z ⊢ yk1 + z, . . . , ykq + z,
30

i.e. for each (i, k),
j (xij

⋀

+ z) 6H

ℓ (ykℓ

⋁

+ z),

from which we deduce that
⋁⋀
⋀⋁
x + z =H
(xij + z) 6H
(ykℓ + z) = y + z.
i

5.3

j

k

ℓ

The Lorenzen divisor group of an integral domain

In this section, we draw the conclusions allowed by Theorem IV for Lorenzen’s
theory of divisibility presented in Section 3.7 on page 25.
Definition 5.3. Let R be an integral domain. The Lorenzen divisor group Lor(R)
of R is the Lorenzen group associated by Deﬁnition 1.16 to the Dedekind system
of ideals ⊲d .
Theorem 5.4. Let R be an integral domain with field of fractions K and divisibility
group G = K × /R× . The entailment relation ⊢⊲d generates the Lorenzen divisor
group Lor(R) together with a morphism of ordered groups ϕ : G → Lor(R) that
satisfies the following properties.
1. The “ideal Lorenzen gcd” of a family (ai )i∈⟦1..n⟧ in K ∗ is characterised by
ϕ(a1 ) ∧ · · · ∧ ϕ(an ) 6 ϕ(b)

⇐⇒
b is integral over the ideal ha1 , . . . , an iR .

(∗∗)

2. The morphism ϕ is an embedding if and only if R is integrally closed.
Proof. As the entailment relation ⊢⊲d is a regular system of ideals (Theorem II),
the corresponding distributive lattice H admits a unique group law such that the
natural morphism ϕ : G → H is a morphism of ordered groups (by Theorem IV):
this justiﬁes Deﬁnition 5.3 since H is the distributive lattice underlying Lor(R).
1. Theorem 3.19 states that ϕ(a1 ) ∧ · · · ∧ ϕ(an ) 6⊢⊲d ϕ(b) if and only if b is
integral over hAiR . On the other hand ϕ(a1 ) ∧ · · · ∧ ϕ(an ) 6⊢⊲d ϕ(b1 ) ∧ · · · ∧ ϕ(bp )
if and only if ϕ(a1 ) ∧ · · · ∧ ϕ(an ) 6⊢⊲d ϕ(bj ) for each j because ϕ(b1 ) ∧ · · · ∧ ϕ(bp ) is
the meet of the bj s in Lor(R). This explains why Property (∗∗) characterises the
element ϕ(a1 ) ∧ · · · ∧ ϕ(an ) of Lor(R).
2. The morphism ϕ is an embedding if and only if ϕ(a) 6⊢⊲d ϕ(b) implies
a ⊲d b, which means that R is integrally closed.
Corollary 5.5 (see Macaulay 1916, pages 108–109). Let R be an integrally closed
domain. When a is a finitely generated ideal, we let a be the integral closure of a.
Then, if a, b, and c are nonzero finitely generated ideals, we have the cancellation
property
a b ⊇ a c =⇒ b ⊇ c.
31

This corollary is a key result for “containment in the wider sense” as considered
by Leopold Kronecker (1883) (see Penchèvre (preprint), pages 36–37). H. S. Macaulay (1916) gives a proof based on the multivariate resultant. We may also
deduce it as a consequence of Prüfer’s theorem 6.7 (see Item (2 ) of Remarks 6.11,
compare Prüfer 1932, § 6, Krull 1935, 46.).
In Items (2 ), (4 ), and (6 ) below, we use the conventional additive notation for
divisor groups of an integral domain.
Corollary 5.6. Let R be an integral domain. The Lorenzen divisor group Lor(R)
can be realised set-theoretically in the following way.
1. Basic nonnegative divisors are realised as integral closures Icl(a1 . . . , an ) of
(ordinary, i.e. integral) finitely generated ideals ha1 . . . , an iR with a1 , . . . , an ∈ R.
Note that if R is not integrally closed, Icl(a1 , . . . , an ) may contain elements not in
R.
2. The neutral element of the group, i.e. the divisor 0, is realised as Icl(1).
3. The meet of two basic nonnegative divisors is realised as
Icl(a1 , . . . , an ) ∧ Icl(b1 , . . . , bm ) = Icl(a1 , . . . , an , b1 , . . . , bm ).
4. The sum of two basic nonnegative divisors is realised as
Icl(a1 , . . . , an ) + Icl(b1 , . . . , bm ) = Icl(a1 b1 , . . . . . . , an bm ).
5. The order relation between basic nonnegative divisors is realised as
Icl(a1 , . . . , an ) 6 Icl(b1 , . . . , bm )

⇐⇒

Icl(a1 , . . . , an ) ⊇ Icl(b1 , . . . , bm ).

In particular, Icl(a) 6 Icl(b) holds if and only if b is integral over hai.
6. General divisors are realised as formal differences of two basic nonnegative
divisors.
Proof. Item (1 ) is a rephrasing of Item (1 ) in Theorem 5.4. Items (2 ) to (5 ) are
clear. Let us consider Item (6 ). Lor(R) is generated by ϕ(G) as an ℓ-group. An
element of ϕ(G) is written as ϕ(a) − ϕ(b) with a, b ∈ R∗ . It remains to verify
that diﬀerences of basic nonnegative divisors are stable by the laws ∧, +, and −
of an ℓ-group. Only the ∧-stability requires a little trick: in order to compute
δ = (ϕ(A) − ϕ(B)) ∧ (ϕ(C) − ϕ(D)), it is suﬃcient to compute δ + ϕ(B) + ϕ(D),
which is equal to (ϕ(A) + ϕ(D)) ∧ (ϕ(C) + ϕ(B)), which can be computed using
the previous items.
Remarks 5.7.
1. When R is a Prüfer domain, the Lorenzen divisor group Lor(R)
coincides with the usual divisor group, the group of ﬁnitely generated fractional
ideals deﬁned by Dedekind and Kronecker. In fact, the relation ⊢⊲d is determined by its trace on Pfe∗ (R∗ ) × R∗ , and in a Prüfer domain all ﬁnitely generated
ideals are integrally closed, so that A ⊢⊲d b simpliﬁes to b ∈ hAiR (see Item (1 ) of
Theorem 3.19). For more general rings with divisors, the Weil divisor group (see
Item (2 ) of Remarks 2.11) is a strict quotient of the Lorenzen divisor group.
32

2. The integral domain R = Q[x, y] is a gcd domain of dimension > 2, so that
its divisibility group G is an ℓ-group. The domain R is not Prüfer and the Lorenzen
divisor group is much greater than G: e.g. the ideal gcd of x3 and y 3 in Lor(R)
corresponds to the integrally closed ideal hx3 , x2 y, xy 2 , y 3 i, whereas their gcd in
R∗ is 1, corresponding to the ideal h1i. In this case, we see that G is a proper
quotient of Lor(R).
⋄

6

Systems of ideals and Prüfer’s theorem

In this section, we account for another way to obtain the Lorenzen group associated
to a system of ideals for an ordered group (Deﬁnition 1.16). This way has historical
precedence, as it dates back to Lorenzen’s Ph.D. thesis (1939), that builds on
earlier work by Prüfer (1932). As a particular case this provides another access to
understanding the Lorenzen divisor group of an integral domain.

6.1

The Grothendieck ℓ-group of a meet-semilattice-ordered
monoid

The following easy construction, for which we did not locate a good reference, is
particularly signiﬁcant in the case where the meet-monoid associated to a system
of ideals proves to be cancellative.
Theorem 6.1. Let (M, +, 0, ∧) be a meet-monoid. Let H be the Grothendieck
group of M with monoid morphism ϕ : M → H.
1. There exists a unique meet-monoid structure on H such that ϕ is a morphism of ordered sets.
2. (H, +, −, 0, ∧) is an ℓ-group: it is the ℓ-group generated by (M, +, 0, ∧) in
the usual meaning of adjoint functors, and called the Grothendieck ℓ-group of M .
3. Assume that M is cancellative, i.e. that x+ y = x+ z implies y = z. Then ϕ
is an embedding of meet-monoids.
Proof.
(1 ) The elements of H are written as a−b for a, b ∈ M , with the equality
a − b = c − d holding if and only if there exists x such that a + d + x = b + c + x.
By transitivity and symmetry, every equality a − b = c − d may be reduced to two
“elementary” ones, i.e. of the form e − f = (e + y) − (f + y):
a − b = (a + d + x) − (b + d + x) = (b + c + x) − (b + d + x) = c − d.
When trying to deﬁne z = (e − f ) ∧ (g − h) we need to ensure that
f + h + z = (e + h) ∧ (g + f ).
def

So we may propose to set (e − f ) ∧ (g − h) = ((e + h) ∧ (g + f )) − (f + h).
33

Let us show ﬁrst that the law ∧ is well-deﬁned on H.
It suﬃces to show that (e − f ) ∧ (g − h) = ((e + y) − (f + y)) ∧ (g − h), which
reduces successively to
((e + h) ∧ (g + f )) − (f + h) = ((e + h + y) ∧ (g + f + y)) − (f + h + y)
and to
((e + h) ∧ (g + f )) + (f + h + y) = ((e + h + y) ∧ (g + f + y)) + (f + h).
Since ∧ is compatible with + in M , both sides are equal to
(e + 2h + f + y) ∧ (g + 2f + h + y).
def

• The map ϕ : M → H preserves ∧: in fact ϕ(a) = a − 0, and the checking is
immediate.
• The law ∧ on H is idempotent, commutative, and associative. This is easy
to check and left to the reader.
• The law ∧ is compatible with + on H. This is easy to check and left to the
reader.
(2 ) Left to the reader.
(3 ) The meet-monoid structure is purely equational. So an injective morphism
is always an embedding.
As an application of this construction, let us state a variant of Theorem IV.
Corollary 6.2 (to Theorem IV). Let (G, 6G ) be an ordered group and ⊲ a system
of ideals for G. The following are equivalent:
1. The system of ideals ⊲ is regular, i.e. it is the restriction of a regular system
of ideals ⊢.
2. The meet-monoid associated to the system of ideals ⊲ for G (Theorem I) is
cancellative.
When this is the case, let (H, 6H ) be the unbounded distributive lattice generated by
the regular system of ideals ⊢. Then the group law and the group morphism ϕ : G →
H constructed by Theorem IV can also be obtained as the Grothendieck ℓ-group of
the monoid in Item (2).
Proof.
(1) =⇒ (2). The subset M ⊆ H of those elements that may be written
ϕ(x1 ) ∧ · · · ∧ ϕ(xn ) for some x1 , . . . , xn is the meet-semilattice associated to the
system of ideals ⊲ obtained by restricting ⊢ to Pfe∗ (G) × G. This subset M is stable
by addition, so that the restriction of addition to M endows it with the structure
of a cancellative meet-monoid. Thus H is necessarily (naturally isomorphic to) the
Grothendieck ℓ-group of M .
(2) =⇒ (1). If the monoid is cancellative, then it embeds into its Grothendieck
ℓ-group H. So, using the observation on page 6 leading to Deﬁnition 1.8, we get
Item (1 ).
34

6.2

Prüfer’s properties Γ and ∆

Let us now express cancellativity of the meet-monoid as a property of the system
of ideals itself, as in Prüfer (1932, § 3).
Lemma 6.3 (Prüfer’s Property Γ). Let ⊲ be a system of ideals for an ordered
group G. The corresponding meet-monoid M is cancellative, i.e. a + b = a + c
implies b = c in M , if and only if the following property holds:
A + B 6⊲ x + B

=⇒

A ⊲ x.

(††)

This holds if and only if
A + B 6⊲ B

=⇒

A ⊲ 0.

Proof. The second implication, a particular case of the ﬁrst one, implies the ﬁrst
one by a translation. Let us work with the ﬁrst implication.
Cancellativity means that if A+B 6⊲ C +B, then A 6⊲ C. Property (††) is necessary: take C = {x}. Let us show that it is suﬃcient. Assume A + B 6⊲ C + B
and let x ∈ C. As C ⊲ x, we get by equivariance C + B 6⊲ x + B, whence
A + B 6⊲ x + B. So A ⊲ x. Since this holds for each x ∈ C, we get A 6⊲ C.
Remark 6.4. The original version for Prüfer’s Property Γ states, for a set-theoretical
star-operation A 7→ Ar on nonempty ﬁnitely enumerated subsets of G as considered
in Item (2 ) of Remarks 1.4, the cancellation property (A + B)r ⊇ (C + B)r =⇒
Ar ⊇ Cr .
⋄
Prüfer’s theorem 6.7 will reveal the signiﬁcance of the following deﬁnition. We
shall check in Proposition 6.10 that it agrees with Deﬁnition 1.10.
Definition 6.5 (Prüfer’s Property ∆ of integral closedness). Let ⊲ be a system
of ideals for an ordered group G. The group G is ⊲-closed if B 6⊲ x + B =⇒
0 6G x.
Remark 6.6. The original version for Prüfer’s Property ∆ states the cancellation
property Br ⊇ x + Br =⇒ 0 6G x.
⋄

6.3

Forcing cancellativity: Prüfer’s theorem

When the monoid M in Theorem I is not cancellative, it is possible to adjust
the system of ideals in order to straighten the situation. A priori, it suﬃces to
consider the Grothendieck ℓ-group of M (Theorem 6.1). But we have to see that
this corresponds to a system of ideals for G, and to provide a description for it.
The following theorem is a reformulation of Prüfer’s theorem (Prüfer 1932,
§ 6). We follow the proofs in Jaﬀard (1960, pages 42–43). In fact, the language
of single-conclusion entailment relations simpliﬁes the proofs. Jaﬀard’s statement
corresponds to Items (1 ) and (4 ), and Items (2 ) and (3 ) have been added by us.
35

Theorem 6.7 (Prüfer’s theorem). Let ⊲ be a system of ideals for an ordered
group G. We define the relation ⊲a between Pfe∗ (G) and G by
A ⊲a y ⇐⇒ ∃B ∈ Pfe∗ (G) A + B 6⊲ y + B.
def

1. The relation ⊲a is a system of ideals for G, and the associated meet-monoid
Ma (Theorem I) is cancellative.
2. Therefore Ma embeds into its Grothendieck ℓ-group Ha .
3. The system ⊲a is the finest system of ideals that is coarser than ⊲ and such
that Ma is cancellative.
4. We have that a ⊲a b implies a 6G b if (and only if) G is ⊲-closed (Definition 6.5); in this case, G embeds into Ha .
Proof. Note that if A+B 6⊲ y +B, then A+B +C 6⊲ y +B +C for all C (see the
proof of Theorem I on page 14). This makes the deﬁnition of ⊲a very easy to use.
In the proof below, we have two preorder relations on Pfe∗ (G) (6⊲ and 6a ), and we
shall do as if they were order relations (i.e. we shall descend to the quotients).
(1 ) • Reflexivity and preservation of order (of the relation ⊲a ). Setting B =
{0} in the deﬁnition of ⊲a shows that x 6G y implies x ⊲a y.
• Monotonicity. It suﬃces to note that the elements (A∪A′ )+B and (A+B)∪
′
(A + B) of Pfe∗ (G) are the same: therefore, if A + B 6⊲ y + B, then (A, A′ ) + B 6⊲
y + B.
• Transitivity. Assume A ⊲a x and A, x ⊲a b: we have a B such that A+B 6⊲
x + B and a C such that (A, x) + C 6⊲ b + C; these inequalities imply respectively
A + B + C 6⊲ x + B + C and (A + B + C), (x + B + C) 6⊲ b + B + C; we deduce
A + B + C 6⊲ b + B + C, so that A ⊲a b.
• Equivariance. If A ⊲a y, we have a B such that A + B 6⊲ y + B, so that,
since 6⊲ is equivariant, x + A + B 6⊲ x + y + B. This yields x + A ⊲a x + y.
• Cancellativity (of the meet-monoid Ma ). Let us denote by A 6a B the order
relation associated to ⊲a . By Lemma 6.3, it suﬃces to suppose that A + B 6a A
and to deduce that B ⊲a 0. But the hypothesis means that A + B ⊲a y for each
y ∈ A,
Pi.e. that for each y ∈ A there is a Cy such that A + B + Cy 6⊲ y + Cy . Let
C = y∈A Cy : we have
A + B + C 6⊲ y + C 6⊲ y + z for each y ∈ A and each z ∈ C,

so that A + B + C 6⊲ A + C. This yields B ⊲a 0 as desired.
(2 ) Follows from Item (1 ) by Theorem 6.1.
(3 ) This is immediate from the deﬁnition of ⊲a : it has been deﬁned in a minimal
way as coarser than ⊲ and forcing the cancellativity of the monoid Ma .
(4 ) If x ⊲a y, then we have a B such that x + B 6⊲ y + B, so that by a
translation B 6⊲ (y − x) + B. The hypothesis on G yields 0 ⊲ y − x. By a
translation, we get x ⊲ y.
36

Comment 6.8. This is the approach proposed in Lorenzen (1939, § 4). Lorenzen
abandoned it in favour of Deﬁnition 1.10 for the purpose of generalising his theory
to noncommutative groups. See also Comments 1.12 and 1.15.
⋄
Definition 6.9 (see Lorenzen 1939, page 546 or Jaﬀard 1960, II, § 2, 2). The
ℓ-group in Item (2 ) of Theorem 6.7 is called the Lorenzen group for the system of
ideals ⊲.
Proposition 6.10 (Lorenzen 1950, Satz 27). The definition of A ⊲a 0 in Theorem 6.7 agrees with Definition 1.10 of A ⊢⊲ 0. So Definition 6.5 of ⊲-closedness
agrees with that of Definition 1.10, and Definition 6.9 of the Lorenzen group agrees
with that of Definition 1.16.
Proof. This proposition expresses that, given a system of ideals ⊲ for an ordered
group G and an A ∈ Pfe∗ (G), we have A ⊢⊲ 0 (Deﬁnition 1.10) if and only if
A + B 6⊲ B for some B ∈ Pfe∗ (G).
First, A + B 6⊲x B and A + C 6⊲−x C imply A + D 6⊲ D for some D. In
fact, we have p and q such that
A + B, A + B + x, . . . , A + B + px 6⊲ B and
A + C, A + C − x, . . . , A + C − qx 6⊲ C,
which yield that for c ∈ C, j 6 q, b ∈ B and k 6 p,
A + B + c − jx, . . . , A + B + c + (p − j)x 6⊲ B + c − jx and
A + b + C + kx, . . . , A + b + C + (k − q)x 6⊲ b + C + kx,
so that A + D 6⊲ D for D = B + C + {−qx, . . . , px}.
In the other direction assume that A + B ⊲ bi for each bi in B = {b1 , . . . , bm }.
Let ci,j = bi − bj (i < j ∈ ⟦1..m⟧) and let us prove that A ⊲ ±c1,2 ,...,±cm−1,m 0. In
fact, for any system of constraints (ǫ1,2 c1,2 , . . . , ǫm−1,m cm−1,m ) with ǫi,j = ±1, the
elements bi in the corresponding meet-monoid Mǫ1,2 ,...,ǫm−1,m are linearly ordered.
E.g. b1 6 b2 6 · · · 6 bm , in which case
⋀
⋀
(A + b1 , . . . , A + bm ) = (A + b1 ) 6 b1
⋀
holds in the monoid Mǫ1,2 ,...,ǫm−1,m , which yields A 6 0 by a translation.
Remarks 6.11.
1. Informally the content of this proposition may be expressed
as follows. By starting from ⊲ and by adding new pairs (A, b) such that A ⊲ ′ b,
on the one side Prüfer forces the cancellativity of the meet-monoid Ma , and on the
other side Lorenzen forces ⊲ to become the restriction of an entailment relation
(which is still a system of ideals, as follows trivially from Lorenzen’s deﬁnition).
In fact, each approach realises both aims, but each one realises its own aim in a
minimal way. So they give the same result.
37

2. Theorem 6.7 enables to recover the results of Theorem 3.19 and of Theorem 5.4 in the Prüfer approach. In particular, one may check that A (⊲d )a b holds
if and only if b is integral over the fractional ideal hAiR (by applying the determinant trick, see Prüfer 1932, § 6), and that the hypothesis in Item (4 ) of Theorem 6.7
is fulﬁlled when R is integrally closed. Furthermore, elements > 1 of the ℓ-group Ma
in Item (2 ) of Theorem 6.7 can be identiﬁed with integrally closed ideals generated by nonempty ﬁnitely enumerated subsets A of R∗ . Therefore Item (1 ) of
Theorem 6.7 yields the cancellation property stated in Corollary 5.5.
⋄
Acknowledgement. This research has been supported through the program “Research in pairs” by the Mathematisches Forschungsinstitut Oberwolfach in 2016
and through the French “Investissements d’avenir” program, project ISITE-BFC,
contract ANR-15-IDEX-03. The second and third authors beneﬁtted from the
hospitality of the university of Gothenburg for leading this research.

References
Jean-Yves Béziau. Les axiomes de Tarski. In La philosophie en Pologne: 1918-1939,
edited by Roger Pouivet and Manuel Rebuschi, 135–149. Analyse et philosophie,
J. Vrin, Paris, 2006. Actes du colloque tenu à Nancy du 21 au 22 novembre 2003.
(p. 2).
Errett Bishop. Foundations of constructive analysis. McGraw-Hill, New York, 1967.
(p. 11).
Nicolas Bourbaki. Commutative algebra. Elements of mathematics, Hermann,
Paris, 1972. Translated from the French. (p. 15).
Douglas Bridges and Fred Richman. Varieties of constructive mathematics. London mathematical society lecture note series, 97, Cambridge university press,
Cambridge, 1987. (p. 11).
Jan Cederquist and Thierry Coquand. Entailment relations and distributive lattices. In Logic Colloquium ’98: proceedings of the annual European summer
meeting of the Association for symbolic logic, held in Prague, Czech Republic,
August 9–15, 1998, edited by Samuel R. Buss, Petr Hájek, and Pavel Pudlák,
127–139. Lecture notes in logic, 13, Association for symbolic logic, Urbana, 2000.
(p. 16).
A. H. Cliﬀord. Partially ordered abelian groups. Ann. of Math. (2), 41, 465–473,
1940. doi:10.2307/1968728. (p. 8).
Thierry Coquand and Henri Lombardi. Anneaux à diviseurs et anneaux de
Krull (une approche constructive).
Comm. Algebra, 44, 515–567, 2016.
doi:10.1080/00927872.2014.975346. (p. 15).
Michel Coste, Henri Lombardi, and Marie-Françoise Roy. Dynamical method in
38

algebra: eﬀective Nullstellensätze. Ann. Pure Appl. Logic, 111(3), 203–256, 2001.
doi:10.1016/S0168-0072(01)00026-4. (pp. 26 and 27).
Gema-Maria Díaz-Toca, Henri Lombardi, and Claude Quitté. Modules sur les anneaux commutatifs : cours et exercices. Calvage & Mounet, Paris, 2014. (p. 16).
Jean Dieudonné. Sur la théorie de la divisibilité. Bull. Soc. Math. France, 69,
133–144, 1941. http://eudml.org/doc/86745. (p. 8).
Harold M. Edwards. Divisor theory. Birkhäuser, Boston, 1990. (p. 15).
Gerhard Gentzen. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen. Math. Ann., 107(1), 329–350, 1933. http://eudml.org/
doc/159597. Translation: On the existence of independent axiom systems for
infinite sentence systems, in Szabo 1969, pages 29–52. (p. 2).
Paul Hertz. Über Axiomensysteme für beliebige Satzsysteme. II, Sätze höheren
Grades. Math. Ann., 89(1–2), 76–102, 1923. http://eudml.org/doc/158993.
(p. 2).
Paul Jaﬀard. Les systèmes d’idéaux. Travaux et recherches mathématiques, IV,
Dunod, Paris, 1960. (pp. 3, 4, 9, 15, 25, 35, and 37).
L. Kronecker. Zur Theorie der Formen höherer Stufen. Königl. Preuss. Akad.
Wiss. Berlin Sitzungsber., 957–960, 1883. Also in Werke, zweiter Band, 419–424.
(p. 32).
Wolfgang Krull. Idealtheorie. Ergebnisse der Mathematik und ihrer Grenzgebiete,
4, Springer, Berlin, 1935. (pp. 4, 10, and 32).
Henri Lombardi and Claude Quitté. Commutative algebra: constructive methods.
Finite projective modules. Algebra and applications, 20, Springer, Dordrecht,
2015. Translated from the French (Calvage & Mounet, Paris, 2011, revised and
extended by the authors) by Tania K. Roblot. (pp. 1, 11, 16, and 28).
Paul Lorenzen. Abstrakte Begründung der multiplikativen Idealtheorie. Math. Z.,
45, 533–553, 1939. http://eudml.org/doc/168865. (pp. 3, 4, 8, 9, 10, 13, 25,
33, and 37).
Paul Lorenzen. Über halbgeordnete Gruppen. Math. Z., 52, 483–526, 1950.
http://eudml.org/doc/169131. (pp. 1, 4, 5, 7, 8, 9, 11, 13, 14, 20, 21, and 37).
Paul Lorenzen. Algebraische und logistische Untersuchungen über freie Verbände.
J. Symbolic Logic, 16, 81–106, 1951. http://www.jstor.org/stable/2266681.
Translation by Stefan Neuwirth: Algebraic and logistic investigations on free
lattices, http://arxiv.org/abs/1710.08138. (pp. 1, 2, 3, 5, 11, and 16).
Paul Lorenzen. Teilbarkeitstheorie in Bereichen. Math. Z., 55, 269–275, 1952.
http://eudml.org/doc/169251. (pp. 7, 11, and 20).
Paul Lorenzen. Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen.
Math. Z., 58, 15–24, 1953. http://eudml.org/doc/169331. (pp. 1, 6, 7, 8, 9,
11, 18, 22, 26, and 29).
39

F. S. Macaulay. The algebraic theory of modular systems. Cambridge tracts in
mathematics and mathematical physics, 19, Cambridge university press, Cambridge, 1916. (pp. 31 and 32).
Ray Mines, Fred Richman, and Wim Ruitenburg. A course in constructive algebra.
Universitext, Springer, New York, 1988. (p. 11).
Erwan Penchèvre. La théorie arithmétique des grandeurs algébriques de Kronecker
(1882), preprint. http://arxiv.org/abs/1801.04327. (p. 32).
Heinz Prüfer. Untersuchungen über Teilbarkeitseigenschaften in Körpern. J. Reine
Angew. Math., 168, 1–36, 1932. http://eudml.org/doc/149823. (pp. 4, 9, 13,
14, 32, 33, 35, and 38).
Davide Rinaldi, Peter Schuster, and Daniel Wessel. Eliminating disjunctions by
disjunction elimination. Bull. Symb. Log., 23(2), 181–200, 2017. http://www.
jstor.org/stable/44259447. (pp. 2 and 20).
Dana Scott. Completeness and axiomatizability in many-valued logic. In Proceedings of the Tarski symposium: held at the university of California, Berkeley,
June 23–30, 1971, edited by Leon Henkin, John Addison, C. C. Chang, William Craig, Dana Scott, and Robert Vaught, 411–435. Proceedings of symposia
in pure mathematics, XXV, American mathematical society, Providence, 1974.
(pp. 1, 5, and 20).
M. E. Szabo (ed.). The collected papers of Gerhard Gentzen. Studies in logic and
the foundations of mathematics, North-Holland, Amsterdam, 1969. (p. 39).
B. L. van der Waerden. Moderne Algebra: unter Benutzung von Vorlesungen von
E. Artin und E. Noether. Zweiter Teil. Die Grundlehren der mathematischen
Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, 24, Springer, Berlin, 1931. (p. 13).
B. L. van der Waerden. Modern algebra: in part a development from lectures by E.
Artin and E. Noether. Volume II. Frederick Ungar, New York, 1950. Translated
from the second revised German edition by Theodore J. Benac. (p. 13).
Hermann Weyl. Algebraic theory of numbers. Annals of mathematics studies, 1,
Princeton university press, Princeton, 1940. (p. 15).

40

