无变元的一阶片段：Fluted逻辑，本文主要内容关键词为：片段论文,逻辑论文,无变元论文,Fluted论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
[中图分类号]B81[文献标识码]A[文章编号]1002-8862(2009)04-0101-04
尽管一阶逻辑得到了广泛的探讨，但仍然存在有待发掘的丰富内容，一阶逻辑的片段研究便是其中之一。选取不同的方式可以定义出一阶逻辑的不同片段，例如对量词进行限制、对变元进行限制等。Fluted逻辑(Fluted Logic，简记为FL)是通过消去变元的方式形成的一阶片段之一。从两个方面看，这种逻辑值得关注。首先，它是既“驯良”又“漂亮”的一阶逻辑片段，①“驯良”是说它既是可判定的又具有有穷模型性，“漂亮”是说它同时具备内插性和模型保持性。这些性质使得它在哲学、逻辑学甚至计算机科学等领域中将扮演越来越重要的角色。其次，FL与自然逻辑相似，FL的演绎系统可以用来模拟自然语言推理中一些有意义的部分。
从历史沿革看，FL可以视为谓词函子逻辑(Predicate Functor Logic)的副产品，②后者是纯谓词逻辑的一种语形变体。③奎因(W.V.Quine)尝试通过谓词函子逻辑将一阶逻辑代数化，谓词函子逻辑是将逻辑代数化的最简单的方法，但相对于其他方法，如柱状代数、多元代数和关系代数，谓词函子逻辑是目前研究记录最少的。④但奎因的后期研究成果都在某种程度上与谓词函子逻辑相关，可见其重视程度。作为其副产品的FL的研究成果也不多见。本文旨在综述FL已有的研究成果及其意义。
简单地说，在纯谓词逻辑中去除变元，所得到的“无变元”的子逻辑即FL。所谓“无变元”有两种意义：如果一个系统中不出现作为句法实体的变元，则称这个系统是无变元的，这称为第一种意义上的“无变元”；另一方面，假如主要关注的是变元提供的方法、特别是连接子表达式的索引方法，那么，如果一个系统中不出现这些方法，则这个系统是无变元的，这称为第二种意义上的“无变元”。⑤FL的“无变元”并非简单地去掉句法上的变元，而是通过一些方法和手段将原本由变元承担的索引作用加以转移。
在谓词函子逻辑中，对于给定的一阶封闭公式，将其中所有谓词字母加上数字下标，标明其量词级，再将所有的全称量词转换为存在量词和否定，然后将所有形如x=y的原子公式记为Ixy，再按照相应规则(包括inv、Inv、pad以及ref的规则)对所得公式进行运算，去掉所有约束变元。⑧所得结果中，仅含有真势函子的公式构成的子逻辑就是FL。
我们将一个既是可判定的又具有有穷模型性的逻辑系统称为“驯良的”，而将一个同时具有内插性和模型保持性的逻辑系统称为“漂亮的”。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的复杂性相同，但不是“漂亮的”；一阶逻辑的安保片段(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公式。
注释：
①⑤(13)(16)W.Purdy,"Complexity and Nicety of Fluted Logic," Studia Logica 71,2002,p.178,pp.177-179,pp.177-190,pp.192-198.
②(15)W.Purdy,"Decidability of Fluted Logic with Identity," Notre Dame Journal of Formal Logic 37,1996,p.84,pp.90-104.
③⑧W.V.Quine,The Ways of Paradox and Other Essays,Enlarged Edition,Harvard University Press,1976,pp.300-302,pp.300-302.W.V.Quine,Methods of Logic,Fourth Edition,Harvard University Press,1982,A.Noah,"Predicate-Functors and the Limits of Decidability in Logic," Notre Dame Journal of Formal Logic 21,1980,pp.701-707.
④http://en.wikipedia.org/wiki/Predicate_functor_logic#Footnotes.
⑥W.V.Quine,"Variables Explained Away," in Proc.American Philosophy Society,vol.104,1960,pp.343-347.
⑦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.
⑨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.
⑩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,pp.1462-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.