Structural Relations Between Programs and Problems

Abstract

By a problem in a universal first-order theory Γ we understand a formula φ(y) with a free variable y. The problem φ(y) is solvable relative to auxiliary problems ψ₁(υ),…_s, (υ) if solution algorithms for the ψ_i can be so composed as to yield all solutions of φ in all models of Γ. The complexity of the composite algorithm is the number of times that the auxiliary algorithms have to be called. A lower bound for the complexity of φ is obtained by developing a generalized Galois theory for theories Γ and problems φ satisfying some reasonable restrictions; our lower bound is the logarithm of the order of the ‘Galois group’ of φ