The isols are a recursive
analogue of the Dedekind finite cardinals originally developed by Dekker. In this
paper a metatheorem is proved which shows that for certain sentences 𝒜 about
addition in which no existential quantifier precedes a universal quantifier, the truth of
𝒜 in the natural numbers is sufficient to ensure the truth of 𝒜 in the isols. A
more general class of sentences is also considered and it is seen that the
applicability of the metatheorem is also necessary for the truth of any sentence in
this class. It follows that there exists a decision procedure for that class of
sentences. Extensions of these results to the case of the cosimple isols are also
considered.
