北京大学：《离散数学》系列课程之三《数理逻辑》第26章 命题逻辑（26.8）N与P的等价性

数理逻辑 第26章§8 N与P的等价性 王捍贫 北京大学信息科学技术学院软件研究所

26 §8 N P ￾✁✂ ✄☎✆✝✞✟✠✝✡☛✝☞✌✍✎✏✑

复习 ●命题演算推理形式系统N和P 相同之处: 都由四个组成部分 公式的构成方式相同 都是为了推理 ●不同之处: 符号库不同 一公理与规则不同 推理形式不同:「上a与}a

• N P • ✒ – ✓ – – – · · · • ✒ – – – ✒Γ ` α ` α – · · · 1

8N与P的等价性 「Fpa当且仅当「卜Na

§8 N P Γ `P α Γ `N α 2

「pa→「卜Na 问题:当厂为无限公式集时, 「+pa有可能成立(如当a∈「时) 但「卜Na不可能成立

Γ `P α ⇒ Γ `N α ✔✒Γ ✕ Γ `P α ( α ∈ Γ ). Γ `N α ✖ 3

定理13 设∑,a分别为P中公式集与公式,若∑Fpa,则存 在∑的有限子集Σ0≤∑,使得∑0pa 证明思路:尽管前提Σ可能有无限多个,但由于证明 过程是有限的,故在证明过程中用到的前提必定是 有限的 证:设a1,a2,…,αm(=α)是在前提∑下推 出a的一个证明. 令∑0=∑∩(a1,a2 则a1,a2,…,αn也是在前提Σ0下推出a的一个 证明,故∑0pa.从而∑0即为所求

13 Σ, α P , Σ `P α, Σ Σ0 ⊆ Σ, Σ0 `P α. ✗✘: Σ , ✙ , . : α1, α2, · · · , αn(= α) Σ α ✚ . Σ0 = Σ ∩ {α1, α2, · · · , αn}, α1, α2, · · · , αn Σ0 α ✚ , Σ0 `P α. Σ0 ✖ 4

引理1 若@是P中公理,则对P中任何有限公式集∑都有 ∑Na 证 a上N3→a 例13 a→(3→),a→Na→y 例13 0+xa→(月→a) 0N(a→(→)→(a→)→(a→))→+ ∑HNa→(6→a) ∑N(a→(→)→((a→3)→(a→)+ a→-3}N6→a 例15 ∑N(→a→6)→(3→a

1 α P , P Σ Σ `N α : α `N β→α 13 α→(β→γ), α→β `N α→γ 13 ∅ `N α→(β→α) → + ∅ `N (α→(β→γ))→((α→β)→(α→γ)) → + Σ `N α→(β→α) + Σ `N (α→(β→γ))→((α→β)→(α→γ)) + ¬ α→¬ β `N β→α 15 Σ `N (¬ α→¬ β)→(β→α) 5

定理14 设∑,O分别为P中有限公式集和公式 若∑Pa,则∑Na 证:设 C1,C2 是P中在前提∑下推出a的一个证明序列,(其中 只要证 对每个(1≤i<m),∑卜Na 下对归纳证之 6

14 Σ, α P . Σ `P α, Σ `N α. : α1, α2, · · · , αn P Σ α ✚ , ( : αn = α). : i (1 ≤ i ≤ n), Σ `N αi i . 6

定理14的归纳证明—奠基步骤 (1)当=1时,a1是P的一个公理,或a1∈∑ (1.1)若a1是P的一个公理,由引理1知∑卜Na1 (1.2)若a1∈∑,由N的规则(∈)知∑卜Na1

14 — (1) i = 1 , α1 P ✚ , α1 ∈ Σ. (1.1) α1 P ✚ , ✓1 Σ `N α1. (1.2) α1 ∈ Σ, ✓N (∈) Σ `N α1. 7

定理14的归纳证明一归纳步骤 (2)假设对满足j<的每个自然数都有∑上Naj 下证∑卜Na (21)当a;∈∑或者a;是P的公理时,类似(1)可 证∑Na (22)若a1,是由ak,a经(M)得到的(1<k,<, 不妨设ak=B,a1=月→a2 由于k,<i,由归纳假设知:∑Nak,∑Na, 即:∑卜Nβ,∑卜N6 应用(→-)规则得∑上a2 归纳证毕

14 — (2) j < i ✛j Σ `N αj, Σ `N αi. (2.1) αi ∈ Σ αi P , (1) Σ `N αi. (2.2) αi ✓αk, αl (M) (1 ≤ k, l < i), αk = β, αl = β→αi. ✓k, l < i, ✓: Σ `N αk, Σ `N αl, : Σ `N β, Σ `N β→αi, (→ −) Σ ` αi. ✖ 8

Na→「pa 问题: N的公式不一定是P的公式(如带联结词的公式)。 约定 aVβ代表(a)→β a∧B代表-(a→- a台B代表-((→)→-(→a)

Γ `N α ⇒ Γ `P α ✜✢ N ✚ P ( ∨ ) ✖ : α ∨ β (¬ α)→β α ∧ β ¬ (α → ¬ β) α ↔ β ¬((α→β) → ¬(β→α)) 9