【刘新文】论命题与括号

从1995年开始，张清宇在《哲学研究》上发表了一系列的论文，为经典命题逻辑提出了一种括号记法并做了较系统的研究。在这一记法中，括号兼具了命题联接词的作用：给定任意有限多个命题，可以把它们并置起来成为一个序列并在这个序列的两端加上一对括号以构造出一个形如“[A, B, ¼, C]”的新命题，这一命题的直观意思是说，括号中的这有限多个命题并非都为真，也就是说，至少有一个为假，当然也可以全部为假。所以，这里定义的是一类广义的“谢弗函数”，或者说任意有穷元的析舍联结词；包括零元的在内，它由一类而不是一个联结词组成。全部广义析舍形成真值联结词的一个元数递增的无穷序列，因此在张清宇所建立的系统中实际上有无穷多个初始联结词，这跟通常只用有穷多个初始联结词的做法是很不一样的；这一记法在谓词逻辑中还可以兼具量词的作用。

我们的工作将基于张清宇提出的括号记法之上在经典命题逻辑范围内再对谢弗函数做一些研究，初步探讨两个系列的命题逻辑系统，它们全部以广义析舍为初始联结词，其中一个系列是基于[ ]-记法之上的，另外一个则是基于[ ]-记法的变异——{}-记法——之上的。在提出一系列前后相继的{}-记法的希尔伯特型系统之后，给出重言式类的一个递归的句法刻画，以作为这些系统的一个直接的推论。

一  括号记法的句法和语义

一、句法

我们所用语言的初始符号一共有两类，左括号“[”和右括号“]”，以及可数无穷多的命题变元字母，用p、q和r等作为命题变元的元变元。公式是指这些符号所构成的有穷序列，可以用Backus-Naur形式递归地定义如下：对于n ³ 0，

WFF  ::=  p  |  [A₀, ¼, A_{n - 1}]

作为公式的命题字母也称为“原子命题”、“原子公式”或者直接就叫“原子”，而不是原子命题的公式则称为“分子命题”、“分子公式”或者直接就叫“分子”；在公式的定义中，当n = 0时，表明空的括号“[ ]”也是我们语言中的公式。现在定义“直接子公式”这个概念如下：（1）原子命题没有直接子公式；（2）[A₀, ¼, A_{n - 1}]的直接子公式刚好就是A₀，…，A_{n - 1}。如果A是B的直接子公式，那么我们写成“A Î B”；这里的符号“Δ与后面用作集合论符号的“Δ是相同的，但在清楚说明的情况下不至于引起混淆。更一般地说，一个公式A是公式B的“子公式”（表示成“A Î^* B”），是说存在一个公式序列C₀，…，C_{m – 1}（m ³ 0），使得A = C₀ Î … Î C_{m – 1} = B。

二、语义

一个“句子赋值”是一个从原子公式集合到集合{1，0}的映射。V ö A，即“句子A在句子赋值V下为真”，递归地定义如下：

（1）       V ö p，当且仅当，V(p) = 1；

（2）       V ö [A₀, ¼, A_{n - 1}]，当且仅当，存在某个公式A_i（0 £ i £ n - 1），并非V ö A_i。

如常所说，如果V ö A，就说公式A在句子赋值V下为真；如果A在每一个句子赋值下都为真，就说A是有效的或重言式，记为ö A。对于公式集合G以及公式A，A是G的“后承”，记为G ö A，是说没有任何赋值使得G中每一个元素为真而使得A为假。由于我们刚刚定义的命题联结词是析舍联结词的推广，因此它是真值函项完备的；为增加直观起见，通常的联结词可以定义如下，其他联结词的定义参见（张清宇，1997年）：

ØA	:=	[A]
(A0 Ú ¼ Ú An - 1)	:=	[[A0], ¼, [An - 1]]
(A0 Ù ¼ Ù An - 1)	:=	[[A0, ¼, An - 1]]
A ® B	:=	[A, [B]]
^	:=	[ ]
T	:=	[[ ]]

由此，我们也可以说公式[A]是公式A的否定。

三、历史注记

自从弗雷格（G. Frege）在1879年提出经典命题逻辑的公理系统以来，对命题演算的变种的研究就开始兴盛起来，其中一个主要领域就是关注命题逻辑的可替代的公理集合以及这些系统内的形式证明，这一传统由卢卡西维茨（J. Łukasiewicz）及其同事在20世纪早期开创，由莱蒙（E.J. Lemmon）等继承到20世纪下半叶；在这个传统中，对只包含一个联结词如析舍联结词的逻辑系统给予过特别的兴趣。

