怎样简化推理??? ●N的公理和规则多,推理当然方便; P的公理和规则相对少,所以造成推理复杂。 ●N的公理和规则直观,所以使用方便; P的公理和规则直观性差,证明思路不好发现。 ●将来会证明,N和P是等价的 ●程序设计语言也有类似现象: 若语言复杂,则描述性好,但可靠性验证困难; 若语言简单,则描述性差,但可靠性验证方便; 怎么发现和简化P中形式推理? —增加元定理 模仿N
ttt • N ✢◗ P ✢✤ • N ✢◗ P ✢✤ • ✢N P ✤ • ✧ ✢✢◗ ✢✢◗ • P ✉ —✈✇①②✗ —③④N 15
定理9 1.若a,}a→B,则β 证 Q的一个证明序列 Q→的一个证明序列 6 仍记为(M),但要注意与分离规则(M)的区别
9 1. ` α, ` α→β, ` β : . . . ` α α ✥ . . . ` α→β α→β ✥ ` β (M) (M) ⑤(M) ⑥ 16
定理9(续) 2.若}a→3,且β→,则a→ 证 (B→)→(a→(3→) →7的一个证明序列 a→(→) (M) ((a→(→))→(→)→(a→7)(A2) (a→)→(a→) <q→/→的一个证明序列 O→ 记为(Tr)
9( ) 2. ` α→β, ` β→γ, ` α→γ. : ` (β→γ)→(α→(β →γ)) (A1) . . . ` β→γ β→γ ⑦⑨⑧ ⑩❶❷❸❹ ` α→(β →γ) (M) ` ((α→(β →γ))→((α→β)→(α→γ)) (A2) ` (α→β)→(α→γ) (M) . . . ` α→β α→β ⑦⑨⑧ ⑩❶❷❸❹ ` α→γ (M) (Tr). 17