姜誉
摘 要:一阶谓词逻辑推理是数理逻辑教学的重要内容之一。在一阶谓词逻辑推理教学中,保证量词引入规则、量词消去规则的内容与形式的统一性对学生正确接受和理解推理过程具有重要作用。文章从离散数学教学实践出发,介绍一阶谓词逻辑推理中的存在量词引入规则与量词消去规则的教学策略。
关键词:离散数学;存在量词;规则
中图分类号:G642.0 文献标识码:A 文章编号:1002-4107(2015)12-0003-02
离散数学是计算机科学与技术、软件工程等本科专业的一门基础课程,而数理逻辑是离散数学课程中的一个重要组成部分,对提高学生理解和构造数学证明的能力以及培养学生的计算思维(computational thinking)具有重要作用[1-2]。
命题逻辑和一阶谓词逻辑是数理逻辑教学内容中的两个部分。一阶谓词逻辑通过引入量词来表达个体与总体之间的内在联系与数量关系[3],从而克服了命题逻辑中无法表达数量关系的局限性。
量词包括全称量词和存在量词。全称量词表达个体域中的所有个体,通常用符号“ ”表示;存在量词表达个体域中的单个个体,通常用符号“ ”表示。一般用小写字母a、b、c等符号表示个体常元,用小写字母x、y、z等符号表示个体变元,用大写字母A、B、C、P、Q、R等符号表示谓词。在谓词公式 xP(x)或 xP(x)中,x是约束变元,也称变元x是约束出现,这时的P(x)称为 x或
x的辖域;如果谓词公式Q(y)中不存在变元y的约束出现,则称变元y在Q(y)中自由出现,或称y是自由变元。在谓词公式 x yP(x,y)或 x yP(x,y)中,变元x在 x或 x的辖域内是约束出现,但在 y或 y的辖域内是自由出现。
一阶谓词逻辑推理系统除了具有与命题逻辑推理中一样推理规则之外,还有4条与量词的引入和消去有关的规则,分别是全称量词引入规则(简记为 +或UG)、全称量词消去规则(简记为 -、UI或US)、存在量词引入规则(简记为 +或EG)、存在量词消去规则(简记为 -、EI或ES)。量词引入也称为量词泛化,量词消去也称为量词实例化或指定。这4条与量词有关的引入和消去规则极大地丰富了一阶谓词逻辑推理的表达能力。
在量词引入规则和量词消去规则的教学中,保证量词引入规则以及量词消去规则的内容与形式的统一性对学生正确理解和接受推理规则及推理过程具有重要作用,否则容易引起学生理解上的困惑。
一、现有的规则
我们以文献[3]中关于存在量词引入规则( +或EG)和存在量词消去规则( -、EI或ES)为例进行说明。文献[3]是普通高等教育“十一五”国家级规划教材,具有代表性。在文献[3]中给出的全称量词引入规则和全称量词消去规则的内容与形式是统一的,不存在理解上的困惑。
文献[3]给出的存在量词引入规则( +或EU)形式为:
或 (1)
以及
或 (2)
其中,x、y是个体变元符号,c是个体常元符号。应用该规则的前提要求是:在谓词公式A中,变元y不在 x和 x的辖域内自由出现,常元c不在 x和 x的辖域内出现。
在上述式(1)这对表述中,第一个表述成立的依据是公式A(c)→ xA(x)永真,因此有A(c) xA(x);第二个表述成立的依据是假言三段论规则:(B→A(c))∧(A(c)→ xA(x)) B→ xA(x)。式(2)的情形类似。 我们看到,这个规则称为“存在量词引入规则”,其推理结果在形式上也体现了存在量词 ,规则的内容与符号形式是统一的,学生易于理解和接受。
然而,文献[3]给出的存在量词消去规则( -或EI)的形式为:
或 (3)
以及
或 (4)
其中,y是个体变元符号,c是个体常元符号,应用该规则的前提要求是:变元y不在推理的任何前提公式以及谓词公式B中自由出现,常元c不在推理的任何前提公式以及谓词公式 xA(x)及B中出现。
我们看到,在这个称为“存在量词消去规则”的推理结果形式中反而出现了存在量词 ,使得规则的内容与符号形式不统一,导致学生理解上的困惑。
实际上,在上述式(3)这对表述中,第一个表述可以当作一条存在量词引入规则;该表述成立的依据是假言三段论规则:
( xA(x)→A(c))∧(A(c)→B) xA(x)→B。其中,常元c是满足谓词公式 xA(x)的个体。
而式(3)中的第二个表述在本质上不是消去存在量词,而是得出结论B,其成立的依据实质上是假言推理规则,即:
( xA(x)→A(c))∧( xA(x)) A(c)
以及
A(c)∧(A(c)→B) B。
其中,常元c是满足谓词公式 xA(x)的个体。因此,在该规则描述中的第二个表述其实是不必要的,可以从该规则中删去。
类似地,在式(4)这对表述中,第一个表述也可以当作一条存在量词引入规则;考虑到变元y的任意性,该表述成立的依据是假言推理规则( xA(x)→A(c))∧
( xA(x)) A(c)、化简规则A(y)→B A(c)→B以及假言三段论规则( xA(x)→A(c))∧(A(c)→B) xA(x)→B 。
其中,常元c是满足谓词公式 xA(x)的个体。
式(4)中的第二个表述在本质上也不是消去存在量词,而是得出结论B,其成立的依据实质上是假言推理规则( xA(x)→A(c))∧( xA(x)) A(c)、化简规则A(y)→B A(c)→B以及假言推理规则A(c)∧(A(c)→B)
B。其中,常元c是满足谓词公式 xA(x)的个体。因此,该表述其实也是不必要的,可以从该规则中删去。
二、修改后的规则
为了保证规则内容与形式的统一性,我们可以将式(3)的第一个表述以及式(4)的第一个表述纳入到存在量词引入规则中,这种做法
其中,x、y是个体变元符号,c是个体常元符号。应用该规则的前提要求是:应用式(5)或(7)时要求常元c、变元y分别不在公式A中 x和 x的辖域内出现和自由出现;应用式(6)或(8)时要求常元c、变元y分别不在公式A中 x和 x的辖域内、公式B以及推理的任何前提公式中出现和自由出现。
在修改后的存在量词引入规则( +或EU)中,式(5)的第二个表述和式(7)的第二个表述可以看成是在蕴含式的后件引入存在量词的情形,式(6)和式(8)的表述可以看成是在蕴含式的前件引入存在量词 的情形。这些表述具有内容与形式的统一性,便于学生理解和记忆,可以根据不同情形选择使用。
那么,存在量词消去规则应具有怎样的形式呢?我们可如下表述存在量词消去规则( -、EI或ES):
其中,c是个体常元符号。应用该规则前二个表述的前提要求是:常元c是满足公式 xA(x)的个体。
在修改后的存在量词消去规则( -、EI或ES)中,当常元c是满足公式 xA(x)的个体时,式(9)中第一个表述成立的依据是公式 xA(x)→A(c)为永真式,因此有
xA(x) A(c);第二个表述成立的依据是假言三段论规则:
(B→ xA(x))∧( xA(x)→A(c)) B→A(c)。第三个表述成立的依据是假言三段论规则:
(A(c)→ xA(x))∧( xA(x)→B) A(c)→B 。
与对修改后的存在量词引入规则( +或EU)形式的看法类似,在修改后的存在量词消去规则( -、EI或ES)中,第二个表述可以看成是在蕴含式的后件消去存在量词 的情形,第三个表述可以看成是在蕴含式的前件消去存在量词 的情形,这样更便于学生理解和记忆。修改后的存在量词消去规则( -、EI或ES)也是对文献[4]中对应规则的进一步扩充。
综上所述,在一阶谓词逻辑推理中,我们应保证规则的内容与形式的统一性,使学生正确理解和接受相应的推理规则,合理构造推理过程,从而有利于培养学生的计算思维能力以及提高学生的推理能力。
参考文献:
[1]Kenneth H.Rosen. Discrete mathematics and its
applications(7th Ed.)[M].McGraw-Hill(Asia)
Education Press,2012:xvi.
[2]Jeannette M.Wing. Computational thinking[J].
Communications of the ACM,2006,49(3):33-35.
[3]屈婉玲,耿素云,张立昂.离散数学(第二版)[M].北京:
高等教育出版社,2015:60,81.
[4]左孝凌,李为鑑,刘永才.离散数学[M].上海:上海科学
技术文献出版社,1982:76.