自由添加一层量词的布尔教义：QA一步布尔教义的Herbrand定理与自由构造

《Annals of Pure and Applied Logic》：Freely adding one layer of quantifiers to a Boolean doctrine

　　

研究人员描述了小范畴上布尔教义（Boolean doctrine）的量词完成（quantifier completion）中量词交替深度（quantifier alternation depth）至多为一的层。这相当于在普遍理论（universal theory）模下，对量词交替深度至多为一的公式给出了Herbrand定理的教义版本（doctrinal version）。所得构造满足一个泛性质（universal property），使其成为自由QA一步布尔教义（free QA-one-step Boolean doctrine）。为实现此版本的Herbrand定理，研究人员在教义框架内刻画了量词自由公式（quantifier-free formulas）的类A，使得存在一个模型M，其中A恰为那些其全称闭包（universal closure）在M中有效的公式之类。

本文研究小范畴上布尔教义（Boolean doctrine）的量词完成中量词交替深度至多为一的层，旨在给出该层的显式描述并构造自由QA一步布尔教义。研究背景在于，一阶公式的复杂度常以其量词交替深度衡量，由此得到公式集合的分层F0?F1?F2?…，其中Fn由量词交替深度至多为n的公式组成。研究人员采用Lawvere的超教义（hyperdoctrine）代数化方法，特别是第一阶布尔教义（first-order Boolean doctrine）的框架，因其公式按自由变量集索引，能忠实反映量词改变自由变量集的事实。核心问题是：给定量词自由公式层F0（以布尔教义P表示），如何构造自由添加一层量词所得的F1？在教义术语中，P表示量词自由公式模普遍理论T的等价类集合，其量词完成P^自由添加量词，而目标子函子P1由P中公式的量词化（quantification）的布尔组合构成。研究动机在于建立该子函子的显式构造，并证明其满足自由QA一步布尔教义的泛性质。

研究人员开展的研究包括：首先在第3节通过对模型的研究（独立有趣且构成技术核心）刻画普遍超滤（universal ultrafilter），即那些恰为某模型中共全称闭包有效公式类的族；其主要结果（定理3.28）在语法情形下即为：给定普遍理论T，刻画量词自由公式的类A，使得T有模型M且A恰为全称闭包在M中有效的量词自由公式类。证明灵感来自Henkin对一阶逻辑完备性定理的证明，并引入普遍滤子（universal filter）、普遍理想（universal ideal）及普遍超滤引理（定理3.20），通过ω步添加常元构造丰富（rich）教义（定理3.27）。其次，第4节证明教义版Herbrand定理（定理4.5、定理4.7），刻画普遍语句的有限合取何时模普遍理论蕴涵普遍语句的有限析取，例如?yα(y)?T?zβ(z)当且仅当存在有限多元项t1(z),…,tn(z)使?i=1nα(ti(z))?Tβ(z)，从而将量词交替深度≤1的条件归约为量词自由条件。再次，第5节通过生成元与关系构造自由QA一步布尔教义Free1P（定义5.5、 notation 5.11），并证明嵌入P?Free1P满足泛性质（定理5.20、推论5.21），且该构造不依赖Herbrand定理；最后第6节利用Herbrand定理证明P1与Free1P同构（定理6.1），故P1确为自由QA一步布尔教义，Free1P给出P1基于P的生成元与关系构造。

结论的重要意义在于：本文建立了量词交替深度≤1模普遍理论的教义版Herbrand定理，给出了量词完成第一层的显式构造，证明了该层恰为自由QA一步布尔教义，从而推进了量词完成的逐步构造计划；同时，普遍超滤与丰富教义的技术为模型论视角下的教义研究提供了新工具。

研究人员为开展研究用到的主要关键技术方法包括：布尔教义与第一阶布尔教义的范畴框架（函子P:C^op→BA，纤维、再索引、伴随量词）；量词完成及其泛性质；普遍超滤、普遍滤子与普遍理想的生成与相交判定（引理3.14–3.19）；普遍超滤引理（基于Zorn引理）；通过添加常元的教义扩张（co-Kleisli构造）与ω步归纳构造丰富教义；生成元与关系及蕴涵关系（entailment relation）的布尔代数表示；以及教义版Herbrand定理的归约论证。样本队列来源方面，本文为纯范畴逻辑理论研究，未涉及实验样本队列；语法情形以第一阶语言L=(F,P)与理论T为来源。

研究结果如下：

3. 普遍有效公式类的刻画：通过引入普遍超滤（定义3.3）并证明其与模型所诱导的族等价（定理3.28），得出普遍超滤恰为某命题模型的全体全称闭包有效公式类；并证明普遍超滤引理（定理3.20）与丰富化构造（定理3.27），为后续Herbrand定理提供模型论工具。

4. Herbrand定理：通过定理3.38与引理4.2–4.4，证明定理4.5：在量词完成中?i(?Yi)Sαi≤?j(?Zj)Sβj当且仅当存在有限项gi使?iP(?prS,gi?)(αli)≤?jP(prS×Zj)(βj)（量词自由条件）；进而定理4.7给出量词交替深度≤1的布尔组合之间的蕴涵刻画，即教义版Herbrand定理，并给出Herbrand定理的经典情形（例4.8）及对前束范式归约失败的讨论（例4.10）。

5. 自由QA一步布尔教义的构造：通过生成元与关系定义Free1P(S)=BS/～S（定义5.5），证明蕴涵关系（引理5.6）与序刻画（定理5.7），构造函子与自然变换?1（引理5.12–5.15），证明(P,Free1P)为QA一步布尔教义（命题5.16），并证明其泛性质（定理5.20），从而得到遗忘函子有左伴随（推论5.21）。

6. 第一层与自由构造的同一性：通过定理5.20与定理4.5[(1)?(2)]，证明(P,Free1P)与(P,P1)同构（定理6.1），即P1为自由QA一步布尔教义，Free1P给出P1的显式构造。

讨论部分总结：本文在教义框架内完全以教义形式证明Herbrand定理，不依赖经典逻辑方法；普遍超滤的引入使模型论论证得以在教义内部展开。未来工作计划逐步构造量词完成：对元组(P0,…,Pm)（其中Pi表示量词交替深度≤i的公式模T的等价类）进行公理化，并研究其Stone对偶（Joyal的多adic空间）。研究结论部分翻译为：本文证明了量词完成的第一层（即量词交替深度至多为一的公式层）与自由QA一步布尔教义同构；因此，该层是自由QA一步布尔教义，而Free1P的定义通过生成元与关系给出了该层基于P的构造。