Recently it was proved that the problem of simultaneous rigid Eunification (SREU) is undecidable. Here we perform an indepth 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 EEfragment of intuitionistic logic with equality. This is an improvement of a recent result regarding the undecidability of the E*fragment in general.
|Series||UPMAIL Technical Report|
|Institution||Uppsala University, Computing Science Department|