現代教育技術在“數理邏輯”課程中的應用

摘 要：基于“數理邏輯”課程的教學特點，利用現代教育技術的教學手段，解決按照傳統的教學方式講授“數理邏輯”課程中兩個比較突出的問題。從而提高學生們學習“數理邏輯”課程的興趣，提高學生們獨立思考、抽象思維和動手解決問題的能力，提高該課程的教學質量。

關鍵詞：現代教育技術；應用；“數理邏輯”課程

隨著邏輯學的發展，特別是近年來人工智能的發展，越來越凸顯了數理邏輯的重要性。“數理邏輯”課程是邏輯學專業乃至哲學專業中的一門核心課程之一，同時它也是一門抽象的理論課程。長期以來，按照傳統的教學方式授課，既不能使學生很好地理解“數理邏輯”課程中一些抽象的思想，也不能使學生熟練地掌握“數理邏輯”課程中的一些具體的方法。因此，它被師生們公認為是一門最難講和最難學的課程。我們團隊從2006年起，不斷地探索現代教育技術的手段，將現代的教學手段引入“數理邏輯”課程的教學中，最終提高了“數理邏輯”課程的教學質量和教學效果。

一、要解決的教學問題及目的

概括地說，我們主要解決的“數理邏輯”課程中的教學問題有兩個：正確地理解“數理邏輯”課程中的思想，熟練地掌握“數理邏輯”課程中的方法。

具體地說，第一，由于“數理邏輯”課程是一門抽象的理論課，在這門課程的學習中，有些學生不能正確地理解公理化、形式化、賦值、邏輯后承、可滿足和邏輯真等一些抽象的邏輯思想和邏輯概念。第二，由于“數理邏輯”課程中有許許多多可操作的方法，在這門課程的學習中，有些方法學生不能熟練地掌握，如：判斷一個公式是否另一個的重言后承；形式證明方法；在給定的論域中，編寫一階公式并判斷公式的真假值，等等。

解決這些問題的目的是激發學生學習“數理邏輯”課程的興趣，提高學生們抽象思維和解決問題的能力，從而掌握數理邏輯乃至整個現代邏輯的核心和精髓。

二、實驗室的建設與發展

為了配合“數理邏輯”課程的教學，為了改善邏輯學學科的教學條件，也為了滿足現代技術條件下新型哲學社會科學研究與應用的復合型人才培養的需要，2007年在南開大學的支持下，我們建立起了 “邏輯推理實驗室”。利用這個實驗教學平臺，從2008年起至今，我們在邏輯學專業中開設了“實驗邏輯學”課程。現在，這門課已是全校的公選課。2015年，我們又完成了新校區邏輯推理實驗室的重建。

實驗室建設和發展可以分為三個階段。

第一個階段（2007—2013年） 模式：局域網+多媒體；實驗室面積40平方米，可以容納18個學生同時上機操作；使用的計算機型號為iMac OS X 10.3.9，規格為800 MHz PowerPC C4 （2.1）/768MB SDRAM。自編實驗教材《數理邏輯實驗教程》[1]和《邏輯學實驗教程》[2]，使用教學軟件3個，自主研發了邏輯學習軟件《邏輯運算3.0》。

第二個階段（2013—2015年） 模式：局域網+多媒體；使用的計算機型號為iMac 5.1 OS X 10.4.11，規格為2.16 GHz Intel Core 2 Duo/2GB 667 MHz DDR2 SDRAM。在第一個階段的基礎上，自主研發了邏輯學習軟件《數理邏輯詞匯字典》。

第三個階段（2015年至今） 模式：局域網+多媒體；實驗室面積80平方米，可以容納40個學生同時上機操作。使用的計算機型號為iMac OS EI Caption，10.11.1，規格為3.1 GHz intel Core i5 /16GB 1867 MHz DDR3/1TB/21.5英寸。自編教材《實驗邏輯學》[3]，使用教學軟件5個。

三、解決教學問題的方法

為了配合“數理邏輯”課程的學習，2006年我們完成了該課程的網上建設，使該課程的所有電子資源，包括課程簡介、教學大綱、授課教案、電子教材、參考文獻、習題、試卷和示范錄像等全部上網。之后，完成了該課程的全程教學錄像。

為了將“數理邏輯”課程中的一些可操作方法轉化為能夠利用現代技術、在計算機上進行操作，我們自主研發了《邏輯運算3.0》和《數理邏輯詞匯字典》兩款邏輯學習軟件，在互聯網上搜索了國際上所有的邏輯學習軟件，解讀了一批有代表性的邏輯學習軟件，并將這些軟件的操作和使用方法編寫到我們的實驗課的教材中。最后，我們將邏輯學習軟件《邏輯運算3.0》和《數理邏輯詞匯字典》、LPL和TPG引入“實驗邏輯學”課程的教學中。

