形式化2：证明系统

系统"/>

形式化2：证明系统

定义：环境Environment

环境 Γ \Gamma Γ是由 n n n个命题构成的命题列表

Γ = P 1 , P 2 , . . . , P n \Gamma = P_1,P_2,...,P_n Γ=P1​,P2​,...,Pn​

若 n = 0 n=0 n=0，则称之为空环境，并经常记作 ϕ \phi ϕ或直接省去。

定义：断言Judgement

断言是由环境 Γ \Gamma Γ和命题 P P P构成的元组

Γ ⊢ P \Gamma \vdash P Γ⊢P

直观上，一个断言表明：我们可以在假定证明环境 Γ \Gamma Γ中命题都成立的前提下，证明命题 P P P。

证明规则

证明规则是形如
Γ 1 ⊢ P 1 . . . Γ n ⊢ P n Γ ⊢ P ( r u l e − n a m e ) \cfrac{\Gamma_1 \vdash P_1 \ \ ... \ \ \Gamma_n \vdash P_n}{\Gamma \vdash P}(rule-name) Γ⊢PΓ1​⊢P1​  ...  Γn​⊢Pn​​(rule−name)

证明规则由以下三部分组成

• 前提：即横线上方的n条断言
• 结论：横线下方唯一的断言
• 规则名：唯一标识该规则

证明规则可以分为以下三类

• 引入规则：在给出的证明规则中，逻辑连接词出现在横线下方的结论中
• 消去规则：在给出的证明规则中，逻辑连接词出现在横线上方的前提中
• 公理var：由于单个命题 P P P中没有显式指明连接词，所以它不属于上面的任何一种

规则1：var

Γ , P ⊢ P ( V a r ) \cfrac{}{\Gamma , P \vdash P}(Var) Γ,P⊢P​(Var)

规则(Var)中前提数量为0，即显然结论成立，结论是一条公理，他表示若命题 P P P在环境中出现，显然可推出 P P P成立。

规则2：真

Γ ⊢ ⊤ ( ⊤ I ) \cfrac{}{\Gamma \vdash \top}(\top I) Γ⊢⊤​(⊤I)

规则 ( ⊤ I ) (\top I) (⊤I)是一条公理，他表示在任意环境中，命题 ⊤ \top ⊤都无条件成立。 ⊤ I \top I ⊤I中的 I I I代表引入（Introduction的首字母）

规则3：假

Γ ⊢ ⊥ Γ ⊢ P ( ⊥ E ) \cfrac{\Gamma \vdash \bot}{\Gamma \vdash P}(\bot E) Γ⊢PΓ⊢⊥​(⊥E)

规则 ( ⊥ E ) (\bot E) (⊥E)表示：若能证明假，则可推出任意命题 P P P为真， ⊥ E \bot E ⊥E中的 E E E表示消去（Elimination首字母）

规则4：合取

Γ ⊢ P . . . Γ ⊢ Q Γ ⊢ P ∧ Q ( ∧ I ) \cfrac{\Gamma \vdash P \ \ ... \ \ \Gamma \vdash Q}{\Gamma \vdash P \land Q}(\land I) Γ⊢P∧QΓ⊢P  ...  Γ⊢Q​(∧I)

规则 ( ∧ I ) (\land I) (∧I)表示，若前提中能够证明 P P P和 Q Q Q分别都成立，则可推出二者的合取命题 P ∧ Q P \land Q P∧Q成立

Γ ⊢ P ∧ Q Γ ⊢ P ( ∧ E 1 ) Γ ⊢ P ∧ Q Γ ⊢ Q ( ∧ E 2 ) \cfrac{\Gamma \vdash P \land Q}{\Gamma \vdash P}(\land E_1) \qquad \cfrac{\Gamma \vdash P \land Q}{\Gamma \vdash Q}(\land E_2) Γ⊢PΓ⊢P∧Q​(∧E1​)Γ⊢QΓ⊢P∧Q​(∧E2​)

规则 ( ∧ E 1 ) (\land E_1) (∧E1​)和 ( ∧ E 2 ) (\land E_2) (∧E2​)分别表示，若前提中能够证明合取命题 P ∧ Q P \land Q P∧Q成立，则可分别证明 P P P和 Q Q Q成立

