Cancellation laws for polynomial-time \(p\)-isolated sets (Q1192348)

In two papers [Contemp. Math. 106, 221-249 (1990; Zbl 0701.03017); Lect. Notes Math. 1432, 323-362 (1990; Zbl 0705.03024)], \textit{A. Nerode} and the second author initiated the study of what happens to the Dekker- Myhill theory of RETs and isols when bounds are imposed on computational resources. By requiring the functions involved to be polynomial-time computable, they developed the notions of \(p\)-time equivalence type (PET) and \(p\)-isolated set. They also proved that cancellation of addition and multiplication hold in \(P\Lambda\), the class of PETs of subsets of \(p\)- time \(p\)-isolated sets. In ``Polynomial-time combinatorial operators are polynomials'' [Feasible mathematics, Prog. Comput. Sci. Appl. Log. 9, 99- 130 (1990; Zbl 0766.03025)], the authors investigated a \(p\)-time version of Myhill's combinatorial operators. The present paper extends this program to a \(p\)-time version of Nerode's frames and proves a \(p\)-time analog of Nerode's 1961 theorem: Any universal Horn sentence (in the appropriate language) is satisfied by the natural numbers iff it is satisfied by \(P\Lambda\).