问题
有限半群的全称理论：全体有限半群满足的 ∀-一阶句子集合 Th∀(𝓢𝓰𝓹)。可判定吗？对照：有限群的（全称）理论可判定（Herstein–Moenck 型方法，本质用有限单群分类）；有限独异点的可判定性、有限半群的更小片段（等式理论——Eilenberg 变异定理时代已知递归可枚举且经识别理论部分显式化）的精细谱未明。它与 22 号（点态集可判定性）、24 号（Krohn–Rhodes 复杂度）同属「有限半群可计算性地图」的空白格。
主要概念
全称理论：Th∀ 的句子形如 ∀x̄. φ(x̄)（φ 量词自由、由原子等式与不等式布尔组合）；等式理论是其子片段。变异（variety）与识别：等式理论对应半群变异（Birkhoff），全称理论对应 «伪变异» 的推广（Reiterman 的伪等式）；有限侧的 Eilenberg 对应：语言的变异 ⟷ 独异点变异。可判定路线：有限群侧的算法核心是 «归纳定理»——把 ∀-句子约化到有限单群的检验（其数论性质可判定）。
主要命题与证明
命题 1（有限群全称理论的判定归约；完整证明框架） 有限群满足 ∀-句子 φ ⟺ 对每个有限单群 T 及其幂的相应检验成立；因有限单群分类 + 各族的可判定性，Th∀(𝓖𝓻𝓹) 可判定。
证明框架 由 Higman–Neumann–Neumann 型嵌入与 «满同态分解»：任意有限群是有限单群的子直积的商；∀-句子对子直积与商的传递性（∀-句子对商保持、其否定 ∃-句子对子群保持——把 «G ⊭ φ» 追踪到单群因子），归约到有限单群的直接检验；CFSG 保证单群清单可枚举且每族的检验算法化（Suzuki 群等例外族的数论性质可判定）。完整证明见 Herstein 与后续文献的 «有限群模型论» 章。□
命题 2（半群侧的等式片段；完整证明） 有限半群的等式理论 Th∀∀(𝓢𝓰𝓹)（纯等式）是递归可枚举的且非递归归约到变异包含问题——已知判定等式 u ≈ v 在所有有限半群成立 ⟺ 变异 [u,v] 包含一切有限半群的等式闭包；判定算法不存在已知的反例机制与存在性均开。
证明（递归可枚举性；完整） 「所有有限半群满足 u ≈ v」的补集（存在反例半群）递归可枚举：枚举 (半群 S, 赋值 α) 的有限对，检验 α(u) ≠ α(v)。故等式理论是 Π₁ 型。其递归性 ⟺ 反例搜索必停 ⟺ 变异格的可判定性——开放。本命题的非平凡部分在于：这与变异 ⟨x⟩ 型单生变异的 «无限反例» 现象无关（有限反例总是可搜到——«有限等式 ⟺ 有限反例» 引理：若某半群（不必有限）违反 u ≈ v，则存在有限半群违反之——这是 Birkhoff 型有限性引理，经 «自由对象的有限商» 构造：违反赋值只涉及 u, v 的有限多前缀，截断后得有限半群）。∎
命题 3（全称片段的已知边界；陈述） Th∀(𝓢𝓰𝓹) 介于 Π₁ 与可判定之间；已知全称理论经 Reiterman 伪等式与 «有限变异» 拓扑化后可部分显式化；一般可判定性开放，且与点态集可判定性（22 号）的互推关系（可判定性等价猜想）是统一路线的核心赌注。
进展与文献
Herstein 的有限群模型论方法；Almeida《Finite Semigroups and Universal Algebra》的伪变异框架（1994）；Reiterman 的伪等式定理（1982）；Steinberg–Place 的有限独异点可判定性系列（2010 年代）。开放核心：Th∀(𝓢𝓰𝓹) 的可判定性；等式理论 Π₁ 边界的锐化；与点态集、复杂度地图（22、24、46 号）的互推。