规则5：析取

Γ ⊢ P Γ ⊢ P ∨ Q ( ∨ I 1 ) Γ ⊢ Q Γ ⊢ P ∨ Q ( ∨ I 2 ) \cfrac{\Gamma \vdash P}{\Gamma \vdash P \lor Q}(\lor I_1) \qquad \cfrac{\Gamma \vdash Q}{\Gamma \vdash P \lor Q}(\lor I_2) Γ⊢P∨QΓ⊢P​(∨I1​)Γ⊢P∨QΓ⊢Q​(∨I2​)

规则 ( ∨ I 1 ) (\lor I_1) (∨I1​)和 ( ∨ I 2 ) (\lor I_2) (∨I2​)分别表示，若前提中能够证明命题 P P P或 Q Q Q成立，则可证明析取命题 P ∨ Q P \lor Q P∨Q成立

Γ ⊢ P ∨ Q Γ , P ⊢ R Γ , Q ⊢ R Γ ⊢ R ( ∨ E ) \cfrac{\Gamma \vdash P \lor Q \qquad \Gamma,P \vdash R \qquad \Gamma,Q \vdash R}{\Gamma \vdash R}(\lor E) Γ⊢RΓ⊢P∨QΓ,P⊢RΓ,Q⊢R​(∨E)

规则 ( ∨ E ) (\lor E) (∨E)表示：在前提中若从环境 Γ \Gamma Γ能够推出析取命题 P ∨ Q P \lor Q P∨Q成立，且在 P P P或 Q Q Q分别成立的前提下都能推出 R R R成立，则可在环境 Γ \Gamma Γ下推出命题 R R R成立。

规则6：蕴含

Γ , P ⊢ Q Γ ⊢ P → Q ( → I ) \cfrac{\Gamma,P \vdash Q}{\Gamma \vdash P \to Q}(\to I) Γ⊢P→QΓ,P⊢Q​(→I)

规则 ( → I ) (\to I) (→I)表示，若能在环境 Γ , P \Gamma,P Γ,P下推出 Q Q Q成立，则可在环境 Γ \Gamma Γ下推出蕴含命题 P → Q P \to Q P→Q成立。

Γ ⊢ P → Q Γ ⊢ P Γ ⊢ Q ( → E ) \cfrac{\Gamma \vdash P \to Q \qquad \Gamma \vdash P}{\Gamma \vdash Q}(\to E) Γ⊢QΓ⊢P→QΓ⊢P​(→E)

规则 ( → E ) (\to E) (→E)表示，若命题 P → Q P \to Q P→Q和 P P P都成立，则可推出 Q Q Q成立

规则7：否定

Γ , P ⊢ ⊥ Γ ⊢ ¬ P ( ¬ I ) \cfrac{\Gamma,P \vdash \bot}{\Gamma \vdash \lnot P}(\lnot I) Γ⊢¬PΓ,P⊢⊥​(¬I)

规则 ( ¬ I ) (\lnot I) (¬I)表示，若在命题 P P P成立的前提下能够推出假，则可推出命题 P P P的否定 ¬ P \lnot P ¬P。这种证明方法通常称为反证法。

Γ ⊢ P Γ ⊢ ¬ P Γ ⊢ ⊥ ( ¬ E ) \cfrac{\Gamma \vdash P \qquad \Gamma \vdash \lnot P}{\Gamma \vdash \bot}(\lnot E) Γ⊢⊥Γ⊢PΓ⊢¬P​(¬E)

规则 ( ¬ E ) (\lnot E) (¬E)表示，若在环境 Γ \Gamma Γ下，能够同时推出命题 P P P和其否定 ¬ P \lnot P ¬P，则可推出 ⊥ \bot ⊥。

规则8：双重否定

Γ ⊢ ¬ ¬ P Γ ⊢ P ( ¬ ¬ E ) \cfrac{\Gamma \vdash \lnot \lnot P}{\Gamma \vdash P}(\lnot \lnot E) Γ⊢PΓ⊢¬¬P​(¬¬E)

规则 ( ¬ ¬ E ) (\lnot \lnot E) (¬¬E)表示，若在环境 Γ \Gamma Γ下推出命题 P P P的双重否定，则可推出 P P P。