数理逻辑 第27章$3 阶谓词演算自然推演系统N 王捍贫 北京大学信息科学技术学院软件研究所
27 §3 NL ✁✂✄ ☎✆✝✞✟✠✡✞☛☞✞✌✍✎✏✑✒
复习 生成的一阶语言 个体变元 个体常元 胃词 符号库:{函数 量词 联结词 辅助符号 项 公式:}公式 自由与约束
L ✓ : • ✔ • ✔ ✕✖ 1
推演系统N的构成 给定非逻辑符号集,Ng的构成如 ●形式语言 g生成的一阶语言 ●形式推理: 形式公理: 形式规则:15条 (1)-(10)如N
NL L, NL : • : – L ✓ • : – : ∅ – : 15 (1)–(10) N 2
增加前提律 若「+a (+) 则「,Ba 思考题: 为什么把(+)作为规则,而不是象在命题演算那样 作为原定理?
Γ ` α Γ, β ` α (+) : ✗(+) ✘✙ ✚ ✛ 3
下消去律 若厂Wxa, 且t对x在a中自由, 则rFa(x/+) 直观含义: 若「能保证对任意的x,a(x)都成立, 则「也能保证当a中的x"取值”为的时候也成立 注意条件”t对x在a中自由”不可少
∀ Γ ` ∀xα, t x α ✕✖✜ Γ ` α(x/t) (∀−) ✔ Γ x, α(x) ✢, Γ ✣α x” ” t ✢✤ : ”t x α ✕✖” ✥ 4
下引入律 若厂Fa, 且x不在「的任何公式中自由出现 (V+) 则「ca 直观含义: 若「(x)能保证a(x)成立,但「没有对x作任何限制, 则「也能保证对任意的x,a(x)都成立。 注意:条件”m不在「的任何公式中自由出现”不可少
∀ Γ ` α, x Γ ✕✖ Γ ` ∀xα (∀+) ✔ Γ(x) α(x) ✢, Γ x , Γ x, α(x) ✢✤ :✦✧”x★✩Γ✪✫✬✭✮✯✰✱✲✳”★✴✵. 5
彐消去律 若「,a+月, 且不在「∪{分}的任何公式中自由出现 则「,彐ma 直观含义: 若「和a(x)一起才能保证(x)成立, 但「和月的性质与x无关 则「和xa(x)也能保证β(x-)也成立。 思考题:条件”a成立”和”彐成立”哪个更强? 注意:条件”x不在「∪{}的任何公式中自由出现”不可少
∃ Γ, α ` β, x Γ ∪ {β} ✕✖ Γ, ∃xα ` β (∃−) ✔ Γ α(x)✶ β(x) ✢, Γ β x Γ ∃xα(x) β(x) ✢✤ : ”α ” ”∃xα ” ✷ :✦✧”x★✩Γ ∪ {β}✪✫✬✭✮✯✰✱✲✳”★✴✵. 6
引入律 若厂Fa(x/t) 且t对x在a中自由, (+) 则厂上彐ca 直观含义: 若「能保证当Q中的x”取值”为的时候成立, 则『一定能保证有一个x使Q成立 (是使得彐a成立的”证据”) 注意条件”对x在a中自由”不可少
∃ Γ ` α(x/t), t x α ✕✖✜ Γ ` ∃xα (∃+) ✔ Γ ✣α x” ” t ✢, Γ✶✶ x α ✢. (t ∃xα ✢” ”.) : ”t x α ✕✖” ✥ 7
两个特例 注意到:a(x/)=a,且x对时x在a中自由 若Vxa, (-)中取+为x) 则「 若厂a, (+)中取t为x) 则+(a)a
: α(x/x) = α, x x α ✕✖. Γ ` ∀xα, Γ ` α ((∀−) t x) Γ ` α, Γ ` (∃x)α ((∃+) t x) 8
N的形式证明序列 若有限序列 「1 1,12 2 满足 (1)每个「(:1≤讠<m)都是Ng的有限公式集 (2)每个「a2(1<<m)都是对此序列中它 之前的若干个「;+a;(1≤j<)应用Ng的 形式规则得到的 则称此序列为NQ中的一个(形式)证明序列 此时也称am可由「n在Ng中形式推出, 记为「 m hna an或「n+an 注:和N中证明序列的定义几乎一样
NL Γ1 ` α1, Γ2 ` α2, · · · , Γn ` αn : (1) Γi(i : 1 ≤ i ≤ n) NL ✥ (2) Γi ` αi (1 ≤ i ≤ n) Γj ` αj (1 ≤ j < i) NL . NL ✓ ( ) ✸. αn ✖Γn NL , Γn `NL αn, Γn ` αn. ✹✺✻✯N ✼✽✾✿✪❀❁❂❃❄ ❅❆ 9
