數理邏輯中命題公式等價證明的程序化研究與實現

楊劍蘭 周青

（昆明醫科大學海源學院 云南省昆明市 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]，正因如此，也為計算機工具自動化實現邏輯問題的求解奠定了數學基礎；而計算機科學家如阿倫?凱所發明的面向對象程序，為計算機程序求解基于同類創建的不同個體實例提供了便利，才使計算機程序證明兩套命題公式是否等價得以高效地實現。阿爾伯特?愛因斯坦說過：“所有科學的宏大目標都是：從最小數量的假說或公理出發通過邏輯演繹推理說明最大數量的實驗事實”，學習和認識邏輯演繹推理并能夠擅長使用現代計算機手段進行相關問題的處理可以在很大程度上幫助學習者以工學應用為導向地進入科學世界。