二元的“析舍联结词”（一般也称为谢弗竖，写成“|”）及其对偶“合舍联结词”（写成“¯”）由谢弗（H.M. Sheffer）于1913年发表的论文中提出，并证明了其函项完全性。1917年，尼科（J.G.P. Nicod）建立了以析舍为初始联结词的、只由一条公理和一条规则组成的系统，涅尔夫妇在《逻辑学的发展》中专门评述了这一系统；1929、1932年，瓦伊斯贝格（M. Wajsberg）和卢卡西维茨分别对这一系统做了进一步研究。1920年，肖菲克尔（M. Schönfinkel）用单个记号“|^x”来发展谓词演算，“fx |^x gx”表示的是“(x).Øf(x) Ú Øg(x)”；这是组合逻辑的起源。在莱蒙等人的影响下，20世纪60、70、80年代，关于谢弗竖的研究涌现出大量文献，多值逻辑、模态逻辑、直觉主义逻辑等领域类似于经典谢弗竖的成果也得到了研究；其中，沙莱（Scharle，1966）为比析舍词更为复杂的合舍词提出过只有一条公理和一条规则的公理系统。2006年，卡品科（Karpenko，2006）概述了多值逻辑的谢弗竖成果应用到素数的研究中。从掌握的文献来看，除了数理逻辑之外，还有布尔代数、自动定理证明这两个领域沿着谢弗1913年的工作在进行研究（参见：Veroff，2003；Łukaszuk & Grabowski，2004；McCune，Padmanabhan，Rose & Veroff，2005）。

张清宇提出的[ ]-记法表示的是广义的析舍联结词，1997年提出的系统Z是对1959年安德森（A.R. Anderson）和贝尔纳普（N.D. Belnap, Jr.）提出的经典命题逻辑的公理系统（1971年被亨特尔（G. Hunter）命名为AB）的一个改进；系统AB以否定和析取为初始联结词，而系统Z中联结词的个数是可数无穷的。关于谢弗竖运算、单个足够的命题联结词及其演算系统的研究在国内还有一些研究成果（参见Yang，2000；宋文淦，2000；杜国平，2000；刘新文，2003，2005）。

二  [ ]-记法系统

我们将在本节中给出的是基于[ ]-记法之上的公理系统，在这一系列中将包含两个系统，系统Z与Z¢。

一、系统Z

为了讨论方便，我们首先简要介绍张清宇在1997年提出的命题逻辑系统Z。如果一个公式的直接子公式都是公式[ ]、命题变元或者命题变元的否定，则称该公式为原子析舍。例如，[[ ]]，[p, [q]]和[p, q, r]等公式都是原子析舍。公理系统Z由两条公理（模式）和两条推演规则组成。两条公理是说：（1）凡是有[ ]为直接子公式的原子析舍都是公理；（2）凡是有某个命题变元及其否定同时为直接子公式的原子析舍也都是公理。对于m、k ≥ 0，两条推演规则为：

I.	[B0, …, Bm - 1, A0, …, An - 1, C0, …, Ck - 1]	，n ≥ 0
	[B0, …, Bm - 1, [[A0, …, An - 1]]，C0, …, Ck - 1]
II.	[B0, …, Bm - 1, [A0], C0, …, Ck - 1]，…，[B0, …, Bm - 1, [An - 1], C0, …, Ck - 1]		，n ≥ 2
	[B0, …, Bm - 1, [A0, …, An - 1], C0, …, Ck - 1]

我们将会在后面特别注意这两条规则中的边款，尤其是规则II中的边款，即规则中的两个条件“n ≥ 0”和“n ≥ 2”。系统Z是可靠的和完全的，分离规则和双重否定规则在其中都不成立。特别值得注意的是Z中内定理的证明。在通常的公理系统中，要想找出一个公式证明，一般来说不是一件十分容易的事，有时还是很难的。但是，在系统Z中寻求一个公式的证明，却是一件机械性很强的工作：每一个重言式都有一个有穷的树形证明；具体叙述参见（张清宇，1997年）。1999年，张清宇为系统Z提出了一种“析舍范式”并基于公理系统之上证明了Z的内插定理。

二、系统Z¢

现在提出的系统Z¢将只有一条规则，系统中的推演以有限树的形式出现，树根是将要推演或者证明的公式，而其每个节点都将用公式来标记。按照这条规则，树的生长从下到上进行：

