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

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