摘 要：基于“數(shù)理邏輯”課程的教學(xué)特點(diǎn)，利用現(xiàn)代教育技術(shù)的教學(xué)手段，解決按照傳統(tǒng)的教學(xué)方式講授“數(shù)理邏輯”課程中兩個(gè)比較突出的問題。從而提高學(xué)生們學(xué)習(xí)“數(shù)理邏輯”課程的興趣，提高學(xué)生們獨(dú)立思考、抽象思維和動手解決問題的能力，提高該課程的教學(xué)質(zhì)量。

關(guān)鍵詞：現(xiàn)代教育技術(shù)；應(yīng)用；“數(shù)理邏輯”課程

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

一、要解決的教學(xué)問題及目的

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

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

解決這些問題的目的是激發(fā)學(xué)生學(xué)習(xí)“數(shù)理邏輯”課程的興趣，提高學(xué)生們抽象思維和解決問題的能力，從而掌握數(shù)理邏輯乃至整個(gè)現(xiàn)代邏輯的核心和精髓。

二、實(shí)驗(yàn)室的建設(shè)與發(fā)展

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

實(shí)驗(yàn)室建設(shè)和發(fā)展可以分為三個(gè)階段。

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

第二個(gè)階段（2013—2015年） 模式：局域網(wǎng)+多媒體；使用的計(jì)算機(jī)型號為iMac 5.1 OS X 10.4.11，規(guī)格為2.16 GHz Intel Core 2 Duo/2GB 667 MHz DDR2 SDRAM。在第一個(gè)階段的基礎(chǔ)上，自主研發(fā)了邏輯學(xué)習(xí)軟件《數(shù)理邏輯詞匯字典》。

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

三、解決教學(xué)問題的方法

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

為了將“數(shù)理邏輯”課程中的一些可操作方法轉(zhuǎn)化為能夠利用現(xiàn)代技術(shù)、在計(jì)算機(jī)上進(jìn)行操作，我們自主研發(fā)了《邏輯運(yùn)算3.0》和《數(shù)理邏輯詞匯字典》兩款邏輯學(xué)習(xí)軟件，在互聯(lián)網(wǎng)上搜索了國際上所有的邏輯學(xué)習(xí)軟件，解讀了一批有代表性的邏輯學(xué)習(xí)軟件，并將這些軟件的操作和使用方法編寫到我們的實(shí)驗(yàn)課的教材中。最后，我們將邏輯學(xué)習(xí)軟件《邏輯運(yùn)算3.0》和《數(shù)理邏輯詞匯字典》、LPL和TPG引入“實(shí)驗(yàn)邏輯學(xué)”課程的教學(xué)中。

因?yàn)檎嬷当矸椒ㄊ钦麄€(gè)數(shù)理邏輯中最重要和最基本的方法，所以我們在“實(shí)驗(yàn)邏輯學(xué)”課上，首先給學(xué)生介紹自主研發(fā)的《邏輯運(yùn)算3.0》的使用。它是一款能夠快速計(jì)算一個(gè)包含至多6個(gè)命題變項(xiàng)的真值形式的真值，并能夠構(gòu)造出相應(yīng)真值形式的真值表的軟件。

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

LPL（Language Proof and Logic）是由美國斯坦福大學(xué)用于數(shù)理邏輯學(xué)習(xí)的計(jì)算機(jī)程序軟件。它是一個(gè)電腦程序文件庫，它的第二版主要包括：Boole 3.1，F(xiàn)itch 3.2，Tarski′s World 7.0三個(gè)子程序文件。

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

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

借助Fitch 3.2和常用的計(jì)算機(jī)命令，可以構(gòu)造數(shù)理邏輯中的自然推理系統(tǒng)F的形式定理的形式證明，也可以構(gòu)造從某些公式到某個(gè)公式的形式推理，并檢驗(yàn)每一步推理是否正確。Fitch也自帶了一個(gè)練習(xí)的文件夾。這些練習(xí)從簡到難，循序漸進(jìn)。通過完成這些練習(xí)，可以使學(xué)生熟練地掌握形式定理的證明方法。

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

