摘 要：基于“数理逻辑”课程的教学特点，利用现代教育技术的教学手段，解决按照传统的教学方式讲授“数理逻辑”课程中两个比较突出的问题。从而提高学生们学习“数理逻辑”课程的兴趣，提高学生们独立思考、抽象思维和动手解决问题的能力，提高该课程的教学质量。
关键词：现代教育技术；应用；“数理逻辑”课程
随着逻辑学的发展，特别是近年来人工智能的发展，越来越凸显了数理逻辑的重要性。“数理逻辑”课程是逻辑学专业乃至哲学专业中的一门核心课程之一，同时它也是一门抽象的理论课程。长期以来，按照传统的教学方式授课，既不能使学生很好地理解“数理逻辑”课程中一些抽象的思想，也不能使學生熟练地掌握“数理逻辑”课程中的一些具体的方法。因此，它被师生们公认为是一门最难讲和最难学的课程。我们团队从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.用Tarski’s World构造的反例
通常，一个有效的推理，我们能用Fitch给出它的一个形式证明。然而，要说明一个推理是无效的，需要构造一个反例。构造反例，相对来说是困难的。但是，借助Tarski’s World，可以使我们轻松地构造反例。例如下面的推理：
A，B，¬A∨B∨C├C
是无效的。我们可以借助Tarski’s 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））
也是无效的。我们仍然可以借助Tarski’s 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
[责任编辑：陈立民]