因為真值表方法是整個數理邏輯中最重要和最基本的方法，所以我們在“實驗邏輯學”課上，首先給學生介紹自主研發的《邏輯運算3.0》的使用。它是一款能夠快速計算一個包含至多6個命題變項的真值形式的真值，并能夠構造出相應真值形式的真值表的軟件。

《數理邏輯詞匯字典》是一款能夠快速查閱數理邏輯中概念和定義的英漢對照的學習庫。借助這款軟件和常用的計算機命令，如果輸入中文的數理邏輯的專有名詞，可以同時顯示所對應的英文詞以及對該名詞的中英文解釋；如果輸入相應的英文詞，可以同時顯示所對應的中文詞，以及對該名詞的中英文解釋。

LPL（Language Proof and Logic）是由美國斯坦福大學用于數理邏輯學習的計算機程序軟件。它是一個電腦程序文件庫，它的第二版主要包括：Boole 3.1，Fitch 3.2，Tarski′s World 7.0三個子程序文件。

借助Tarski′s World 7.0和常用的計算機命令，可以使學生在Tarski′s World 7.0的三維空間里使用和改造已有的世界，創造新世界，編寫一階邏輯語句，判斷它們的真值，并通過做游戲的方式檢驗自己對語句真值的判斷是否正確，從而認識到自己的錯誤，并從改正錯誤中學習。通過自行完成圍繞Tarski′s World 7.0精心設計的大量練習，學生能夠輕松理解各個邏輯聯結詞和量詞的意義，快速熟悉它們的用法。

借助Boole 3.1和常用的計算機命令，可以構造任意真值形式（公式）的真值表，還可以自行檢驗所構造的真值表的對錯；驗證一個真值形式是否重言式，判斷它是否可滿足式或矛盾式；還可以構造兩個真值形式的共享真值表，判斷它們是否重言等值。此外，還可以構造幾個真值形式的共享真值表，判斷其中一個真值形式是否其他真值形式的重言后承。最后，還可以自行檢驗自己的判斷是否正確。

借助Fitch 3.2和常用的計算機命令，可以構造數理邏輯中的自然推理系統F的形式定理的形式證明，也可以構造從某些公式到某個公式的形式推理，并檢驗每一步推理是否正確。Fitch也自帶了一個練習的文件夾。這些練習從簡到難，循序漸進。通過完成這些練習，可以使學生熟練地掌握形式定理的證明方法。

TPG（Tree Proof Generater）是互聯網上的一款邏輯學習軟件。網址：http：//www.umsu.de/logik/trees/。借助它可以檢驗數理邏輯中各種邏輯公式的有效性。該軟件為判斷命題公式是否重言式和不含等詞的一階公式是否永真式提供了一種動態的樹形式證明方法。

通過這些計算機軟件的學習和操作，使學生掌握作為現代邏輯的核心部分——數理邏輯的思想和方法，從而實現學習目的。

四、邏輯學習軟件LPL的應用

1.用Boole解釋的后承關系

當考慮公式B是否公式A∨B和公式?A的一個重言（或者邏輯）后承時，按照通常的方法，需要用重言后承的定義去驗證。也就是要考慮所有滿足A∨B和?A的真值賦值σ是否也滿足B。如果滿足B，那么B就是A∨B和?A的一個重言后承；否則，B就不是A∨B和?A的重言后承。而所有滿足A∨B和?A的真值賦值σ是一種抽象的描述。但是，用Boole解釋B是否A∨B和?A的一個重言后承，只需用Boole構造A∨B，?A和B的一個共享真值表，在這個共享真值表中，所有滿足和不滿足A∨B和?A的真值賦值σ都被列了出來。檢查這個真值表中的兩個前提A∨B和?A下面的列，我們可以看到只有一行，也就是在第三行中兩個前提都是真的，并且在此行結論B也是真的。這就證明了所有滿足A∨B和?A的真值賦值σ也滿足B。因此，B是A∨B和?A的一個重言（邏輯）后承。不難看出：A∨B也是?A 和B的一個重言后承。除此之外，我們還可以通過Boole上的評價鍵（Assessment）來給出我們的斷言，并通過Boole來驗證我們的斷言是否正確。驗證后的結果是→Last；→First。其中：→Last表明B是A∨B和?A的一個重言后承，→First表明A∨B也是?A 和B的一個重言后承。于是，有：

A∨B，?AB 和 ?A，BA∨B。