任意一个分子公式A = [A₀, ¼, A_{n – 1}]及其直接子公式都将作为树的某个顶点的n + 1个直接后继。

这一规则可以粗略地图示如下：

[A₀, ¼, A_{n - 1}]  A₀   ¼  A_{n - 1}

推演的直观想法是，如果意欲推演或者证明的公式为假，那么根据语义解释，至少有一个前提为假，而树的分枝是分情况讨论，不管如何，[A₀, ¼, A_{n - 1}]及其所有的子公式A₀，…，A_{n – 1}中总有一个为假。对这一系统的研究暂且只到这里，更为详细的工作留在以后再做。

三  命题逻辑的递归枚举

根据亨德力和马赛（Hendry & Massey，1969，pp. 288-289）提出的概念，主目数固定的联结词称为“单级联结词（unigrade connective）”，而可以应用到任意有穷多个主目的联结词则称为“多级（multigrade）联结词”；形式语言中，根岑型系统带某些限制的“®”就是多级的。在非形式数学和普通语言中，多级联结词可以找到大量例子，最简单的莫过于集合构造算子“{…}”和n元序组构造算子“á…ñ”。张清宇以[ ]-记法进行研究的“广义析舍”也属于多级联结词。

在前面我们知道，公式[A₀, ¼, A_{n – 1}]为真当且仅当由它的直接子公式所组成的公式集合{A₀, ¼, A_{n - 1}}是不协调的；另外，当n = 0时，也就是说当公式序列A₀，…，A_{n – 1}为一个空序列时，公式[A₀, ¼, A_{n – 1}]就“退化”为空的括号，即公式[ ]，这也合乎集合论中“空集”概念的定义。由此，我们把集合构造算子引入形式语言，直接把公式集合{A₀, ¼, A_{n - 1}}就看作是一个公式，从语义上讲，作为公式的符号序列{A₀, ¼, A_{n - 1}}为真当且仅当作为公式集合的{A₀, ¼, A_{n - 1}}是不协调的。这样，引入集合构造算子“{…}”来替换掉前面用到的方括号“[ ]”记法还使得命题中的括号可以再兼具集合括号的作用，同时带来一些有意思的问题。现在的句法除了括号被替换掉之外，与[ ]-记法的句法是一样的；两种括号都是广义析舍的记法，当然语义解释也是一样的。具体来讲，现在用{A₀, ¼, A_{n – 1}}来替换原来的[A₀, ¼, A_{n – 1}]，它是说，任意一个有穷的公式集合也都是公式。公式的元变元用A，B，C等字母来表示。一些约定：

1、不是原子公式的公式称为分子。

2、如果A Î B，那么称A是B的直接子公式；这里的符号“Δ将是集合论意义上的“属于”符号，此后也将在这个意义上使用。

3、如果有一个公式序列C₀，…，C_{m - 1}使得C₀ Î … Î C_{m - 1}，那么C₀是C_{m - 1}的子公式。

另外，一个将要用到的、非常重要的概念是公式的“复杂度”；公式A的复杂度（记为deg(A)）定义为：

（1）       deg(p) = 0；

（2）       deg({A₀, ¼, A_{n - 1}}) = deg(A₀) + … + deg(A_{n - 1}) + 1。

有了上述概念上的准备，我们来研究一系列的形式系统及其推论。

一、公理系统（一）

公理系统（一）由一条公理和两条规则组成。

1.       公理模式：A È {A}。

2.       推演规则：（1）从A可以推出A È B；（2）从A È B和A È {B}可以推出A。

这里用到的并集符号“È”并非我们的形式语言。一个具体的公理将具有下述形式：{{}}，{p, {p}}，{p, q, {r}, {p, q, {r}}}，等等，因为

{{}}	:=	{} È {{}}
{p, {p}}	:=	{p} È {{p}}
{p, q, {r}, {p, q, {r}}}	:=	{p, q, {r}} È {{p, q, {r}}}

这里的公理{p, q, {r}, {p, q, {r}}}不是系统Z的公理；相反，{p, {p}, q, r}在这里不是公理，但在系统Z中是。一般地说，这里的每一条具体公理都是以一个集合的元素以及这个集合本身作为元素的集合；因为系统Z的公理都是原子析舍，其直接子公式都是[ ]、命题变元以及命题变元的否定，所以只有当公理模式A È {A}中的A为空集或者仅以某命题变元为元素的单元素集合时，每一条具体公理才是系统Z的公理，当然，这些公理也只是Z的一部分公理而非全部，此时的公理就是两个系统中共同的公理。

