【夏素敏】无变元的一阶片段：Fluted逻辑
尽管一阶逻辑得到了广泛的探讨，但仍然存在有待发掘的丰富内容，一阶逻辑的片段研究便是其中之一。选取不同的方式可以定义出一阶逻辑的不同片段，例如对量词进行限制、对变元进行限制等。Fluted逻辑（Fluted Logic，简记为FL）是通过消去变元的方式形成的一阶片段之一。从两个方面看，这种逻辑值得关注。首先，它是既然“驯良”又“漂亮”的一阶逻辑片段，[1]“驯良”是说它既是可判定的又具有有穷模型性，“漂亮”是说它同时具备内插性和模型保持性。这些性质使得它在哲学、逻辑学甚至计算机科学等领域中将扮演越来越重要的角色。其次，FL与自然逻辑相似，FL的演绎系统可以用来模拟自然语言推理中一些有意义的部分。
从历史沿革看，FL可以视为谓词函子逻辑（Predicate Functor Logic）的副产品，[2]后者是纯谓词逻辑的一种语形变体。[3]奎因尝试通过谓词函子逻辑将一阶逻辑代数化，谓词函子逻辑是将逻辑代数化的最简单的方法，但相对于其他方法，如柱状代数、多元代数和关系代数，谓词函子逻辑却是目前研究记录最少的。[4]奎因的后期研究成果都在某种程度上与谓词函子逻辑相关，可见其重视程度。作为其副产品的FL的研究成果也不多见。本文综述FL已有的研究成果及其意义。
一
在纯谓词逻辑中去除变元，所得到的“无变元”的子逻辑即FL。所谓“无变元”有两种意义：如果一个系统中不出现作为句法实体的变元，则称这个系统是无变元的，这称为第一种意义上的“无变元”；另一方面，假如主要关注的是变元提供的方法、特别是连接子表达式的索引方法，那么，如果一个系统中不出现这些方法，则这个系统是无变元的，这称为第二种意义上的“无变元”。[5]FL的“无变元”并非简单地去掉句法上的变元，而是通过一些方法和手段将原本由变元承担的索引作用加以转移。
那么，如何做到“无变元”呢？为了对带变元的一阶逻辑进行无变元处理，奎因引入了谓词函子，[6]并逐步修订了谓词函子逻辑。[7]谓词函子逻辑为消解谓词逻辑的变元提供了一种自然而有效的方法。不同的谓词函子逻辑系统含有不同的谓词函子，但无论如何，都可分为真势函子和组合函子。一般来说，真势函子即直接对应于谓词逻辑中相应符号的算子，如“否定（Ø）”、“合取（Ù）”以及“存在量词（$）。组合函子inv、Inv、pad以及ref等作用于变元，其中inv和Inv是两个“倒置算子”，这两个算子相结合，可以对变元的顺序进行任意排序，pad是“增加算子”，ref是“自返算子”。利用这些谓词函子，便可以使每个谓词的变元的顺序恰为量词辖域内谓词的顺序，这样，便为去掉变元同时又清晰地描述了谓词逻辑中变元的作用打下了基础。例如$x$yPyxyx经过转化，成为$ ref $ ref Inv inv P。在谓词函子逻辑中，对于给定的一阶封闭公式，将其中所有谓词字母加上数字下标，标明其量词级，再将所有的全称量词转换为存在量词和否定，然后将所有形如x = y的原子公式记为Ixy，再按照相应规则（包括inv、Inv、pad以及ref的规则）对所得公式进行运算，去掉所有约束变元。[8]所得结果中，仅含有真势函子的公式构成的子逻辑就是FL。
二
在FL的公式中，每个谓词的变元的顺序恰为相应的量词辖域内谓词的顺序，因此，完全去掉变元是可能的，换言之，元数与谓词符号的空位完全可以确定跟在谓词符号后面的变元序列。不过，在句法上暂时保留变元可以使表达更清晰，只是这样的变元并不起实质作用。[9]例如，常见的例句“所有人都是会死的”，其相应的FL-公式为"(H ® D)。再看一个比较复杂的例子，“所有动物或者吃所有植物或者吃那些只吃某些植物但比自己小的动物”可以由如下FL公式表达：
"x1(Ax1 ® ("x2(Px2 ® Ex1x2)Ú∨"x2((Ax2 Ù Lx1x2 Ù $x3(Px3 Ù Ex2x3)) ® Ex1x2)))
或直接表述为
"(A ® ("(P ® E)Ú "((A Ù L Ù $(P Ù E)) ® E)))。
结合纯谓词逻辑，我们具体来看FL-公式的定义。谓词逻辑语言包括逻辑算子“否定”、“合取”、“恒真（ò）”和“存在量词”，以及一个谓词符号集和变元符号集X = {xi：i Î w}，没有常元和函数符号。谓词符号集中的元素是那些出现在某些给定的有穷公式集或前提集中的符号。基本语言及其语义可以扩充至包括一些缩写，如通常定义的“析取”，“蕴涵”，“等值”，“恒假（^）”以及“全称量词”。公式、满足、内插以及模型等句法和语义概念的定义都是标准的。另外，对于谓词符号R，ar(R)指的是R的元数。假定L为有穷的谓词符号集，Xm := {x1, …, xm}为m（m ≥ 0）个变元的有序集。在定义FL-公式前，先要定义“原子FL-公式”。L在X上的原子FL-公式为Rxm-n+1…xm，其中R Î L，ar(R) = n ≤ m。L在Xm上的所有原子FL-公式集合记为AFL(Xm)，定义AFL(X0) := {ò}。
Xm上的FL-公式集归纳定义如下：（1）Xm上的原子FL-公式是Xm上的FL-公式；（2）如果φ是xm+1上的FL-公式，那么，$xm+1φ与"xm+1φ是Xm上的FL-公式；（3）如果φ与ψ是Xm上的FL-公式，那么，φ Ù ψ，φ Ú ψ，φ ® ψ，φ « ψ与Øφ都是Xm上的FL-公式。需要注意的是，当m = 0时，X0上的FL-公式是FL-句子。定义中的FL-公式是标准的FL-公式；标准FL-公式的字母变易[10]构成的公式亦为FL-公式。
如果𝜑为标准的FL-句子，其约束变元为Xn，那么，φ的量词级qr(φ)定义为n。任意一个FL-句子的量词级即其标准的字母变易的量词级。一个FL-公式的量词级是其全称闭包的量词级。
L的FL-公式形成带谓词符号L的纯谓词逻辑公式的真子集。L的FL-公式的语义恰为纯谓词逻辑的通常语义。也可以简单地说，纯谓词逻辑的FL-公式，与纯谓词逻辑的语义结合起来，便是FL。
FL-推演系统S由公理和推演规则组成。公理是如下（1）、（2）的全称闭包：
（1）所有重言的FL-公式；
（2）量词规则：（i）$x(φ Ú ψ) « ($x φ Ú $x ψ)；（ii）$x θ « θ,其中x不在θ中自由出现。注意，在FL中，规则（2）也就是说要求θ中没有自由变元出现。
推演规则是单调性原则，有正负两种形式：假定θ为FL公式φ的正（或负）子公式，θ ® ρ（或ρ ® θ）为FL-公式，φ¢是将φ中的θ替换为ρ而得到的公式，那么由θ ® ρ（或ρ ® θ）可得φ ® φ¢。这一规则在FL中起着十分重要的作用。
对于n Î w，Sn是将S限制为量词级小于或等于n的那些FL公式，这样，Sn有两个重要的性质：有穷性和可靠性。假设G为一个FL-句子的有穷集，并设φ1，φ2，…，φk为FL-句子的序列，它们每一个或者都是G的元素（即Sn的公理），或者是将单调性原则应用于在前的元素而得到的后承。这样，φk即由演绎得出，记为⊢Sn φk。由于L为有穷的谓词符号集，因此Sn的论域是有穷的，量词级不超过n的L也就具有有穷多个标准的FL-句子。因此，⊢Sn φ是可判定的。确保FL之可判定性的正是对一阶逻辑中变元和主目排序的限制。珀迪（W. Purdy）证明，Sn既是可靠的，也是完全的。[11]
三
我们将一个既是可判定的又具有有穷模型性的逻辑系统称为“驯良的”，而将一个同时具有内插性和模型保持性的逻辑系统称为“漂亮的”。FL既是“驯良的”又是“漂亮的”。
1969年，奎因最先证明，如果一个FL-公式仅含同态合取式，即仅含元数相同的子公式的合取，那么其可满足性就是可判定的。到1990年代中期珀迪又证明了没有这种限制的FL-公式也是可判定的。对FL及其二元逆和等词的扩充中的可判定性问题，珀迪也进行了探讨[12]。他还说明，FL的可满足性的计算复杂性是NEXPTIME-完全的。[13] 施密特（R.A. Schmidt）和胡斯塔德（U. Hustadt）描述了FL的不同消解判定程序。[14] 珀迪也证明了带逻辑等词的FL也是可判定的。[15]
很自然地，我们希望知道，增加哪些组合算子，FL的扩充仍然可以保持可判定性。或者说，从FL到一阶逻辑，可判定与不可判定的界限在哪里。由于反射函子可以在带等词的FL中得到定义，因此带反射函子的FL也是可判定的。增加pad算子或ref算子形成的扩充后，其可满足性仍是可判定的，但Inv与inv两个算子的增加则会导致不可判定性。
FL的内插性和子模型保持性得到了证明：也就是说，如果φ和ψ为两个FL公式，φ ® ψ是有效的，其符号集分别为Lφ和Lψ，二者的交集不空，那么存在一个以其交集为符号集的公式θ，使得φ ® θ与θ® ψ都是有效的。如果其交集为空，那么φ有效或者其否定有效。而对于量词级为n的、一致的FL-语句φ，φ是全称的当且仅当其模型对包含于关系（子模型）封闭。[16]
与其他一阶片段相比，同时具有上述性质是FL最大的优点。通过对各种一阶片,段之间关系的研究，我们已经发现：一阶逻辑的二变元片段（FO2）与FL的复杂性相同，但FO2不是“漂亮的”；一阶逻辑的安保片段（Guarded Fragment）是“驯良的”，但也不是“漂亮的”。描述逻辑ALC可以嵌入FL，也可以嵌入安保片段、二变元片段和马斯洛夫类（Maslov’s class）K，这也就意味着三种片段的交集非空；但是我们也可以找到这样的公式，仅在某一种片段中成立，说明上述片段各有区别于其他片段的部分。两个结构可通过公式区别开来，当且仅当，这两个结构的刻画内容不同。不过需要注意的是，目前这些逻辑之间的正交性只在句法层面上被证明。
四
FL与自然语言的密切关系也是我们关注它的重要原因。
对于FL而言，变元的缺位将导致表达力的缺失。为FL添加不同的组合算子就得到相应的一个格（lattice），其中FL表达力最弱，而带等词的一阶逻辑是最具表达力的逻辑。[17]
在FL中，不能重置谓词主目的顺序，不能识别不同谓词的主目或判定相同的主目，也不能在谓词主目中加入空主目。珀迪已经证明，FL不能直接表达关系的自返性、对称性和传递性。但大多数自然语言推理可以在FL中得以表达。[18]FL及其不同扩充系统更适用于模拟自然语言推理。带等词的FL系统的可判定性已由珀迪证明，由于等词可用于定义表述指代的谓词，FL与自然逻辑的关联就更多了。自然语言中并不使用变元，在用到相互关联的子句时，可能需要用到指代介词，但这不能简单地看作变元。不含变元的形式系统都试图利用这一点。但是与FL不同，由于表达力上的局限，使得其中大部分系统重新引入了谓词函子逻辑中的组合算子，因此也就背离了自然语言。谓词演算或许并不适用于模拟自然语言推理。
FL相对于其他逻辑，更具自然性和直观性，这是一阶逻辑及其他大多数片段都不具备的。因此它同自然逻辑具有密切关系。尽管如上所述，变元的缺失会导致表达力的缩减，但FL演绎系统可用来模拟自然语言推理中某些有意义的部分并加以研究。许多可以用自然语言描述的逻辑问题，都可以在FL中得到处理，FL及其扩充到多元关系的系统为自然语言推理提供了良好的背景。以往提到的模拟自然语言的许多系统（如结构、代数和演算）都是“无变元”的，但却含有变元的替代物，因此其表达方式并非无变元的。其他很多用于模拟自然语言的系统也都不是真正无变元的，因为其中可能含有这样或那样的代理变元（surrogate variables）。所谓代理变元是指起着一部分变元作用的那些算子，例如谓词函子逻辑中的τ函子、选择算子等等，无论它们的运算方式如何，实际上都是经过伪装的变元，区别仅在于发挥作用的范围有所不同。如果在FL中增加代理变元的表达式，可以形成“扩充的FL”（Extended Fluted Logic，简记为EFL）。需要注意的是，相对于通常的逻辑算子，EFL是FOLI（带等词的一阶逻辑）的最大可判定子逻辑。
FL与描述逻辑的紧密关系是其表达力的进一步证明。描述逻辑是为表达有关概念及其谱系而量身打造的知识表示语言，也是一阶逻辑的一个可判定子集，具有完好的语义和很强的表达能力。施密特和胡斯塔德与乔治维亚（L. Georgieva）指出，描述逻辑ALC可以嵌入到FL。FL又能够将描述逻辑ALC的标准翻译推广到一阶逻辑。从描述逻辑的角度来看，这一片段也很值得研究。
对FL感兴趣的另一个原因在于它和模态逻辑的关系。模态逻辑关注无处不在的关系结构，而FL可以看成是模态逻辑的一个推广，就像安保片段那样。FL和模态逻辑共同具有的性质是可判定性和有穷模型性。从模态逻辑的角度来看，FL优于安保片段的一个方面在于关系原子可以被否定。这一特点意味着一些不能嵌入到安保片段的逻辑、其他更具表达力的模态逻辑以及描述逻辑如（不带逆的）ALB却可以嵌入到FL。更有意思的是，模态命题公式通过关系翻译和函数翻译一个变易的翻译都是FL公式。
【注释】
[1][5][13][16] W. Purdy. “Complexity and Nicety of Fluted Logic,” Studia Logica 71, 2002, pp. 177~198.
[2][15] W. Purdy. “Decidability of Fluted Logic with Identity,” Notre Dame Journal of Formal Logic 37, 1996, pp.84~104.
[3]W.V. Quine. The Ways of Paradox and Other Essays, Enlarged Edition, Harvard University Press, 1976, pp.300~302. W.V. Quine. Methods of Logic, Fourth Edition, Harvard University
[4] http: //en.wikipedia.org/wiki/Predicate_functor_logic#Footnotes
[6] W.V. Quine. “Variables Explained Away,” in Proc. American Philosophy Society, vol. 104, 1960, pp.343~347.
[7] W.V. Quine. “Algebraic Logic and Predicate Functors,” in R. Rudner and I. Scheffer (eds.), Logic and Art: Esssays in Honor of Nelson Goodman. Bobbs-Merrill, 1971. W. V. Quine. “Predicate Functors Revisited,” Journal of Symbolic Logic 46, 1981, pp. 649~652.
[8] W.V. Quine. The Ways of Paradox and Other Essays, Enlarged Edition, Harvard University Press, 1976, pp.300~302.
[9] W. Purdy., “Surrogate Variables in Natural Language,” in M. Boettner & W. Thuemmel (eds.), Variable-Free Semantics, Articulation and Language, vol. 3, 2000, University of Osnabrueck.
[10] H.B. Enderton. A Mathematical Introduction to Logic, Academic Press, 1972, pp. 118~120.
[11] http: //www.cis.syr.edu/~wcpurdy/dsfl.pdf
[12][17] W. Purdy. “Quine’s ‘Limits of Decision’,” Journal of Symbolic Logic 64, 1999, pp. 1439~1466.
[14] R.A. Schmidt & U. Hustadt. “A Resolution Decision Procedure for Fluted Logic,” in D. McAllester (ed.), Proc. CADE-17, vol. 1831 of LNAI, Springer, 2000, pp. 433~448.R.A. Schmidt, E. Orlowska & U. Hustadt. “Two Proof Systems for Peirce Algebras,” in Proc. RelMiCS-7, vol. 3051 of LNCS, Springer, 2004, pp. 238~251.
[18] F. Sommers. “The Calculus of Terms,” in G. Englebretsen (ed.), The New Syllogistic, Peter Lang, 1987, pp.11~56.
（原载《哲学动态》，2009年第4期。录入编辑：神秘岛）