Recursively enumerable sets in ZF

Question

I read often definition of recursively enumerable set based on the concept of recursive function from N to the set, based on Turing machine, or on Levy hierarchy. How can i define recursively enumerable set only in the language of ZF without metalanguage's tricks? I would have a formula of ZF wich says 'x is recursively enumerable'. The class of r.e sets is transitive? If it is not, how can express 'x is hereditary r.e' in ZF language?

Answer 1

A notion now considered standard of primitive recursive set function is introduced in

MR0281602 (43 #7317). Jensen, Ronald B.; Karp, Carol. Primitive recursive set functions. In 1971 Axiomatic Set Thoory (Proc. Sympos. Pure Math., Vol. XIII, Part I, Univ. California, Los Angeles, Calif., 1967) pp. 143–176 Amer. Math. Soc., Providence, R.I.

The concept is useful when dealing with arguments that require verifying absoluteness of certain notions, typically in contexts where one only has access to limited resources (for instance, working in admissible sets; Jensen also uses it in some fine-structural arguments, particularly by considering properties of primitive recursive ordinals). As with the classical notion, one can characterize the functions in terms of complexity of definitions, see

MR1187458 (94b:03090). Rathjen, Michael. A proof-theoretic characterization of the primitive recursive set functions. J. Symbolic Logic 57 (1992), no. 3, 954–969.

This MO question may be of interest in this respect, illustrating the notions in actual practice, and because of some of the additional references it suggests.

You may also be interested in recursion over admissible sets and, more generally, higher recursion theory, for which an excellent introduction is the book

MR1080970 (92a:03062). Sacks, Gerald E. Higher recursion theory. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1990. xvi+344 pp. ISBN: 3-540-19305-7.

For a modern update and recent applications, see

MR3381097. Chong, Chi Tat; Yu, Liang. Recursion theory. Computational aspects of definability. With an interview with Gerald E. Sacks. De Gruyter Series in Logic and its Applications, 8. De Gruyter, Berlin, 2015. xiv+306 pp. ISBN: 978-3-11-027555-1; 978-3-11-038129-0.