Halting and Equivalence of Program Schemes in Models of Arbitrary Theories

Abstract

In this note we consider the following decision problems. Let Σ be a fixed first-order signature.

(i) Given a first-order theory or ground theory T over Σ of Turing degree α, a program scheme p p over Σ, and input values specified by ground terms t₁,...,t _n , does p p halt on input t₁,...,t _n in all models of T?

(ii) Given a first-order theory or ground theory T over Σ of Turing degree α and two program schemes p p and p q over Σ, are p p and p q equivalent in all models of T?

When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is $\Sigma^\alpha_1$-complete and problem (ii) is $\Pi^\alpha_2$-complete. Both problems remain hard for their respective complexity classes even if Σ is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence over models of theories of any Turing degree.