数理逻辑 第27章$2 一阶语言 王捍贫 北京大学信息科学技术学院软件研究所
27 §2 ✁✂✄ ☎✆✝✞✟✠✡✞☛☞✞✌✍✎✏✑✒
复习 阶谓词演算的符号化: 个体变元:x, 个体常元:a,b,c, 谓词:P",G",H 函数:門,gn,bn, 量词:全称量词v,存在量词彐 联结词:-,V,∧,←,→ 用这些符号可以更深入描述命题的结构。 怎么对这些符号进行推理? 下面直接建立推理的形式系统
✓ : • : x, y, z, . . . • : a, b, c, . . . • : Fn, Gn, Hn, . . . • : fn, gn, hn, . . . • : ∀, ∃ • : ¬, ∨, ∧, ←, ↔ ✔ ✕ ✔ 1
2-阶语言 阶语言是将要介绍的谓词演算系统形式语言。 符号/非逻辑符号 逻辑符号 谓词公式公式
§ 2 ✖ ✓ ✔ • • 2
非逻辑符号 可能包括下列符号: 个体常元符号: C, C1, C2 Cn, ●谓词符号: F",G,P",Q",R等 m(∈N,m>0)表示此谓词符号的元数 ●函数符号 fm,gmn,hm等 m(m∈N,n>0)表示此函数符号的元数 由一些非逻辑符号作为元素组成的集合常记为C
: • : c, c1, c2, · · · , cn, . . . • : Fn, Gn, Pn, Qn, Rn — n(n ∈ N, n > 0) • : fm, gm, hm — m(m ∈ N, n > 0) ✗✓ L. 3
逻辑符号 包括下列符号: 个体变元符号 0,北1,2 ●联结词符号: ●量词符号: 辅助符号:
: • : x0, x1, x2, . . . • : ¬, ∧, ∨, →, ↔ • : ∀, ∃ • : ), , , ( 4
逻辑符号与非逻辑符号 ●非逻辑符号更象是所描述的特定对象中的符号. 而逻辑符号是逻辑系统中的符号. 故此得名 在描述特定对象时,并不需要所有非逻辑符号. l可能用到所有逻辑符号. 阶语言与符号库指定的非逻辑符号集有关, 称为生成的一阶语言
• . . • , . . ✓ L , L ✘ 5
项 又生成的一阶语言的”项归纳定义如下 1.个体变元符号和中的个体常元符号都是项; 2.若m是中一个m元函数符号,t1,t2,…,tm是 C中项,则严m(t1,t2,…,tm)是中项; 3每个项都是有限次应用(1)和(2)得到的 ”项”相当于”复合个体
L ✓ ” ” : 1. L ; 2. fm L ✓ m , t1, t2, · · · , tm L , fm(t1, t2, · · · , tm) L ; 3. (1) (2) . ” ” ” ”. 6
公式 又生成的一阶语言的”公式”归纳定义如下: (1)如果F是c中的一个n元谓词符号,t1,t2,……,tn 是中项,则F(t1,t2,…,tn)是中公式, 称为原子公式 (2)若a是公式,则(a)是公式; (3)若a,β是公式,则(aVβ),(a∧B),(→), (a台6)是中公式; (4)若a是公式,x是个体变元符号,则(vx)a,(3x)a也 是公式; (5)每个公式都是有限次使用(1)-(4)得到的
L ✓ ” ” : (1) Fn L ✓ n , t1, t2, · · · , tn L , Fn(t1, t2, · · · , tn) L , — (2) α , (¬ α) ; (3) α, β , (α ∨ β), (α ∧ β), (α → β), (α ↔ β) L ; (4) α , x , (∀x)α, (∃x)α ; (5) (1)–(4) . 7
些注记 注1:与命题演算的形式语言相比,一阶语言中没有命 题符号,代之的是原子公式 注2:所有一阶语言中都含有相同的逻辑符号,但所含 的非逻辑符号不一定相同 注3:在定义中没有要求个体变元x一定要在a中出现: (x1)F2(x1,02)和(3)F2(m1,2)都是公式 注4:总假设:中至少有一个谓词符号. 否则生成的一阶语言中没有公式
✖ 1: , ✓ , . 2: ✓ , ✓ . 3: x ✓ α : (∀x1)F2(x1, x2) (∀x3)F2(x1, x2) . 4: : L ✘ . L ✓ ✔ 8
括号省略规则 ()省略公式最外层的括号; i)联结词符号””的优先级高于其它的四个联结词, 可以去掉(a)中的外层括号; 2 表示 (a1→(a2→…→(an-1→am)…); 对∨,∧,台也类似规定 (iV)x,彐c的优先级高于所有联结词 将(x)a、(3c)a分别记为wxa、3aa (v)(Vx1)…(wxn)a简记为vx1:xna; (3x1)…(3xn)o简记为彐x1 ama 9
(i) ; (ii) ”¬” , (¬ α) ; (iii) α1→α2→· · ·→αn−1→αn (α1→(α2→· · ·→(αn−1→αn) · · · )); ∨, ∧, ↔ . (iv) ∀x, ∃x . (∀x)α ✙(∃x)α ∀xα ✙∃xα. (v) (∀x1) · · · (∀xn)α ∀x1 · · · xnα; (∃x1) · · · (∃xn)α ∃x1 · · · xnα. 9