Manaster and Nerode showed that the theory of order of isols and the theory of recursive equivalence types (RETs) with order is undecidable. The results of Manaster and Nerode rely on coding an arbitrary binary relation in the isols using indecomposable RETs and indecomposable covers of ω-sequences of recursive equivalence types (RETs). RETs were generalized from sets to many other structures. In the chapter, the undecidability results analogous to those of Manaster and Nerode and Nerode and Shore for five theories of constructive order types (COTs) is proved with addition and in two planned sequels to matroids, vector spaces, and algebraically closed fields. A quasi finite COT is one that has a representative with no infinite recursive ascending or descending chain and a losol is a COT with an immune representative. All losols are, therefore, quasi-finite COTs.