Papers With

← All papers
First page of On canonicity of almost linear minimal orders

On canonicity of almost linear minimal orders

Grzegorz Jagiella

math.LO Sep 28, 2026 · v2
autoformalization formalization logic
Read PDF arXiv abstract
TL;DR
An earlier version of the manuscript and a prior paper were autoformalized into Lean 4 with Harmonic's Aristotle. Aristotle suggested replacing an ordering with a colexicographical order.
Abstract
We prove that if a minimal ordered structure $(M, <, \ldots)$ with infinite chains in an arbitrary language extending the language of strict orders interprets (in some power $M^n$) the linear order $(ω, <)$, then this fact can be witnessed for $n=1$ via the incomparability relation of an $<$-definable strict order $R$; that $R$ is unique up to “almost equality”, i.e., finite rearrangements of elements of $M$; and that $R$ can be defined from $<$ in a constructive way. We also show that several variants of the question whether a minimal ordered structure interprets an infinite linear order are all equivalent.
Problem

Tanović asked whether every minimal ordered structure with arbitrarily long chains interprets an infinite linear order. The question is linked to conjectures of Pillay, Podewski (minimal fields are algebraically closed) and Kueker. The paper studies minimal ordered structures assumed to interpret (ω,<).

Approach

Building on Tanović's classification of minimal ordered structures by type, the authors analyze definable strict orders up to almost equality, meaning agreement on a cofinite set. They give an explicit iteration of definable relations from < and a finite-stabilization criterion. A transfer result reduces interpretations in higher dimensions to dimension 1, using a colexicographical order. Earlier versions of the work were autoformalized in Lean 4 using Aristotle.

Results

If such a structure interprets (ω,<), this is witnessed in dimension 1 by the incomparability relation of a strict order R definable from <. R is unique up to almost equality and can be constructed explicitly. Several variants of the main question are shown to be equivalent, and the orders definable in (ω,≤) are classified via cofinite submonoids of ℕ.