形式陈述

固定形式系统 $\mathcal{S}$。对公式集 $\mathrm{\Gamma }$ 与公式 $\phi$，记 $\mathrm{\Gamma }{⊢}_{\mathcal{S}}\phi$，若存在以 $\phi$ 结尾的有限公式序列，其中每一项要么是前提、要么是公理实例、要么由先前各项按推理规则得到。任一具体证明只使用有限多个前提；无前提时写作 $⊢\phi$。

直觉

语义蕴涵检查所有模型，句法可推导检查是否存在一份有限、机械可验的证明证书；可靠性与完备性研究两者何时吻合。

例子与边界

在自然演绎中 $P\wedge Q⊢P$。符号 $⊢$ 依赖所选语言、公理和规则，不是对象语言中的蕴含联结词，也不自动表示语义真。

推论与应用

它是演绎定理、可靠性与完备性、一致性、可判定性和证明检查的共同接口。

参考资料

• Open Logic Project contributors, Open Logic Project (2026), proof systems and derivations.
• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed. (2001), formal deductions and metatheory.