AI 中文总结
该研究证明了单类有限签名上不含不动点的基础匹配逻辑的全局完备性，指出加入名签后对应良基演算不再全局完备，而含不动点时有效性非递归可枚举。
AI 中文摘要
基础匹配逻辑是不包含定义性（definedness）的匹配逻辑。符号被解释为集值运算，元素变量表示单元素集且受∃约束，不存在任何连接词可统一内化全体性（totality）。对于任意单类有限签名上不含不动点的基础匹配逻辑，我们证明了**全局完备性**（即对任意可能无限的Γ，Γ⊨φ当且仅当Γ⊢φ），并由此得到定义性扩展的保守性作为推论。该证明将Γ局部化为理论Δ_Γ，把语义后承与可推导性归约为同一局部关系：Γ⊨φ当且仅当Δ_Γ⊨_locφ，当且仅当Γ⊢φ。双覆盖构造确立了该语义等价性。最小不动点会破坏有效公理化。在含1个一元符号、2个二元符号且无常量的签名上，有效性不是递归可枚举的；因此，即便针对空理论且不含定义性，不存在具有递归可枚举证明关系的可靠演算能满足弱完备性。正结果在类的数量上是严格的：对于可满足的Γ，当类数为3时全局完备性不成立。因此，完备性猜想在单类时成立，一般情况下不成立。负面结果源于类流、不动点有效性，以及对于混合逻辑，每个良基演算存在一个障碍——该演算的叶节点为假设或有效模式，且其规则符合局部化要求。这产生了一个与匹配逻辑无关的二分：在对任意元数的模态词应用∃和∀约束状态变量的语言中，不含名签（nominals）时是全局完备的；而一旦加入名签，该良基类中就没有任何演算是全局完备的。
英文摘要
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.
