A Decidable Subclass of the Minimal Goedel Case with Identity

The minimal Gddel class with identity (MGCI) is the class of closed, prenex quantificational formulas whose prefixes have the form Vx1 Vx2x3 and whose matrices contain arbitrary predicate letters and the identity sign ” = “, but contain no function signs or individual constants. The MGCI was shown undecidable (for satisfiability) in 1983 [Go2]; this both refutes a claim of Gddel’s [Gd, p. 443] and settles the decision problem for all prefix-classes of quantification theory with identity.