类型一阶逻辑的理论证明探讨

开篇：润墨网以专业的文秘视角，为您筛选了一篇类型一阶逻辑的理论证明探讨范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！

摘要:类型一阶逻辑在传统的一阶逻辑上,引入了类型,它是多态多类逻辑程序设计语言的理论基础,对编译系统设计与实现的进一步发展具有重要意义。论文在类型一阶逻辑的理论层面进行了探讨,引入了基本简单导出的可靠性定理和等值符号的可替换性定理,并予以证明。通过这两个定理,可以简化类型一阶逻辑理论证明中的工作量,使得将来的理论研究更加方便。

关键词:一阶类型逻辑;B类型简单导出;原子简单导出;可靠性;可替换性定理

中图分类号:TP311文献标识码:A文章编号:1009-3044(2010)07-1657-03

Theoretical Proof of Typed First-order Logic

XU Dan

(Department of Computer Science of Xiamen University, Xiamen 361005, China)

Abstract: Type is introduced into the typed first-order logic, which is based on the traditional first-order logic and the theoretical foundation of polymorphic and polytypic logic programming language. Typed first-order is significant to the further development of the design and implementation of compilation system. This paper is a research at the theoretical level and it introduces reliability theorem of the basic and simple derivation and the exchangeability theorem of the equivalent symbols, and the two theorems are proved in this paper. With the two theorems, the workload of the first-order logic proof can be simplified and the future theoretical research will be easier.

Key words: typed first-order logic; B-typed simple derivation; atomic simple derivation;reliability; exchangeability theorem

自Prolog语言[1]诞生以来,逻辑程序设计成为一个新的方向。1970年代后期和1980年代初,在为Prolog语言建立了Horn子句理论之后,如何扩展Prolog,将无类型的逻辑程序设计语言改造成带类型的逻辑程序设计语言,同时建立新型逻辑程序设计语言的理论基础,扩展逻辑程序设计的应用范围,就成为一个重要的研究课题。1990年代中期,J. W. Floyd等人在系统总结前人工作的基础上,借鉴Prolog语言的诸多元素,并从Prolog语言的众多变形如IC-Prolog、NU-Prolog等以及ML语言、Modula-2语言中吸收新思想,推出了新型逻辑程序设计语言G?idel[2-4],试图改进Prolog语言中存在的不足并解决其中有争议的语义问题。作为一种逻辑程序设计语言,研究与开发G?idel,首先需要为其建立严格的数学基础,包括其语法和语义理论基础。从Prolog语言和G?idel语言的关系看,与传统的一阶逻辑[5-8]比较,G?idel的数学基础应该是多态多类的一阶逻辑,而且,G?idel语言的语法与多态多类一阶逻辑的类型合式公式之间有着密切的联系,G?idel语言的语义应该与多态多类一阶逻辑的模型之间有着密切的联系。于是,发展带类型的一阶逻辑理论(简称类型一阶逻辑)成为一种选择。

1 带类型的一阶逻辑的语法

本文继续文献[2-3]的工作。带类型的一阶逻辑来源于对G?idel语言的抽象,也来源于对一阶逻辑的扩展。我们约定,一阶类型逻辑中的基类型有:Integer,Real,String,Boolean,分别称为整型、实型、字符串型和布尔型。一阶类型逻辑语法和语义部分的内容见参考文献[2-3]。

2 简单导出的可靠性定理

为了定理说明的方便,以下引入几个定义。

定义2.1:记所有在解释下与基类型Boolean保持一致的类型符为B。

定义2.2:将无类型一阶命题逻辑P*中的某个合式公式做替换,使得原先的所有命题词替换为一阶类型逻辑中的某个布尔值类型的形式符号,由此得到一个类型合式公式的过程称为简单导出。特别的,如果替换的一阶类型逻辑中的某个布尔值类型的形式符号中的符号全部是类型为B的个体词(或者原子),则将此过程称为B类型简单导出(或者原子简单导出);如果命题词全部替换,每个命题词都只能使用B类型个体词和原子两者之一做替换,则称为基本简单导出。

定理2.1 B类型简单导出的可靠性定理

如果在无类型一阶命题逻辑P*中,有合式公式A是恒真的,则A经过B类型简单导出,得到的一阶类型逻辑下的合式公式也是恒真的。

原来的无类型逻辑中的命题词在某个赋值之下只有真假两种情况,和我们替换的个体词刚好一致,直观上看,这个公式是成立的。对此,我们做证明如下:

[数学归纳法]

设A中所有的命题词的集合为N={p1,p2,…,pn},生成C的替换函数(或者置换)为g={,,…,}(或者为σ={d1/p1,d2/p2,…,dn/pn}),其中的di是一阶类型逻辑中的某个类型为B的个体词。记A中命题词替换为某个个体词生成的一阶类型逻辑中的合式公式为g(A)=C(或者Aσ=C)。

