A representation of recursively enumerable sets through Horn formulas in higher recursion theory (Q1677584)

In the late 1950's, R. Smullyan showed: the r.e. (recursively enumerable) sets are exactly those that are representable in his elementary formal systems. This is a result in ordinary recursion theory in arithmetical setting. The authors of this article extend it to other recursion theories in set-theoretic setting: primitive set recursion, \(\beta\)-recursion, and recursion in admissible structures. First, they give careful definitions of r.e. sets and Horn clause theories (modern reformulation of elementary formal systems) in set-theoretic context. Also, succinct definitions of recursion theories in question are given. The direction of an r.e. set is representable is proved inductively following how that set is constructed. The proof of the other implication uses the fact that local satisfaction relation is definable. In the last section, the authors look at Smullyan's result from the set-theoretic view-point, utilizing the equivalence of the system of natural numbers and the system of hereditarily finite sets.