经典命题逻辑的一个公理系统，本文主要内容关键词为：公理论文,命题论文,逻辑论文,经典论文,系统论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
1959年，安德林和贝尔纳普在文[1] 中合作发表了经典命题逻辑的一个公理系统，这系统后来被亨特尔命名为AB（见文[2]）。系统AB 是一个很有特色的系统，它以否定联结词
和析取联结∨为初始联结词，分离规则（从A和A∨B推出B）在此系统中不成立，但此系统的可判定性、可靠性、完全性和独立性等证明却都很简单。系统AB自发表以来，几乎成了一个孤立的现象，很少有人论及。本文将建立经典命题逻辑的公理系统Z，以期对系统AB稍作改进。系统Z只用一类初始联结词——广义析舍，而且采用括号记法，因而使得系统的陈述更为直接明了。系统Z也拥有AB一样的简晰性，它的可判定性、可靠性、 完全性和独立性等证明也都很简单。
一、语形和语义
系统Z所使用的形式语言中有下列两类初始符号：
（1）命题符：P[,0]，P[,1]，P[,2]……；其全体记为P； 元变元用P，q，r等；
（2）逗号和六角括号：，〔〕。符是指用初始符号组成的有穷序列，也就是有穷多个初始符号依次并列而得的结果。初始符号所形成的符的全体，记作Expr（P）。 我们用黑正体小写字母u、v（或加上、下标）表示任意符。任何两个符u和v依次并列而得的结果仍是一个符，这个符记为uv。我们以白正体大写字母X，Y，Z等表示任意的符集，即，由任意多个符组成的集合。我们只对一部分符感兴趣，这部分符形成Expr（P）的一个子集，记作Form（P）。它的精确定义如下。
定义 1.1.符集Form（P）是所有满足下列条件的符集X的交：
（1）P
X；
（2）如果n个符u[,0]，u[,1]…，u[,n-1]（n≥0）都属于Χ， 那么符〔u[,0]，u[,1]，…，u[,n-1]〕属于X。
Form（P）中的元素统称为公式（简称式）。我们用正体大写字母A，B，C（或加上、下标）表示任意公式。如果一公式A作为另一公式B的一个相继连续的部分出现，那么就称A为B的子公式（简称子式）。公式〔A[,0]，…A[,n-1]〕的直接子公式是指它的子公式A[,0]，…A[,n-1]。注意，定义1.1.中允许n＝0，因此符〔〕、〔〔〕〕、〔〔〔〕〕〕、……等都是公式。由下面的语义定义可知，符〔〕和〔〔〕〕将分别表示恒假命题和恒真命题。符〔A〕被称为A的否定。
系统Z的语义由下述定义组成。
定义1.2. 一个真值赋值，就是为各个公式A指定一个真值σ（A）的一个映射σ（即，从Form（P）到集合｛0,1｝的一个映射），它满足下述条件：
二、公理系统Z
在叙述系统Z的公理和推证规则之前，我们先引进一个概念。
如果一公式的直接子公式都是公式〔〕、命题符、或者命题符的否定，则称该公式为原子析舍。例如，〔〔〕〕，〔p，〔q〕〕，〔p，q，r〕等公式都是原子析舍。
公理系统Z由下列公理和推证规则组成。
公理：
（1）凡是有〔〕为直接子公式的原子析舍都是公理；
（2 ）凡是有某个命题符及其否定同时为直接子公式的原子析舍也都是公理。
推证规则：m，n，k都为非正整数，
关于系统Z，我们有下述结论：
（1）没有一个公理是推证规则的结论；
（2）任一个公理都不能由其它公理据推证规则而得；
（3）只有用推证规则（Ⅰ）才能证明形如〔B[,0]，…B[,m-1]，
〔〔A[,0]，…，A[,n-1]〕〕，C[,0]，…，C[,k-1]〕的公式；
（4）只有用推证规则（Ⅱ）才能证明形如〔B[,0]，…B[,m-1]，〔〔A[,0]，…，A[,n-1]〕〕，C[,0]，…，C[,k-1]〕的公式，这里n≥2。
依据这些结论可知，系统Z是独立的。
在系统Z中，跟在系统AB中一样，分离规则是不成立的，即，假定A和〔A，〔b〕〕并不能推出B。实际上，系统Z 的推证规则都是从较短的公式推出较长的公式，因此要想从假定较长的公式推出较短的公式那都是不可能的。但是在另一种意义下，分离规则还是成立的，即，如果A 和〔A，〔B〕〕都可证那么B也可证。
在系统AB中，双重否定规则是成立的，即，从A可以推出A的双重否定
A。但是，在系统Z中双重否定规则却是不成立的，因为从命题符p不能推出它的双重否定〔〔p〕〕。双重否定规则在系统Z中只能有条件地成立，也就是说，当A 不是命题符时从A可以推出它的双重否定〔〔A〕〕。由此可见，系统Z 是很有其独特之处的。