P的证明序列 定义15由P中公式组成的一个序列 1,a2, 若对每个(1<im),下列两条件之一成立 (1)a;是公理; (2)a是由序列(*)中a之前的某两个公式ay;ak(1≤ k<a)应用分离规则(M)得到的. 则an称为P的一个内定理,记作pan或amn 称(米)为Qn的一个证明序列 由例20知:卜P(a→6)→(a→a)
P 15 ✜P ✥ : α1, α2, · · · , αn (∗) i (1 ≤ i ≤ n), ✥ : (1) αi ; (2) αi ✜(∗) αi αj, αk(1 ≤ j, k < i) (M) . αn P ✥ ♣, `P αn ` αn, (∗) αn ✥ q. ✜20 : `P (α→β)→(α→α) 10
两个简单性质 (1)P的每个公理a都是P的一个内定理 (2)若a1,a2,…,am是P中的一个证明序列,则 对每个a;(1<<m)都有a
(1) P α P ✥ r. (2) α1, α2, · · · , αn P ✥ , αi (1 ≤ i ≤ n) ` αi. 11
例21 证明:}a→Q 证 (1)}a→((B→a)→a) (A1) (2)}(a→((→a)→a))→ (a→(→a))→(a→a) (A2) (3)(a→(→a)→(a→a)M(1)(2) (4)Fa→(→a) (A1) (5)Fa→a (M)(3)(4) 问:为什么可以在每个式的前面都可以加+?
21 ✧` α→α : (1) ` α→((β→α)→α) (A1) (2) ` (α→((β→α)→α))→ ((α→(β→α))→(α→α)) (A2) (3) ` (α→(β→α))→(α→α) M(1)(2) (4) ` α→(β→α) (A1) (5) ` α→α (M)(3)(4) s✧`? 12
补充例 证明:a→((a→)→) 证 (1)(a→)→(a→(a→6)→(a→) (2)(a→B)→((a→(a→)→(a→B)→ (a→)→(a→(a→)→(a→)→(a→8) (3)(a)-(a-(a→8)-(a-8)-(a→0) (4)(a→)→(a→(a→)) (5)(a→B)→(a→
: ` α → ((α → β) → β) : (1) (α → β) → (α → (α → β)) → (α → β) (2) (α → β) → (α → (α → β)) → (α → β)! → (α → β) → (α → (α → β)) → (α → β) → (α → β)! (3) (α → β) → (α → (α → β)) → (α → β) → (α → β) (4) (α → β) → (α → (α → β)) (5) (α → β) → (α → β) 13
补充例(续) (6)(a→)→(a→B) (a→)→a)→(a→)→B) (7)(a→)→a)→(a→6)→6 (8)((a→B)→a)→(a→B)→ a→((a→B)→a)→(a→6)→) (9)a→((a→6)→a)→(a→6)→3) (10)(a→((a→8)→a)→(a→)→) (a→((a→3)→a))→(a→((a→B)→) (11)(a→(a→)→a)→(a→((a→6)→) (12) →a (13)a→(a→B)→)
( ) (6) ( α → β ) → ( α → β ) → (( α → β ) → α ) → (( α → β ) → β ) (7) (( α → β ) → α ) → (( α → β ) → β ) (8) (( α → β ) → α ) → (( α → β ) → β ) ! → α → ((( α → β ) → α ) → (( α → β ) → β)) ! (9) α → ((( α → β ) → α ) → (( α → β ) → β)) (10) α → ((( α → β ) → α ) → (( α → β ) → β)) ! → ( α → (( α → β ) → α)) → ( α → (( α → β ) → β)) ! (11) ( α → (( α → β ) → α)) → ( α → (( α → β ) → β)) (12) α → (( α → β ) → α ) (13) α → (( α → β ) → β ) 14