Ordering groups constructively
Daniel Wessel · Communications in Algebra · 2019
The existence of a linear order on a group that is compatible with the group structure generally requires transfinite methods. However, this can be circumvented by concentrating on the consistency of a suitable propositional theory. To this end, we work with Scott’s multiple-conclusion entailment relations to describe the positive cones of a group. The commutative case then leads to a constructive version of Levi’s theorem that an Abelian group be orderable if and only if it is torsion-free. Subsequently, Cederquist and Coquand’s fundamental theorem of entailment relations prompts a finitary version of Sikora’s theorem.