Uniform representation of recursively enumerable sets with simultaneous rigid E-unification

Margus Veanes

Abstract

Recently it was proved that the problem of simultaneous rigid E­unification (SREU) is undecidable. Here we perform an in­depth investigation of this matter and obtain that one can use SREU to uniformly represent any recursively enumerable set. From the exact form of this representation follows that SREU is undecidable already for 6 rigid equations with ground left hand sides and 2 variables. There is a close correspondence between solvability of SREU problems and provability of the corresponding formulas in intuitionistic first order logic with equality. Due to this correspondence we obtain a new (uniform) representation of the recursively enumerable sets in intuitionistic first order logic with equality with one binary function symbol and a countable set of constants. From this result follows the undecidability of the EE­fragment of intuitionistic logic with equality. This is an improvement of a recent result regarding the undecidability of the E*­fragment in general.

Details

Publication typeTechReport
Number126
SeriesUPMAIL Technical Report
InstitutionUppsala University, Computing Science Department
> Publications > Uniform representation of recursively enumerable sets with simultaneous rigid E-unification