【刘新文】经典一阶逻辑的希尔伯特型系统
经典一阶逻辑的希尔伯特型系统Z以一类广义的谢夫竖函数为初始联结词、以存在量词为初始量词，把两者结合起来统一写成括号记法。下面按照逻辑系统研究的一般过程，首先给出系统的句法，然后给出其语义，在此基础上建立一个希尔伯特型系统（即公理系统），最后进行元理论研究，运用反模型方法证明了系统的完全性即系统中所有有效式都是可推演的。
一、句法
一阶语言L的初始符号划分成下述五类:
(1) 个体变项：x0，x1，x2，…，xn-1，…；
(2) 命题变项：p，q，r，…；
(3) 对各个自然数n，有一组n元函项符：f，g，…；
(4) 对各个正自然数n，有一组n元谓词符：P，Q，…；
(5) 逗号、分号和左右方括号： ， ； []。
定义1（项）：
(1) （个体）变项都是项；
(2) 若¦是n元函项符并且t0，…，tn-1都是项，则符¦t0…tn-1亦是项。
当n = 0时，定义1（2）表明个体常项是项。
定义2（公式）：
(1) 命题变项是公式；
(2) 如果P是n元谓词符，t0，…，tn-1（n＞0）都是项，则Pt0…tn-1是公式；
(3) 如果x0，…，xm-1是任意m（m≥0）个不相同的个体变项，b0，…，bn-1是任意n（n≥0）个公式，则[x0，…，xm-1；b0，…，bn-1]也是公式。
定义2（2）中，当P是等号时，等式＝t1t2记为t1＝t2；（3）中，当m = n = 0时，[ ]（意指恒假）是公式，称为命题常项；m =0，n =1时，[b0]称为b0的否定。
命题变项、Pt0…tn-1以及命题常项统称为原子。
公式序列b0，…，bn-1可记成Γ或Δ。公式a的复杂度dega是指出现在a中的左括号及个体变项的总数。由于括号在公式中成对出现，公式中的左括号总数也就是出现在该公式中的括号对的总数。
[b0，…，bn-1]的直接子公式是指b0，…，bn-1。
二、语义
定义3（模型）：
(1) L的一个模型是一个二元序对U=áD，Iñ，非空集D是U的个体域，外逻辑符集上的解释映射I为L的各个函项符¦指定某个n元运算¦I：Dn®D，为L的各个谓词符P指定某个n元关系PIÍDn，为L的各个命题变项p指定一个真值pI=1或pI=0。
(2) U=áD，Iñ的一个指派是指个体变项集上的一个映射d，为各个个体变项x指定某个个体xdÎD。
(3) 给定一个模型U=áD，Iñ和U中的一个指派d，L的项t的所指tI, d递归定义如下：
（i）xI, d=xd；
（ii）(¦t0…tn-1)I, d= ¦It0I, d…tn-1I, d。
若d是模型U中的一个指派，u0，…，um-1ÎD，对任意的i，j＜m，若xi=xj则ui=uj那么，d(x0/u0，…，xm-1/um-1)是指除在x0，…，xm-1处的值分别为u0，…，um-1外而与d有相同的指派。
定义4：设U是一个模型，d是U中的一个指派。公式a相对于U和d的真值aI, d的递归定义如下：
（1）pI, d=pI；
（2）(Pt0…tn-1)I, d=1，当且仅当，át0 I, d，…，tn-1I, dñÎPI；
（3）([x0，…，xm-1；b0，…，bn-1])I, d=1，当且仅当，有u0，…，um-1ÎD和某个i＜n使得(bi) i,δ（x0/u0,L，xm-1/um-1）=0。
定义5：
（1）若对U中的任一指派d都有aI, d=1，则称a在U中为真；
（2）若a在L的任一模型中都为真，则称a为有效式。
（3）若U中的某个指派d对于公式集G中的任一公式都有aI, d=1，则称G为在U中可满足；G在某个模型周可满足时，称G为可满足的。
（4）对于任意模型U=áD，Iñ和U中的任一指派d，若在d的指派下G中公式都在U中为真，则在d的指派下a也在U中为真，那么称a为G的逻辑后承。
三、希尔伯特型系统
定义6（原子析舍）：
若a的直接子公式都是命题变项或命题变项的否定，Pt0t1…tn-1或其否定[Pt0t1…tn-1]，或者命题常项[ ]，则称a为原子析舍。
定义7（Z的公理）：
（1）含有[ ]为直接子公式的原子析舍；
（2）含有某个命题变项及其否定，或者Pt0t1…tn-1及其否定为直接子公式的原子析舍；
（3）[[t＝t]]；
（4）[t0＝s0，…，tn-1＝sn-1，[¦t0…tn-1＝¦s0…sn-1]]；
（5）[t0＝s0，…，tn-1＝sn-1，Pt0…tn-1，[Ps0…sn-1]]。
在系统Z中引进称为参变项的个体变项a0，…，ai-1，…。
Z的推证规则称为构树规则。非形式地，树由分枝构成，分枝依据规则中从结论到前提的顺序向上生长，所有分枝得以开始的公式称为该公式的树根。当碰到公理时，分枝的生长就停止，否则按两个规则分别继续向上生长。树根为a的树称为a的推演树。系统中每一个可推演的公式的证明过程就是按照从上到下的顺序把推演树中所有的公式写成线性形式。这一过程是能行的。
定义8（Z的推证规则）：
（1）从[Γ，[α0{x0/a0，…，xm-1/am-1}]，Δ]，……，[Γ，[αn-1{x0/a0，…，xm-1/am-1}]，Δ]推出[Γ，[x0，…，xm-1；α0，…，αn-1]，Δ]，其中，a0，…，am-1是还未用到的m个参变项，m³0，n³2；
（2）从[Γ，α0{x0/a0，…，xm-1/am-1}，……，αn-1{x0/a0，…，xm-1/am-1}，Δ]推出[G，[[x0，…，xm-1；α0，…，αn-1]]，D]，其中，a0，…，am-1是该分枝中下面没有用到的参变项，m³0，n³0。
四、完全性定理
定理9（可靠性）：
如果一个推演树的所有分枝都终止于公理，那么树根上的公式为有效式。
证明：公理都是有效式，规则保持有效。□
推演树中，不终止于公理的分枝称为败枝。败枝中任一公式的直接子公式都可能为真。因此，如果某个分枝不终止于公理，那么可以利用该分枝来构造作为树根的公式的反模型，即为各个参变项指定个体的一个个体指派，使得该公式为假。
定义10（完全正规分枝）：
一个分枝B是a的推演树中的一个完全正规分枝，仅当，a是B的第一个成员a1，并且对B中的各个ai，有
（ⅰ）若ai是原子析舍，则ai是B的终点；否则
（ⅱ）ai有形式[G，β，D]，其中，β不是命题变项或命题变项的否定，Pt0t1…tn-1或其否定[Pt0t1…tn-1]，或者命题常项[ ]，并且：
（1）若β=[x0，…，xm-1；β0，…，βn-1]，则ai+1是
[G，[βj{x0/a0，…，xm-1/am-1}]，D]，0£j£n-1；
（2）若β=[[x0，…，xm-1；β0，…，βn-1]]，则ai+1是
[G，β0{x0/a0，…，xm-1/am-1}，…，βn-1{x0/a0，…，xm-1/am-1}，D]。
公式a是一个分枝B的一个直接子公式，是指a是B中某公式的一个直接子公式。
引理11：
如果B是A的一个完全正规分枝，并且B不终止于公理，那么，若一原子β的否定[β]是B的一个直接子公式，则β不是B的直接子公式。
证明：B不终止于公理，所以B是一个败枝。从A出发败枝向上生长的每一步都不会漏失原子或原子的否定，在败枝的每一个公式[G，a，D]中，它们或是a，或是属于G，或是属于D。这样，如果[β]作为直接子公式在B中某公式处出现，而且以后B中某公式处又出现作为直接子公式的β，则[β]和β作为直接子公式都会出现在B的终点公式中，从而得到一个公理，这与B不终止于公理矛盾。□
引理12：
设B是不终止于公理的一个完全正规分枝。那么，
（1）如果[x0，…，xm-1；α0，…，αn-1]是B的直接子公式，则有i ，0£ i £n-1，使得
[αi{x0/a0，…，xm-1/am-1}]
是B的直接子公式；
（2）如果[[x0，…，xm-1；α0，…，αn-1]]是B的直接子公式，则对所有i ，0£ i £n-1，有
αi{x0/a0，…，xm-1/am-1}
是B的直接子公式。
证明：由定义10（ii）而得。□
假定公式α的推演树中有一个败枝B，我们构造一个模型U =áD，Iñ：
（1）D={0，1，2，…，n，…}；
（2）pI=T（真），当且仅当，p是B的直接子公式；
（3）对于每一个参变项ai，指定自然数i为其值，i=0，1，2，…；
（4）对于每一个n元谓词符P，指定如下确定的n元自然数函数：
（a）<i1，…，in>映成T，仅当，Pa0…an-1是B的直接子公式；
（b）<i1，…，in>映成F（假），仅当，[Pa0…an-1]是B的直接子公式。
定理13（完全性）：
如果B是公式α的一个完全正规分枝且不终止于公理，那么，上述模型将使B中任一直接子公式为真，从而α为假。
证明：假设B中长度小于n的直接子公式都为真。下面分别证明B中所有直接子公式都为真。
（1）若p或Pa0…an-1是B的直接子公式，则所指定的真值为T；若[p]或[Pa0…an-1]是B的直接子公式，则依据引理10，p和Pa0…an-1不是B的直接子公式，从而被指定为F，所以，[p]或[Pa0…an-1]的真值为T。
（2）若[x0，…，xm-1；α0，…，αn-1]是B的直接子公式，则由引理11和归纳假设，可知某个[αi{x0/a0，…，xm-1/am-1}]的真值为T，所以，[x0，…，xm-1；α0，…，αn-1]的真值为T。
（2）若[[x0，…，xm-1；α0，…，αn-1]]是B的直接子公式，则由引理11和归纳假设，可知所有αi{x0/a0，…，xm-1/am-1}的真值为T，所以，[[x0，…，xm-1；α0，…，αn-1]]的真值为T。
所以，系统的每一个有效式都是可推演的。□
【参考文献】
A.R. Anderson & N.D. Belnap, JR.. “A Simple Treatment of Truth Function”, The Journal of Symbolic Logic, 1959(4), 301-302；
H.B. Enderton. A Mathematical Introduction to Logic. Academic Press,Inc.,1972；
M. Fitting. First Order Logic and Automated Theorem Proving, 2nd edition, Springer Verlag, 1996；
G. Hunter. Metalogic: an Introduction to the Metatheory of Standard First Order Logic, Macmillan and Co. Ltd., 1971；
A.S. Troelstra & H. Schwichtenberg. Basic Proof Theory, 2nd edition, Cambridge University Press, 2000；
宋文淦：《符号逻辑基础》，北京师范大学出版社，1993年；
刘新文：“以广义析舍和存在量词为初始符号的一阶系统”，《哲学研究》（逻辑学专刊），2003年；
张清宇：“不用联结词和量词的一阶逻辑系统”，《哲学研究》，1996年第5期；
张清宇：“经典命题逻辑的一个公理系统”，《哲学研究》，1997年第8期；
张清宇、郭世铭、李小五：《哲学逻辑研究》，社会科学文献出版社，1997年。
（原载《湖南科技大学学报，2005年第2期。录入编辑：神秘岛）