论经典命题逻辑公理系统L中的证明技巧

• 作者: 刘强 程和祥
• 来源期刊: 重庆理工大学学报（社会科学版）
• 学科: 哲学
• 关键词: 经典命题逻辑 公理系统L 消件法 换位法 演绎定理 构造性程序
• 年，卷（期）: 2019,（3）
• 所属期刊栏目: 逻辑与科学方法论
• 页码范围: 7-12
• 页数: 6页
• 分类号: B81
• 字数: 5658字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-8425(s).2019.03.002

摘要

在经典命题逻辑的学习中,公理系统L中的定理证明只能使用公理模式和推理规则,对于初学者而言,常常显得强人所难,主要表现为找不到证明的突破口.事实上,可以从两个方向出发:一方面,从公理模式出发,分析每条公理模式的特性,由此可得消件法和换位法两个小技巧;另一方面,通过使用演绎定理,一般我们可得到待证定理的演绎证明序列,而通过对演绎证明序列的“仔细观察”,可以获得相应公理证明的“突破口”.这些技巧,可以提高初学者的学习效率,优化数理逻辑的教学,也可以为定理机械化证明的理论和方法提供必要的实践准备,以促进新时代逻辑学教学现代化的实现.