注意：利用Boole構造的真值表，它的每個真值的計算是否正確，可以通過它的Table菜單中的Verify命令進行驗證。如果真值表的每個真值計算的都正確，那么Boole會在該真值表的每一行中的前面放一個√，表示該真值表中每個真值的計算都是正確的；如果計算有誤，Boole會在錯誤的真值所在行的前面放一個×，表示該行中真值的計算有錯誤。遇到這種情況，我們可以重新計算，對已有的結論進行

修正。

現在，假設我們使用Boole去驗證A∨C是否A∨?B和B∨C的一個后承，只要構造它們的一個共享真值。在這個共享真值表中，前提A∨?B和B∨C都取真的有四行：第一、二、三和七行。在每行中結論A∨C也是這樣，結論中還有其他兩行為真，但是那些不是我們關心的。因此，A∨C是前提A∨?B和B∨C的一個重言（因而也是邏輯）后承。

作為一個反例。我們也可以用Boole即真值表揭示結論不是前提的一個重言后承。事實上，最后一個真值表可達到這一目的。因為在這個真值表的第5行中，前提B∨C和A∨C的值都為真，但結論 A∨?B的值為假。因此，A∨?B不是前提B∨C和A∨C的一個后承，即：

B∨C，A∨C╞A∨?B。

用Boole還可以解釋重言式和邏輯等值。特別地，利用Boole還可以解釋可滿足式和矛盾式。

2.用Fitch展示的形式證明

Fitch是一種自然推理系統。它是以引進假設、利用推理規則建立的一種形式演繹系統。這種系統的形式推理規則、形式推理關系、形式證明比較直接并且能比較自然地反映推理過程。實際上，自然推理系統可以看成公理系統的一種變形。原因是它的推理規則都是根據刻畫邏輯聯結詞性質的公理設計而來的，并且在形式系統的證明中，與公理系統的約定一樣，只能用系統本身給出的推理規則，而不能隨意地添加任何東西。Fitch給出的自然推理系統，包括25條推理規則。這25條規則出現在證明中新增加的每個語句的后面。例如，在Fitch中證明如下推理：

? （A∨B）├?A∧?B。

第一步：按照Fitch的規定，首先把假設公式?（A∨B）輸入在橫線的上面；并把要推出的結論?A∧?B放入目標欄。

第二步：我們想得到的結果是?A∧?B。但是，它是一個合取式。因此，必須在既得到?A又得到?B的情況下，才能根據∧-Intro（∧引入規則）得到?A∧?B。而要得到?A，根據?規則的規定，必須在假設A成立的情況下得出矛盾才能得到?A。對?B也同理。

第三步：在假設A成立的情況下，構造一對矛盾的公式。由于目前可用的公式只有?（A∨B）和A，而要構造一對矛盾的公式，只能在A上右析取B得到A∨B。在由A得到A∨B時，使用的規則只能是∨-Intro（∨引入規則）。因此，在A∨B所在行的Rule？規則欄中點擊Intro下的∨，Rule？變成了∨-Intro，它表示：選取的規則是∨-Intro。然后，點擊A所在的行，再點擊頁面上的驗證按鈕，∨-Intro 前出現了一個√，它表明這一步的證明是正確的，我們可以繼續下一步的工作。否則，當∨-Intro的前方出現×，此時表明這一步的證明是不正確的，我們要修正錯誤，直至出現√為止。同理可得：在B上左析取A，得到A∨B。

第四步：由于?（A∨B）和A∨B是一對矛盾的公式，所以，在A∨B的下方引入矛盾符號⊥，并在Rule？規則欄中選取⊥-Intro（⊥引入規則）。然后分別點擊?（A∨B）和A∨B所在的行，最后點擊頁面上的驗證按鈕，這一步的證明可以得到驗證。

第五步：點擊Proof菜單中的End Subproof（結束子證明）命令，根據?-Intro（?引入規則）的規定，在新的一行上，輸入公式?A或者?B，并在Rule？規則欄中選取?-Intro，然后點擊A所在的子證明，這一步的證明可以得到驗證。

第六步：在Proof菜單中點擊Add Step After（在……之后加一行）命令，在新的一行中，輸入?A∧?B，并在Rule？規則欄中選取∧-Intro，然后點擊?A和?B所在的行，最后點擊驗證按鈕，這一步的證明可以得到驗證。

最后，再點擊Proof菜單中的Verify Proof命令，目標語句?A∧?B這一行將出現一個√，它表明這個證明是正確的。

在Fitch中證明如下推理：

?xP（x）├x?P（x）。

第一步：按照Fitch的規定，首先把假設公式?xP（x）輸入在橫線的上面；并把要推出的結論x?P（x）放入目標欄。

