经典一阶逻辑的希尔伯特型系统，本文主要内容关键词为：希尔伯特论文,逻辑论文,经典论文,系统论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：O141 文献标识码：A 文章编号：1672-7835(2005)02-0027-03
1 句法
一阶语言L的初始符号划分成下述五类[1～2]：
(1)个体变项：x[,0]，x[,1]，x[,2]，…，x[,n - 1]，…；
(2)命题变项：p，q，r，…；
(3)对各个自然数n，有一组n元函项符：f，g，…；
(4)对各个正自然数n，有一组n元谓词符：P，Q，…；
(5)逗号、分号和左右方括号：，；[ ]。
定义1(项)：
(1)(个体)变项都是项；
(2)若f是n元函项符并且t[,0]，…，t[,n - 1]都是项，则符ft[,0]…t[,n - 1]亦是 项。
当n = 0时，定义1(2)表明个体常项是项。
定义2(公式)：
(1)命题变项是公式；
(2)如果P是n元谓词符，t[,0]，…，t[,n - 1](n＞0)都是项，则Pt[,0]…t[,n - 1] 是公式；
(3)如果x[,0] ，…，x[m - 1]是任意m(m≥0)个不相同的个体变项，β[，0]，…，β[,n - 1]是任意n(n≥0)个公式，则[x[,0]，…，x[,m - 1]；β[,0]，…，β[,n - 1] ]也是公式。
定义2(2)中，当P是等号时，等式 = t[,1]t[,2]记为t[,1] = t[,2]；(3)中，当m = n = 0时，[ ](意指恒假)是公式，称为命题常项；m = 0，n = 1时，[β[,0]]称为β[,0]的否定。
命题变项、Pt[,0]…t[,n - 1]以及命题常项统称为原子。
公式序列β[,0]，…，β[,n - 1]可记成Γ或△。公式α的复杂度degα是指出现在α中的左括号及个体变项的总数。由于括号在公式中成对出现，公式中的左括号总数也就是出现在该公式中的括号对的总数。
(3)给定一个模型U = (D，I)和U中的一个
Z′的推证规则称为构树规则。非形式地，树由分枝构成，分枝依据规则中从结论到前 提的顺序向上生长，所有分枝得以开始的公式称为该树的树根。当碰到公理时，分枝的 生长就停止，否则按两个规则分别继续向上生长。树根为α的树称为α的推演树。
定义8(Z′的推证规则)：
定理9(可靠性定理)：
如果一个推演树的所有分枝都终止于公理，那么树根上的公式为有效式。
证明：公理都是有效式，规则保持有效。□
推演树中，不终止于公理的分枝称为败枝。败枝中任一公式的直接子公式都可能为真 。因此，如果某个分枝不终止于公理，那么可以利用该分枝来构造作为树根的公式的反 模型，即为各个参变项指定个体的一个个体指派，使得该公式为假。
定义10(完全正规分枝)：
一个分枝B是α的推演树中的一个完全正规分枝，仅当，α是B的第一个成员α[,1]，并且对B中的各个α[,i]，有
(i)若α[,i]是原子析舍，则α[,i]是B的终点；否则
公式α是一个分枝B的一个直接子公式，是指α是B中某公式的一个直接子公式。
引理11：
如果B是A的一个完全正规分枝，并且B不终止于公理，那么，若一原子β的否定[β]是B的一个直接子公式，则β不是B的直接子公式。
证明：B不终止于公理，所以B是一个败枝。从A出发败枝向上生长的每一步都不会漏失 原子或原子的否定，在败枝的每一个公式[Γ，α，△]中，它们或是α，或是属于Γ，或是属于△。这样，如果[β]作为直接子公式在B中某公式处出现，而且以后B中某公式处又出现作为直接子公式的β，则[β]和β作为直接子公式都会出现在B的终点公式中，从而得到一个公理，这与B不终止于公理矛盾。□
引理12：
设B是不终止于公理的一个完全正规分枝。那么，
(3)对于每一个参变项α[,i]，指定自然数i为其值，i = 0，1，2，…；
所以，每一个有效式都是可证的。□
收稿日期：2004-12-09