(In)dependence of the axioms of $\Lambda$-trees

TL;DR

This paper investigates the relationships between axioms defining $ ext{Lambda}$-trees, characterizing when certain axioms imply others and exploring independence among axioms within the framework of ordered abelian groups.

Contribution

It provides a characterization of ordered abelian groups where axioms (1) and (2) imply (3), and examines the independence of axiom (2) from (1) and (3), with formalization in Lean.

Findings

Axioms (1) and (2) imply (3) for certain $ ext{Lambda}$-groups.

For $ ext{Lambda}$ with $ ext{Lambda}=2 ext{Lambda}$, axiom (3) follows from (1) and (2).

Axiom (2) is independent of (1) and (3) for some $ ext{Lambda}$ groups.

Abstract

A $\Lambda$-tree is a $\Lambda$-metric space satisfying three axioms (1), (2) and (3). We give a characterization of those ordered abelian groups $\Lambda$ for which axioms (1) and (2) imply axiom (3). As a special case, it follows that for the important class of ordered abelian groups $\Lambda$ that satisfy $\Lambda=2\Lambda$, (3) follows from (1) and (2). For some ordered abelian groups $\Lambda$, we show that axiom (2) is independent of the axioms (1) and (3) and ask whether this holds for all ordered abelian groups. Part of this work has been formalized in the proof assistant \textsf{Lean}.