数理逻辑 第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