Logical equations in monadic logic (Q843613)

The authors regard a formula of logic, \(F(\mathbf{X,P})\), as an equation with unknowns \(\mathbf X\) and parameters \(\mathbf P\). Then, two questions arise naturally: under what conditions is it solvable, and what is the most general solution. [An example the authors list explains the situation. Let \(F(\mathbf {X,P})\) be \(\forall x({\mathbf P}x\to {\mathbf X}x)\&({\mathbf X}x\to {\mathbf Q}x)\). Then the solvability condition is \(\forall x({\mathbf P}x\to {\mathbf Q}x)\), and the general solution is \({\mathbf P}x\lor({\mathbf Q}x\& {\mathbf Y}x)\) with a fresh variable \(\mathbf Y\).] The authors answer these questions completely for monadic first-order formulas with equality, MFO. Based on the familiar procedure of quantifier elimination for MFO, they put the given formula in a special normal form that indicates how many elements there are in what classes. From this form and using \(\varepsilon\)-terms as witness constants, they give the solution in a detailed and easy manner.