Completeness and incompleteness of basic matching logic

Abstract

Basic matching logic is matching logic without definedness. Symbols are interpreted as set-valued operations, element variables denote singletons and are bound by $\exists$, and no connective uniformly internalizes totality. For basic matching logic without fixpoints over an arbitrary one-sorted finitary signature, we prove \emph{global completeness} ($Γ\vDashφ$ iff $Γ\vdashφ$, for arbitrary, possibly infinite $Γ$) and, as a corollary, conservativity of the definedness extension. The proof localizes $Γ$ to a theory $Δ_Γ$ and reduces semantic consequence and derivability to the same local relation: $Γ\vDashφ$ iff $Δ_Γ\vDash_\text{loc}φ$ iff $Γ\vdashφ$. A double-cover construction establishes the semantic equivalence. Least fixpoints destroy effective axiomatizability. Over a signature with one unary and two binary symbols and no constants, validity is not recursively enumerable; hence no sound calculus with a recursively enumerable proof relation is even weakly complete, already for the empty theory and without definedness. The positive result is also sharp in the number of sorts. Global completeness fails with three sorts for a satisfiable $Γ$. Thus the completeness conjecture holds for one sort and fails in general. The negative results arise from sort flow, fixpoint effectivity, and, for hybrid logic, an obstruction to every well-founded calculus whose leaves are hypotheses or valid patterns and whose rules respect localization. This yields a matching-logic-independent dichotomy: the language with state variables bound by $\exists$ and $\forall$ over modalities of arbitrary arity is globally complete without nominals, while no calculus in that well-founded class is globally complete once nominals are added.