任取一阶类型逻辑中的赋值φ,构造无类型一阶命题逻辑下的赋值φ,使得

φ(pi)=t当且仅当φ(g(pi))=φ(ej)=

φ(pi)=f当且仅当φ(g(pi))=φ(ej)=,其中ej是pi替换的目标。

显然,A和C的层数是相等的。由于A是恒真的,所以一定有φ(A)=t。施归纳于它们的层数t,需要证明的命题是φ(A)=t时,φ(C) =(为了证明的方便,以下同时证明φ(A)=f时,φ(C) =)。

基始:t=0时,A是一个命题词,C是一个个体词。根据φ的定义,若φ(A)=t则必有φ(C) =,若φ(A)=f则必有φ(C) =。

归纳:t=k(k>0)时。由于A来此于无类型一阶命题逻辑P*,故A和C只可能有以下五种形式(为了将无类型一阶命题逻辑中的逻辑连接词与一阶类型逻辑中的逻辑连接词区分开来,在类型一阶命题逻辑的逻辑连接词上添加下划线)。

1) A=■A1,C= C1,其中C1=g(A1)。若φ(A)=t,则φ(A1)=f,依据基始,有φ(C1) =。据 的定义,有φ(C) =。同理,φ(A)=f时,有φ(C) =< false,Boolean>。

2) A=A1■A2,C=C1∧C2,其中C1=g(A1),C2=g(A2)。若φ(A)=t,则φ(A1)=t且φ(A2)=t,依据基始,有φ(C1) =且φ(C2) =。据∧的定义,有φ(C) =。若φ(A)=f,则φ(A1)=f或φ(A2)=f。不妨设φ(A1)=f,依据基始,有φ(C1) =。据∧的定义,有φ(C) =。

3) A=A1■A2,C=C1?C2,其中C1=g(A1),C2=g(A2)。若φ(A)=t,则φ(A1)=t或者φ(A2)=t,不妨设φ(A1)=t,则依据基始,有φ(C1) =。据∨的定义,有φ(C) =。若φ(A)=f,则φ(A1)=f且φ(A2)=f,依据基始,有φ(C1) =且φ(C2) =。据∨的定义,有φ(C) =。

4) A=A1■A2,C=C1C2,其中C1=g(A1),C2=g(A2)。若φ(A)=t,则φ(A1)=f或者φ(A2)=t。当φ(A1)=f时,依据基始,有φ(C1) =,据的定义,有φ(C) =;当φ(A2)=t时,依据基始,有φ(C2) =,据的定义,有φ(C) =。若φ(A)=f,则φ(A1)=t且φ(A2)=f,依据基始,有φ(C1) =且φ(A2)= ,据的定义,有φ(C) =。

5) A=A1■A2,C=C1?圮C2,其中C1=g(A1),C2=g(A2)。若φ(A)=t,则φ(A1A2)=t且φ(A2A1)=t。依据第4步的结论,有φ(C1C2)=且φ(C2C1)=。据?圮的定义,有φ(C) =。若φ(A)=f,则φ(A1■A2)=f或者φ(A2■A1)=f。此处不妨设φ(A1■A2)=f,则依据第4步的结论,有φ(C1C2)=。据?圮的定义,有φ(C) =。

综上所述,φ(A)=t时,φ(C) =,φ(A)=f时,φ(C) =。

由于A是恒真的,所以一定有φ(A)=t。又因为φ是任取的一阶类型逻辑上的赋值,所以对于任意的一阶类型逻辑上的赋值?,都能通过构造无类型一阶逻辑上的赋值φ来证明φ(C) =,所以C是恒真的。

定理2.2 原子简单导出的可靠性定理

如果在无类型一阶命题逻辑P*中,有合式公式A是恒真的,则将A中所有的命题词一一替换为一阶类型逻辑中的某个原子,则新得到的一阶类型逻辑下的合式公式也是恒真的。

要证明这个定理,只要按照定理2.1的证明思路,构造赋值即可,此处不再证明,仅提供一个例子作为验证。

我们知道德・摩尔根律在P*下一定是成立的,由之,我们有以下恒真合式公式:

H1= (A∧B) ?圮A∨ B和 H2= (A∨B) ?圮A∧ B

构造替换函数g1={,},g2={,},其中,C1、C2和D都是一阶类型逻辑中的原子,则得到一阶类型逻辑中的g1(H1)= ( C1∧ C2)?圮 C1∨ C2,g2(H2)= ( D∧D)?圮 D∨ D。不论是哪一种赋值,C1、C2和D都只有或者两种值,所以以下我们分别对各种情况作讨论(假设赋值为φ):

对于g1(H1),