一个推演是一个有穷的公式序列A₀，A₁，…，A_{n - 1}，使得对于任意的i（0 £ i £ n - 1），A_i是公理模式A È {A}的一条具体公理、或者是由此前的某个公式按照规则（1）得到、或者是由此前的某两个公式按照规则（2）得到。公式C的一个证明是一个以C为最后一个元素的推演；如果这样一个证明存在，我们写作ð₁ C，这里的下标1表示公理系统（一），此后的下标与此类似。

二、公理系统（二）

公理系统（一）中的第一条规则是说，从A可以推出A È B。如果我们把这条规则中的A直接看成是形如C È {C}的公式，那么也可以把公理系统（一）中的这条规则和它的公理组合成一条公理，由此我们得到现在的公理系统。这一公理系统由这样得到的一条公理和原来剩下的一条推演规则组成：

1.       公理模式： C È {C} È B。

2.       推演规则：从B È C和B È {C}可以推出B。

当公理中的B为空集时，我们又回到了公理系统（一）的公理，即C È {C}。从直观上讲，公理和规则在下述意义上是互补的。公理反映的事实是C必须包含一个假的元素或者它本身为假，无论哪种情况，这个假的元素或者C本身都会作为整个公理的元素而使得公理本身为真。而规则是说，对于任意一个公式C来说，B È C和B È {C}都真意味着C有一个假的元素和C本身为假这两者不能同时成立，同时B的元素和C的元素组合而成的集合以及B的元素和C本身组合而成的集合都包含假的元素，既然如此，我们可以知道B中一定包含了假的元素，从而可以得知B本身为真。既然公理为真，而且规则保持真，由此我们也可以得到公理系统（二）的可靠性定理。公理系统（一）的公理A È {A}的真是明显的，所以我们也得到公理系统（一）的可靠性定理。一个逻辑系统的可靠性证明一般都比较简单，而其完全性证明相对来讲复杂一些。如果证明了公理系统（二）的完全性，那么公理系统（一）的完全性就可以作为推论而得到（关于形式系统的可靠性和完全性问题的论述，参阅余俊伟，2005年）。

三、公理系统（三）

在系统Z中我们已经提到其推演规则中的边款问题，特别是其第二条规则的边款：其实在那里也可以用n ³ 0替换掉n ³ 2；当n = 1时，相当于说从公式C可以推出C来，这是没有问题的；而当n = 0时，此时m、k都必须都为0，这时候，前提中将没有任何前提出现，即空的前提，我们就可以从空的前提得到[[ ]]，即T，恒真式，而从公理的定义中可知这是Z的公理——它是原子析舍又以[ ]为直接子公式。这样一来，公理和规则仿佛缠绕在一起；当然，公理系统（二）已经这样实现过一次了。根据这一思路，我们现在也可以再次考虑公理系统（二）的公理，以期系统中公理和规则的数目更少。下面所得到的是公理模式和推理规则合二为一的推理系统：这样的系统也是一个希尔伯特型系统，因为抽象地来讲，一个希尔伯特演算是一个序对H = áC，Rñ，使得C是一个字母表（signature），R是一个推理规则集合即由序对áD，yñ构成的集合，其中D是一个C-公式集合，y是一个C-公式；当D = Æ时，推理规则是一条公理，否则称为一条规则（Carnilli，etc，2008，p. 9）。

公理模式/推理规则：从n个公式A È B È C₀，…，A È B È C_{n - 1}可以推出单个公式A È B È {B È {C₀，…，C_{n - 1}}}。其中，当n = 0时，得到的就是系统的公理A È B È {B}。

现在来看这个系统是否是可靠的和完全的。对于可靠性定理，只要证明规则是保真的就可以了，也就是说，只要证明保持下述性质就可以了：包含至少一个假的元素。假设对于0 £ i £ n - 1，A È B È C_i都包含着一个假的元素——这样才能使得各个前提都为真。现在只需要考虑两种情况：（1）在各个A È B È C_i中，如果A È B中有一个假的元素，那么作为结论的A È B È {B È {C₀，…，C_{n - 1}}}中也有一个假的元素。否则（2）A È B中的元素都为真，这就要求各个C_i中都至少包含一个假的元素才能使得各个前提为真，此时各个C_i也都为真；这样一来，由于B中的元素都为真，各个C_i也都为真，所以B È {C₀，…，C_{n - 1}}只包含真的元素，使得B È {C₀，…，C_{n - 1}}本身为假；而B È {C₀，…，C_{n - 1}}本身又是结论A È B È {B È {C₀，…，C_{n - 1}}}中的一个元素。

