_ukasiewicz命题演算形式系统公理独立性证明_宋伟.pdf

2023年第2期第41卷（总第223期）NO.2，2023Vol.41General No.223贵州工程应用技术学院学报JOURNAL OF GUIZHOU UNIVERSITY OF ENGINEERING SCIENCE ukasiewiczukasiewicz命题演算形式系统公理独立性证明命题演算形式系统公理独立性证明宋 伟(湖北大学哲学学院，湖北武汉430062)收稿日期：2022-04-25作者简介：宋伟（1973-），男，安徽临泉人，哲学博士，湖北大学哲学学院副教授。研究方向：逻辑史与逻辑哲学。摘要：在有关ukasiewicz命题演算形式系统的公理独立性证明中，一种常见的做法是直接运用模型论的方法构造出若干三值模型来表明各公理的独立性。不过，这种做法既没有详细解释构造这些三值模型的原因和依据，也没有系统说明构造这些三值模型的过程和方法。实际上，一种直观而自然的思考进路完全可以弥补上述做法的不足。关键词：命题演算；形式系统；公理；独立性中图分类号：B81文献标识码：A文章编号：2096-0239（2023）02-0057-08许多数理逻辑教科书在讨论ukasiewicz命题演算形式系统的公理独立性时，常常都是运用模型论的证明方法直接给出一些三值模型来表明公理之间的独立性，并且常常在构造模型时即使对于同一系统也不断变换指派给公理和推论规则的指定值（designated value），因而显得有些随意和凌乱。如，在亨特(Hunter)的 元逻辑：标准一阶逻辑的元理论导论 中1、在门德尔森（Mendelson）的 数理逻辑导论 中2，由于相关的讨论没有系统而详细地解释其中所给出的三值模型的具体构造思路和构造方法，给人一种似乎全凭随机猜想和试错、仅靠灵感来寻求答案的感觉，所以常常令初学者颇为困惑，不知为什么在证明这些公理的独立性时一定要构造三值模型而不是二值模型？三值模型的构造有无可遵循的思路或方法？其背后有什么样的机制和关联？这里就来尝试解答一下这些问题，希望能为初学者消除一些困惑。一这里所考虑的ukasiewicz命题演算形式系统（以下简称为系统L），包含有如下三个公理模式(L1)、(L2)、(L3)和一个推论规则modus ponens（即分离规则，通常缩写为MP）：3(L1)(A(BA)(L2)(A(BC)(AB)(AC)(L3)(A)(B)(BA)MP A,ABLB其中的A、B、C表示系统L的任意公式。现在，如何证明(L1)、(L2)和(L3)的独立性呢？直观上看，(L3)比(L1)和(L2)在语形上更为独特，即多了一个在后两者中并无直接出现的符号“”，从而先从证明(L3)的独立性入手似乎就成了一个非常自然的想法。这里不妨将这一想法的出现称为证明系统L公理独立性过程的步骤1。根据上述三个公理模式的特点，尤其是(L3)与(L1)和(L2)相比所显现出的语形上的差异，按照模型57论的证明方法，令系统L中公式的可取值集合或者说可指派给公式的值的集合为0,1，同时令公理模式和推论规则的指定值为“0”或者说可指派给公理模式和推论规则的值的集合为0。当公式(A)和(AB)具有如下表 1 中的赋值时，稍加检验即可发现当(L1)、(L2)都取值为 0 且MP具有保0 性（即如果公式 A 和(AB)取值为 0，那么公式 B 取值为 0）的情况下，(L3)取值不为 0。换句话说，当(L1)和(L2)都为“逻辑有效式”且MP保持“逻辑有效性”的情况下，(L3)不是“逻辑有效式”。这也就意味着，(L3)具有相对于(L1)和(L2)的独立性，在系统L中不可从(L1)和(L2)推出。由此可见，公理模式(L3)的独立性完全可以通过构造一个二值模型来证明。实际上，当注意到表 1 中公式 A和(A)的取值时，不难发现这一二值模型就是一些数理逻辑教科书中所说的“否定号消去”的具体体现1125，即当(A)与 A 的取值相同时，通常所谓的否定号“”就失去了其否定的功能，相当于消失了。在此情况下，公理模式(L3)即(A)(B)(BA)实际上变成了(AB)(BA)，这时，(L3)显然不再是一个取值全为指定值“0”的公理模式或“重0式”，而(L1)和(L2)显然不受“否定号消去”的影响，仍然是“重0式”。表1证明(L3)独立性的二值模型A01(A)01A0011B0101(AB)0100现在的问题是，既然(L3)的独立性可以通过二值模型来证明，那么(L1)和(L2)的独立性是否也可以通过二值模型来证明呢？这似乎是一个很自然的问题，不妨将这一问题的提出称为证明系统L公理独立性过程的步骤2。通过观察、对比(L1)和(L2)不难发现，这一问题的答案可由(AB)的取值来决定，也即是说，当指定值为“0”时，看看是否存在一种(AB)的取值使得(L1)为“重0式”而(L2)不为“重0式”或者(L2)为“重0式”而(L1)不为“重0式”。这里不妨把(AB)的222种可能的取值即16种取值全部列出来加以考察。表2即为在公式A、B的22种取值组合下，(AB)的16种可能的取值情况。在这16种可能的取值情况中，考虑到分离规则MP要具有“保0性”，即当A和(AB)取值为“0”时，B也要取值为“0”，显然可以直接将、11、12这8种情况排除。除此之外，考虑到(L1)和(L2)的构成特点，当A、B取值分别为“1”时(AB)取值为“1”的、14、16这4种情况也应当排除，因为在这4种情况中(L1)和(L2)的取值都会出现取值为“1”的情形，不会出现一个为“重0式”、另一个不为“重0式”的情形，因而无法证明二者的独立性。这样，就只需要检验剩下的、13和15和这4种情况了。检验后可以发现，在这种情况下，(L1)和(L2)都为“重0式”，而在、13和15和这3种情况下(L1)和(L2)都不为“重0式”，显然在这4种情况下也无法证明(L1)和(L2)的独立性。由此可见，在这16种可能的取值情况中没有一种取值使得(L1)为“重0式”而(L2)不为“重0式”或者(L2)为“重0式”而(L1)不为“重0式”，这也就意味着不可能存在可以证明(L1)和(L2)的独立性的二值模型，要想运用模型论的方法成功证明(L1)和(L2)的独立性，现在所能作出的选择似乎只能是尝试扩大公式的可取值范围或者说扩大可指派给公式的值的集合。这样，三值模型自然而然就成了优先考虑的对象。三值模型的自然出现可称为证明系统L公理独立性过程的步骤3。58表2(AB)的16种取值A0011B0101(AB)000010001200103001140100501016011070111810009100110101011101112110013110114111015111116二现在，令系统L中公式的可取值集合为0,1,2，指派给公理模式和推论规则的指定值仍然为“0”。在构造三值模型来证明公理模式(L1)、(L2)和(L3)的独立性时，考虑到(L3)的独立性在二值模型中运用“否定号消去”的方法即可得证，自然，在构造证明(L3)的独立性的三值模型时似乎可以继续尝试运用一下“否定号消去”这种方法。这一自然的想法可称为证明系统L公理独立性过程的步骤4。这样，(A)即有如下表3中的赋值：表3证明(L3)独立性的“”的取值A012(A)012接下来考虑(AB)的赋值。这里要注意的是，既然分离规则MP必须具有“保0性”，即如果A和(AB)取值为“0”那么B也要取值为“0”，所以当B取值不为“0”且A取值为“0”时(AB)不能取值为“0”，而只能取值为“1”或“2”。由于现在的目标是证明(L3)的独立性，即构造一个三值模型使得(L1)和(L2)都为“重0式”而(L3)不为“重0式”，所以从“保0性”（当A取值为“0”、B取值不为“0”时(AB)的赋值不为“0”）、“否定性”（当A、B都取值为“1”时(AB)不能赋值为“1”，A、B都取值为“2”时(AB)不能赋值为“2”，否则，(L1)和(L2)都只能为“重1式”或“重2式”而不能为“重0式”）和“简单性”（尽可能多地给(AB)赋值为“0”且尽可能减少(AB)赋值的多样性）这三个方面考虑，不妨尝试赋予(AB)如下表4中4种可能的取值。这一赋值的想法可称为证明系统L公理独立性过程的步骤5。运用归谬赋值法不难发现，在表4中的、四种赋值情况下，(L1)和(L2)都为“重0式”，而在“否定号消去”的情况下，(L3)在这4种情况下都不为“重0式”。因而，根据表3和表4的赋值，可以轻松找到四种能够证明(L3)独立性的三值模型。表4证明(L3)独立性的“”的取值A000111222B012012012(AB)01100000002200000001200000002100000059接下来，同样自然的一个想法是：能不能在表4赋值的基础上来构造能够证明(L1)和(L2)独立性的三值模型？这一想法可称为证明系统L公理独立性过程的步骤6。考虑到公理模式(L1)比(L2)具有更为简单的语形特征（就公理模式的长度而言），所以不妨先来证明(L1)的独立性。这一想法可称为证明系统L公理独立性过程的步骤7。这样，在指定值保持不变即仍旧为“0”的情况下，就需要找到一个三值模型使得(L2)和(L3)都为“重0式”而(L1)不为“重0式”。就表4中(AB)的四种赋值情况而言，现在的问题是：能否尽可能少地改变(AB)的赋值使得(L2)和(L3)都为“重0式”而(L1)不为“重0式”？首先，来看一下第种赋值，由于在这种情况中(AB)两种不为“0”的取值都为“1”，本着“简单性”原则，可以尝试寻找一下是否存在着另外一种(AB)取值为“1”的情况使得(L1)不再为“重0式”而(L2)仍然为“重0式”。这时，如何在增加了另外一种(AB)取值为“1”的情况下使得(L2)仍然为“重0式”显然就成了问题的关键。通过观察(L2)的语形结构，直观上似乎有理由猜测，在表4中的赋值情况下从A取值为“2”的三种情况中挑选一种令(AB)取值为“1”应该对(L2)为“重0式”的结果影响最小，因为在(AB)的取值不是“0”就是“1”、没有“2”的情况下，(L2)的前件(A(BC)不会出现取值为“2”的情况。换句话说，在新增加的一种(AB)取值为“1”的情况中(L2)不会出现因其前件(A(BC)取值为“2”而使得(L2)取值为“1”从而不再为“重0式”的情况。当然，这种增加并不必然保证(L2)仍然一定为“重0式”，其仅仅是进一步验证之前的一种初步的、直观的猜测。不过，这种初步的、直观的猜测无疑是相当自然的一种思考方向。这一方向可称为证明系统L公理独立性过程的步骤8。现在就来看看这一思考方向能够带来什么样的结果。表5不可证明(L1)或(L2)独立性的“”的取值A000111222B012012012(AB)011000100当A、B取值分别为“2”、“0”时如果令(AB)取值为“1”，如表5所示，通过归谬赋值法或逐一检验(L1)的32种取值和(L2)的33种取值可以发现，在这种赋值下，(L1)和(L2)都不为“重0式”。当A、B取值分别为“2”、“1”时如果令(AB)取值为1，如表6所示，通过归谬赋值法或逐一检验法可以发现，(L1)不为“重0式”而(L2)为“重0式”（这一结果与猜测相符）。当A、B取值分别为“2”、“2”时如果令(AB)取值为“1”，如表7所示，检验后可以发现，(L1)为“重0式”而(L2)不为“重0式”（这一结果与猜测相反，可以说是一意外收获）。这样，根据表6和(L3)的语形结构及其取值情况可以构造出一种使得(L3)为“重0式”的(A)的赋值，如表8所示。而根据表7和(L3)的语形结构及其取值情况则可以构造出另一种使得(L3)为“重0式”的(A)的赋值，如表9所示。显然，表6和表8可以构成一个能够证明(L1)的独立性的三值模型，而表 7 和表 9 则可以构成一个能够证明(L2)的独立性的三值模型。至此，通过步骤1到步骤8的过程，可以说已经找到了或者构造出了能够证明(L1)、(L2)和(L3)各自独立性的三值模型。整个过程应该说是一个较为自然的思考过程，而为了看看其中是否有规可循，不妨继续探讨一下表4中的、这三种情况。60表6可证明(L1)独立性的“”的取值表7可证明(L2)独立性的“”的取值表 8可证明(L1)独立性的“”的取值表9可证明(L2)独立性的“”的取值三依循相似的思路，对于表4中的这种赋值情况，本着“简单性”原则，可以尝试寻找一下是否存在着另外一种(AB)取值为“2”的情况使得(L1)不再为“重0式”而(L2)仍然为“重0式”。同样，直观上似乎有理由认为，从A取值为“1”的三种情况中挑选一种令(AB)取值为“2”应该对(L2)为“重0式”的结果影响最小。因为在(AB)的取值不是“0”就是“2”、没有“1”的情况下，(L2)的前件(A(BC)不会出现取值为“1”的情况。换句话说，在新增加的一种(AB)取值为“2”的情况中(L2)不会出现因其前件(A(BC)取值为“1”而使得(L2)取值为“2”从而不再为“重0式”的情况。通过归谬赋值法或逐一检验(L1)的32种取值和(L2)的33种取值，可以构造出(AB)的赋值及相应的(A)的赋值，从而构造一个能够证明(L1)独立性的、如表10所示的三值模型（与猜测相符的一个结果）。此外，还可以构造出一个能够证明(L2)独立性的、如表11所示的三值模型（与猜测相反的一个意外收获）。表10可证明(L1)独立性的三值模型A012(A)210A000111222B012012012(AB)022002000A000111222B012012012(AB)011000001A000111222B012012012(AB)011000010A012(A)201A012(A)10261表11可证明(L2)独立性的三值模型A012(A)110A000111222B012012012(AB)022020000对于表4中的这种赋值情况，由于(AB)不为“0”的取值既有“1”又有“2”，所以可以考虑增添另一种(AB)取值为“1”或“2”的情况。理论上，这既可以在 A 取值为“1”的三种情况中来赋值，也可以在 A 取值为“2”的三种情况中来赋值。通过综合运用归谬赋值法或逐一检验法，可以构造出一个能够证明(L1)独立性的三值模型（表 12），也可以构造出一个能够证明(L2)独立性的三值模型（表13）。不过，对于表4中的这种赋值情况，通过归谬赋值法或逐一检验法可以发现，在仅仅增加一个(AB)的非“0”取值的情况下，可以构造出多种(AB)的赋值使得(L1)在这种赋值下为“0”而(L2)在这种赋值下不为“0”，但却无法构造出一种(AB)的赋值使得(L2)在这种赋值下为“0”而(L1)在这种赋值下不为“0”（这一点实际上由(AB)在表4中的这种赋值情况以及(L1)和(L2)这两个公理模式的语形特征及取值情况所决定）。这也就意味着，对于表 4 中的这种赋值情况，只能从中构造出可以证明(L2)的独立性的三值模型（如表14、表15所示的三值模型），而构造不出可以证明(L1)独立性的三值模型。当然，这对于证明公理模式(L1)、(L2)和(L3)的独立性这一根本目的来说已经无关紧要了。表12可证明(L1)独立性的三值模型A012(A)110A000111222B012012012(AB)01220000062表13可证明(L2)独立性的三值模型A012(A)210A000111222B012012012(AB)012001000表14可证明(L2)独立性的三值模型A012(A)111A000111222B012012012(AB)021020000表15可证明(L2)独立性的三值模型A012(A)202A000111222B012012012(AB)021000001上述结果无疑表明，系统L的三个公理模式(L1)、(L2)和(L3)的独立性均可在三值模型中得以证明，而且在“保0性”、“否定性”和“简单性”的原则指导下可以以一种较为自然的、循序渐进的方式构造出简洁清晰的相关三值模型，至少可以给出有关(L1)、(L2)和(L3)的独立性证明的一个完整的过程，从而不至于让(L1)、(L2)和(L3)的独立性证明显得好像是一个毫无章法可依的、全凭随机猜想和蛮力验证的发现过程。当然，上述三值模型并不是能够证明三个公理模式独立性的所有模型，在保持指定值不变的情况下，要找出该指定值下的所有三值模型，理论上需要考虑33332即312种(A)和(AB)的赋值组合，上述模型仅仅是这些组合中的极小一部分。而如果改变指定值，即除了可令指定值为“0”外，还可令指定值63为“1”或“2”，那么仅仅从具有表面上的差异而言，或者说在不考虑“0”、“1”、“2”这些指定值实质上具有可相互替换性的情况下，所要考虑的可能的三值模型总数还要再翻3倍，即为313种。如此繁多的可能性无疑正是许多数理逻辑教科书中随机给出三值模型来表明(L1)、(L2)和(L3)的独立性时令初学者感到困惑不解的根源。实际上，就系统L而言，由于否定号或符号“”并不在(L1)、(L2)和推论规则MP中出现，而仅在(L3)中出现，所以直观上易于让人首先注意到(L3)的独立性，而其独立性也可仅仅在一个二值模型中就轻松确立。在一个不改变(L1)、(L2)和推论规则MP仅仅改变(L3)、与系统L等价的系统L*中（如下），这一点同样适用。(L*1)(A(BA)(L*2)(A(BC)(AB)(AC)(L*3)(A)(B)(A)B)A)MPA,ABLB当然，对于一个其中各个公理或公理模式并无明显语形特征差异的形式系统来说，从哪一个公理或公理模式入手更易于证明其中各公理或公理模式的独立性还需具体情况具体分析，其中的思路、过程和方法还需进一步总结。但不管怎样，对ukasiewicz命题演算形式系统L中公理模式独立性的上述分析足以消除或弥补许多数理逻辑教科书中有关这一问题讨论的含糊或不足了。总之，通过上述讨论，初次接触ukasiewicz命题演算形式系统的学习者应该能够更为清晰地把握到该系统中三个公理模式(L1)、(L2)和(L3)独立性证明的大致思考进路和方式方法，并且能够进一步认识到不同模型背后的因果关联和构成机制，从而能够举一反三，顺利给出其他形式系统的公理独立性证明。参考文献：1 Hunter,G.Metalogic:An Introduction to the Metatheory of Standard First Order LogicM.London:Macmillan,1971：122-125.2 Mendelson,E.Introduction to Mathematical LogicM.6thed.Boca Raton:Taylor&Francis Group,2015:36-38.3 Copi,I.Symbolic LogicM.5thed.New York:Macmillan Publishing Co.Inc.,1979:237.A Proof of Independence of Axioms in ukasiewicz s Formal System for Propositional CalculusSONG Wei(School of Philosophy,Hubei University,Wuhan,Hubei430062,China)Abstract:Among the known proofs of independence of axioms in so-called ukasiewicz s formalsystem for propositional calculus,a common way is by the model-theoretic method to construct several ofthree-value models which can present the independence of different axioms.The common way,however,doesn t adequately investigate the reasons and the grounds by which those three-value models come tohappen,and doesn t systematically explain the processes and the methods by which those three-value modelscome to be constructed,either.As a matter of fact,a kind of natural and intuitive thinking approach cancompletely rule out the defects of the common way.Keywords:propositional calculus;formal system;axiom（责编：彭麟淋）64