国防科学技术大学：《数理逻辑》课程考试模拟试卷

《数理逻辑》课程考试模拟试卷 1.(每题2分,共10分)判断题(若正确,则在题前的括号中打√;否则,打 ): (a)()若合式公式A是永真式当且仅当合式公式B是永真式,则AB 是永真式。 (b)()若合式公式A是可满足的,则~A是不可满足的。 (c)()v((,x)y~(,y)是可满足的 (d)()设P是一个由P系统增加单个合式公式pq作为公理所得到 的系统,则P是协调的。 (e)()假定除个体常元外,一阶逻辑形式系统F1和F2的其余符号相 同。若F1F2,则Th(F1)CTh(F2)∩L(F1)。 2.(每题6分,共18分)简答题: (a)试证明P的推理规则MP是独立的 (b)试给出以下公式的矫正范式和前束范式 Vx( 是T的等词模型当且仅当D是无穷集合,并证明你的结 论。 1

￾✂✁☎✄☎✆☎✝✟✞✡✠☞☛☞✌☞✍☞✎☞✏☞✍☞✑ 1. (✒✔✓ 2 ✕✔✖✂✗ 10 ✕) ✘✔✙✔✓✛✚✢✜✔✣✔✤✔✖✂✥✔✦✔✓✔✧✔★✔✩✔✪✬✫✮✭ √ ✯✂✰✥✔✖✂✭ × ✱✳✲ (a) ( ) ✜✵✴✵✶✵✷✵✶ A ✸✵✹✵✺✵✶✵✻✵✼✵✽✵✻✵✴✵✶✵✷✵✶ B ✸✵✹✵✺✵✶✵✖✾✥ A ⊃ B ✸✔✹✔✺✔✶✔✿ (b) ( ) ✜✔✴✔✶✔✷✔✶ A ✸✔❀✔❁✔❂✔★✔✖❃✥ ∼ A ✸✔❄✔❀✔❁✔❂✔★✔✿ (c) ( )∀x(P(x, x) ⊃ ∀y ∼ P(x, y)) ✸✔❀✔❁✔❂✔★✔✿ (d) ( ) ❅ P 0 ✸✔❆✔❇✬❈ P ❉✔❊✔❋✔●✔❍✔❇✔✴✔✶✔✷✔✶ p ⊃ q ■✔❏✔✷✔❑✔▲✔▼✔◆ ★✔❉✔❊✔✖❃✥ P 0 ✸✔❖✔P✔★✔✿ (e) ( ) ◗❙❘❙❚❙❇❙❯❙❱❙❲❙❳❙✖❃❆❙❨❙❩❙❬❙❭❙✶❙❉❙❊ F1 ❪ F2 ★❙❫❙❴❙❵❙✪❙❛ ❜ ✿❃✜ F1 ⊆ F2 ✖❃✥ Th(F1) ⊂ Th(F2) T L(F1) ✿ 2. (✒✔✓ 6 ✕✔✖❃✗ 18 ✕) ❝✔❞✔✓✔✲ (a) ❡✔❢✬❣ P ★✔❤✔❑✔✐✔✥ MP ✸✔❥✔❦✔★✔✿ (b) ❡✔❧✔♠✔♥✔♦✔✷✔✶✔★✔♣✔✣✔q✔✶❪✧✔r✔q✔✶✔✿ ∀x(x ✸ Γ ★✔➡✔➐✔➔✔→✔✻✔✼✔✽✔✻ D ✸✔➢✔➤✔➈✔✴✔✖⑤②✔❢✬❣✮➥✔★✔➦ ➣✔✿ 1

阶逻辑(带等词)演算系统=导出规则和定理 A∈r THA (∈+) TAF B TAFB T.NAHB I卜B I卜A A TAVB’T+BVA TAFC TBFC TFAVB THC AI卜B FA^B I卜A∧B I卜AAB F.A卜B I上AB THA TFADB FADB TAHB TAH B THNA I卜AF~A I卜B THA THA (≡+) TFADB TFBA r}A≡B IFA三B IA2B’IB2A I卜A≡B ~A三~B P卜A (-) xA(在r中无自由出现) (t对A中x是自由的) TA(对A中x是自由的) TAFB(x在rU{B}中不自由) F彐xAr,SAB y对A中的x是自由的且 I卜B y在PU{BxA,B}中不自由 (EA) x=x(x为个体变元) (EAS) x=3(S2A=S4)(x,y对A中的z是自由的) (a3) 三ySC (y在C中不自由且y对C中的x是自由的) ([P]) 若r}A1,……,P卜An,且A1∧…AAnB为P-永真的,则卜B 若A,M在A中为肯定的且MN,则r+AN (D suba) 若+A,M在A中为否定的且+NM,则AN (≡su) 若A,且M≡N,则r+A ([sub-x])若ThA,x在r中不自由且t对A中的x为自由的则rhSA ([sub-p)若rhA,p在r中不出现且D对A中的p为自由的则SA

➧➉➨➉➩➉➫ (➭➉➯➉➲) ➳➉➵➉➸➉➺ F = ➻➉➼➉➽➉➾➉➚➉➪➉➶ (∈) A ∈ Γ Γ ` A (∈+) Γ ` B Γ, A ` B (∈−) Γ, A ` B Γ, ∼ A ` B Γ ` B (∨+) Γ ` A Γ ` A ∨ B , Γ ` A Γ ` B ∨ A (∨−) Γ, A ` C Γ, B ` C Γ ` A ∨ B Γ ` C (∧+) Γ ` A Γ ` B Γ ` A ∧ B (∧−) Γ ` A ∧ B Γ ` A , Γ ` A ∧ B Γ ` B (⊃+) Γ, A ` B Γ ` A ⊃ B (⊃−) Γ ` A Γ ` A ⊃ B Γ ` B (⊃ ¬) Γ ` A ⊃ B Γ `∼ B ⊃∼ A (¬+) Γ, A ` B Γ, A `∼ B Γ `∼ A (¬−) Γ ` A Γ `∼ A Γ ` B (¬¬+) Γ ` A Γ `∼∼ A (¬¬−) Γ `∼∼ A Γ ` A (≡+) Γ ` A ⊃ B Γ ` B ⊃ A Γ ` A ≡ B (≡−) Γ ` A ≡ B Γ ` A ⊃ B , Γ ` A ≡ B Γ ` B ⊃ A (≡ ¬) Γ ` A ≡ B Γ `∼ A ≡∼ B (∀+) Γ ` A Γ ` ∀xA (x ➹ Γ ➘➉➴❃➷➉➬ ➼➉➮) (∀−) Γ ` ∀xA Γ ` S x t A (t ➱ A ➘ x ✃❃➷➉➬❒❐) (∃+) Γ ` S x t A Γ ` ∃xA (t ➱ A ➘ x ✃❃➷➉➬❒❐) (∃−) Γ, A ` B Γ, ∃xA ` B (x ➹ Γ ∪ {B} ➘➉❮❃➷➉➬) (C) Γ ` ∃xA Γ, S x yA ` B Γ ` B  y ➱ A ➘➉❐ x ✃❃➷➉➬❒❐➉❰ y ➹ Γ ∪ {∃xA, B} ➘➉❮❃➷➉➬  (EA) Γ ` x = x (x Ï➉Ð➉Ñ➉Ò➉Ó) (EAS) ` x = y ⊃ (S z xA ≡ S z yA) (x, y ➱ A ➘➉❐ z ✃❃➷➉➬❒❐) (αβ) Γ ` A Γ ` A ∀xC ∀ySx y C , Γ ` A Γ ` A ∃xC ∃ySx y C (y ➹ C ➘➉❮❃➷➉➬❒❰ y ➱ C ➘➉❐ x ✃❃➷➉➬❒❐) ([P]) ÔΓ ` A1, · · · , Γ ` An, ❰A1 ∧ · · · ∧ An ⊃ BÏ P- Õ➉Ö➉❐, ➾Γ ` B ([⊃ sub1]) ÔΓ ` A, M ➹ A ➘➉Ï➉×➪❐➉❰ ` M ⊃ N, ➾Γ ` A M N . ([⊃ sub2]) ÔΓ ` A, M ➹ A ➘➉Ï➉Ø➪❐➉❰ ` N ⊃ M, ➾Γ ` A M N . ([≡ sub]) ÔΓ ` A, ❰ ` M ≡ N, ➾Γ ` A M N . ([sub − x]) Ô Γ ` A Ù x ➹ Γ ➘➉❮❃➷➉➬❒❰ t ➱ A ➘➉❐ x Ï❃➷➉➬❒❐ ➾Γ ` S x t A. ([sub − p]) Ô Γ ` A Ù p ➹ Γ ➘➉❮➼➉➮❰ D ➱ A ➘➉❐ p Ï❃➷➉➬❒❐ ➾Γ ` S p DA. 2