On simplicity of formulas (Q757354)

Given an axiom system S, it is natural to ask if S has an equivalent simpler reformulation. The authors give a precise notion of simplicity using a generalized Kleene-Mostowski classification that takes into account not only the number of quantifier alternations, but also the number of quantifiers. To prove that formulas are written in their simplest form, they develop the appropriate preservation theorems, using Fraïssé's partial isomorphisms. Extensions are given to languages with function symbols, many-sorted languages, and nonelementary logics. It is proved that some well-established axiom systems cannot be simplified.