A formal derivation of the decidability of the theory SA (Q1325831)

By \textbf{SA} the authors mean the first order theory of the rationals under addition, with unary functions that give the result of dividing by the positive natural number \(n\) (one for each such \(n\)), and with the \(<\) relation and a unary predicate that picks out the integers. \textbf{SA} is axiomatized and a syntactic decision procedure is described. A key element is the introduction of ``basic'' formulas that assert the existence of a unique integer satisfying a given formula within a prescribed rational interval.