Completeness of Canonical Closure Representations Is coNP-Complete: A Thirty-Year Problem Across Horn Logic, FCA, Convex Geometries, and Databases

A finite closure system on a finite set U is a family of subsets that contains U and is closed under intersections. It can be specified in two elementary ways. An implicational specification lists rules A → b and consists of all subsets X ⊆ U that satisfy every rule: if A ⊆ X, then b ∈ X. An intersection specification lists subsets M1, ..., Mt and consists of all intersections of subfamilies of that list. We ask whether one specification of each kind defines exactly the same family of subsets. This simple question has remained open in several guises for about thirty years. In 1995, Khardon showed that efficiently translating between Horn formulas and their characteristic models is equivalent to deciding whether a proposed list of characteristic models is complete, but left the exact complexity open. At ISAAC 2025, the corresponding problem of enumerating irreducible closed sets from implications was still described as "widely open," even for acyclic convex geometries. Closely connected open questions concerned pseudo-intents and the Duquenne–Guigues basis in Formal Concept Analysis, and functional dependencies and Armstrong relations in database theory. We prove that the equivalence test is coNP-complete. Hardness holds for acyclic implications whose premises contain at most three elements, even when every listed subset is correct and no listed subset can be removed without changing the closure system generated by the list. Thus the hard part is simply deciding whether a required set is missing. Unless P = NP, the complete canonical lists cannot in general be generated in time polynomial in the input plus the total output size, even for acyclic convex geometries. Through standard correspondences, the theorem makes Characteristic Models Identification and FD–Relation Equivalence coNP-complete and rules out such output-polynomial algorithms for Horn characteristic models, all pseudo-intents (equivalently, the Duquenne–Guigues basis), and premises of minimum functional-dependency covers. AI-assistance disclosure: The main proof was obtained by OpenAI's GPT-5.6 Pro through ChatGPT and checked by the author. The author takes full responsibility for the mathematical claims and the final manuscript.