通過這些計(jì)算機(jī)軟件的學(xué)習(xí)和操作，使學(xué)生掌握作為現(xiàn)代邏輯的核心部分——數(shù)理邏輯的思想和方法，從而實(shí)現(xiàn)學(xué)習(xí)目的。

四、邏輯學(xué)習(xí)軟件LPL的應(yīng)用

1.用Boole解釋的后承關(guān)系

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

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

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

修正。

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

作為一個(gè)反例。我們也可以用Boole即真值表揭示結(jié)論不是前提的一個(gè)重言后承。事實(shí)上，最后一個(gè)真值表可達(dá)到這一目的。因?yàn)樵谶@個(gè)真值表的第5行中，前提B∨C和A∨C的值都為真，但結(jié)論 A∨?B的值為假。因此，A∨?B不是前提B∨C和A∨C的一個(gè)后承，即：

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

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

2.用Fitch展示的形式證明

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

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

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

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

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

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

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

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

最后，再點(diǎn)擊Proof菜單中的Verify Proof命令，目標(biāo)語句?A∧?B這一行將出現(xiàn)一個(gè)√，它表明這個(gè)證明是正確的。

在Fitch中證明如下推理：

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

第一步：按照Fitch的規(guī)定，首先把假設(shè)公式?xP（x）輸入在橫線的上面；并把要推出的結(jié)論x?P（x）放入目標(biāo)欄。

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

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

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

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

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

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

第七步：第6行產(chǎn)生的矛盾，是因?yàn)榈谒牟降募僭O(shè)?P（c）不成立，所以在第7行中輸入公式??P（c），并在Rule？規(guī)則欄中選擇?-Intro。點(diǎn)擊以 ?P（c）開始的子證明，再點(diǎn)擊頁面上的驗(yàn)證按鈕，這一步可以得到驗(yàn)證。

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

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

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

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

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

最后，點(diǎn)擊Proof菜單中的Verify Proof命令，目標(biāo)語句x?P（x）這一行將出現(xiàn)一個(gè)√，它表明這個(gè)證明是正確的。

3.用Tarskis World構(gòu)造的反例

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

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

是無效的。我們可以借助Tarskis World構(gòu)造一個(gè)前提真結(jié)論假的世界（即：模型）。其中，用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行，然后點(diǎn)擊頁面上的驗(yàn)證按鈕鍵，得到在當(dāng)前的世界窗口中，前提語句Dodec（e），Meduim（e）和? Dodec（e）∨ Meduim（e）∨ Dodec（f）的值為真，而結(jié)論語句Dodec（f）的值為假。因此，該推理是無效的。

下面的推理：

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

也是無效的。我們?nèi)匀豢梢越柚鶷arskis World構(gòu)造一個(gè)前提真結(jié)論假的世界（即：模型）。其中，用Cube（x）代表P（x），用Small（x）代表Q（x）。于是，在未命名世界窗口中，放置一個(gè)大的立方體和一個(gè)小的錐體；在未命名語句窗口中，將xCube（x）∧xSmall（x）和x（Cube（x）∧ Small（x））分別輸入在未命名語句窗口的1至2行，然后點(diǎn)擊頁面上的驗(yàn)證按鈕鍵，得到在當(dāng)前的世界窗口中，前提語句

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

參考文獻(xiàn)：

[1]李娜.數(shù)理邏輯實(shí)驗(yàn)教程[M].武漢：武漢大學(xué)出版社，2010.

[2]李娜.邏輯學(xué)實(shí)驗(yàn)教程[M].天津：南開大學(xué)出版社，2012.

[3]李娜.實(shí)驗(yàn)邏輯學(xué)[M].天津：南開大學(xué)出版社，2017.8

[責(zé)任編輯：陳立民]