摘要
Ａｎｄｒｅｗｓ在《ＡｎＩｎｔｒｏｄｕｃｔｉｏｎｔｏＭａｔｈｅｍａｔｉｃａｌＬｏｇｉｃａｎｄＴｙｐｅＴｈｅｏｒｙ：ＴｏＴｒｕｔｈＴｈｒｏｕｇｈＰｒｏｏｆ》一书中给出的语义树方法是一种能直接适用于句子集的反驳方法，但其中关于语义树方法的可靠性和完备性定理（３２０１）及其证明是错误的。本文通过例子指出并纠正了这一错误，同时对修正后的可靠性和完备性定理给出了详细的证明。
The semantic tableaux given in the book'An Introduction to Mathematical Logic and Type Theory:To Truth Through Proof' by Andrews is a refutation method which can be directly used for sentence sets.Nevertheless,the soundness and completeness theorem(3201) of the semantic tableaux method and the proving process are incorrect.In this paper,we illustrate and correct the mistake.In addition,we prove the revised theorem of the soundness and completeness.
出处
《国防科技大学学报》
EI
CAS
CSCD
北大核心
1994年第3期49-53,共5页
Journal of National University of Defense Technology
关键词
抽象协调类
语义树
可靠性
完备性
ss:abstract consistency class,semantic tableaux,soundness,completeness