第二步：我們決定在證明中采用反證法。因此，構造以?x?P（x）開始的子證明。

第三步：用-Intro（引入規則）來證明與前提xP（x）矛盾，因此，建立第三個子證明，并選擇常項c。

第四步：以?P（c）為假設公式，建立第四個子證明。

第五步：利用-Intro（引入規則），將

x?P（x）寫在?P（c）的下方，點擊?P（c），在點擊頁面上的驗證按鈕，這一步可以得到驗證。

第六步：由于第5行中的公式x?P（x）與第2行的公式?x?P（x）矛盾，所以在第6行中輸入矛盾符號⊥，并在Rule？規則欄中選擇⊥-Intro。然后，點擊Proof菜單中的End Subproof命令，退出第4個子證明。

第七步：第6行產生的矛盾，是因為第四步的假設?P（c）不成立，所以在第7行中輸入公式??P（c），并在Rule？規則欄中選擇?-Intro。點擊以 ?P（c）開始的子證明，再點擊頁面上的驗證按鈕，這一步可以得到驗證。

第八步：對第7行的公式??P（c）使用?-Elim（?消去規則），得到P（c）。點擊??P（c）所在的行，再點擊頁面上的驗證按鈕，這一步可以得到驗證。

第九步：點擊Proof菜單中的End Subproof命令，根據-Intro，在新的一行上，輸入公式xP（x）。點擊以 c開始的子證明，再點擊頁面上的驗證按鈕，這一步可以得到驗證。

第十步：第9行上的公式xP（x）與第1行假設的公式?xP（x）矛盾。因此，在第10行上輸入⊥，并在Rule？規則欄中選擇⊥-Intro。點擊xP（x）和?xP（x）所在的行，再點擊頁面上的驗證按鈕，這一步可以得到驗證。

第十一步：點擊Proof菜單中的End Subproof命令，根據?-Intro，在新的一行上，輸入公式??x?P（x）。點擊以?x?P（x）開始的子證明，再點擊驗證按鈕，這一步可以得到驗證。

第十二步：對第11行的公式??x?P（x）使用否定消去規則?-Elim，得到x?P（x）。點擊第11行，再點擊頁面上的驗證按鈕，這一步可以得到驗證。

最后，點擊Proof菜單中的Verify Proof命令，目標語句x?P（x）這一行將出現一個√，它表明這個證明是正確的。

3.用Tarskis World構造的反例

通常，一個有效的推理，我們能用Fitch給出它的一個形式證明。然而，要說明一個推理是無效的，需要構造一個反例。構造反例，相對來說是困難的。但是，借助Tarskis World，可以使我們輕松地構造反例。例如下面的推理：

A，B，?A∨B∨C├C

是無效的。我們可以借助Tarskis World構造一個前提真結論假的世界（即：模型）。其中，用Dodec（e）代表A，用Meduim（e）代表B，用Dodec（f）代表C。于是，在未命名世界窗口中，將大的立方體命名為f，將大的十二面球體命名為e；在未命名語句窗口中，將Dodec（e），Meduim（e）和? Dodec（e）∨ Meduim（e）∨ Dodec（f）以及Dodec（f）分別輸入在未命名語句窗口的1至4行，然后點擊頁面上的驗證按鈕鍵，得到在當前的世界窗口中，前提語句Dodec（e），Meduim（e）和? Dodec（e）∨ Meduim（e）∨ Dodec（f）的值為真，而結論語句Dodec（f）的值為假。因此，該推理是無效的。

下面的推理：

xP（x）∧xQ（x）├x（P（x）∧Q（x））

也是無效的。我們仍然可以借助Tarskis World構造一個前提真結論假的世界（即：模型）。其中，用Cube（x）代表P（x），用Small（x）代表Q（x）。于是，在未命名世界窗口中，放置一個大的立方體和一個小的錐體；在未命名語句窗口中，將xCube（x）∧xSmall（x）和x（Cube（x）∧ Small（x））分別輸入在未命名語句窗口的1至2行，然后點擊頁面上的驗證按鈕鍵，得到在當前的世界窗口中，前提語句

xCube（x）∧xSmall（x）的值為真，而結論語句x（Cube（x）∧ Small（x））的值為假。因此，該推理是無效的。

參考文獻：

[1]李娜.數理邏輯實驗教程[M].武漢：武漢大學出版社，2010.

[2]李娜.邏輯學實驗教程[M].天津：南開大學出版社，2012.

[3]李娜.實驗邏輯學[M].天津：南開大學出版社，2017.8

[責任編輯：陳立民]