現(xiàn)代教育技術(shù)在“數(shù)理邏輯”課程中的應(yīng)用

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

當(dāng)考慮公式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構(gòu)造A∨B，?A和B的一個共享真值表，在這個共享真值表中，所有滿足和不滿足A∨B和?A的真值賦值σ都被列了出來。檢查這個真值表中的兩個前提A∨B和?A下面的列，我們可以看到只有一行，也就是在第三行中兩個前提都是真的，并且在此行結(jié)論B也是真的。這就證明了所有滿足A∨B和?A的真值賦值σ也滿足B。因此，B是A∨B和?A的一個重言（邏輯）后承。不難看出：A∨B也是?A 和B的一個重言后承。除此之外，我們還可以通過Boole上的評價鍵（Assessment）來給出我們的斷言，并通過Boole來驗證我們的斷言是否正確。驗證后的結(jié)果是→Last；→First。其中：→Last表明B是A∨B和?A的一個重言后承，→First表明A∨B也是?A 和B的一個重言后承。于是，有：

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

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

修正。

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

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

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

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

2.用Fitch展示的形式證明

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

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

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

第二步：我們想得到的結(jié)果是?A∧?B。但是，它是一個合取式。因此，必須在既得到?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時，使用的規(guī)則只能是∨-Intro（∨引入規(guī)則）。因此，在A∨B所在行的Rule？規(guī)則欄中點擊Intro下的∨，Rule？變成了∨-Intro，它表示：選取的規(guī)則是∨-Intro。然后，點擊A所在的行，再點擊頁面上的驗證按鈕，∨-Intro 前出現(xiàn)了一個√，它表明這一步的證明是正確的，我們可以繼續(xù)下一步的工作。否則，當(dāng)∨-Intro的前方出現(xiàn)×，此時表明這一步的證明是不正確的，我們要修正錯誤，直至出現(xiàn)√為止。同理可得：在B上左析取A，得到A∨B。

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

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

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

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

在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）矛盾，因此，建立第三個子證明，并選擇常項c。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

參考文獻(xiàn)：

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

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

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

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