The undecidability of formal definitions in the theory of finite groups
Newton Ca da Costa, Francisco Antônio Dória, Marcelo Tsuji · 1995
In this paper a set of explicit expressions for a family of finite groups will be constructed in the language of Zermelo-Fraenkel plus the Axiom of Choice set theory in such a way that there is no general procedure to decide whether a given expression of this set is representing a finite solvable group or not.