数理逻辑中命题公式等价证明的程序化研究与实现

杨剑兰 周青

（昆明医科大学海源学院 云南省昆明市 650106）

逻辑学是研究思维形式、思维规律的科学，其中思维形式结构包括对事物的概念单位呈现、属性肯定或否定的判断和由此产生的关联推理；思维规律是指在思维过程中必须遵守的法则，这些法则是保证思维符合正确发展的必要条件，对思维的无限延伸和发散具有科学地制约作用。以数学方法、建立符号和运算式来研究推理规律、展现推理过程，则为数理逻辑。数理逻辑的奠基人莱布尼茨提出：

（1）建立如同“数学的符号”的一种通用语言，这种语言中每一符号表示一个概念；

（2）并确立一个完善的逻辑演算体系，演算是根据确立的逻辑规则进行符号运算。

以上两点正是数理逻辑的基本特征[1]，而以符号依据相应标准来表示自然事物的结构则为命题公式。莱布尼兹还提出了“不可分辨同一性”原理，即一个元素能被另一元素所替换而保持原命题的真值，那么它们就是同一的[2]，可理解为用于表示一件事物的符号与连结词不止一种，即命题公式是存在相互等价的。本文以真值表法判断两个命题公式等价与否，并结合计算机语言程序设计将求解过程以计算机工具实现对两组包含两个及以上命题变项的任意命题公式的等价判断，从而体现现代计算机科学技术处理数理逻辑问题的能力，启迪更多的学习者深刻理解理论发展与应用之间的关联。

1 命题公式

1.1 命题

属性可在真假之一判定的陈述句被称为命题，用自然语言表示的命题在数理逻辑中可用符号进行表示，并且每条命题对应可判断的真值，成立为真（T，1），不成立为假（F，0）。不可再进行逻辑结构分割的命题为原子命题，由原子命题组成的命题为复合命题。如表1。

表1：判断语句是否是命题的例题

数理逻辑的主要使命是消除自然语言的局限性和不规则性，创建具有简明符号、合理规则的“通用语言”，为此，莱布尼茨做了两方面的努力：一是寻找能够代表所有概念并可认作最根本的不可分析的符号，对应原子命题；二是给出表述诸如断定、合取、析取、否定、全称、特殊、条件联结等形式概念的设计，对应连结词[2]，由连结词和原子命题构成复合命题。如表2。

表2：命题的符号化

表2 中三道命题均因明确对应的语句而具备确定真值，则为命题常项。而基于符号层面剥离自然语境是进行数理推演是数理逻辑的使命和目的，因此在对一串符号进行推导和演算具体真值结果时，往往是对组合成该命题的各个元素做不同情况的真值指派，再结合出现的连结词和法则推算，如表3。

表3：复合命题p →q 真值与组成符号真值的关系

由表3 可见，复合命题p →q 真值由其所包含的原子命题以及连结词的具体真值指派决定，某些情况下使其为T，某些情况下为F。即p 与q 的真值可以代入不同的原子命题及相应的T/F 值，则p、q 为命题变项。

1.2 命题公式及其等价判断

命题公式是对由命题常项，命题变项、联结间和括号按照一定逻辑关系构成的复合命题的形式化描述。命题公式本身不是命题，没有真值，只有对其命题变项进行赋值后，它才有真值。两组命题公式A 与B 即使构成形式上不一致，但只要对包含的全部n 个命题变项作2n组真值指派后，所有同一组真值指派后得到的命题公式A 与B 真值完全相同，则A 与B 等价。例如表4。

表4：命题公式q →(p∨(p∧q))与q →p 真值表

从表4 可见，命题公式q →(p∨(p∧q))与q →p 形式虽不相同，但在四组对p，q 的不同真值指派组合下得到的真值完全一致，则命题公式q →(p∨(p∧q))与q →p 等价。

2 计算机程序化

2.1 计算机程序与离散数学关系简述

计算机程序是一组有序指令的集合，是用来定义计算机指令执行流程的形式化语言。每种程序语言都包含一整套词汇和语法规范，这些规范通常包括数据类型和数据结构、指令类型和指令控制、调用机制和库函数以及不成文的规定（如递进书写、变量命名等）[3]。离散数学思想与计算机程序对逻辑问题的处理密切关联，并且能反映事物本身在微观视角的离散特性下存在与运行的机制。Curry-Howard 同构显示了推理系统和程序语言之间的相似性[4]，命题即类型，证明即程序，在直觉主义逻辑中，所有基于形式化方法构造的证据写成的命题证明，都可以解释为一个具有类型的程序交由计算机进行验证。

2.2 连结词与程序逻辑运算符

（1）﹁（取反），∧（合取），∨（析取）三种最为基本和简单的逻辑连结词与对应的程序语言逻辑运算符如表5。

表5：命题连结词与对应的Java 语言逻辑运算符

（2）→（蕴含），↔（当且仅当）连结词的逻辑性质符合以下程序分支结构，如表6。

表6：命题连结词与对应的Java 程序分支结构示例

（3）也可根据等价关系，将p →q 转化为﹁p∨q，将p↔q 转化为(﹁p∨q)∧(p∨﹁q)再进行后续运行。

2.3 对应计算机程序思路

（1）面向对象程序设计构成模块的基本单元是类，可基于一个类的属性创建不同的具体对象，并且在类中创建不同的运行机制（方法）供不同对象反复调用。为能够实现两组及以上命题公式的等价判断，可使用面向对象程序设计功能，基于命题公式类创建两个命题公式对象A 与B；

（2）建立for 循环遍历用户输入的公式对象中各个元素，并利用栈结构来实现把公式从中缀表达式转换为后缀表达式便于运算，如a+b*(c+d*e)-f 转换为abcde*+*+f-；

（3）在后缀表达式中判断命题变元的数量n；

（4）将n 个命题变元共2n真值存储在数组中，循环遍历输出真值表；

（5）让A 与B 分别调用上述已构造好的方法；

（6）对得到的两组命题公式真值做遍历匹配，若完全一致则两组公式等价。

程序核心代码如下：

2.4 上机验证

例题：求解命题公式q →(p∨(p∧q))与q →p 是否等价，在IDEA 下运行结果正确，如图1。

图1：Java 程序运行结果

3 结语

莱布尼茨对逻辑问题的最早探索和最初贡献是试图沿着笛卡尔和霍布斯的思路建构所谓的“通用语言”，这是一套表达思想和事物的符号系统[2]，正因如此，也为计算机工具自动化实现逻辑问题的求解奠定了数学基础；而计算机科学家如阿伦•凯所发明的面向对象程序，为计算机程序求解基于同类创建的不同个体实例提供了便利，才使计算机程序证明两套命题公式是否等价得以高效地实现。阿尔伯特•爱因斯坦说过：“所有科学的宏大目标都是：从最小数量的假说或公理出发通过逻辑演绎推理说明最大数量的实验事实”，学习和认识逻辑演绎推理并能够擅长使用现代计算机手段进行相关问题的处理可以在很大程度上帮助学习者以工学应用为导向地进入科学世界。