推导与希尔伯特系统
一个推导系统(Deductive System)由一组称为公理(Axioms)的公式和一组推导规则(Rules of Inference)构成。
在推导系统中,一个证明(Proof)由一个公式序列构成:
其中,每一个公式要么是公理,要么是由前面公式 ()根据规则推导出来的公式。
序列里的最后一个公式称为定理(Theorem), 序列称为的一个证明(Proof). 称是可证明的(Provable),表示成.
如果, 那么可当作公理一样用于其它定理的证明。
希尔伯特系统是最早的推导系统之一。
希尔伯特系统()
公理 1:
公理 2:
公理 3:
假言推理(Modus Ponens):
由三个公理和一个推导规则构成。
Theorem
Proof.
在基本的系统中,也可以派生出其它规则。
如前提引入规则(Assumption and Deduction):
下面借助前提引入规则,证明定理:
证明:
定理:
证明:
定理:
证明:
逆否规则(Contrapositive):
定理:
定理:
证明:
传递规则(Transitivity):
定理:
证明:
前提交换规则(Exchange of Antecedent):
定理:
证明:
否定之否定规则(Double Negation):
反证规则(Reductio Ad Absurdum):
定理:
希尔伯特系统的变种:
Axiom
Axiom
Axiom
.
不一定是三个公理,以下是四个公理的推导系统:
梅瑞狄斯定理(Meredith's Axiom):