完全性定理的证明通过对公式的复杂度进行归纳来完成。对于任意命题S，如果deg(S) = 0，即S是一个原子，条件明显成立。如果deg(S) > 0，那么假设对于任意命题Q，deg(Q) < deg(S)并且Q对条件成立。那么第一种情形是：S的每一个分子元素都有一个原子元素而这个原子元素不是S的元素。对于每一个原子p，定义

V(p)  =		1，p Î S；
		0，p Ï S。<,/SP,AN>

不失一般性，考虑一个任意的公式D Î S。如果D是原子，那么由语义解释和上述定义可知V ö D。如果D是一个分子，那么有一个原子p Î D使得V û p。这样一来，可以得到V ö D。因此V û S。

现在来看第二种情形。存在某个分子D Î S使得D中的每一个原子元素都是S的元素。令A = S - {D}，B是D中所有原子元素组成的集合，{C₀，…，C_{n - 1}}是D中所有分子元素组成的集合。这里还要考虑两种情形：（1）对于某个赋值V和某个i（0 £ i £ n - 1），V û A È C_i。那么在V下A的每一个元素都为真，C_i的每一个元素都为真。C_i的每一个元素都为真使得C_i本身为假；因此D有一个假的元素使得D本身为真；因此S = A È {D}只有真的元素，从而使得S在V下为假。（2）对于每一个i（0 £ i £ n - 1）都有ö A È C_i。根据定义，B È {C₀，…，C_{n - 1}} = D Ï A，由此，对于每一个i，deg(A È C_i) < deg(A È {B È {C₀，…，C_{n - 1}}}) = deg(A È {D}) = deg(S)。这样就可以用到复杂度。由归纳假设，有ð₃ A È C_i。由于B是D中所有原子元素组成的集合，B Í S = A È {D}，D又是分子，可以得到B Í A。所以，对于每一个i（0 £ i £ n - 1）都有ð₃ A È B È C_i；所以根据规则可以得到ð₃ A È B È {B È {C₀，…，C_{n - 1}}} = A È {D} = S。这就证明了公理系统（三）的完全性。

四、命题逻辑的递归枚举

在公理系统（三）的完全性证明中，惟一一次用到规则的地方是证明的最后一步（2）：A、B、C₀，…，C_{n - 1}都出现了且B È {C₀，…，C_{n - 1}} Ï A。所以，对公理系统的公理/规则再加上这一点作为边款以为限制的话同样可以得到一个公理系统（四）：

公理模式/推理规则：从n个公式A È B È C₀，…，A È B È C_{n - 1}可以推出单个公式A È B È {B È {C₀，…，C_{n - 1}}}，其中B È {C₀，…，C_{n - 1}} Ï A。当n = 0时，我们得到系统的公理A È B È {B}。

现在对这一系统做一些讨论以期得到经典命题逻辑的一个递归枚举。如果ð₄ S，那么有一些公式A、B、C₀，…，C_{n - 1}，使得：（1）S = A È B È {B È {C₀，…，C_{n - 1}}}，（2）B È {C₀，…，C_{n - 1}} Ï A，（3）对于每一个i（0 £ i £ n - 1），都有ð₄ A È B È C_i。推广这一点，可以得到这样一个判断：如果ð₄ S，那么存在某个分子D Î S使得D - S中的每一个元素W都有ð₄ (S - {D}) È W。例如，D = B È {C₀，…，C_{n - 1}}。反过来，假设存在某个分子D Î S使得D - S中的每一个元素W都有ð₄ (S - {D}) È W，令D - S = {C₀，…，C_{n - 1}}，S - {D} = A，(S - {D}) Ç D = B。那么由假设有：对于每一个i（0 £ i £ n - 1）都有ð₄ A È B È C_i。由于B È {C₀，…，C_{n - 1}} = D Ï A，根据公理系统（四）的规则可得到：

ð₄ A È B È {B È {C₀，…，C_{n - 1}}} = (S - {D}) È {D} = S

所以，在这些讨论的基础上，直接就可以得到下述推论——经典命题逻辑没有公理和推演规则的递归枚举：

