On the status of proving program properties in effective interpretations

AbstractWe present a sufficient condition for a class C of effective interpretations in order that C has a uniform procedure enumerating (when first-order oracle and recursive presentation of the interpretation involved are given) dynamic theories of interpretations in C. Under some additional assumption on the enumerating procedure, this condition is necessary. The main result states that if arithmetical notions are first-order-definable by universal or existential formulas within interpretations in C then C has an appropriate uniform procedure