Some Undecidable Problems Related to the Herbrand Theorem

We improve upon a number of recent undecidability results related to the so-called Herbrand Skeleton Problem, the Simultaneous Rigid E-Unification Problem and the prenex fragment of intuitionistic logic with equality. Partially supported by grants from NSF, ONR and the Faculty of Science and Technology of Uppsala University. 1 Introduction We study classical first-order logic with equality but without any other relation symbols. The letters ' and / are reserved for quantifier-free formulas. The signature of a syntactic object S (a term, a set of terms, a formula, etc.) is the collection of function symbols in S augmented, in the case when S contains no constants, with a constant c. The language of S is the language of the signature of S. Any syntactic object is ground if it contains no variables. A substitution is ground if its range is ground, and it is said to be in a given language if the terms in its range are in that language. A set of substitutions is ground if each membe..