1) φ(C1)=,φ(C2)=,则φ(( C1∧ C2))=,φ( C1∨C2)=,故φ(g1(H1))= 。

2) φ(C1)=,φ(C2)=,则φ(( C1∧ C2))=,φ( C1∨C2)=,故φ(g1(H1))= 。

3) φ(C1)=,φ(C2)=,同2理,有φ(g1(H1))= 。

4) φ(C1)=,φ(C2)=,则φ(( C1∧C2))=,φ( C1∨C2)=,故φ(g1(H1))= 。

因此g1(H1)必是恒真合式公式。

对于g2(H2),它的情况比g1(H1)简单,显然也是恒真的。

定理2.3 基本简单导出的可靠性定理

如果在无类型一阶命题逻辑P*中,有合式公式A是恒真的,则A经过基本简单导出,得到的一阶类型逻辑下的合式公式也是恒真的。证明方法同定理2.1及定理2.2。

3 等值符号的可替换性定理

再次引入定义:

定义3.1:所有由基本简单导出得到的类型合式公式的集合称为基本简单导出集合。

等值符号的可替换性定理:设A、B、C是基本简单导出集合中的类型合式公式,Г是基本简单导出集合的子集,如果B和C等值(即B?圮C),由Г和A把B在其中的某些出现替换为C而得到Г'和A'。那么

[1] A?圮 A'

[2] (ГA) ?圮(Г'A')

分析:我们可以把式子[1]描述为M=(BC)?圮(AA'),于是只要证明(BC)?圮(AA')为恒真,原命题则得证。同理对于[2]式,只需证明N=(B?圮C)((ГA)?圮(Г'A'))为恒真即可。

证明:由于A、B、C是基本简单导出集合中的类型合式公式,Г是基本简单导出集合的子集,故一定存在无类型一阶命题逻辑P*中的合式公式A0、B0、C0和合式公式集合Г0,使得A、B、C分别由A0、B0、C0基本简单导出,Г中的所有合式公式都是由Г0中的某一个基本简单导出。

令GA(X)表示将A中某些B的出现替换为X,使得B的一个出现被替换当且仅当在构造A'时,该位置的B被替换。则A=GA(B),A'=GA(C)。显然一定有无类型一阶命题逻辑P*中的公式GA0(),使得GA()是由GA0()将其中的命题词替换为带类型一阶逻辑中的B类型个体词和原子得到的。于是对GA0(C0)做基本简单导出可以得到GA(C)= A'。记GA0(C0)= A0',即证明A'可以由导出A的A0替换部分B0的出现(即A0')再做基本简单导出得到。同理可证,有Г0'使得对Г0'中的所有合式公式做基本简单导出得到的集合是Г'。

构造无类型一阶命题逻辑P*中的合适公式M0=(B0?圮C0)(A0?圮A0'),N0=(B0?圮C0)((Г0A0) /(Г0'A0')),由A、B、C、Г和A0、B0、C0、Г0之间的被导出和导出的关系,显然可知,M0和N0做基本简单导出可以相应得到M和N。

已知在无类型一阶命题逻辑P*中,有等值公式的可替换性定理,则任意的M0和N0形式的公式都是恒真的。又因为M0和N0是由M和N分别作基本简单导出得到,根据基本简单导出的可靠性定理,M和N为恒真公式,于是定理得证。

4 结论

本文探讨了带类型一阶逻辑的理论证明方法,通过证明基本简单导出的可靠性定理,方便了带类型一阶逻辑的理论证明。比如,我们可以利用该可靠性定理,直接证明(+),如果Γ,b 则 Γ b 。

另外,等值符号的可替换性定理的证明,也一定程度上减轻了证明过程中的工作量。但是,基本简单导出的可靠性定理和等值符号的可替换性定理的应用范围只局限在基本简单导出集合之内。我们之后的任务是通过更多的理论探讨,拓展这两个定理的应用范围,从而更好的简化理论证明,构造完备的带类型一阶逻辑理论体系。

参考文献:

[1] 刘椿年,曹德和.Prolog语言、它的应用与实现[M].北京:科学出版社,1990.

[2] Hill P M, Lloyd J W. The Godel programming Language [M]. London:MIT Press,1994.

[3] 高伟.逻辑程序设计语言Godel的说明性语义[D].厦门:厦门大学计算机科学系,2009.

[4] 昌杰.逻辑程序设计语言Godel的过程性语义[D].厦门:厦门大学计算机科学系,2009.

[5] 胡世华,陆钟万.数理逻辑基础(上,下)[M].北京:科学出版社,1980.

[6] 耿素云,屈婉云,王捍贫.离散数学教程[M].北京:北京大学出版社,2003.

[7] 陆钟万.面向计算机的数理逻辑[M].北京:科学出版社, 1998.

[8] 孙明湘.数理逻辑[M].长沙:中南大学出版社,2004.