Expressing properties in second- and third-order logic: hypercube graphs and SATQBF
Flavio Antonio Ferrarotti, W. Ren, J. M. T. Torres · Logic Journal of IGPL · 2013
It follows from the famous Fagin's theorem that all problems in NP are expressible in existential second-order logic (∃SO), and vice versa. Indeed, there are well-known ∃SO characterizations of NP-complete problems such as 3-colourability, Hamiltonicity and clique. Furthermore, the ∃SO sentences that characterize those problems are simple and elegant. However, there are also NP problems that do not seem to possess equally simple and elegant ∃SO characterizations. In this work, we are mainly interested in this latter class of problems. In particular, we characterize in second-order logic the class of hypercube graphs and the classes SATQBFk of satisfiable quantified Boolean lformulae with k alternations of quantifiers. We also provide detailed descriptions of the strategies followed to obtain the corresponding non-trivial second-order sentences. Finally, we sketch a third-order logic sentence that defines the class SATQBF = ∪k≥1SATQBFk. The sub-formulae used in the construction of these complex second- and third-order logic sentences, are good candidates to form part of a library of formulae. Same as libraries of frequently used functions simplify the writing of complex computer programs, a library of formulae could potentially simplify the writing of complex second- and third-order queries, minimizing the probability of error.