关于一阶逻辑范式定理的几个等值式的一个注记
关于一阶逻辑范式定理的
几个等值式的一个注记
王金华 钱李新
(数学系)
摘 要
以{→,～}为连词完全集的一阶逻辑前束范式定理是由4个等值式得到的。对于4个等值式,本文得到了它们之间的一个基本关系;同时,利用不带等词的一阶系统K中的两个定理来证明了
4个等值式是两两等价的。
关键词:一阶逻辑;前束范式;范式定理
文献[1]是关于数理逻辑的较为著名的教材,目前国内已有数种译本[3～4]流行。该书第四章给出了一阶逻辑范式定理:对L的任意合式公式A,总存在前束范式B,并在证明上等价
于A。该定理须经以下4个等值式得到:
令A,B为L中的合式公式,K是不带等词的一阶系统,在K中有:
(i) 若x i在A中不自由出现,则
K
(( x i)(A→B)←→(A→( x i)B))
K (( x i)(A→B)←→(A→( x i)B))
(1)
(2)
(ii) 若x i在B中不自由出现,则
K
(( x i)(A→B)←→(( x i)A→B))
K (( x i)(A→B)←→(( x i)A→B))
(3)
(4)
文献[1]与文献[2]都只指出了这4个等值式可各自给出证明,我们查阅了其他文献,也未见它们之间的相互联系。本文得到了这4个等值式之间有下列关系:
定理1 一阶逻辑的等值式(1)式与(3)式等价,(2)式与(4)式等价。
为了证明定理1,我们先给出一个引理,以下所有讨论所引用的记号与结果均可参见文献[1]。
引理1 令A,B为L中的合式公式,x i为任意变元,则
K
(( x i)(A→B)←→( x i)(～B→～A))
K (( x i)(A→B)←→( x i)(～B→～A))
第22卷第3期浙江师大学报(自然科学版)Vol.22,No.3 1999年8月 JOURNAL OF ZHE JIANG NORM AL U NIVERS IT Y(Nat.S ci.) Aug.1999
收文日期:1998-12-05
证明 (1) ( x i )(A →B ) 假设
(2) (A →B )→(～B →～A )K 3
(3) ( x i )(A →B )→(A →B )K 4或K 5
(4) A →B (1),(3)MP
(5) ～B →～A (2),(4)MP
(6) ( x i )(～B →～A )(5)G
所以,有
( x i )(A →B ) K
( x i )(～B →～A )由演绎定理得
K (( x i )(A →B )→( x i )(～B →～A ))
同理可得
K
(( x i )(～B →～A )→( x i )(A →B ))综合上述两式得
K
(( x i )(A →B )←→( x i )(～B →～A ))即引理1中的第一个式子成立。下面来证明引理1中的第二个式子成立。因为已知
K ((～B →～A )→(A →B ))
所以,有
K
(～(A →B )→～(～B →～A ))( x i )(～(A →B )) K
～(～B →～A ) K
(( x i )(～(A →B ))→( x i )(～(～B →～A ))) K
(( x i )(～B →～A )→( x i )(A →B ))同理可得
K
(( x i )(A →B )→( x i )(～B →～A ))从而有
K
(( x i )(A →B )←→( x i )(～B →～A )) 下面来证明定理1。
证明 若(1)式成立,当x i 在B 中不自由出现时,则x i 在～B 中也不自由出现。所以,有
K
(( x i )(～B →～A )←→(～B →( x i )～A ))由引理1知 x i )(～B →～A ))17第3期 关于一阶逻辑范式定理的几个等值式的一个注记 王金华 钱李新
又
K
((( x i )A →B )←→(～B →( x i )～A ))所以,有
K
(( x i )(A →B )←→(( x i )A →B ))即(3)式成立。同理可得:若(3)式成立,则(1)式也成立,所以(1)式与(3)式等价。同样,若(2)式成立,当x i 在B 中不自由出现时,则x i 在～B 中也不自由出现,有
K
(( x i )(～B →～A )←→(～B →( x i )～A ))由引理1知
K
(( x i )(A →B )←→( x i )(～B →～A ))又
K
((～B →( x i )～A )←→(( x i )A →B ))所以,有
K
(( x i )(A →B )←→(( x i )A →B ))即(4)式成立。同理可得:若(4)式成立,则(2)式也成立。所以,(2)式与(4)式等价。
致谢:本文是在何伯镛教授的建议和指导下完成,深表感谢!
参考文献
1 Ham ilton A G .Iogic for M athem atics .Lannbridge U nivers ity Press ,1978
2 沈复兴.模型论导引.北京:北京师范大学出版社,1995
3 汉密尔顿A G 著;朱水林译.数理逻辑.上海:华东师范大学出版社,1986
4 汉密尔顿A G 著;骆如枫,陈慕昌,菇季札,黄万徽译.数学家的逻辑.上海:商务印书馆,1989
A Remark on Serveral Equivalent -valued Form ulas
of Prenex N ormal Form T heorem of First Order Iogic
Wang Jinhua Qin Lix in
(Dep ar tment of M athematics )
ABSTRACT
In the first order log ic w hose adequate set of co nnective is (→,～),we can use the four equivalent-v alued fo rmulas to show that the pr enex nor mal form theo rem is true.W e find that there ′s a basic relationship betw een the fo ur equiv alent -valued form ulas .In this paper ,w e make use of tw o theor em s o f the first order sy stem w ithout equality to prov e that tw o o f the four equivalent-v alued fo rmulas ar e equivalent to each other.
Key words :first order log ic ;prenex norm al form ;prenex norm al form theor em (责任编辑 陶立方)18
浙江师大学报(自然科学版) 1999年