Axiomatization and undecidability results for metrizable betweenness relations
Robert Mendris, Pavol Jan Zlatos · Proceedings of the American Mathematical Society · 1995
Let d be a metric on a nonempty set A . The ternary betweenness relation T d {T_d} induced by d on A is defined by \[ T d ( x , y , z ) ⇔ d ( x , y ) + d ( y , z ) = d ( x , z ) {T_d}(x,y,z) \Leftrightarrow d(x,y) + d(y,z) = d(x,z) \] for x , y , z ∈ A x,y,z \in A . Allowing the range of d to vary over some "reasonable" ordered additive algebraic structures (not just the real numbers), we will prove that the class M \mathcal {M} of all metrizable ternary structures, i.e., the class of all structures ( A , T d ) (A,{T_d}) , where d is some metric on A , is an elementary class which can be axiomatized by a set of universal Horn sentences. Further, using an algorithm of linear programming, we will show that the first-order theory of M \mathcal {M} is recursively axiomatizable and its universal part is decidable. On the other hand, the theory of M \mathcal {M} is not finitely axiomatizable and the theory of finite members of M \mathcal {M} is hereditarily undecidable.