ON THE STATUS OF PROVING PROGRAM PROPERTIES IN EFFECTIVE INTERPRETATION

We present a sufficient condition for a class C of effective interpret ations in order that C has a uniform procedure enumerating (when first -order oracle and recursive presentation of the interpretation involve d are given) dynamic theories of interpretations in C. Under some addi tional assumption on the enumerating procedure, this condition is nece ssary. The main result states that if arithmetical notions are first-o rder-definable by universal or existential formulas within interpretat ions in C then C has an appropriate uniform procedure.