协调、一致与一阶公理系统的强完全性

Harmonious,Consistent and the Strong Completeness of First-Order Axiom System

在公理系统中演绎定理是连接一致性和协调性的桥梁。对于带演绎定理的公理系统,可以证明公式集的一致性和协调性是等价的。在不带演绎定理的一阶公理系统中,一致性和协调性的差异集中体现在强完全性证明过程中。基于一致性的证明不依赖演绎定理,但基于协调性的强完全性证明多处受演绎定理束缚。文中将给出一个松绑方案,基于协调性上证明一阶公理系统QC1的强完全性。

In the axiom system,deduction theorem is the link connecting the harmony and consistency.For axiom systems which have deduction theorem,it can be proved that the consistent formulas set is equivalent to the harmonious one.For axiom systems without deduction theorem,the difference between harmony and consistency is embodied in strong complete proof process of the axiom system.The consistency-based proof of completeness does not rely on deduction theorem,but harmony-based one is constrained by the deduction theorem.This paper will give a harmony-based strong complete proof for the first-order axiom system of QC1.