Existential Second Order Logic Expression With Horn First Order for Maximum Clique (Decision Version)

TL;DR

This paper explores expressing the maximum clique decision problem within existential second order logic using Horn formulas, but the results are invalidated due to logical limitations and errors in the initial claims.

Contribution

The paper attempts to formalize the maximum clique problem in ESO logic with Horn first order parts, proposing new logical characterizations.

Findings

The initial claims about expressing maximum clique in ESO logic are incorrect.

Horn formulas do not necessarily decompose into Horn components when conjoined.

Cardinality constraints cannot be expressed as universal Horn sentences in ESO.

Abstract

We show that the maximum clique problem (decision version) can be expressed in existential second order (ESO) logic, where the first order part is a Horn formula in second-order quantified predicates. Without ordering, the first order part is $\Pi_2$ Horn; if ordering is used, then it is universal Horn (in which case, the second order variables can be determined in polynomial time). UPDATE: Manuscript withdrawn, because results are incorrect. If phi = phi_1 AND phi_2, and phi is a Horn formula, it does NOT mean that both phi_1 and phi_2 are Horn formulae. Furthermore, the cardinality constraint CANNOT be expressed as a universal Horn sentence in ESO (NOT even when the structure is ordered). Graedel's theorem is valid at a lower (machine) level, but probably NOT at a higher level.