推论1：对于任意一个公式A，ð A仅当存在一个分子B Î A使得对于每一个C Î B - A都有ð (A - {B}) È C。

这个定义是良定义的：定义项(A - {B}) È C的复杂度总是小于被定义项A的复杂度。因为公理系统（四）是可靠的和完全的，所以，这一递归枚举的可靠性和完全性定理就等价于：ð A当且仅当ð₄ A；而这一点已经在上述讨论中证明了，也就是说：ð A当且仅当ö A。

 

【参考文献】

Anderson, A.R. & N.D. Belnap, Jr., 1959: “A Simple Treatment of Truth Function,” Journal of Symbolic Logic 24(4), pp. 301-302.

Carnilli, W., Coniglio, M., Gabbay, D.M., Gouveia, P. & C. Sernadas, 2008: Analysis and Synthesis of Logics, Springer.

Hendry, H.E. & G.J. Massey, 1969: “On the Concepts of Sheffer Functions,” in The Logical Way of Doing Things, K. Lambert (ed.), Yale University Press.

Hunter, G., 1971: Metalogic, Macmillan and Co. Ltd..

Karpenko, A.S., 2006: Łukasiewicz’s Logics and Prime Numbers, Beckington, U.K.: Luniver Press.

Lemmon, E.J., Meredith, C.A., Meredith, D., Prior, A.N. & I. Thomas, 1969: “Calculi of Pure Strict Implication,” in Philosophical Logic, J.W. Davis (ed.), D. Reidel.

Łukaszuk, A., & A. Grabowski, 2004: “Short Sheffer Stroke-Based Single Axiom for Boolean Algebras,” Formalized Mathematics 12(3), pp. 363-369.

McCune, W., Padmanabhan, R., Rose, M. A. & R. Veroff, 2005: “Automated Discovery of Single Axioms for Ortholattices,” Algebra Universalis 52(4), pp. 541-549.

Meredith, C.A., 1953: “Single Axioms for the Systems (C, N), (C, 0), and (A, N) of the Two-Valued Propositional Calculus,” Journal of Computing Systems 1(3), pp. 155-164.

Meredith, C.A., 1969: “Equational Postulates for the Sheffer Stroke,” Notre Dame Journal Formal Logic 10(3), pp. 266-270.

Scharle, T.W., 1966: “Single Axiom Schemata for D and S,” Notre Dame Journal Formal Logic 7(4), pp. 344-348.

Schönfinkel, M., 1924: “On the Building Blocks of Mathematical Logic,” in From Frege to Gödel, J. van Heijenoort (ed.), Harvard University Press, 1967, pp. 355-366.

Sheffer, H., 1913: “A Set of Five Independent Postulates for Boolean Algebras, with Application to Logical Constants,” Transactions of the American Mathematical Society 14(4), pp. 481-488.

Veroff, R., 2003: “A Shortest 2-Basis for Boolean Algebra in Terms of the Sheffer Stroke,” Journal of Automatic Reasoning 31(1), pp. 1-9.

Yang, A.Z., 2000: “Six Classes of Sheffer’s Stroke,” 载《摹物求比》，中国社会科学院哲学所逻辑室 编，社科文献出版社。

杜国平，2000年：“单独函数完全的算子”，《哲学研究》第6期。

刘新文，2003年：“以广义析舍和存在量词为初始符号的一阶系统”，《哲学研究》（逻辑学增刊）。

刘新文，2005年：“经典一阶逻辑的希尔伯特型系统”，《湖南科技大学学报》（社会科学版）第2期。

宋文淦，2000年：“关于只有单个足够的初始联结词的经典命题逻辑演算”，载《摹物求比》，中国社会科学院哲学所逻辑室 编，社科文献出版社。

威廉·涅尔，玛莎·涅尔，1962年：《逻辑学的发展》，张家龙 洪汉鼎译，商务印书馆，1985年。

余俊伟，2005年：“形式系统的可靠性和完全性问题”，《湖南科技大学学报》（社科版）第1期。

张清宇，1995年：“不用联结词的经典命题逻辑系统”，《哲学研究》第5期。

1996年：“不用联结词和量词的一阶逻辑系统”，《哲学研究》第5期。

1997年：“经典命题逻辑的一个公理系统”，《哲学研究》第8期。

1999年：“系统Z中的范式和插入定理”，《哲学研究》第12期。

 

（原载《哲学研究》，2008年第9期。录入编辑：神秘岛）