›
›

Giáo trình Hệ toán tân từ - Chương 3: Hệ toán tân từ

pdf 58 trang ngocly 1800
Download
Bạn đang xem 20 trang mẫu của tài liệu "Giáo trình Hệ toán tân từ - Chương 3: Hệ toán tân từ", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

  • pdfgiao_trinh_he_toan_tan_tu_chuong_3_he_toan_tan_tu.pdf

Nội dung text: Giáo trình Hệ toán tân từ - Chương 3: Hệ toán tân từ

  1. Hệ toán tân từ
  2. Chương 3. Hệ toán tân từ Trần Thọ Châu Logic Toán. NXB Đại học quốc gia Hà Nội 2007. Tr 70-125. Từ khoá: Logic toán, Đại số mệnh đề, Lượng từ, Đồng nhất đúng, Định lý suy diễn, Tính phi mâu thuẫn, Tính đầy đủ. Tài liệu trong Thư viện điện tử ĐH Khoa học Tự nhiên có thể sử dụng cho mục đích học tập và nghiên cứu cá nhân. Nghiêm cấm mọi hình thức sao chép, in ấn phục vụ các mục đích khác nếu không được sự chấp thuận của nhà xuất bản và tác giả.
  3. Chu.o.ng 3 . Hˆe. to´antˆant`u . . . 3.1 C´acluo. ng t`u 71 3.2 C´ackh´ainiˆe.mv`adi.nhngh˜ıa 77 . 3.3 Minh hoa. ,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh . . . 81 3.3.1 Minh hoa. 81 . . . 3.3.2 T´ınhthu. chiˆe.n duo. c 83 . 3.3.3 Su. dˆo`ng nhˆa´t d´ung (h˘a`ng d´ung) 85 3.3.4 Mˆoh`ınh 85 3.3.5 Mˆo.tsˆo´ hˆe. qua’ 86 3.3.6 Mˆo.tsˆo´ di.nhngh˜ıakh´ac 89 . 3.3.7 C´accˆongth´uc logic dˆo`ng nhˆa´t d´ung trong hˆe. to´an tˆant`u. 92 . 3.3.8 Da.ng chuˆa’nt˘a´c trong logic tˆant`u 93 3.4 L´ythuyˆe´t tˆant`u. cˆa´p1K 100 3.4.1 Di.nhngh˜ıa 100 . 3.4.2 Mˆo.t v`aith´ıdu. vˆe` L´ythuyˆe´ttˆant`ucˆa´p 1K . . . . 103 . 3.5 Di.nh l´ysuy diˆe˜n trong logic tˆant`u 104
  4. . . . 3.1. C´acluo. ng t`u 71 3.6 T´ınhphi mˆauthuˆa˜n v`a dˆa` y du’ cu’a logic tˆant`u. 110 3.6.1 C´ackh´ainiˆe.mv`adi.nhngh˜ıa 110 3.6.2 T´ınhphi mˆauthuˆa˜ncu’a l´ythuyˆe´t tˆant`u. cˆa´p 1 PP111 . 3.6.3 Mˆo.tsˆo´ di.nh l´ytrong l´ythuyˆe´t tˆant`u cˆa´p1K 112 3.6.4 T´ınh dˆa`y du’ cu’a l´ythuyˆe´t tˆant`u. cˆa´p 1K . . . . . 120 ´ . 3.7 Ap du. ng trong ch´ung minh di.nh l´ycu’a l´ythuyˆe´t tˆant`u. cˆa´p1 121 . . 3.8 B`aitˆa. p chuong3 123 . . Logic tˆant`u l`amˆo.thˆe. thˆo´ng logic phˆo’ biˆe´n nhˆa´t m`angˆonng˜u cu’an´o . gi´upta h`ınhth`anhc´ackh´ainiˆe.m, c´acthuˆo.c t´ınh,c´acquan hˆe.,v`at`u d´o di . . . . dˆe´n ph´an do´an,c˜ungnhu c´acco chˆe´ lˆa.p luˆa.nch˘a.t ch˜e,gi´upcon ngu`oihiˆe’u . . . r˜ov`asˆaus˘a´cba’nchˆa´tcu’a c´ac dˆo´ituo. ng. Do d´oc´othˆe’ n´oilogic tˆant`u . l`amˆo.t cˆongcu. nˆe` nta’ng cho su. ph´attriˆe’ncu’a nhiˆe` u l´ythuyˆe´t khoa ho.c, . d˘a.cbiˆe.t l`aTo´anho.c, ch˘a’ ng ha.nnhub`aito´an“Tˆo`nta.i ´ıtnhˆa´tmˆo.t nghiˆe.m . . . . x1,x2, , xn”cu’a da th´uc n biˆe´n f(x1,x2, , xn) duo. cbiˆe’udiˆe˜n nh`o logic tˆant`u. nhu. sau: ∃x1∃x2 ∃xn(f(x1,x2, , xn)=0). . . . 3.1 C´acluo. ng t`u . . . . Logic tˆant`u l`asu. ph´attriˆe’nmo’ rˆo.ng tu. nhiˆencu’a logic mˆe.nh dˆe` nh˘a`mthˆe’ . . hiˆe.nmˆo.t c´ach dˆa`y du’ v`ach˘a.tch˜enh˜ung kˆe´t luˆa.t thu. ctˆe´ m`alogic mˆe.nh dˆe` . . khˆongthˆe’ n`aodiˆe˜nta’ duo. c, ch˘a’ ng ha.n: . . (1) Mˆo˜imˆo.t ngu`oiba.ncu’a Mai l`aba.ncu’aYˆe´n. Ph´uckhˆongpha’i l`aba.n cu’aYˆe´n, nˆenPh´uckhˆongpha’i l`aba.ncu’a Mai. . . . . . . (2) Mo.i ngu`oi dˆe` ubˆa´ttu’ . Socrates l`angu`oi, nˆenSocrates l`abˆa´ttu’ . . . Dˆe’ c´othˆe’ mˆota’ b˘a`ng To´anho.cnh˜ung mˆe.nh dˆe` trˆen,ta dua ra mˆo.tsˆo´ k´yhiˆe.u d˘a.cbiˆe.t:
  5. . . . 72 Chuong 3. Hˆe. to´antˆant`u –Nˆe´u P (x) c´ongh˜ıa l`a“x c´ot´ınhchˆa´t P ” th`ıkhi d´o ∀xP (x) c´ongh˜ıa l`a“Mˆo˜imˆo. tvˆa. t x c´ot´ınh chˆa´t P ”, hay n´oic´ach kh´ac:“Mo. i x c´ot´ınh chˆa´t P ”. –Nˆe´utak´yhiˆe.u ∃xP (x) c´ongh˜ıal`a“Tˆo`nta. i ´ıtnhˆa´tmˆo. tvˆa. t x c´ot´ınh chˆa´t P ”. Khi d´otrong c´acbiˆe’uth´u.c trˆen: . . . . . – ∀xP (x) th`ıphˆa`n ∀x duo. cgo.i l`aphˆa`nluo. ng t`u, trong d´ok´yhiˆe.u ∀ - . . . . . . . . . . duo. cgo.il`aluo. ng t`u to`anthˆe’,v`ax duo. cgo.il`abiˆe´nluo. ng t`u. . . . . . – ∃xP (x) th`ıphˆa`n ∃x duo. cgo.i l`aphˆa`nluo. ng t`u, trong d´ok´yhiˆe.u ∃ . . . . . . . . . . duo. cgo.il`aluo. ng t`u tˆo`nta. i, c`on x duo. cgo.il`abiˆe´nluo. ng t`u. . . . – Trong ca’ 2biˆe’uth´uc th`ıphˆa`n P (x) duo. cgo.il`amiˆe` n t´acdu. ng (scope) . . . cu’aluo. ng t`u. . Dˆo´iv´oi c´acth´ıdu. d˜acho, nˆe´utak´yhiˆe.u: m, y, p, s, F (x, y),M(x), I(x) . . . tuong ´ung l`a“Mai”, “Yˆe´n”, “Ph´uc”, “Socrates”, “x l`aba.ncu’a y”, “x l`a . . . . . . ngu`oi”, “x l`abˆa´ttu’ ” th`ıkhi d´oc´ackˆe´t luˆa.nt`u (1) dˆe´n (2) duo. cbiˆe’udiˆe˜n nhu. sau: (10 ) ∀x(F (x, m) → F (x, y)) (a) ¬F (p, y)(b) ¬F (p, m) (20 ) ∀x(M(x) → I(x)) (c) M(s)(d) I(s) . 0 Trong cˆongth´uc(1), ta d˜ak´yhiˆe.u“F (y,z)” c´ongh˜ıal`a“y l`aba.ncu’a . . . . . . . z” . Khi d´o dˆo´iv´oimˆe.nh dˆe` (a) ta ´apdu.ng luo. ng t`u ∀x cho tru`ong ho. p . . riˆeng“x l`a p”, ta nhˆa.n duo. cmˆe.nh dˆe` sau l`amˆe.nh dˆe` d´ung: F (p, m) → F (p, y) (e)
  6. . . . 3.1. C´acluo. ng t`u 73 . Trong logic mˆe.nh dˆe` ta c´ocˆongth´uc sau: (A → B) → (¬B →¬A)l`a cˆongth´u.c dˆo`ng nhˆa´t d´ung. Do d´ota thay A = F (p, m), v`a B = F (p, y), ta nhˆa.nmˆe.nh dˆe` sau dˆayl`a d´ung: ¬F (p, y) →¬F (p, m)(f) . . . nh`o qui t˘a´c Modus Ponens. Ap´ du. ng Modus Ponens mˆo.tlˆa`nn˜ua dˆo´iv´oi . . (b) v`a(f), ta nhˆa.n duo. ckˆe´t qua’: ¬F (p, m), ngh˜ıa l`a“Ph´uckhˆongpha’i l`aba. ncu’a Mai”  . 0 . . . . Trong cˆongth´uc(2) ta ´apdu.ng luo. ng t`u to`anthˆe’ ∀x dˆo´iv´oimˆe.nh dˆe` . . (c) b˘a`ng c´ach thay “x l`a s”, ta nhˆa.n duo. cmˆe.nh dˆe` sau dˆayl`a d´ung: M(s) → I(s)(g) . . Ap´ du.ng qui t˘a´c Modus Ponens cho (d) v`a(g), ta nhˆa.n duo. ckˆe´t qua’ l`a: I(s), ngh˜ıa l`a“Socrates l`abˆa´ttu’.”.  . . . Mˆo.t diˆe` uth´uvi. l`ata c´othˆe’ kiˆe’m tra b˘a`ng chuong tr`ınhth´ıdu. th´u 2 . . . v´oikˆe´t qua’ “Socrates l`abˆa´ttu’ ”b˘a`ng ngˆonng˜u lˆa.p tr`ınhPROLOG version 2.0 ([6]) d`ung trong Tr´ıtuˆe. nhˆanta.o. . . Khi ta v`aomˆoitru`ong l`amviˆe.ccu’a TURBO PROLOG m`anh`ınhbao gˆo`m4cu’.asˆo’ sau dˆay: . . H˜ayv`aomu.c File/Load, cho.n tˆen chuong tr`ınhAI1.PRO v`athˆemchı’ thi. trace (vˆe´t) lˆen dˆa`u chu.o.ng tr`ınh:
  7. . . . 74 Chuong 3. Hˆe. to´antˆant`u /*AI1.PRO*/ trace domains human, immortal=symbol predicates is(symbol, symbol) clauses is(X, immortal): - is(X, human). is(“Socrates”, human). goal is(X, Y ), write(X, “is”, Y ). . . . . . Ta cha.y chuong tr`ınht`ung bu´o c (theo vˆe´t): *Bˆa´m Alt-R . –O’ cu’.asˆo’ Edit con tro’ chı’ t`u. goal . –O’ cu’.asˆo’ Trace ta thˆa´y CALL: goal () * H˜aybˆa´m F10 (lˆa`nth´u. nhˆa´t) . –O’ cu’.asˆo’ Edit con tro’ chı’ tˆant`u. is(X, Y ) . –O’ cu’.asˆo’ Trace ta thˆa´y CALL: is( , )
  8. . . . 3.1. C´acluo. ng t`u 75 *Bˆa´m F10 (lˆa`nth´u. 2) . –O’ cu’.asˆo’ Edit con tro’ chı’ qui t˘a´c is(X, immortal): - is(X, “human” ) *Bˆa´m F10 (lˆa`nth´u. 3) . –O’ cu’.asˆo’ Edit con tro’ chı’ is (X, human) . –O’ cu’.asˆo’ Trace ta thˆa´y CALL: is ( , “human” ) *Bˆa´m F10 (lˆa`nth´u. 4) ’. . . O cu’ asˆo’ Edit con tro’ chı’ vi. tr´ıt`u is (X, immortal) *Bˆa´m F10 (lˆa`nth´u. 5) ’. . . –Ocu’ asˆo’ Edit con tro’ chı’ su. kiˆe.n is (“Socrates”, human) . –O’ cu’.asˆo’ Trace ta thˆa´y REDO: is( , “human” ) *Bˆa´m F10 (lˆa`nth´u. 6) . –O’ cu’.asˆo’ Edit con tro’ vˆa˜nchı’ is (“Socrates”, human) ’. . . . –Ocu’ asˆo’ Trace ta duo. c RETURN: is (“Socrates”, “human” ) *Bˆa´m F10 (lˆa`nth´u. 7)
  9. . . . 76 Chuong 3. Hˆe. to´antˆant`u ’. . –Ocu’ asˆo’ Edit con tro’ la.ichı’ is (X, immortal) . –O’ cu’.asˆo’ Trace ta c´o RETURN: *is (“Socrates”, “immortal” ) *Bˆa´m F10 (lˆa`nth´u. 8) . –O’ cu’.asˆo’ Edit con tro’ chı’ ch˜u. X trong write (X, “is”, Y ) . –O’ cu’.asˆo’ Trace ta c´o write(“Socrates” ) *Bˆa´m F10 (lˆa`nth´u. 9) ’. . . –Ocu’ asˆo’ Dialog xuˆa´thiˆe.nt`u Socrates . –O’ cu’.asˆo’ Edit con tro’ chuyˆe’nt`u. X sang chı’ “is” trong write(X, “is”, Y ) . –O’ cu’.asˆo’ Trace ta c´o write(“is” ) *Bˆa´m F10 (lˆa`nth´u. 10) ’. . . . . . –Ocu’ asˆo’ Dialog ta duo. cthˆemt`u is, t´ucl`aSocrates is . –O’ cu’.asˆo’ Edit con tro’ chuyˆe’nt`u. “is” sang chı’ sˆo´ Y trong write(X, “is”, Y ) . –O’ cu’.asˆo’ Trace ta c´o write(“immortal” ) *Bˆa´m F10 (lˆa`nth´u. 11) . –O’ cu’.asˆo’ Dialog ta c´othˆemt`u. immortal, t´u.c l`aSocrates is im- mortal
  10. 3.2. C´ackh´ainiˆe.mv`adi.nh ngh˜ıa 77 . –O’ cu’.asˆo’ Edit con tro’ chı’ t`u. goal . –O’ cu’.asˆo’ Trace ta c´o RETURN: goal() *Bˆa´m F10 (lˆa`nth´u. 12) . –O’ cu’.asˆo’ Dialog thˆem cˆaunh˘a´c nho’. Press the SPACE bar t´u.cl`a . . . bˆa´m thanh ngang dˆe’ tro’ vˆ`e mˆoitru`ong l`amviˆe.cc˜u. . . . . . . . Nhu vˆa.y sau 12 bu´oc thu. chiˆe.nbˆa´m F10 ta d˜athu duo.cl`oi gia’i d´ap: Socrates is immortal hay l`a Socrates l`abˆa´ttu’  . . Thu. cchˆa´ttad˜asu’ du.ng c´acda.ng cˆaulˆe.nh dˆe’ chı’ cˆa´utr´uc logic cu’avˆa´n . dˆe` .Cˆa´utr´uc n`ayphu. thuˆo.c v`aoc´acliˆen kˆe´tmˆe.nh dˆe` c˜ung nhu da.ng suy . . . . . diˆe˜n c´osu’ du.ng c´acluo. ng t`u,ch˘a’ ng ha.nnhuc´acth´ıdu. (1) v`a(2), ta d˜ac´o . . . 0 0 thˆe’ biˆe’udiˆe˜nch´ung mˆo.t c´ach tr`uutuo. ng qua (1 ) v`a(2 ). . . . . Dˆe’ da.t duo. cmu.c d´ıch n`ay, ta cˆa`n pha’isu’ du.ng c´ack´yhiˆe.unhudˆa´u phˆa’y, c´acc˘a.pdˆa´u ngo˘a. c, dˆa´uphu’ di.nh ¬,dˆa´uk´eo theo → cu’ahˆe. to´an mˆe.nh dˆe` , c´acbiˆe´n c´athˆe’ x1,x2, , xn, ,; c´ach˘a`ng c´athˆe’ a1,a2, , an, ; . 1 2 j 1 2 j c´ack´yhiˆe.u tˆant`u A1,A1, , Ak, ,; v`ac´ac biˆe´n h`am f1 ,f1 , , fk, , trong . . . . d´ochı’ sˆo´ trˆen j l`achı’ sˆo´ ngˆoi,chı’ sˆo´ du´oi k l`achı’ sˆo´ th´u tu. . . Trong c´acth´ıdu. (1) v`a(2) ta su’ du.ng c´ack´yhiˆe.u m, y, p, s l`ac´ach˘a`ng . . c´athˆe’, F l`atˆant`u 2 ngˆoi,c`on M v`a I l`ac´actˆant`u mˆo.t ngˆoi. . . Tˆant`u n ngˆoil`amˆo.t h`am n ngˆoinhˆa.n gi´atri. True ho˘a.c False dˆo´iv´oi . n mˆo.t danh s´ach c´ach˘a`ng, t´uc l`a´anhxa. cu’a D v`ao {T,F}, trong d´o D l`a . miˆe` n x´ac di.nh cu’a tˆant`u. . . n Biˆe´n h`am n ngˆoil`amˆo.t to´antu’ t`u tˆa.p D v`ao D, trong d´o D l`amiˆe` n x´ac di.nh. 3.2 C´ac kh´ai niˆe.mv`a di.nh ngh˜ıa . Di.nh ngh˜ıa3.2.1 (term hay ha. ng tu’ ) (a) Tˆa´tca’ c´acbiˆe´n v`ah˘a`ng c´athˆe’ dˆe` u l`aterm.
  11. . . . 78 Chuong 3. Hˆe. to´antˆant`u n n (b) Nˆe´u fi l`amˆo.tbiˆe´n h`amv`a t1,t2, , tn l`ac´acterms, th`ı fi (t1,t2, , tn) l`amˆo.t term. . . . . . . (c) Mˆo.tbiˆe’uth´uc l`amˆo.t term, nˆe´un´oduo. clˆa.pnˆent`u co so’ (a) v`a(b). . . Di.nh ngh˜ıa3.2.2 (cˆongth´ucsocˆa´p) n . n Nˆe´u Ai l`amˆo.tk´yhiˆe.u tˆant`u v`a t1,t2, , tn l`ac´acterm th`ı Ai (t1,t2, , tn) . . l`amˆo.t cˆongth´ucsocˆa´p. . . Di.nh ngh˜ıa3.2.3 (cˆongth´uctˆant`u) . . . a) Mˆo˜imˆo.t cˆongth´ucsocˆa´p l`amˆo.t cˆongth´uc . b) Nˆe´u A v`a B l`ac´accˆongth´uc, v`a y l`amˆo.tbiˆe´nth`ı(¬A), (A→B), (∀yA) l`acˆongth´u.c. . . . . . . . c) Mˆo.tbiˆe’uth´uc l`amˆo.t cˆongth´uc, nˆe´un´oduo. clˆa.pnˆent`u co so’ (a) v`a (b). . . . . . . Trong biˆe’uth´uc ∀yA th`ı“A” duo. cgo.il`amiˆe` n t´acdu. ng cu’aluo. ng t`u ∀y. Ch´u´y1 . . . . . . (1) A khˆongnhˆa´t thiˆe´tch´uabiˆe´n y. Trong tru`ong ho. p n`ay,thˆongthu`ong ta hiˆe’u ∀yA v`a A l`anhu. nhau. . . . . . . . (2) C´accˆongth´uc A∧B, A∨B, A↔Bduo. c x´ac di.nh tuong tu. nhu . . . trong l´y thuyˆe´ttiˆen dˆ`e L cu’a chuong 2 t`u D1 − D3. . . . . . . . . (3) K´yhiˆe.u ∃ duo. cbiˆe’udiˆe˜n qua ∀ nh`o cˆongth´uctuong duong sau dˆay: ∃xA≡¬(∀x¬A).
  12. 3.2. C´ackh´ainiˆe.mv`adi.nh ngh˜ıa 79 . (4) R´ut go. n c´achviˆe´tdˆa´u ngo˘a. c trong logic tˆant`u: . . . . . . . . . . . . Quy u´octuong tu. nhu trong chuong 1, nhung c`onthˆem2 luo. ng t`u . . . ∀ v`a ∃ duo. cxˆe´p ch˘a. tch˜egi˜ua hai nh´om ↔, → v`a ∨, ∧, ¬, ngh˜ıa l`a . . . . . mˆo. tth´u tu. duo. cxˆe´p nhu sau: ↔, →, ∀, ∃, ∨, ∧, ¬ 7654321 Th´ıdu. 3.2.1 1 2 (a) ∀x1A1(x1) → A1(x1,x2) pha’iviˆe´t ngo˘a. cl`a 1 2 ((∀x1A1(x1)) → A1(x1,x2)). 1 2 (b) ∀x1A1(x1) ∨ A1(x1,x2) pha’iviˆe´t ngo˘a.cl`a 1 2 . (∀x1(A1(x1)∨A1(x1,x2))), nhung nˆe´u ta ho´anvi. hai sˆo´ ha.ng cho nhau: 2 1 A1(x1,x2) ∨∀x1A1(x1) th`ıta pha’iviˆe´t ngo˘a. cl`a 2 1 (A1(x1,x2) ∨ (∀x1A1(x1))). . . . . . Ngo`aira tru`ong ho. p cˆongth´ucc´oda.ng QA th`ıta duavˆ`e da.ng Q1(Q2A), . . . . . . . trong d´o A khˆongch´ualuo. ng t`u v`a Q, Q1, Q2 l`ac´acluo. ng tu’ n`ao d´o. 3 Th´ıdu. 3.2.2 ∀x1∃x2∀x4A1(x1,x2,x4) th`ıta pha’iviˆe´t ngo˘a.cl`a 3 (∀x1(∃x2(∀x4A1(x1,x2,x4)))) . Di.nh ngh˜ıa3.2.4 (vi. tr´ıtu. do v`ar`angbuˆo. c) . . . Vi. tr´ıcu’abiˆe´n x trong mˆo.t cˆongth´uc d˜acho duo. cgo.il`ar`angbuˆo. c,nˆe´u . . . . x n˘a`m trong miˆ`en t´acdu.ng cu’aluo. ng t`u ∀x c´om˘a.t trong cˆongth´uc d´o; . . . Tr´aila.i, n´o duo. cgo.il`atu. do. Th´ıdu. 3.2.3
  13. . . . 80 Chuong 3. Hˆe. to´antˆant`u 2 (1) A1(x1,x2) 2 1 (2) A1(x1,x2) →∀x1A1(x1) 2 1 (3) ∀x1(A1(x1,x2) →∀x1A1(x1)). . . . – Trong cˆongth´uc (1), vi. tr´ıth´u nhˆa´tcu’abiˆe´n x1 l`atu. do. . . . – Trong cˆongth´uc (2), vi. tr´ıth´u nhˆa´tcu’abiˆe´n x1 l`atu. do, c`onc´acvi. tr´ı . . th´u 2, th´u 3cu’abiˆe´n x1 l`ar`angbuˆo.c. . –Tˆa´tca’ c´acvi. tr´ıcu’abiˆe´n x1 trong cˆongth´uc (3) dˆe` u l`ar`angbuˆo.c. . . –Mˆo˜imˆo.tvi. tr´ıcu’abiˆe´n x2 trong ca’ 3 cˆongth´uc dˆe` ul`atu. do. . . . Ch´u´y2 C`ung mˆo. tbiˆe´nvi. tr´ıcu’an´oc´othˆe’ v`ua l`atu. do, v`ua l`ar`angbuˆo. c . . trong c`ung mˆo. t cˆongth´uc, ch˘a’ ng ha. n nhu (2). . Di.nh ngh˜ıa3.2.5 (biˆe´ntu. do v`abiˆe´n r`angbuˆo. c) . . . . Mˆo.tbiˆe´n duo. cgo.il`abiˆe´ntu. do (biˆe´n r`angbuˆo. c) trong mˆo.t cˆongth´uc, . . nˆe´utˆo`nta.i c´acvi. tr´ı tu. do (r`angbuˆo. c)cu’a n´otrong cˆongth´uc d´o. . . . Ch´u´y3 Mˆo. tbiˆe´n c´othˆe’ v`ual`abiˆe´ntu. do, v`uabiˆe´n r`angbuˆo. c trong c`ung . . mˆo. t cˆongth´uc, ch˘a’ ng ha. n nhu (2). . . Di.nh ngh˜ıa3.2.6 (term tu. do dˆo´iv´oimˆo. tbiˆe´n) . . . . . Mˆo.t term t duo. cgo.il`atu. do dˆo´iv´oibiˆe´n xi trong cˆongth´uc A,nˆe´u . . . khˆongc´omˆo.tvi. tr´ıtu. do n`aocu’a xi n˘a`m trong miˆe` n t´acdu. ng cu’aluo. ng . t`u ∀xj, trong d´o xj l`abiˆe´nc´om˘a.t trong term t.
  14. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 81 Th´ıdu. 3.2.4 . . . 1 . (1) Term t = xj l`atu. do dˆo´iv´oibiˆe´n xi trong cˆongth´uc A = A1(xi), nhung . . . khˆongtu. do dˆo´iv´oibiˆe´n xi trong cˆongth´uc: 2 B = ∀xjA1(xi,xj). 2 . . . (2) Term t = f1 (x1,x3) l`atu. do dˆo´iv´oibiˆe´n x1 trong cˆongth´uc A = 2 1 . . . ∀x2A1(x1,x2) → A1(x1), nhung khˆongtu. do dˆo´iv´oibiˆe´n x1 trong cˆongth´u.c 2 1 B = ∃x3A1(x1,x3) → A1(x1). . Di.nh ngh˜ıa3.2.7 (cˆongth´uc d´ong) . . . . . Mˆo.t cˆongth´uc A duo. cgo.il`acˆongth´uc d´ong,nˆe´u A khˆongch´ua c´acbiˆe´n . tu. do. . 3.3 Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`a mˆoh`ınh . . . Mˆo.t cˆongth´ucchı’ c´ongh˜ıa khi mˆo.t minh hoa. duo. cchı’ ra cho c´ack´yhiˆe.u cu’a n´o. 3.3.1 Minh hoa. Di.nh ngh˜ıa3.3.1 . . . Mˆo.t minh ho.a (Interpretation) bao gˆo`mmˆo.ttˆa.pho. p D kh´acrˆo˜ng duo. c . . . . go.il`atru`ong minh hoa. (hay miˆe` n x´ac di.nh) v`amˆo.tsˆo´ tuong quan n`ao d´o sao cho: ˜ . n . . -Mˆoimˆo.t tˆant`u Aj l`amˆo.t quan hˆe. n ngˆoitrong D,t´uc l`a´anhxa. t`u tˆa.p Dn v`ao {T,F}. n . . . -Mˆo˜imˆo.tbiˆe´n h`am fj l`amˆo.t to´antu’ n ngˆoitrong D,t´uc l`a´anhxa. t`u Dn v`ao D. . . -Mˆo˜imˆo.th˘a`ng tu’ ai l`amˆo.t phˆa`ntu’ cu’a D. Ch´u´y1
  15. . . . 82 Chuong 3. Hˆe. to´antˆant`u . . . . (1) Khi d˜acho mˆo. t minh hoa. n`ao d´oth`ı c´acbiˆe´n duo. c x´ac di.nh trˆen tru`ong . . . minh hoa. D, c`onc´acph´epto´anv`ac´acluo. ng t`u vˆa˜nhiˆe’u theo ngh˜ıa . . thˆongthu`ong, v`acho ph´epta hiˆe’umˆo. t quan hˆe. n ngˆoitrong D l`amˆo. t tˆa. p con cu’atˆa. p Dn. . . . . (2) Dˆo´iv´oimˆo. t minh hoa. d˜acho th`ımˆo. t cˆongth´uc khˆongch´uabiˆe´ntu. . do (hay l`acˆongth´uc d´ong)thˆe’ hiˆe.nmˆo. tmˆe.nh dˆ`e ho˘a. cl`ad´ung, ho˘a. c . . . . l`asai, c`on dˆo´iv´oimˆo˜imˆo. t cˆongth´uc c´och´uabiˆe´ntu. do thˆe’ hiˆe.n . . . mˆo. t quan hˆe. n`ao d´otrˆen tru`ong minh hoa. . Quan hˆe. n`ayc´othˆe’ thu. c . . . . . hiˆe. n duo. c(d´ung) dˆo´iv´oimˆo. tsˆo´ gi´atri. n`ao dˆa´ycu’abiˆe´n trong tru`ong . . . . minh hoa. , v`ac˜ungc´othˆe’ khˆongthu. chiˆe. n duo. c (sai) dˆo´iv´oimˆo. tsˆo´ . . gi´atri. kh´accu’abiˆe´n trong tru`o ng minh hoa. . 2 Th´ıdu. 3.3.1 (a) A1(x1,x2) 2 (b) ∀x2A1(x1,x2) 2 (c) ∃x2∀x1A1(x2,x1) . . . . . Nˆe´u ta cho.n tru`ong minh hoa. l`atˆa.pho. p c´acsˆo´ nguyˆen duong D = N + = {1, 2, 3, , ∞}, v`atˆant`u. 2 ngˆoi: 2 A1(y,z)=def “y ≤ z” th`ıkhi d´o: . . . . . - Cˆongth´uc (a) thˆe’ hiˆe.n quan hˆe. x1 ≤ x2 l`athu. chiˆe.n duo. c dˆo´iv´oimo.i . . . . c˘a.ps˘a´pth´u tu. (a, b) nguyˆen duong sao cho a ≤ b. . . . . - Cˆongth´uc (b) thˆe’ hiˆe.n t´ınhchˆa´t“Dˆo´iv´oimˆo˜imˆo. tsˆo´ nguyˆen duong . . . . x2: x2 ≥ x1” l`athu. chiˆe.n duo. c dˆo´iv´oisˆo´ 1. . - Cˆongth´uc (c) thˆe’ hiˆe.nmˆo.tmˆe.nh dˆe` d´ung: “Tˆo`nta. imˆo. tsˆo´ nguyˆen du.o.ng nho’ nhˆa´t”. . . . . . M˘a.t kh´ac,nˆe´uc˜ung dˆo´iv´oi tˆant`u trˆenv`atru`o ng minh hoa. bˆaygi`o . ta cho.nl`atˆa.pho. p c´acsˆo´ nguyˆen Z = {−∞, , −1, 0, 1, , +∞} th`ıkhi d´o . cˆongth´uc (c) nhˆa.n gi´atri. sai, v`ır˘a`ng ∃x2∀x1(x2 ≤ x1) ≡∀x2∃x1(x2 >x1) = True
  16. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 83 . . . 3.3.2 T´ınhthu. chiˆe.n duo. c . . . . . . C´ackh´ainiˆe.mvˆe` su. thu. chiˆe.n duo. cv`asu. dˆo`ng nhˆa´t d´ung theo tru. c quan . . l`arˆa´t r˜or`ang,nhung dˆe’ hiˆe’u sˆaus˘a´chonba’nchˆa´tcu’aviˆe.c t´ınhgi´atri. cu’a . . . mˆo.t cˆongth´uc logic tˆant`u, ta cˆa`n thu. chiˆe.n n´omˆo.t c´ach ch´ınh x´actheo t`u.ng bu.´o.c t´ınhto´an. . . . Gia’ su’ cho mˆo.t minh hoa. n`ao d´ov`a D l`atru`ong minh hoa P l`atˆa.ptˆa´t . . . ca’ c´acd˜ay dˆe´m duo. c trˆen D. Gia’ su’ s =(b1,b2, ) ∈ P. Khi d´ota di.nh ∗ . . . . ngh˜ıa h`ammˆo.t ngˆoi s l`a´anhxa. t`u tˆa.pho. p c´acterms (ha.ng tu’ ) v`ao D nhu sau: ∗ (1) Nˆe´u term t l`abiˆe´n xi th`ı s (t)=bi. ∗ (2) Nˆe´u term t l`amˆo.th˘a`ng c´athˆe’ th`ı s (t)b˘a`ng h˘a`ng d´o. n . . . . (3) Nˆe´u fj l`abiˆe´n h`am duo. c minh hoa. bo’ i to´antu’ g trong D,v`at1,t2, , tn ∗ n ∗ ∗ ∗ l`ac´acterms th`ı s (fj (t1,t2, , tn)) = g(s (t1), s (t2), , s (tn)). . ∗ . Nhu vˆa.y s l`amˆo.t h`amx´ac di.nh trˆentˆa.pho. ptˆa´tca’ c´acterms v`anhˆa.n . gi´atri. trong D nh`o c´od˜ay s =(b1,b2, ). . N´oimˆo.t c´ach kh´ac,v´oibˆa´tk`ymˆo.t d˜ay s =(b1,b2, , ) ∈ P v`abˆa´tk`y ∗ . . ∗ . . term t th`ı s (t) l`amˆo.t phˆa`ntu’ cu’atˆa.p D. Phˆa`ntu’ n`ay(s (t)) nhˆa.n duo. c . . b˘a`ng c´ach thˆe´ dˆo´iv´oimˆo˜i i phˆa`ntu’ bi v`aotˆa´tca’ c´acvi. tr´ıcu’abiˆe´n xi trong . . . . . . term t, v`asau d´othu. chiˆe.n to´antu’ tuong ´ung cu’abiˆe´n h`am dˆo´iv´oi term t. 2 2 2 2 Th´ıdu. 3.3.2 Cho term t = f1 (x3,f2 (x1,a1)) v`a D = Z, trong d´o f1 v`a f2 . . . tuong ´ung l`aph´epnhˆanv`aph´epcˆo.ng, c`on a1 =2. . Khi d´ov´oibˆa´tk`y d˜ay s =(b1,b2, ) ∈ P ta c´o: ∗ s (t)=b3 ∗ (b1 +2). . . . Di.nh ngh˜ıa3.3.2 (T´ınh thu. chiˆe.n duo. c) . . n n . . (1) Nˆe´u A l`amˆo.t cˆongth´ucsocˆa´p Aj (t1,t2, , tn)v`aBj l`aquan hˆe. tuong . . . . . . . u´ng cu’a n´otrong minh hoa. th`ıcˆongth´uc A duo. cgo.il`athu. chiˆe.n duo. c
  17. . . . 84 Chuong 3. Hˆe. to´antˆant`u n ∗ ∗ ∗ trˆend˜ay s =(b1,b2, ) ∈ P khi v`achı’ khi Bj (s (t1),s (t2), , s (tn)), . . ∗ ∗ ∗ n t´uc l`abˆo. n phˆa`ntu’ (s (t1),s (t2), , s (tn)) n˘a`m trong quan hˆe. Bj . Th´ıdu. 3.3.3 . . . . 2 (a) Cho tru`ong minh hoa. D = R (sˆo´ thu. c); tˆant`u A1 l`aquan hˆe. 1 x . . “ ≤ ” v`abiˆe´n h`am f1 (x)=e . Khi d´ocˆongth´ucsocˆa´p A = 2 1 . . . A1(f1 (x1),x5) l`athu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, ), khi v`a chı’ khi b1 e ≤ b5. . . . 4 (b) Cho tru`ong minh hoa. D = Z, tˆant`u A1(x, y, u, v) l`aquan hˆe. xv = . . 4 uy,v`aa1 = 2. Khi d´ocˆongth´ucsocˆa´p A = A1(x3,a1,x1,x3)l`a . . . thu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, ), khi v`achı’ khi 2 b3 =2∗ b1. . . . . (2) Cˆongth´uc ¬A l`athu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, ) ∈ P, khi v`a . . . chı’ khi A khˆongthu. chiˆe.n duo. c trˆen s. . . . . (3) Cˆongth´uc A→Bl`athu. chiˆe.n duo. c trˆen s =(b1,b2, ) ∈ P, khi v`a . . . . . . chı’ khi A khˆongthu. chiˆe.n duo. c trˆen s ho˘a.c B thu. chiˆe.n duo. c trˆen s. . . (4) Cˆongth´uc ∀xiA l`athu. chiˆe.n trˆend˜ay s =(b1,b2, , bi, ) ∈ P, khi v`a . . . 0 chı’ khi A l`athu. chiˆe.n duo. c trˆenmˆo˜i d˜aybˆa´tk`y s ∈ P kh´ac s khˆong qu´ath`anhphˆa`nth´u. i. . . . . N´oimˆo.t c´ach kh´ac,cˆongth´uc A l`a thu. chiˆe.n duo. c trˆend˜ay s = . (b1,b2, ) ∈ P, khi v`achı’ khi ph´ep thˆe´ dˆo´iv´oimˆo˜i i,k´yhiˆe.u bi ta.imo.i . . . vi. tr´ıtu. do cu’a xi trong A th`ıta duo. cmˆo.tmˆe.nh dˆe` d´ung trong minh hoa. d˜acho.
  18. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 85 . 3.3.3 Su. dˆo`ng nhˆa´t d´ung(h˘a`ng d´ung) . . . Di.nh ngh˜ıa3.3.3 Mˆo.t cˆongth´uc A duo. cgo.il`adˆo`ng nhˆa´t d´ung trong minh . . . hoa. d˜acho, khi v`achı’ khi A l`athu. chiˆe.n duo. c trˆenmˆo˜i d˜aybˆa´tk`y s = (b1,b2, ) ∈ P. . . . Di.nh ngh˜ıa3.3.4 Mˆo.t cˆongth´uc A duo. cgo.il`adˆo`ng nhˆa´t sai trong minh . . . . hoa. d˜acho, khi v`achı’ khi A khˆongthu. chiˆe.n duo. c dˆo´iv´oibˆa´t k`yd˜ay s =(b1,b2, ) ∈ P. Th´ıdu. 3.3.4 X´et mˆo.t minh hoa. bao gˆo`m: . . + -Tru`ong minh hoa. D = N = {1, 2, } . 1 1 ˜ -Tˆant`u mˆo.t ngˆoi A1 : A1(x)=def “x l`ach˘an”. . 1 1 Khi d´ocˆongth´uc A = ∀x1(A1(x1) → A1(x1)) l`a dˆo`ng nhˆa´t d´ung. Thˆa.tvˆa.y ta h˜ayx´et mˆo.t d˜ay s =(b1,b2, ) ∈ P. . . . • Tru `ong ho. p1: Nˆe´u b1 l`amˆo.tsˆo´ ch˘a˜n th`ıkhi d´ota c´o 1 1 A1(b1) → A1(b1)=True . . . • Tru `ong ho. p2: 1 1 Nˆe´u b1 l`amˆo.tsˆo´ le’ th`ı A1(b1)=False, do d´ota c˜ung c´o: A1(b1) → 1 . . . . . A1(b1)=True. Kˆe´tho. p hai tru`o ng ho. p ta thˆa´y cˆong th´uc A = 1 1 . . . ∀x1(A1(x1) → A1(x1)) l`athu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, ) ∈ P. . . . 1 1 V`ı s duo. ccho.n tu`y´y,do d´ocˆongth´uc A = ∀x1(A1(x1) → A1(x1)) l`a dˆo`ng nhˆa´t d´ung trong minh hoa. d˜acho.  3.3.4 Mˆoh`ınh . . . Di.nh ngh˜ıa3.3.5 Mˆo.t minh hoa. duo. cgo.il`amˆoh`ınh (model) dˆo´iv´oimˆo.t . . . tˆa.pho. p Γ c´accˆongth´uc, nˆe´umˆo˜imˆo.t cˆongth´uccu’aΓl`adˆo`ng nhˆa´t d´ung trong minh hoa. d˜acho.
  19. . . . 86 Chuong 3. Hˆe. to´antˆant`u 3.3.5 Mˆo.tsˆo´ hˆe. qua’ . 1) Cˆongth´uc A l`a dˆo`ng nhˆa´t sai trong minh hoa. d˜acho, khi v`achı’ khi ¬A l`a dˆo`ng nhˆa´t d´ung trong c`ung minh hoa. d´o. . . . 2) Khˆongc´omˆo.t cˆongth´uc n`aov`ua dˆo`ng nhˆa´t d´ung, v`ua dˆo`ng nhˆa´t sai trong c`ung mˆo.t minh hoa 3) Nˆe´u A v`a A→Bl`a dˆo`ng nhˆa´t d´ung trong minh hoa. d˜acho th`ı B c˜ung dˆo`ng nhˆa´t d´ung trong minh hoa. d´o. 4) A→Bl`a dˆo`ng nhˆa´t sai trong minh hoa. d˜acho, khi v`achı’ khi A l`a dˆo`ng nhˆa´t d´ung v`a B l`a dˆo`ng nhˆa´t sai trong c`ung minh hoa . . . 5) (i) −A∧B l`athu. chiˆe.n duo. c trˆend˜ay s ∈ P, khi v`achı’ khi A v`a B . . . c`ung thu. chiˆe.n duo. c trˆen s. . . . . - A∨B l`athu. chiˆe.n duo. c trˆend˜ay s ∈ P, khi v`achı’ khi A thu. chiˆe.n . . . . . duo. c trˆen s, ho˘a.c B thu. chiˆe.n duo. c trˆen s. . . . - A↔Bl`athu. chiˆe.n duo. c trˆend˜ay s ∈ P khi v`achı’ khi A v`a B ho˘a.c . . . . c`ung thu. chiˆe.n trˆen s ho˘a.c khˆongc`ung thu. chiˆe.n duo. c trˆen s. Ch´u´y2 ’. . . . . . . O dˆayta su’ du. ng c´accˆongth´uctuong duong sau: * A∧B tu.o.ng du.o.ng v´o.i ¬(A→¬B) * A∨B tu.o.ng du.o.ng v´o.i (¬A → B) * A↔Btu.o.ng du.o.ng v´o.i (A→B) ∧ (B→A) . . . . . * ∃xiA tuong duong v´oi ¬(∀xi¬A) . . . . (ii) Cˆongth´uc ∃xiA l`athu. chiˆe.n duo. c trˆend˜ay s ∈ P, khi v`achı’ khi A . . . . 0 l`athu. chiˆe.n duo. c dˆo´iv´oi ´ıtnhˆa´tmˆo.t d˜ay s ∈ P kh´ac s khˆongqu´ath`anh phˆa`nth´u. i.
  20. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 87 . Th´ıdu. 3.3.5 Gia’ su’ cho mˆo.t minh hoa. bao gˆo`m: . . + -Tru`ong minh hoa. D = N = {1, 2, 3, } . 2 - Tˆant`u A1 l`a“=” 2 -Biˆe´n h`am f1 l`aph´epnhˆan -H˘a`ng c´athˆe’ a1 =1. . . . . . Khi d´oquan hˆe. mˆo.t ngˆoitrong D tuong ´ung v´oi cˆongth´uc: 2 2 2 A =¬A1(x1,a1) ∧∀x2(∃x3A1(x1,f1 (x2,x3)) 2 2 → A1(x2,x1) ∨ A1(x2,a1)) . l`atˆa.pho. p c´acsˆo´ nguyˆen tˆo´: M = {b ∈ N +|b l`asˆo´ nguyˆen tˆo´} . . . . Vˆa.y cˆong th´uc A l`a thu. chiˆe.n duo. c trˆen mˆo˜i d˜ay bˆa´tk`y s = {b1,b2, }∈P, trong d´o b1 l`amˆo.tsˆo´ nguyˆen tˆo´. . . Ta thu’ kiˆe’mch´ung kh˘a’ ng di.nh trˆen: . Gia’ su’ ta x´etmˆo.t d˜ay s = {b1,b2, }∈P. . . . . • Tru `ong ho. p1: b1 l`asˆo´ nguyˆen tˆo´,ch˘a’ ng ha.n b1 = 7. Trong cˆongth´uc . d˜acho, ta thˆa´y x1 l`abiˆe´ntu. do v`a d´ongvai tr`ol`asˆo´ nguyˆen tˆo´, c`on x2 v`a x3 dˆe` ul`abiˆe´n r`angbuˆo.c. Khi d´o x1 =7= 1.7= 7.1 ↑ ↑ x2 x2 2 - ¬A1(x1,a1) =True - x2 =1 x1 = x2.x3 = True → x2 = x1 ∨ x2 = 1} True F T x T y
  21. . . . 88 Chuong 3. Hˆe. to´antˆant`u - x2 =7: x1 = x2.x3 = True → x2 = x1 ∨ x2 = 1} True T F x T y . . . . Vˆa.ytad˜akiˆe’mch´ung duo. cr˘a`ng v´oi b1 = 7 l`amˆo.tsˆo´ nguyˆen tˆo´ th`ı . . . . cˆongth´uc A l`athu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, ). . . . • Tru `ong ho. p2: b1 khˆongpha’i l`asˆo´ nguyˆen tˆo´,ch˘a’ ng ha.n b1 = 12. Khi d´ota c´o: x1 =1.12 = 2 .6= 6.2= 3.4= 4.3= 12.1 ↑ ↑ ↑ ↑ ↑ ↑ x2 x2 x2 x2 x2 x2 2 - ¬A1(x1,a1)=True - x2 =1 x1 = x2.x3 = True → x2 = x1 ∨ x2 = 1} True F T x T y - x2 =2 x1 = x2.x3 = True → x2 = x1 ∨ x2 = 1} False F F x F y . . . . - x2 =6, 3, 4 t´ınhto´antuong tu. nhu x2 =2v`akˆe´t qua’ l`aFalse. - x2 =12 x1 = x2.x3 = True → x2 = x1 ∨ x2 = 1} True T F x T y . . Ta d˜akiˆe’m tra duo. cr˘a`ng nˆe´u b1 = 12 - khˆongpha’i l`amˆo.tsˆo´ nguyˆen tˆo´ th`ıkˆe´t qua’ t´ınhto´anl`a 2 2 2 2 2 ¬A1(x1,a1) ∧∀x2(∃x3A1(x1,f1 (x2,x3)) → A1(x2,x1) ∨ A1(x2,a1)) = True ∧ False = False. . . . . . Vˆa.ych´ung to’ r˘a`ng cˆongth´uc A l`akhˆongthu. chiˆe.n duo. c trˆend˜ay s = (b1,b2, ) trong d´o b1 khˆongpha’i l`asˆo´ nguyˆen tˆo´. 
  22. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 89 3.3.6 Mˆo.tsˆo´ di.nh ngh˜ıakh´ac . . . Di.nh ngh˜ıa3.3.6 Mˆo.t cˆongth´uc A duo. cgo.il`alogic dˆo`ng nhˆa´t d´ung trong . . hˆe. to´antˆant`u, khi v`achı’ khi A l`a d´ung dˆo´iv´oimo.i minh hoa. bˆa´tk`y. . . . . . . Di.nh ngh˜ıa3.3.7 Mˆo.t cˆongth´uc A duo. cgo.il`athu. chiˆe. n duo. c trong hˆe. . . to´antˆant`u, khi v`achı’ khi nˆe´utˆo`nta.imˆo.t minh hoa.,m`adˆo´iv´oi minh hoa. . . . d´o A l`athu. chiˆe.n duo. c trˆen´ıtnhˆa´tmˆo.t d˜ay s ∈ P. Ch´u´y3 . . . (1) A l`alogic dˆo`ng nhˆa´t d´ung khi v`achı’ khi ¬A l`akhˆongthu. chiˆe.n duo. c, . . . v`a A l`athu. chiˆe.n duo. c, khi v`achı’ khi ¬A l`akhˆonglogic dˆo`ng nhˆa´t d´ung. . . . . (2) Nˆe´u A l`amˆo. t cˆongth´uc d´ongth`ı A l`athu. chiˆe.n duo. c, khi v`achı’ khi . A l`a d´ung dˆo´iv´oimˆo. t minh hoa. n`ao d´o. . . . Di.nh ngh˜ıa3.3.8 Mˆo.t cˆongth´uc A duo. cgo.il`amˆauthuˆa˜n (contradictory) . trong hˆe. to´antˆant`u, khi v`achı’ khi ¬A l`alogic dˆo`ng nhˆa´t d´ung, hay l`akhi . v`achı’ khi A l`asai dˆo´iv´oimo.i minh hoa. bˆa´tk`y. . . . Di.nh ngh˜ıa3.3.9 Cˆongth´uc A duo. cgo.il`alogic k´eotheo B trong hˆe. to´an . . . . . tˆant`u, khi v`achı’ khi dˆo´iv´oibˆa´tk`y minh hoa., B l`athu. chiˆe.n duo. c trˆenmˆo˜i . . . d˜aym`ata.i d´o A thu. chiˆe.n duo. c. . . . . Mˆo.t c´ach tˆo’ng qu´athon, B l`a logic k´eo theo t`u tˆa.pho. p Γ c´accˆongth´uc, . . . . khi v`achı’ khi, dˆo´iv´oi minh hoa., B l`athu. chiˆe.n duo. c trˆenmˆo˜i d˜ay, m`ata.i . . . . d´omˆo˜i cˆongth´uccu’a Γ l`athu. chiˆe.n duo. c. . . . . . . . Di.nh ngh˜ıa3.3.10 Hai cˆongth´uc A v`a B duo. cgo.il`alogic tuong duong . trong hˆe. to´antˆant`u, khi v`achı’ khi A logic k´eo theo B v`a B logic k´eo theo A. Hˆe. qua’ 3.3.1
  23. . . . 90 Chuong 3. Hˆe. to´antˆant`u a) A logic k´eotheo B khi v`achı’ khi cˆongth´u.c (A→B) l`alogic dˆo`ng nhˆa´t d´ung. b) A v`a B l`alogic tu.o.ng du.o.ng, khi v`achı’ khi cˆongth´u.c (A↔B) l`alogic dˆo`ng nhˆa´t d´ung. c) Nˆe´u A l`alogic k´eo theo B,v`aA d´ung trong mˆo. t minh hoa. d˜acho th`ı B c˜ung d´ung trong minh hoa. d´o. . . . . d) Nˆe´u B l`alogic k´eo theo t`u tˆa. pho. p Γ c´accˆongth´ucv`amo. i cˆongth´uc cu’a Γ d´ung trong minh hoa. d˜acho th`ı B c˜ung d´ung trong minh hoa. . . . Di.nh ngh˜ıa3.3.11 Gia’ su’ S = {A1, A2,.,An} l`amˆo.ttˆa.pho. p c´accˆong . . . . . . th´uc tˆant`u. Khi d´o, S duo. cgo.i phi mˆauthuˆa˜n (hay thoa’ duo. c), nˆe´utˆo`n . ta.imˆo.t minh hoa. cu’a S sao cho mo.i cˆongth´uc A1, A2,.,An dˆe` u d´ung trong minh hoa. d´o. . . . . - S duo. cgo.il`amˆauthuˆa˜n (khˆongthoa’ m˜an duo. c), nˆe´u khˆongtˆo`nta.i . mˆo.t minh hoa. n`aonhu vˆa.y. . . . . - Cˆongth´uc A duo. cgo.il`alogic k´eo theo t`u S,k´yhiˆe.u S |= A,nˆe´u trong . mo.i minh hoa. m`ata.i d´omo.i cˆongth´uccu’a S dˆe` u d´ung th`ı A c˜ung d´ung. . D˘a.cbiˆe.t, nˆe´u S = ∅ th`ı |= A c´ongh˜ıa A l`acˆongth´uch˘a`ng d´ung. Ch´u´y4 . . . . Di.nh l´y 2.2.1 (nguyˆen l´y suy diˆe˜n) trong chuong2c˜ung d´ung cho tru`ong . . . . ho. p c´accˆongth´uc A, B, H1, H2,,Hn l`acˆongth´uc logic tˆant`u. . Th´ıdu. 3.3.6 Cho mˆoh`ınh suy diˆ˜en trong logic tˆant`u ∀x1(P (x1) → Q(x1)) (H1) ∃x1P (x1)(H2) ∀x1(Q(x1) → R(x1)) (H3) ∀x1(S(x1) → R(x1)) (H4) ∴ ∃x1S(x1)(A)
  24. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 91 . trong d´o P (x1),Q(x1),R(x1),S(x1) l`ac´actˆant`u mˆo.t ngˆoix´ac di.nh trˆen . . mˆo.t tru`ong minh hoa. D n`ao d´o. Mˆoh`ınh suy diˆe˜n trˆenc´o dˆo`ng nhˆa´t d´ung hay khˆongtrˆentru.`o .ng minh . . . hoa. v`axˆaydu. ng c´acbu´oc suy diˆ˜encu’a mˆoh`ınhtrˆen? . . Gia’i: Tas˜ech´ung minh r˘a`ng cˆongth´uc B =(H1 ∧ H2 ∧ H3 ∧ H4 →A)l`a . . dˆo`ng nhˆa´t d´ung trˆentru`ong minh hoa. D theo nguyˆen l´ysuy diˆ˜encu’a di.nh l´y2.2.1 v`aphu.o.ng ph´apgia’icu’a Robinson trong chu.o.ng 2. . Thˆa.tvˆa.y, x´etmˆo.t d˜ay s =(b1,b2, ) ∈ P.T`u H1,H2,H3,H4 v`a A, . ta c´ohˆe. suy diˆ˜en sau nh`o thay k´yhiˆe.uh˘a`ng c´athˆe’ b1 v`aoc´acvi. tr´ıcu’a x1 . trong hˆe. cˆongth´uc d˜acho: P (b1) → Q(b1) P (b1) ∨ Q(b1) P (b1) P (b1) Q(b1) → R(b1) ⇔ Q(b1) ∨ R(b1) S(b1) → R(b1) S(b1) ∨ R(b1) ∴ S(b1) ∴ S(b1) . . v`achı’ cˆa`nch´ung minh tˆa.p c´accˆongth´uc S = {P (b1) ∨ Q(b1), P (b1), Q(b1) ∨ R(b1), S(b1) ∨ R(b1), S(b1)} . . l`amˆauthuˆa˜n (theo nguyˆen l´y suy diˆe˜ncu’a di.nh l´y2.4.1 (3) v`aphuong ph´ap gia’icu’a Robinson (chu.o.ng 2)). . Tac´ohˆe. suy diˆ˜ennhusau:
  25. . . . 92 Chuong 3. Hˆe. to´antˆant`u 1.P(b1) ∨ Q(b1)   2. P (b1)   3. Q(b1) ∨ R(b1)  (S) 4. S(b1) ∨ R(b1)    5.S(b1)  . 6.Q(b1)(1, 2, gia’ith´uc) . 7.R(b1)(3, 6, gia’ith´uc) . 8. S(b1)(4, 7, gia’ith´uc) 9.  (5, 8, gia’ith´u.c) Theo nguyˆenl´ysuy diˆ˜en: S l`amˆauthuˆa˜n (hay dˆo`ng nhˆa´t sai) ⇔ S dˆa˜n vˆ`e suy diˆ˜en  (rˆo˜ng) theo phu.o.ng ph´apgia’icu’a Robinson (chu.o.ng 2). . . V`ı s duo. ccho.n tu`y´y,nˆenmˆoh`ınhsuy diˆe˜n d˜acho l`a dˆo`ng nhˆa´t d´ung.  . 3.3.7 C´accˆongth´uc logic dˆo`ng nhˆa´t d´ungtrong hˆe. to´antˆant`u. 1) ¬∀xA≡∃x¬A 2) ¬∃xA≡∀x¬A 3) (∀xA∧∀xB) ≡∀x(A∧B) 4) (∃xA∨∃xB) ≡∃x(A∨B) 5) (∀xA∧G) ≡∀x(A∧G) 6) (∀xA∨G) ≡∀x(A∨G) 7) (∃xA∧G) ≡∃x(A∧G) 8) (∃xA∨G) ≡∃x(A∨G) . . . trong d´ov´oi 4 cˆongth´uc cuˆo´ic`ung x khˆongpha’i l`abiˆe´ntu. do trong cˆong th´u.c G.
  26. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 93 . 3.3.8 Da.ng chuˆa’nt˘a´c trong logic tˆant`u 3.3.8.1 Da.ng chuˆa’nt˘a´ctiˆe` ntˆo´ . . . . Di.nh ngh˜ıa3.3.12 Mˆo.t cˆongth´uctˆant`u A duo. cgo.il`achuˆa’nt˘a´ctiˆe` ntˆo´, . . . . nˆe´u A khˆongch´ua c´acluo. ng t`u ho˘a.cc´oda.ng Q1x1Q2x2 QnxnM, trong . . . . d´o Qi (i =1 n) ho˘a.cl`a∀ ho˘a.cl`a∃,v`aM l`acˆongth´uc khˆongch´ualuo. ng t`u . . . . . . Da.iluo. ng Q1x1Q2x2 Qnxn duo. cgo.il`atiˆe` ntˆo´, c`on M duo. cgo.il`ama . trˆa. n cu’a cˆongth´uc A. Th´ıdu. 3.3.7 ∃x∀y(x ≤ y). . . . Di.nh l´y3.3.1 Mo. i cˆongth´uc tˆant`u A dˆ`eutˆo`nta. imˆo. t cˆongth´uc chuˆa’n t˘a´ctiˆe` ntˆo´ tu.o.ng du.o.ng v´o.i n´o. Ch´u.ng minh . . . . Ta c´othˆe’ vˆa.ndu.ng c´accˆongth´uch˘a`ng d´ung (c´accˆongth´uctuong . . . . duong) trong mu.c 3.3.7 v`athˆemc´accˆongth´uch˘a`ng d´ung sau dˆe’ dua A vˆ`e . . da.ng chuˆa’nt˘a´ctiˆe` ntˆo´ (phuong ph´ap dˆo’itˆenbiˆe´n): 1) ∀xA(x) ∨∀xB(x) ≡∀x∀y(A(x) ∨B(y)) 2) ∃xA(x) ∧∀xB(x) ≡∃x∀y(A(x) ∨B(y)) 3) ∀xA(x) ∧∃xB(x) ≡∀x∃y(A(x) ∧B(y)) 4) ∃xA(x) ∨∀xB(x) ≡∃x∀y(A(x) ∨B(y)) 5) ∀xA(x) ∨∃xB(x) ≡∀x∃y(A(x) ∨B(y)). . . . . Dˆo`ng th`oi ta thu. chiˆe.n c´acbu´ocbiˆe´n dˆo’i liˆentiˆe´p sau dˆay: . . . . . . • Tru ´o chˆe´t loa.ibo’ ph´epk´eotheo → nh`o cˆongth´uc: A → B tuong du.o.ng v´o.i A ∨ B, v`aph´ep ↔ nh`o. cˆongth´u.c: A ↔ B tu.o.ng du.o.ng v´o.i(A → B) ∧ (B → A).
  27. . . . 94 Chuong 3. Hˆe. to´antˆant`u . . • Dˆo’i t ˆe n b i ˆe´n r`angbuˆo.c(nˆe´ucˆa`n) sao cho khˆongc´obiˆe´n dˆo´ituo. ng n`ao . . . . v`ua l`atu. do, v`ua l`ar`angbuˆo.c trong c`ung mˆo.t cˆongth´uc (v`ac˜ung ´ap . du.ng cho mˆo˜i cˆongth´uc con). . . . • Xo´abo’ mo.iluo. ng t`u ∀x v`a ∃x,nˆe´u trong miˆe` n t´acdu.ng cu’ach´ung khˆongc´obiˆe´n x. . . . . . • Duamo.i xuˆa´thiˆe.ncu’aph´ep phu’ di.nh ¬ v`ao d´ung tru. ctiˆe´p tru´oc c´ac . . . . . cˆongth´ucsocˆa´p, v`asau d´ochuyˆe’ndˆa`n c´ack´yhiˆe.uluo. ng t`u ra ph´ıa tru.´o .c cˆongth´u.c nh`o. cˆongth´u.ctu.o.ng du.o.ng d˜an´oio’. trˆen. . Th´ıdu. 3.3.8 Cho cˆongth´uc 1 2 3 A = ∀x(A1(x) ∧∀y∃x(¬A1(x, y) →∀zA1(a, x, y))). T`ım da.ng chuˆa’nt˘a´ctiˆe` ntˆo´ cu’a A? Gia’i - Loa. ibo’ ph´epk´eo theo →: 1 2 3 A≡∀x(A1(x) ∧∀y∃x(¬¬A1(x, y) ∨∀zA1(a, x, y))) - Dˆo’i tˆenbiˆe´n r`angbuˆo.c: 1 2 3 A≡∀x(A1(x) ∧∀y∃u((¬¬A1(u, y) ∨∀zA1(a, u, y)))) . . . . -Bo’ luo. ng t`u th`ua: 1 2 3 A≡∀y(A1(x) ∧∀y∃u((¬¬A1(u, y) ∨ A1(a, u, y)))) -Bo’ dˆa´uphu’ di.nh ¬¬: 1 2 3 A≡∀x(A1(x) ∧∀y∃u((A1(u, y) ∨ A1(a, u, y)))) . . . . . - Chuyˆe’n c´acluo. ng t`u ∀, ∃ lˆenph´ıa tru´oc: 1 2 3 A≡∀x∀y(A1(x) ∧∃u((A1(u, y) ∨ A1(a, u, y))) 1 2 3 ≡∀x∀y∃u(A1(x) ∧ (A1(u, y) ∨ A1(a, u, y))).
  28. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 95 3.3.8.2 Da.ng chuˆa’nt˘a´c tuyˆe’n v`achuˆa’nt˘a´chˆo.i . . Sau khi ta d˜a da.t duo. cda.ng chuˆa’nt˘a´ctiˆe` ntˆo´,ch˘a’ ng ha.ntago.il`a . . . Q1x1Q2x2 Qnxn Ak n`ao d´ot`u cˆongth´uc d˜acho A, khi d´ota thu. chiˆe.n . . thˆemmˆo.tbu´o c: a) Da. ng chuˆa’nt˘a´c tuyˆe’n . Trong Ak,nˆe´u ta ´apda.ng cˆongth´uc: A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C) . . . ∗ . ∗ . . ta thu duo.c cˆongth´uc Ak ≡Ak, v`acˆongth´uc Ak n`ay duo. cgo.il`ada. ng chuˆa’nt˘a´c tuyˆe’n cu’a Ak, hay l`a: ∗ . . . A = Q1x1Q2x2 QnAk, trong d´oluo. ng t`u Qixi ho˘a.cl`a∀xi ho˘a.cl`a ∃xi (i =1, 2, , n). b) Da. ng chuˆa’nt˘a´chˆo. i . Trong Ak,nˆe´u ta ´apdu.ng cˆongth´uc: A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) . . . ∗∗ . ∗∗ . . ta thu duo. c cˆongth´uc Ak ≡Ak, v`acˆongth´uc Ak n`ay duo. cgo.il`a da. ng chuˆa’nt˘a´chˆo. i cu’a Ak, hay l`a: ∗∗ . . . A = Q1x1Q2x2 QnxnAk , trong d´oluo. ng t`u Qixi ho˘a.cl`a∀xi ho˘a.c l`a ∃xi (i =1, 2, ,n). Ch´u´y:A → B ≡ A ∨ B. . . Th´ıdu. 3.3.9 Cho cˆongth´uctˆant`u sau dˆay: A =[∀x(P(x) → Q(x)) ∧∃xP (x) ∧∀x(Q(x) → R(x)) ∧∀x(S(x) → R(x)))] →∃xS(x). . T`ım da.ng chuˆa’nt˘a´c tuyˆe’ncu’a cˆongth´uc A?
  29. . . . 96 Chuong 3. Hˆe. to´antˆant`u Gia’i: A≡[∀x(P(x) ∨ Q(x)) ∧∃xP(x) ∧∀x(Q(x) ∨ R(x)) ∧∀x(S(x) ∨ R(x))] →∃xS(x) ≡∀x(P (x) ∨ Q(x)) ∧∃xP (x) ∧∀x(Q(x) ∨ R(x)) ∧∀x(S(x) ∨ R(x)) ∨∃xS(x)] ≡∃x(P (x) ∧ Q(x)) ∨∀xP (x) ∨∃x(Q(x) ∧ R(x))∨ ∃x(S(x) ∧ R(x)) ∨∃xS(x) ≡∃x(P (x) ∧ Q(x)) ∨∀xP (x) ∨∃x(Q(x) ∧ R(x))∨ ∃x(S(x) ∧ R(x)) ∨∃xS(x) ≡∃x((P(x) ∧ Q(x)) ∨ (Q(x) ∧ R(x)) ∨ (S(x)∧ R(x)) ∨ S(x)) ∨∀yP(y) ≡∃x∀y((P(x) ∧ Q(x)) ∨ (Q(x) ∧ R(x)) ∨ (S(x) ∧ R(x)) ∨ S(x) ∨ P (y)). 3.3.8.3 Da.ng chuˆa’nt˘a´c SKOLEM . . Mˆo.tda.ng chuˆa’nt˘a´c quan tro.ng v`ahay duo. cd`ung trong lˆa.p tr`ınhlogic v`aTr´ıtuˆe. nhˆanta.o, d´ol`ada.ng chuˆa’nt˘a´c Skolem. Da.ng n`aygi´up cho c´ac . . . . . nh`alˆa.p tr`ınhdˆ˜e d`ang dua cˆongth´uc tˆant`u v`aotrong m´aynh`o su. chuˆa’n . . . . . . . . ho´aSkolem: t`u cˆongth´ucda.ng tiˆe` ntˆo´ c´ac da.iluo. ng g˘a´nv´oiluo. ng t`u tˆo`n . . . ta.i ∃ duo. c thay thˆe´ bo’ i c´ach˘a`ng c´athˆe’ ho˘a.c h`amSkolem, v`akhi d´okhˆong . . . . . . . c`onsu. hiˆe.ndiˆe.ncu’aluo. ng t`u tˆo`nta.i ∃ m`achı’ c`onluo. ng t`u to`anthˆe’ ∀ trong . . cˆongth´uc d´o.Do d´oc´acnh`alˆa.p tr`ınhchı’ viˆe.c dua v`aom´ayphˆa`n thˆancu’a . . . . cˆongth´uc tˆant`u d˜achuˆa’n ho´a(duo. cgo.il`ama trˆa. n) v`amˆo˜imˆo.tbiˆe´n xuˆa´t . . . . hiˆe.n trong cˆongth´uc d´o dˆe` u liˆenquan dˆe´nluo. ng t`u to`anthˆe’ ∀. . . . . Di.nh ngh˜ıa3.3.13 Gia’ su’ A l`amˆo.t cˆongth´uc tˆant`u o’ da.ng tiˆe` ntˆo´: . . . Q1x1Q2x2 Qnxn M v`a Qr l`amˆo.tluo. ng t`u tˆo`nta.i trong A. . . . . . . . - Khi d´o,nˆe´u dˆo´iv´oiluo. ng t`u Qr khˆongc´omˆo.tluo.ng t`u to`anthˆe’ n`ao . . . . d´ung tru´oc n´oth`ıta thay tˆa´tca’ xr trong M bo’ imˆo.th˘a`ng a cu’amiˆe` n x´ac di.nh D.
  30. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 97 Th´ıdu. 3.3.10 ∃x∃y∀zP(x, y, z)(P l`atˆant`u. 3 ngˆoi) ↑ ∃y∀zP(a, y, z)(a -h˘a`ng c´athˆe’ thuˆoc D) ↑ . ∀zP(a, b, z)(b -h˘a`ng c´athˆe’ thuˆo.c D) . . . . . . . . . . - Trong tru`ong ho. pnˆe´u dˆo´iv´oiluo. ng t`u Qr m`a d´ung tru´ocn´oc´o(r −1) . . . . . . . luo. ng t`u to`anthˆe’ tuong ´ung v´oi c´acbiˆe´n x1,x2, , xr−1 th`ıkhi d´ota thay . . . mo.ik´yhiˆe.u xr bo’ i h`am f(x1,x2, ,xr−1). H`amn`ay duo. cgo.il`ah`amSkolem. . . . . . . . . Cˆongth´uc nhˆa.n duo. ct`u A b˘a`ng c´ach thu. chiˆe.nnhutrˆen duo.cgo.il`a da. ng chuˆa’nt˘a´c Skolem. Th´ıdu. 3.3.11 ∀x∀y∃z∀t∃uP (x, y, z, t, u) ↑ ∀x∀y∀t∃uP (x, y, f(x, y),t,u) ↑ ∀x∀y∀tP (x, y, f(x, y),t,g(x, y, t)) - da. ng chuˆa’nt˘a´c Skolem (viˆe´tt˘a´tl`a FSS). Mˆo. tsˆo´ kˆe´t qua’ . . Dˆo´iv´oi cˆongth´uc A,tak´yhiˆe.u SA l`ada.ng chuˆa’nt˘a´c Skolem. Di.nh l´y3.3.2 . (1) Cˆongth´uc (SA →A) l`alogic dˆo`ng nhˆa´t d´ung, v`ado d´onˆe´u A l`amˆau thuˆa˜n (logic dˆo`ng nhˆa´t sai) th`ı SA c˜ung mˆauthuˆa˜n. . . . . (2) Nˆe´u A l`athoa’ duo. cth`ıSA c˜ung thoa’ duo. c. . (3) Cˆongth´uc A l`amˆauthuˆa˜n, khi v`achı’ khi SA l`amˆauthuˆa˜n(di.nh l´y Skolem). . Ch´u´y5 Cˆongth´uc (A→SA) n´oichung l`akhˆonglogic dˆo`ng nhˆa´t d´ung, . . . . do d´o A v`a SA l`akhˆonglogic tuong duong, ch˘a’ ng ha. n: A = ∀x∃y(y>x),SA = ∀x(f(x) >x)
  31. . . . 98 Chuong 3. Hˆe. to´antˆant`u . . −x v`ata cho. n tru`ong minh hoa. D = R, f(x)=e . Khi d´o A nhˆa. n gi´atri. True v`a SA nhˆa. n gi´atri. False. ´ . . 3.3.8.4 Ap du. ng di.nh l´ySkolem, nguyˆenl´ysuy diˆe˜n, v`aphuong ph´apphˆangia’i Ch´u.ng minh r˘a`ng cˆongth´u.c sau dˆayl`alogic dˆo`ng nhˆa´t d´ung trong logic tˆant`u.: A =(∀x∃y(P (x) → Q(y))) ∧ (∀y∃z(Q(y) → R(y))) → (∀x∃z(P (x) → R(z))). Ch´u.ng minh: . . . . . . . Tru ´ochˆe´t, ta cˆa`n thu. chiˆe.nmˆo.tsˆo´ bu´ocbiˆe´n dˆo’icoba’ncu’a cˆongth´uc d˜acho vˆ`e da.ng quen thuˆo.c theo c´act´ınhchˆa´t d˜abiˆe´t. - Theo nguyˆen l´ysuy diˆ˜en v`anguyˆenl´yphu.o.ng ph´apphˆangia’i, ta cˆa`n ch´u.ng minh r˘a`ng cˆongth´u.c: B =(∀x∃y(P(x) ∨ Q(y))) ∧ (∀y∃z(Q(y) ∨ R(z)))∧ ∀x∃z(P(x) ∨ R(z)) . . l`amˆauthuˆa˜n (chuong 2 mu.c 2.4.3). . . . . . Viˆe.cdˆa˜n duo. cmˆo.t cˆongth´ucvˆe` da.ng chuˆa’nt˘a´c Skolem thu. csu. c´o´y . . . ngh˜ıa thu. ctiˆe˜nrˆa´t cao, d˘a.cbiˆe.t dˆo´iv´oi b`aito´anlˆa.p luˆa.n trong c´achˆe. co . . . . . . . . . . so’ tri th´uc duo. c xˆaydu. ng trˆenco so’ cu’a c´actˆant`u. Trong chuong 2, ta d˜a . . . biˆe´t b`aito´anlˆa.p luˆa.nc´othˆe’ duavˆ`e b`aito´anch´ung minh mˆo.ttˆa.p cˆongth´uc . S (hay mˆo.t cˆongth´uc) c´omˆauthuˆa˜n hay khˆong. Di.nh l´y3.3.2 (3) trˆen dˆay . . cho ta biˆe´tmˆo.t cˆongth´uc A l`amˆauthuˆa˜n, khi v`achı’ khi cˆongth´uc Skolem . . . . . SA tuong ´ung l`amˆauthuˆa˜n. Gia’ su’ M l`ama trˆa.ncu’a cˆongth´uc SA,v`av`ı . . . . SA duo. cviˆe´tdu´oida.ng chuˆa’nt˘a´ctiˆe` ntˆo´,nˆenSA l`amˆauthuˆa˜n, khi v`achı’ . . khi M l`amˆauthuˆa˜n. Cˆongth´uc M chı’ ch´ua c´acph´ep to´anlogic mˆe.nh dˆe` , . . do d´ota c´othˆe’ duavˆe` da.ng chuˆa’nt˘a´chˆo.icu’amˆo.ttˆa.p c´acClause, v`anhu vˆa.y M l`amˆauthuˆa˜n, khi v`achı’ khi tˆa.p c´acClause d´ol`amˆauthuˆa˜n. Ch´u´y . . . r˘a`ng trong tru`ong ho. p n`aymˆo˜imˆo.t clause l`atuyˆe’ncu’amˆo.tsˆo´ c´acliteral,
  32. . 3.3. Minh hoa.,su. dˆo`ng nhˆa´t d´ung v`amˆoh`ınh 99 . . . . nhung literal trong logic tˆant`u l`amˆo.t cˆongth´ucsocˆa´p ho˘a.cphu’ di.nh cu’a . . . . . mˆo.t cˆongth´ucsocˆa´p, v`acˆa´utr´uc cu’a literal ph´ucta.phon nhiˆ`eu so v´oi . logic mˆe.nh dˆe` ,nˆenviˆe.c x´ac di.nh c´acgia’ith´uc, rˆo`i sau d´o´apdu.ng nguyˆen . . . . . . l´ysuy diˆ˜env`aphuong ph´apphˆangia’ituong ´ung l`aviˆe.c l`amc´onhiˆ`euph´uc . . . . ta.phon so v´oihˆe. to´anmˆe.nh dˆe` . Tuy nhiˆenphuong ph´apphˆangia’i l`amˆo.t . . . . . trong nh˜ung phuong ph´apc´ohiˆe.u qua’ trong viˆe.cch´ung minh mˆo.t cˆongth´uc . . logic dˆo`ng nhˆa´t d´ung. Mu.ctiˆe´p theo ta s˜e´apdu. ng nguyˆen l´ycu’aphuong . . ph´apphˆangia’i dˆe’ l`ams´angto’ t´ınhhiˆe.u qua’ cu’aphuong ph´apn`ay. Ta biˆe´n dˆo’inhu. sau: B≡∀x∃y(P(x) ∨ Q(y)) ∧∀y∃z(Q(y) ∨ R(z)) ∧∃x∀z(P(x) ∧ R(z)) ≡∀x∃u(P (x) ∨ Q(u)) ∧∀y∃v(Q(y) ∨ R(v)) ∧∃t∀z(P (t) ∧ R(z)) ↑ ↑ ↑ ≡∀x∀y∀z(∃u(P(x) ∨ Q(u)) ∧∃v(Q(y) ∨ R(v)) ∧∃t(P (t) ∧ R(z))) ≡∀x∀y∀z∃u∃v∃t((P (x) ∨ Q(u)) ∧ (Q(y) ∨ R(v)) ∧ (P (t) ∧ R(z))) ↑ ↑ ↑ ≡∀x∀y∀z((P(x) ∨ Q(f(x, y, z)) ∧ (Q(y) ∨ R(g(x, y, z))) ∧ (P (h(x, y, z)) ∧ R(z)))) Khi d´ota d˘a.t: S = {P (x) ∨ Q(f(x, y, z), Q(y) ∨ R(g(x, y, z)),P(h(x, y, z)), R(z)} trong d´oc´ach`am f(x, y, z),g(x, y, z),h(x, y, z) l`ac´ach`amSkolem v`amˆo˜i . . . . mˆo.t phˆa`ntu’ cu’a S l`amˆo.t clause. Mˆo˜imˆo.t clause duo. clˆa.pnˆent`u c´acliteral l`anh˜u.ng cˆongth´u.cso. cˆa´p. - Theo di.nh l´ySkolem: B l`amˆauthuˆa˜n ⇔ S l`amˆauthuˆa˜n(dˆo`ng nhˆa´t sai). . . Thˆa.tvˆa.y, ta xˆaydu. ng hˆe. dˆa˜n xuˆa´tt`u S vˆ`e  (rˆo˜ng) theo nguyˆen l´ycu’a phu.o.ng ph´apphˆangia’icu’a Robinson nhu. sau:
  33. . . . 100 Chuong 3. Hˆe. to´antˆant`u 1. P (x) ∨ Q(f(x, y, z))   2. Q(y) ∨ R(g(x, y, z))   (S) 3.P(h(x, y, z))  4. R(z)  5.Q(f(h(x, y, z),y,z)) (1, 3, thˆe´ {x/h(x, y, z)}, gia’ith´u.c) 6. Q(y)(2, 4, thˆe´ {z/g(x, y, z)}, gia’ith´u.c) 7.  (5, 6, thˆe´ {y/f(h(x, y, z), y, z)}, gia’ith´u.c) . . Vˆa.y theo nguyˆen l´ycu’aphuong ph´apphˆangia’icu’a Robinson ta nhˆa.n . . . . duo. ctˆa.p S nhu trˆenl`amˆauthuˆa˜n hay cˆongth´uc B d˜acho l`alogic dˆo`ng nhˆa´t sai, t´u.cl`aA logic dˆo`ng nhˆa´t d´ung.  3.4 L´ythuyˆe´ttˆan t`u. cˆa´p1K 3.4.1 Di.nh ngh˜ıa L´ythuyˆe´t tˆant`u. cˆa´p 1K bao gˆo`m 1) C´ack´yhiˆe.u: - ¬, → l`a2 ph´epto´annguyˆenthuy’, -C˘a.pdˆa´u ngo˘a.c: (,) . . -Mˆo.ttˆa.p dˆe´m duo. c c´acbiˆe´n x1,x2, ,xn, . . . . n -Mˆo.ttˆa.ph˜uuha.n ho˘a.c dˆe´m duo. c c´actˆant`u Aj (n, j ≥ 1) v`atˆa.p n`aypha’i kh´acrˆo˜ng. . . . -Mˆo.ttˆa.ph˜uuha.n (c´othˆe’ rˆo˜ng) ho˘a.c dˆe´m duo. c c´acbiˆe´n h`am n fj (n, j ≥ 1) . . . . -Mˆo.ttˆa.ph˜uuha.n (c´othˆe’ rˆo˜ng) ho˘a.c dˆe´m duo. c c´ach˘a`ng tu’ ai (i ≥ 1) 2) C´actiˆen dˆe` : 2 loa.i
  34. 3.4. L´ythuyˆe´t tˆant`u. cˆa´p1K 101 (i) Tiˆen dˆ`e logic:v´o.i cˆongth´u.c A, B, C tu`y´ytrong K (A1) (A→(B→A)) (A2) (A→(B→C)) → ((A→B) → (A→C)) (A3) (¬B → ¬A) → ((¬B → A) →B) . . (A4) ∀xi A(xi) →A(t), trong d´oterm t l`atu. do dˆo´iv´oibiˆe´n xi trong A(xi) . (A5) ∀xi (A→B) → (A→∀xiB), trong d´o A khˆongch´ua c´ac . vi. tr´ıtu. do cu’abiˆe´n xi (ii) Tiˆen dˆ`e riˆeng: . C´actiˆen dˆe` n`ao d´o,nhung khˆongmˆota’ cu. thˆe’, tu`ythuˆo.c v`ao . t`ung hˆe. riˆengbiˆe.t. 3) Qui t˘a´cdˆa˜n xuˆa´t: 2 qui t˘a´c (i) Modus Ponens (Kˆe´t luˆa. n) Nˆe´u A v`a A→Bth`ı B (ii) GEN (Tˆo’ng qu´atho´a): . T`u A k´eo theo ∀xiA Ch´u´y . . . . (1) L´ythuyˆe´t tˆant`u cˆa´p 1K khˆongch´ua c´actiˆen dˆ`e riˆeng duo. cgo. il`aHˆe. to´antˆant`u. cˆa´p 1 (viˆe´tt˘a´t l`aPP) . . (2) Dˆo´iv´oimˆo. tmˆoh`ınh cu’a l´ythuyˆe´t tˆant`u cˆa´p 1K, ta hiˆe’ul`amˆo. t minh hoa. m`atrong d´omo. i tiˆen dˆ`e dˆ`eu dˆo`ng nhˆa´t d´ung. . (3) Nˆe´u ta ´apdu. ng qui t˘a´c Modus Ponens v`aTˆo’ng qu´atho´a dˆo´iv´oi c´ac . cˆongth´uc dˆo`ng nhˆa´t d´ung trong mˆo. t minh hoa. d˜acho th`ıkˆe´t qua’ ta . . . nhˆa. n duo. cc˜ung l`amˆo. t cˆongth´uc dˆo`ng nhˆa´t d´ung trong minh hoa. d´o.
  35. . . . 102 Chuong 3. Hˆe. to´antˆant`u . . . . (4) Dˆo´iv´oi hai tiˆen dˆ`e (A4) v`a(A5), ngu`o itaduaramˆo. tsˆo´ ha. nchˆe´ cˆa`n thiˆe´t, nˆe´u khˆongs˜edˆa˜n dˆe´n sai, ch˘a’ ng ha. n: . 2 . ∗ Gia’ su’ A(x1)=¬∀x2A1(x1,x2) v`agia’ su’ term t l`a x2. Khi d´or˜o . . . r`angterm t = x2 l`akhˆongtu. do dˆo´iv´oibiˆe´n x1 trong cˆongth´uc A(x1). X´et cˆongth´u.c sau: 2 2 ∀x1(¬∀x2A1(x1,x2)) →¬∀x2A1(x2,x2) . Cˆongth´uc n`ayc´oda. ng cu’a tiˆen dˆ`e (A4): ∀x1A(x1) →A(t), . . . nhung term t = x2 l`akhˆongtu. do dˆo´iv´oi x1 trong A(x1). . . Ta xˆaydu. ng minh hoa. nhu sau: . . -Tru`ong minh hoa. D = {1, 2, 3, } . 2 -Tˆant`u A1 l`a“=” Khi d´ota c´o: 2 A = ∀x1(¬∀x2A1(x1,x2)) = ∀x1∃x2(x1 =6 x2)=True . . 2 nhung cˆongth´uc B = ¬∀x2A1(x2,x2) nhˆa. n gi´atri. False. . . . . Vˆa. y tiˆen dˆ`e (A4) l`asai trong tru`ong ho. p term t l`akhˆongtu. do dˆo´i . v´oi xi. . . . ∗ Dˆo´iv´oitiˆen dˆ`e (A5), nˆe´uha. nchˆe´ bi. vi pha. m, t´ucl`ax1 l`abiˆe´ntu. . do trong cˆongth´uc A, th`ıkhi d´okˆe´t qua’ c˜ung dˆa˜n dˆe´n sai, ch˘a’ ng ha. n: . . 1 . gia’ su’ hai cˆongth´uc A v`a B dˆ`eul`aA1(x1). Khi d´o x1 l`abiˆe´ntu. do trong A. Ta x´et da. ng tiˆen dˆ`e (A5) sau dˆay: 1 1 1 1 ∀x1(A1(x1) → A1(x1)) → (A1(x1) →∀x1A1(x1)) 1 1 Khi d´or˜or`angphˆa`n gia’ thiˆe´t: ∀x1(A1(x1) → A1(x1)) nhˆa. n gi´atri. . 1 1 True, nhung phˆa`nkˆe´t luˆa. n: (A1(x1) →∀x1A1(x1)) nhˆa. n gi´atri. False,
  36. 3.4. L´ythuyˆe´t tˆant`u. cˆa´p1K 103 . . . ch˘a’ ng ha. nnˆe´u ta cho. n tru`ong minh hoa. : D = {1, 2, 3, } v`atˆant`u 1 A1 l`a 1 ˜ A1(x)=def “x l`ach˘an” 1 khi d´ota c´ophˆa`nkˆe´t luˆa. n: ∀x1A1(x1) nhˆa. n gi´atri. False, c`onphˆa`n gia’ 1 . . thiˆe´t: A1(x1), trong d´o x1 l`abiˆe´ntu. do, nˆenn´onhˆa. n gi´atri. True v´oi . . . x1 l`asˆo´ ch˘a˜n, v`ata c´okˆe´t qua’ l`aFalse. Do d´otrong tru`ong ho. p, nˆe´u . . xi l`abiˆe´ntu. do trong cˆongth´uc A th`ıtiˆen dˆ`e (A5) s˜e nhˆa. n gi´atri. False. . 3.4.2 Mˆo.t v`aith´ıdu. vˆe` L´ythuyˆe´t tˆant`u cˆa´p1K . . 1) L´y thuyˆe´ts˘a´pth´u tu. bˆo. phˆa.n . . . 2 Gia’ su’ K ch´ua duy nhˆa´tmˆo.t tˆant`u A1: 2 A1(y,z)=def “y<z” v`akhˆongch´u.a c´acbiˆe´n h`amv`ah˘a`ng. Ta k´yhiˆe.u 2 . . . A1(x1,x2)tuong ´ung l`a“x1 <x2” 2 . . . ¬A1(x1,x2)tuong ´ung l`a“x1 <x6 2” C´actiˆen dˆe` riˆenggˆo`m c´o: (1) ∀x1(x1 <x6 2)(khˆongpha’nxa. ) (2) ∀x1∀x2∀x3(x1 <x2 ∧ x2 <x3 → x1 <x3)(b˘a´ccˆa`u) . . Khi d´omˆo˜imˆo.t mˆoh`ınhcu’a l´ythuyˆe´t n`ayngu`oi ta go.il`amˆo. tcˆa´u . . tr´uc s˘a´pth´utu. bˆo. phˆa. n. 2) L´y thuyˆe´t nh´om . . 2 Gia’ su’ Kc´omˆo.t tˆant`u A1: 2 A1(t, s)=def “t = s”,
  37. . . . 104 Chuong 3. Hˆe. to´antˆant`u 2 2 . mˆo.tbiˆe´n h`am f1 : f1 (t, s)=def “t + s”, v`amˆo.th˘a`ng tu’ a1 =0. C´ac tiˆen dˆe` riˆenggˆo`m c´o: . (1) ∀x1∀x2∀x3(x1 +(x2 + x3)=(x1 + x2)+x3) (kˆe´tho. p) . . (2) ∀x1(0 + x1 = x1) (tˆo`nta. i phˆa`ntu’ donvi.) . (3) ∀x1∃x2(x2 + x1 =0) (tˆo`nta. i phˆa`ntu’ dˆo´i) (4) ∀x1(x1 = x1) (pha’nxa. ) . (5) ∀x1∀x2(x1 = x2 → x2 = x1) (dˆo´ix´ung) (6) ∀x1∀x2∀x3(x1 = x2 → (x2 = x3 → x1 = x3)) (b˘a´ccˆa`u) (7) ∀x1∀x2∀x3(x2 = x3 → (x1 + x2 = x1 + x3 ∧ x2 + x1 = x3 + x1)) (ph´ep thˆe´ cu’a d˘a’ ng th´u.c) . . Khi d´omˆo˜imˆo.t mˆoh`ınhcu’a l´ythuyˆe´t n`ayngu`oi ta go.il`amˆo. t nh´om. Ngo`aira nˆe´u n´othoa’ m˜antiˆen dˆe` sau: (8) ∀x1∀x2(x1 + x2 = x2 + x1)(giao ho´an) . . th`ınh´om d´o duo. cgo.il`anh´omgiao ho´an hay nh´omAbel. . 3.5 Di.nh l´y suy diˆ˜en trong logic tˆan t`u . . . . Dˆo´iv´oi di.nh l´ysuy diˆ˜en trong logic mˆe.nh dˆe` ta khˆongthˆe’ chuyˆe’ntuong tu. . . sang di.nh l´ysuy diˆe˜n trong logic tˆant`u mˆo.t c´ach dˆ˜e d`ang,ch˘a’ ng ha.n: V´oi . . cˆongth´uc A n`ao d´o, A`K ∀x1A, ta suy ra: `K A→∀x1A,t´uc l`acˆong . . th´uc(A→∀x1A) l`amˆo.t di.nh l´ytrong l´y thuyˆe´t tˆant`u cˆa´p 1K. Diˆ`eu n`ay . 1 . . l`asai. Ta x´etcˆongth´uc A c´oda.ng sau dˆay: A = A1(x1) v`aminh hoa. duo. c . . xˆaydu. ng nhu sau: . . -Tru`ong minh hoa. D = {1, 2, 3, } . 1 1 ˜ - Tˆant`u A1 : A1(x)=def “x l`ach˘an” Khi d´odˆe˜ d`angta c´o: 1 (1) ∀x1A1(x1) = False
  38. . 3.5. Di.nh l´ysuy diˆe˜n trong logic tˆant`u 105 1 (2) X´et mˆo.t d˜ay s =(b1,b1, ) ∈ P. Ta thˆa´yr˘a`ng: A1(x1) = True , khi v`a ˜ chı’ khi b1 l`amˆo.tsˆo´ ch˘ancu’a D. . . . . 1 1 Do d´ot`u (1) v`a(2) ta t´ınh duo. c cˆongth´uc B =(A1(x1) →∀x1A1(x1)) . . nhˆa.n gi´atri. False trˆend˜ay s =(b1,b2, ). V`ı s =(b1,b2, ) duo. ccho.n tu`y´y,nˆen cˆongth´u.c B khˆonglogic dˆo`ng nhˆa´t d´ung. Ho.nn˜u.a, ta dˆ˜e d`ang . thˆa´yr˘a`ng mˆo˜imˆo.t di.nh l´ycu’a l´ythuyˆe´t tˆant`u cˆa´p 1K l`alogic dˆo`ng nhˆa´t d´ung (di.nh l´y3.6.7). . 1 1 Vˆa.y cˆongth´uc(A1(x1) →∀x1A1(x1)) - l`akhˆong di.nh l´ytrong K.  . . . . Diˆ`eu n`aybuˆo.c ta pha’i c´onh˜ung thay dˆo’i th´ıch ho. p, dˆe’ nhˆa.n duo. c di.nh . l´ysuy diˆ˜enmˆo.t c´ach d´ung d˘a´n trong logic tˆant`u. . . Di.nh ngh˜ıa3.5.1 Gia’ su’ Γ l`amˆo.ttˆa.p c´accˆongth´uc, v`a A l`amˆo.t cˆong . . . th´uccu’a Γ. Gia’ su’ B1, B2, ,Bn l`amˆo.tdˆa˜n xuˆa´tt`u Γ. Khi d´ota n´oir˘a`ng . cˆongth´uc Bi l`a phu. thuˆo. c v`ao A trong dˆa˜n xuˆa´t trˆen,khi v`achı’ khi: (i) Bi ho˘a.cl`aA ho˘a.c . . . . . . . . . (ii) Bi l`adˆa˜n duo. c tru. ctiˆe´pt`u c´accˆongth´uc d´ung tru´oc n´onh`o qui t˘a´c dˆa˜n xuˆa´t Modus Ponens ho˘a.c GEN, trong d´o´ıtnhˆa´tmˆo.t trong c´ac . cˆongth´uc d´ophu. thuˆo.c v`ao A. Th´ıdu. 3.5.1 A, ∀x1A→C`∀x1C (B1) A (gia’ thiˆe´t) (B2) ∀x1A (B1, GEN) (B3) ∀x1A→C (gia’ thiˆe´t) (B4) C (B2, B3, MP) (B5) ∀x1C (B4, GEN) . O’ dˆay B1 phu. thuˆo.c v`ao A;
  39. . . . 106 Chuong 3. Hˆe. to´antˆant`u B2 phu. thuˆo.c v`ao A; B3 phu. thuˆo.c v`ao ∀x1A→C; B4 phu. thuˆo.c v`ao A v`a ∀x1A→C; B5 phu. thuˆo.c v`ao A v`a ∀x1A→C. Di.nh l´y3.5.1 Nˆe´u B khˆong phu. thuˆo. c v`ao A trong suy diˆe˜n Γ, A`Bth`ı Γ `B.Nˆe´u B khˆongphu. thuˆo. c v`ao A trong suy diˆe˜n Γ, A`Bth`ı Γ `B. Ch´u.ng minh . . Gia’ su’ B1, B2, ,Bn l`amˆo.tdˆa˜n xuˆa´tt`u Γ ∪ {A}, trong d´o B khˆong . phu. thuˆo.c v`ao A.Ch´ung minh b˘a`ng qui na.p theo dˆo. d`aicu’adˆa˜n xuˆa´t i : i =1, 2, ,n. . Gia’ thiˆe´tmˆe.nh dˆe` d˜a d´ung dˆo´iv´oimo.idˆa˜n xuˆa´tc´odˆo. d`ai <n.Tacˆa`n . . . . . ch´ung minh mˆe.nh dˆe` c˜ung d´ung v´oi i = n.Tax´et c´actru`ong ho. p sau: . . -Nˆe´u B thuˆo.c v`aoΓ ho˘a.c B l`amˆo.t tiˆen dˆe` th`ıta duo. cΓ`B(theo ch´u y´ 2 chu.o.ng 2 trang 29). . . . . . . . . -Nˆe´u B l`adˆa˜n duo. c tru. ctiˆe´pt`u mˆo.t ho˘a.c hai cˆongth´uc d´ung tru´ocn´o . . . . th`ıkhi d´o,v`ı B khˆongphu. thuˆo.c v`ao A, nˆenc´accˆongth´uc d´ung tru´ocn´o . c˜ung khˆongphu. thuˆo.c v`ao A.Dod´otheo gia’ thiˆe´t qui na.p c´accˆongth´uc . . . . . . . . . n`ay d´ung tru´o cn´odˆe` udˆa˜n duo. ct`u Γmˆo.t c´ach donphuong. V`ıvˆa.y suy ra . . . r˘a`ng B c˜ung dˆa˜n duo. ct`u Γ.  . . Di.nh l´y3.5.2 (di.nh l´ysuy diˆ˜en trong logic tˆant`u) Gia’ su’ Γ, A`Bv`ac´o . . mˆo. t suy diˆ˜encu’a B t`u Γ v`a A, trong d´okhˆongsu’ du. ng qui t˘a´c GEN cho . . . . . . mˆo. t cˆongth´uc n`aophu. thuˆo. c v`ao A v´oibiˆe´nluo. ng t`u l`amˆo. tbiˆe´ntu. do cu’a cˆongth´u.c A. Khi d´o Γ `A→B Ch´u.ng minh:
  40. . 3.5. Di.nh l´ysuy diˆe˜n trong logic tˆant`u 107 . . Gia’ su’ B1, B2, , Bn = B l`adˆa˜n xuˆa´tcu’a B t`u Γ ∪ {A} thoa’ m˜anc´acgia’ . thiˆe´tcu’a di.nh l´y d˜acho. Ta s˜ech´ung minh b˘a`ng qui na.p theo dˆo. d`aidˆa˜n xuˆa´t i =1 n :Γ`A→Bi. . -Nˆe´u Bi l`amˆo.t tiˆen dˆe` ho˘a.c l`aphˆa`ntu’ cu’aΓth`ıΓ`A→Bi,v`ı Bi → (A→Bi) l`atiˆen dˆe` . -Nˆe´u Bi l`a A th`ıΓ `A→Bi, v`ıtheo bˆo’ dˆe` : `A→A. -Nˆe´utˆo`nta.i j, k < i sao cho Bk = Bj →Bi th`ıtheo gia’ thiˆe´t qui na.p Γ `A→Bj v`aΓ `A→(Bj →Bi). Do d´ota c´oΓ `A→Bi b˘a`ng c´ach . ´ap du.ng tiˆen dˆe` A2 v`aqui t˘a´c MP. Cuˆo´ic`ung, gia’ su’ tˆo`nta.i j<isao cho Bi = ∀xkBj. Khi d´otheo gia’ thiˆe´t qui na.pΓ`A→Bj v`aho˘a.cl`aBj khˆong . phu. thuˆo.c v`ao A ho˘a.c xk khˆongpha’i l`abiˆe´ntu. do cu’a A. ∗ Nˆe´u Bj khˆongphu. thuˆo.c v`ao A th`ıkhi d´otheo di.nh l´y 3.5.1 ta c´o: . . . Γ `Bj, v`atiˆe´p theo su’ du. ng qui t˘a´c GEN ta duo. c: Γ `∀xkBj.Dod´ota c´o: Γ `Bi. Theo tiˆen dˆe` A1: `Bi → (A→Bi). Vˆa.y ta c´ongay kˆe´t qua’ Γ `A→Bi nh`o. qui t˘a´cMP. . ∗ Nˆe´u xk khˆongpha’i l`abiˆe´ntu. do trong A th`ıkhi d´otheo tiˆen dˆe` A5: `∀xk(A→Bj) → (A→∀xkBj) V`ır˘a`ng Γ `A→Bj, nˆentheo qui t˘a´c GEN: Γ `∀xj(A→Bj), v`ado . . vˆa.ytac´okˆe´t qua’:Γ`A→∀xkBj nh`o qui t˘a´cMP,t´ucl`a Γ `A→Bi. . . Vˆa.ytad˜ach´ung minh xong cˆongth´uc: Γ `A→Bi ∀i =1 n . . . Trong tru`ong ho. p d˘a.cbiˆe.t i = n, ta c´o: Γ `A→Bn hay Γ `A→B 
  41. . . . 108 Chuong 3. Hˆe. to´antˆant`u Hˆe. qua’ 3.5.1 . . . a) Nˆe´u Γ, A`Bkhˆongsu’ du. ng qui t˘a´c GEN v´oibiˆe´ntu. do c´om˘a. t trong A th`ı Γ `A→B. . b) Nˆe´u A l`amˆo. t cˆongth´uc d´ongv`a Γ, A`Bth`ı Γ `A→B. Th´ıdu. 3.5.2 . a) Ch´ung minh r˘a`ng: `∀x1∀x2A→∀x2∀x1A. Ch´u.ng minh: 1. ∀x1∀x2A (gia’ thiˆe´t) 2. ∀x1∀x2A→∀x2A (A4) 3. ∀x2A (1, 2, MP) 4. ∀x2A→A (A4) 5. A (3, 4, MP) 6. ∀x1A (5, GEN) 7. ∀x2∀x1A (6, GEN) . . T`u 1-7tac´o∀x1∀x2A`∀x2∀x1A, trong d´okhˆongsu’ du. ng qui t˘a´c . . GEN dˆo´iv´oibiˆe´ntu. do c´om˘a.t trong ∀x1∀x2A.Dod´otheo hˆe. qua’ 3.5.1(a) ta c´o: `∀x1∀x2A→∀x2∀x1A. . . b) Nˆe´u term t l`atu. do dˆo´iv´oibiˆe´n xi trong A(xi)th`ı∀xiA(xi) `A(t)v`a A(t) `∃xiA(xi). Ch´u.ng minh : (1) ∀xiA(xi) `A(t) . . Xˆaydu. ng dˆa˜n xuˆa´tnhusau: 1. ∀xiA(xi) (gia’ thiˆe´t)
  42. . 3.5. Di.nh l´ysuy diˆe˜n trong logic tˆant`u 109 2. A(xi) (1, A4, MP) 3. A(t) (2, thˆe´ {xi/t}) . Vˆa.yt`u 1-3 ta c´o: ∀xiA(xi) `A(t)  . . Dˆe´n dˆay´apdu.ng thˆemhˆe. qua’ 3.5.1(a), ta thu duo. c di.nh l´ysau dˆay: `∀xiA(xi) →A(t). (2) A(t) `∃xiA(xi) . . Xˆaydu. ng dˆa˜n xuˆa´tnhusau: 1. A(t) (gia’ thiˆe´t) 2. ∀xi¬A(xi) →¬A(t) (A4) 3. (∀xi¬A(xi) →¬A(t)) → (A(t) →¬∀xi¬A(xi)) (A3) 4. A(t) →¬∀xi¬A(xi) (2, 3, MP) 5. ¬∀xi¬A(xi) (1, 4, MP) 6. ∃xiA(xi)(∃xiA(xi) ≡¬∀xi¬A(xi)) . Vˆa.yt`u 1 – 6 ta c´o: A(t) `∃xiA(xi)  Ap´ du.ng thˆemhˆe. qua’ 3.5.1(a) ta c´o di.nh l´ysau: `A(t) →∃xiA(xi).
  43. . . . 110 Chuong 3. Hˆe. to´antˆant`u 3.6 T´ınh phi mˆau thuˆa˜nv`a dˆ`ay du’ cu’a logic tˆan t`u. 3.6.1 C´ackh´ainiˆe.mv`adi.nh ngh˜ıa . . . Kh´ainiˆe.ml´ythuyˆe´t tˆant`u cˆa´p1duo. c x´ac di.nh kh´arˆo.ng r˜ainh˘a`m bao h`am . . mˆo.t pha.m vi rˆo.ng c´acl´y thuyˆe´t logic v`al´y thuyˆe´t to´anho.c m`ata thu`ong . . g˘a.p. Hˆe. to´antˆant`u cˆa´p 1 (viˆe´tt˘a´t l`aPP) l`amˆo.tl´y thuyˆe´t tˆant`u cˆa´p1, . . . . . . trong d´on´och´ua c´actˆa.p dˆe´m duo. cnhuc´ack´yhiˆe.uh˘a`ng dˆo´ituo. ng, k´yhiˆe.u . . . biˆe´n h`am,v`ak´yhiˆe.utˆant`u,nhung khˆongch´ua c´actiˆen dˆe` riˆeng. C´acl´y . . . thuyˆe´t to´anho.cthu`ong ch´uac´ack´yhiˆe.uh˘a`ng, k´yhiˆe.ubiˆe´n h`am,k´yhiˆe.u . . . tˆant`u co ba’n(t´uc l`ac´acthuˆo.c t´ınhho˘a.c c´acquan hˆe. riˆengcu’a l´ythuyˆe´t) v`ac´actiˆen dˆe` riˆengcu’a l´ythuyˆe´t d´o. . Di.nh ngh˜ıa3.6.1 Mˆo.t mˆoh`ınh cu’a l´ythuyˆe´t tˆant`u cˆa´p1Kl`amˆo.t minh hoa. cu’a K, trong d´omo.i tiˆen dˆe` riˆengcu’a K dˆe` u d´ung trong minh hoa. d´o. . . D˘a.cbiˆe.t, nˆe´u K = PP th`ımo.i minh hoa. cu’aPPdˆe` u duo. c xem l`amˆo h`ınhcu’aPP. Di.nh ngh˜ıa3.6.2 . . . . -L´ythuyˆe´t tˆant`u cˆa´p1Kduo. cgo.il`aphi mˆauthuˆa˜n (ng˜u ngh˜ıa - . Semantic), nˆe´umo.i di.nh l´ycu’a K dˆe` u l`acˆongth´uc d´ung trong mo.i mˆoh`ınh cu’a K. . . . . -L´ythuyˆe´t tˆant`u cˆa´pmˆo.t K duo. cgo.il`adˆa`y du’ (ng˜u ngh˜ıa), nˆe´umˆo˜i . mˆo.t cˆongth´uc d´ung trong mo.i mˆoh`ınhcu’a K dˆe` ul`adi.nh l´ycu’a l´ythuyˆe´t K. Di.nh ngh˜ıa3.6.3 . . . . -L´ythuyˆe´t tˆant`u cˆa´p1Kduo. cgo.il`aphi mˆauthuˆa˜n (h`ınhth´uc - formal), . nˆe´umo.i cˆongth´uc A cu’a K dˆe` u khˆongthˆe’ c´oca’ `Av`a `¬A. . . . . . -L´y thuyˆe´t tˆant`u cˆa´p1Kduo. cgo.il`adˆa`y du’ (h`ınhth´uc), nˆe´u dˆo´iv´oi . mo.i cˆongth´uc d´ong A: ho˘a.cl`a`Aho˘a.cl`a`¬A.
  44. 3.6. T´ınh phi mˆauthuˆa˜nv`adˆa`y du’ cu’a logic tˆant`u. 111 Ch´u´y1 . . ∗ Nˆe´u K l`a mˆau thuˆa˜n(h`ınh th´uc) th`ı c´o mˆo. t cˆong th´uc A . . sao cho `Av`a `¬A.Dod´o theo hˆe. qua’ 2.1.2 (chuong 2): . `x ¬A → (A→B) v`aqui t˘a´c Modus Ponens suy ra r˘a`ng mo. i cˆongth´ucbˆa´t k`y B dˆ`eul`adi.nh l´ytrong K. . . Bo’ ivˆa. y, nˆe´u trong K tˆo`nta. imˆo. t cˆongth´uc khˆongpha’il`adi.nh l´yth`ıl´y thuyˆe´t K d´ol`aphi mˆauthuˆa˜n(h`ınh th´u.c). . . . ∗ Nˆe´ul´y thuyˆe´ttˆant`u cˆa´p 1K c´och´ua ´ıtnhˆa´tmˆo. tk´yhiˆe.u tˆant`u P khˆongc´om˘a. t trong c´actiˆen dˆ`e riˆeng th`ı ta khˆongc´o `K A v`a `K ¬A, trong . . d´o A l`acˆongth´uc d´ong ∀x1P (x1). Theo ngh˜ıa d´oth`ıl´ythuyˆe´t tˆant`u cˆa´p1 . . PP l`al´y thuyˆe´t khˆong dˆa`y du’ h`ınh th´uc, v`ır˘a`ng cˆongth´uc d´ong ∀x1P (x1) . chuathˆe’ xem l`amˆe. nh dˆ`e x´ac di.nh m`ac`onphu. thuˆo. c v`aominh hoa. , trong . . . . d´o P duo. c x´ac di.nh. T´ınh dˆa`y du’ (h`ınh th´uc) chı’ c´o´yngh˜ıa dˆo´iv´oic´acl´y . thuyˆe´t to´anho. criˆeng ch`ung n`aotrong l´ythuyˆe´t d´okhˆongc´oc´ack´yhiˆe. u tˆan . . . . t`u (ho˘a. cbiˆe´n h`am)n`aom`anˆo. i dung cu’a n´okhˆong duo. c qui di.nh bo’ i c´ac tiˆen dˆ`e riˆeng cu’a l´ythuyˆe´t d´o. 3.6.2 T´ınhphi mˆauthuˆa˜ncu’al´y thuyˆe´t tˆant`u. cˆa´p1 PP . Ta d˜abiˆe´tnˆe´u K l`amˆo.tl´ythuyˆe´t tˆant`u cˆa´p 1 th`ımo.i di.nh l´ytrong K dˆe` u . l`acˆongth´uc d´ung trong mo.i mˆoh`ınhcu’a K. . . Di.nh l´y3.6.1 Hˆe. to´antˆant`u cˆa´p 1PP l`aphi mˆauthuˆa˜n (ng˜u ngh˜ıa), ngh˜ıa l`amo. i di.nh l´ycu’aPPdˆ`eul`ah˘a`ng d´ung trong mo. i minh hoa. cu’a PP. . . Di.nh l´y3.6.2 Hˆe. to´antˆant`u cˆa´p 1 PP l`aphi mˆauthuˆa˜n(h`ınh th´uc). Ch´u.ng minh: . . . Ta x´et ´anhxa. h biˆe´n dˆo’imˆo.t cˆongth´uc tˆant`u th`anhmˆo.t cˆongth´uc mˆe.nh dˆe` b˘a`ng c´ach sau dˆay: . . . . . - Cho cˆongth´uc tˆant`u A, ta loa.ibo’ tˆa´tca’ c´acdˆa´uluo. ng t`u v`ac´ac . . . . . . terms c`ung v´oi c´acdˆa´u ngo˘a.c, dˆa´u phˆa’ytuong ´ung. Kˆe´t qua’ thu duo. cl`a . mˆo.t cˆongth´ucmˆe.nh dˆe` h(A).
  45. . . . 112 Chuong 3. Hˆe. to´antˆant`u -Nˆe´u A l`amˆo.t di.nh l´y trong PP th`ı h(A)c˜ung l`a di.nh l´y trong logic mˆe.nh dˆe` L. . -Nˆe´u PP l`amˆauthuˆa˜n, ngh˜ıal`atˆo`nta.i cˆongth´uc A sao cho `PP A v`a . `PP ¬A th`ıkhi d´otrong logic mˆe.nh dˆe` L, ta c´o `x h(A)v`a`x h(¬A)(t´uc l`a `x ¬h(A)). . . . Diˆ`eu n`aymˆauthuˆa˜nv´oi di.nh l´y2.3.3 trong chuong 2: Hˆe. L l`aphi mˆau thuˆa˜n. . . Vˆa.y ta c´ol´ythuyˆe´t tˆant`u cˆa´p 1 PP l`aphi mˆauthuˆa˜n (h`ınhth´uc).  . 3.6.3 Mˆo.tsˆo´ di.nh l´ytrong l´y thuyˆe´t tˆant`u cˆa´p1K . . Di.nh ngh˜ıa3.6.4 Gia’ su’ xi v`a xj l`ahai biˆe´n kh´acnhau, A(xi) khˆongch´ua . . . . biˆe´ntu. do xj, xj tu. do dˆo´iv´oibiˆe´n xi trong A(xi), v`a A(xj) l`acˆongth´uc . . . . nhˆa.n duo. ct`u A(xi)b˘a`ng c´ach thˆe´ xj v`aomo.ivi. tr´ıtu. do cu’a xi trong A(xi). . Khi d´ota n´oir˘a`ng A(xi)v`aA(xj)l`adˆo`ng da. ng v´oi nhau. . . . . . . Nhu vˆa.y trong tru`o ng ho. p n`ay, ta c˜ung c´o A(xj) khˆongch´uabiˆe´ntu. do . . xi v`a xi l`atu. do dˆo´iv´oi xj trong A(xj). Bˆo’ dˆe` 3.6.1 Nˆe´u A(xi) v`a A(xj) l`a dˆo`ng da. ng th`ı `∀xiA(xi) ↔∀xjA(xj) Ch´u.ng minh Theo tiˆen dˆe` (A4): `∀xiA(xi) →A(xj). . Su’ du.ng qui t˘a´c GEN: `∀xj(∀xiA(xi) →A(xj)). . M˘a.t kh´actheo tiˆen dˆe` (A5): `∀xiA(xi) →∀xjA(xj) nh`o qui t˘a´c Modus Ponens. . . . . . B˘a`ng c´ach tuong tu. ta nhˆa.n duo. c: `∀xjA(xj) →∀xiA(xi). . Do d´otheo cˆongth´uc dˆo`ng nhˆa´t d´ung: (A1 → (A2 → A1 ∧ A2)) v`a´ap du. ng 2 lˆa`n qui t˘a´c MP ta c´o `∀xiA(xi) ↔∀xjA(xj).
  46. 3.6. T´ınh phi mˆauthuˆa˜nv`adˆa`y du’ cu’a logic tˆant`u. 113  . . . Di.nh l´y3.6.3 Nˆe´u cˆongth´uc d´ong ¬A cu’a l´ythuyˆe´t K l`akhˆongdˆa˜n duo. c 0 . . . . trong K th`ıl´y thuyˆe´t K nhˆa. n duo. ct`uK b˘a`ng c´achthˆem A nhu mˆo. ttiˆen dˆ`e l`aphi mˆauthuˆa˜n(h`ınh th´u.c). Ch´u.ng minh: Pha’nch´u.ng . . . 0 . Gia’ su’ nguo. cla.i K l`amˆauthuˆa˜n. Khi d´otˆo`nta.imˆo.t cˆongth´uc B sao cho `K0 B v`a `K0 ¬B.M˘a.t kh´ac,ta c´o: `L (B → (¬B →¬A)), nˆenta c˜ung ´ c´o: `K0 (B→(¬B → ¬A)). Ap du.ng 2 lˆa`n qui t˘a´c MP ta c´o: `K0 ¬A.Do d´o A`K ¬A. . Theo gia’ thiˆe´t A l`acˆongth´uc d´ong,nˆen theo hˆe. qua’ 3.5.1 (b) cu’a di.nh l´ysuy diˆ˜en ta c´o: `K A→¬A. . . Honn˜ua, ta c´o: `L ((A →¬A) →¬A), nˆen ta c˜ung c´o: `K ((A→¬A) → ´ . ¬A). Ap du.ng qui t˘a´c MP ta c´o: `K ¬A, tr´aiv´oi gia’ thiˆe´tcu’a di.nh l´y.Vˆa.y K 0 l`aphi mˆauthuˆa˜n.  . . . Bˆo’ dˆe` 3.6.2 Tˆa. pho. ptˆa´tca’ c´acbiˆe’uth´uc (d˜ayh˜uuha. n c´ack´yhiˆe.u) cu’a . . . . . l´y thuyˆe´t tˆant`u cˆa´p1Kl`adˆe´m duo. c. Diˆ`eu n`ayc˜ung d´ung cho c´actru`o ng . . . . . . ho. p l`atˆa. pho. p c´acterm, tˆa. pho. p c´accˆongth´uc, tˆa. pho. p c´accˆongth´uc d´ong. Ch´u.ng minh . . . Tru ´o chˆe´t ta thiˆe´tlˆa.pmˆo.t h`amsˆo´ le’ phˆanbiˆe.t g(u) dˆo´iv´oimˆo˜imˆo.tk´y . hiˆe.u u nhu sau: g(() = 3; g()) = 5; g(, )=7; g(¬)=9; g(→)=11; g(xk)= n n k n n k 5+8k; g(ak)=7+8k; g(fk )=9+8(2 3 ); g(Ak ) = 11 + 8(2 3 ). . . . . . g(u1) g(u2) Khi d´o dˆo´iv´oimˆo.tbiˆe’uth´uc u1u2 ur tuong ´ung l`asˆo´ 2 3 g(ur ) . . . pr , trong d´o pi l`a sˆo´ nguyˆen tˆo´ th´u i. Ta c´o thˆe’ dˆe´m duo. c . . . tˆa´tca’ c´ac biˆe’uth´uc theo th´u tu. cu’a c´ac con sˆo´ liˆen quan dˆe´nch´ung. 
  47. . . . 114 Chuong 3. Hˆe. to´antˆant`u 0 . . Di.nh ngh˜ıa3.6.5 Mˆo.t l´ythuyˆe´t K c´oc`ung c´ack´yhiˆe.ucoba’nnhul´y . . . thuyˆe´t K duo. cgo.il`amo’ rˆo. ng cu’a K,nˆe´umo.i di.nh l´ycu’a K c˜ung l`a di.nh l´ycu’a K 0 . . 0 . . Ch´u´y2 Dˆe’ ch´ung minh K l`amo’ rˆo.ng cu’a K chı’ cˆa`nch´ung minh r˘a`ng 0 mˆo˜imˆo.t tiˆen dˆe` riˆengcu’a K l`amˆo.t di.nh l´ytrong K . Di.nh l´y3.6.4 (Lindenbaum) . Nˆe´u K l`amˆo. tl´y thuyˆe´t tˆant`u cˆa´p 1 phi mˆauthuˆa˜nth`ıtˆo`nta. imˆo. tl´y . . thuyˆe´tmo’ rˆo. ng cu’a K phi mˆauthuˆa˜nv`adˆa`y du’ (theo ngh˜ıa h`ınhth´uc). Ch´u.ng minh . . . . Theo bˆo’ dˆe` 3.6.2, tˆa.pho. ptˆa´tca’ c´accˆongth´uc d´ongcu’a K l`a dˆe´m duo. c, . . . ch˘a’ ng ha.n theo th´u tu. sau: B1, B2, B3, Ta xˆaydu. ng mˆo.t d˜ayc´acl´ythuyˆe´t . J0,J1,J2, nhu sau: - J0 = K. - Gia’ thiˆe´t d˜ax´ac di.nh Jn(n ≥ 0). -Nˆe´u `Jn ¬Bn+1 th`ı d˘a.t Jn+1 = Jn, c`ontr´aila.i, nˆe´u khˆongpha’i `Jn . . . . ¬Bn+1 th`ı d˘a.t Jn+1 l`al´ythuyˆe´tthuduo. ct`u Jn b˘a`ng c´ach thˆem Bn+1 nhu l`amˆo.t tiˆen dˆe` . Theo di.nh l´y3.6.3, nˆe´u Jn l`aphi mˆauthuˆa˜nth`ıJn+1 c˜ung phi mˆauthuˆa˜n. Do d´omo.i l´ythuyˆe´t Jn (n ≥ 0) dˆe` u phi mˆauthuˆa˜n. Bˆay . . . gi`o ta d˘a.t J l`al´ythuyˆe´t tˆant`u cˆa´p1v´oihˆe. tiˆen dˆe` gˆo`mtˆa´tca’ c´actiˆen dˆe` cu’a Ji (i ≥ 0). . . R˜or`ang Jn+1 l`amo’ rˆo.ng cu’a Jn v`a J l`amo’ rˆo.ng cu’amo.i Ji,kˆe’ ca’ J0 = K. . . Dˆe’ ch´ung minh r˘a`ng J l`aphi mˆauthuˆa˜n, ta pha’ich´ung minh mo.i Ji dˆe` u . . . l`aphi mˆauthuˆa˜n, v`ır˘a`ng mˆo.t suy diˆe˜ncu’a mˆauthuˆa˜n trong J duo. c thu. c . hiˆe.nchı’ trong mˆo.tsˆo´ h˜uuha.n c´actiˆen dˆe` ,c˜ung l`amˆo.t suy diˆ˜encu’a mˆau . thuˆa˜n trong mˆo.t Jn n`ao d´o.Ta ch´ung minh t´ınhphi mˆauthuˆa˜ncu’amo.i Ji b˘a`ng qui na.p. - Theo gia’ thiˆe´t J0 = K l`aphi mˆauthuˆa˜n. . - Gia’ su’ r˘a`ng Ji l`aphi mˆauthuˆa˜n. Nˆe´u Ji+1 = Ji th`ı Ji+1 l`aphi mˆauthuˆa˜n.
  48. 3.6. T´ınh phi mˆauthuˆa˜nv`adˆa`y du’ cu’a logic tˆant`u. 115 . . Nˆe´u Ji+1 =6 Ji v`ahonn˜ua, theo di.nh ngh˜ıa cu’a Ji+1 : ¬Bi+1 l`akhˆongdˆa˜n . . duo. c trong Ji, nˆenkhi d´otheo di.nh l´y3.6.3 th`ı Ji+1 c˜ung phi mˆauthuˆa˜n. . Do vˆa.y Ji+1 l`aphi mˆauthuˆa˜n, nˆe´u Ji l`aphi mˆauthuˆa˜n, v`at`u d´ota c´o J l`aphi mˆauthuˆa˜n. Ta ch´u.ng minh t´ınh dˆa`y du’ cu’a J. Gia’ su’. A l`acˆong . . . th´uc d´ongcu’a K. Khi d´o A = Bj+1 dˆo´iv´oi j ≥ 0 n`ao d´o.Bo’ ivˆa.y ho˘a.cl`a ` ´ . . `Jj ¬Bj+1 ho˘a.c `Jj+1 Bj+1,v`ır˘ang nˆeu khˆongpha’i `Jj ¬Bj+1 th`ı Bj+1 duo. c . . . bˆo’ sung v`ao Jj+1 nhu l`amˆo.t tiˆen dˆe` .T`u d´odˆa˜nt´oi ho˘a.cl`a`J ¬Bj+1 ho˘a.c . l`a `J Bj+1.Vˆa.y J l`amˆo.tmo’ rˆo.ng dˆa`y du’ v`aphi mˆauthuˆa˜ncu’a K. 
  49. . . . 116 Chuong 3. Hˆe. to´antˆant`u Di.nh l´y3.6.5 (Go¨del) . Mo. il´y thuyˆe´t tˆant`u cˆa´p 1 K phi mˆauthuˆa˜n dˆ`euc´omˆo. tmˆoh`ınh dˆe´m . . . . . . . duo. c(t´uc l`amˆoh`ınhc´omiˆe` n dˆo´ituo. ng l`a dˆe´m duo. c). Ch´u.ng minh: Gia’ su’. K l`al´ythuyˆe´t tˆant`u. cˆa´p 1 phi mˆauthuˆa˜n. . . . 1) Ta go.i K0 l`al´ythuyˆe´t nhˆa.n duo. ct`u K b˘a`ng c´ach thˆemv`ao K mˆo.ttˆa.p . . . . . . dˆe´m duo. c {b1,b2, } c´ack´yhiˆe.uh˘a`ng dˆo´ituo. ng m´oi. Ta ch´ung minh r˘a`ng K0 l`aphi mˆauthuˆa˜n. . . . Thˆa.tvˆa.y, gia’ su’ nguo.cla.i, K0 l`amˆauthuˆa˜n. Khi d´oc´otˆo`nta.imˆo.t cˆong . th´uc A sao cho c´omˆo.t suy diˆe˜n trong K0 cu’a A∧¬A. . . . Ta thay thˆe´ trong suy diˆe˜n n`aymˆo˜imˆo.t xuˆa´thiˆe.ncu’a bi duo. cthaybo’ i . . . . . . mˆo.tk´yhiˆe.ubiˆe´n chua c´om˘a.t trong suy diˆe˜n v`atru´o c d´ochua duo. cd`ung . . dˆe’ thay thˆe´.Dˆ˜e d`angthˆa´yr˘a`ng viˆe.c thay thˆe´ n`ayta thu duo. cmˆo.t suy diˆ˜en . 0 0 . trong K cu’amˆo.t cˆongth´ucda.ng A ∧¬A,t´uc l`amˆauthuˆa˜n. Diˆ`eu n`aytr´ai v´o.i gia’ thiˆe´t K l`aphi mˆauthuˆa˜n. Vˆa.y ta c´o K0 l`aphi mˆauthuˆa˜n. . . . 2) Theo bˆo’ dˆe` 3.6.2, tˆa.ptˆa´tca’ c´accˆongth´ucch´ua khˆongqu´amˆo.tbiˆe´ntu. . . do trong K0 l`atˆa.p dˆe´m duo.c, ch˘a’ ng ha.n theo c´ach d´anhsˆo´ sau dˆay: F1(xi1),F2(xi2), , Fk(xik), . . . (xik l`abiˆe´ntu. do cu’a Fk,nˆe´u Fk khˆongch´uabiˆe´ntu. do; tr´aila.i, d˘a.t . . xik = x1). Ta cho.nmˆo.t d˜ay bj1,bj2, , bjk, t`u c´ack´yhiˆe.uh˘a`ng m´oi sao . cho bjk khˆongch´ua trong F1,F2, , Fk v`akh´ac bj1,bj2, , bjk−1. . . . . X´et cˆongth´uc duo. c x´ac di.nh nhu sau: Sk = ¬∀xkFk(xik) →¬Fk(bjk). . . . . . Gia’ su’ Kn l`al´y thuyˆe´t tˆant`u cˆa´p 1 nhˆa.n duo. ct`u K0 b˘a`ng c´ach thˆem . . . . S1,S2, , Sn nhu l`ac´actiˆen dˆe` m´oi, v`a K∞ l`al´ythuyˆe´t nhˆa.n duo. cb˘a`ng . . c´ach thˆemtˆa´tca’ c´accˆongth´uc Si nhu l`ac´actiˆen dˆe` v`ao K0. . . Mˆo˜imˆo.t suy diˆ˜en trong K∞ chı’ ch´uamˆo.tsˆo´ h˜uuha.n c´ac Si,v`adod´o n´oc˜ung l`asuy diˆe˜n trong mˆo.t Kn n`ao d´o.Do vˆa.y, nˆe´umo.i Ki l`aphi mˆau
  50. 3.6. T´ınh phi mˆauthuˆa˜nv`adˆa`y du’ cu’a logic tˆant`u. 117 . thuˆa˜nth`ıK∞ c˜ung phi mˆauthuˆa˜n. Dˆe’ ch´ung minh r˘a`ng mo.i Ki l`aphi mˆau . thuˆa˜n, ta ch´ung minh b˘a`ng qui na.p. - K0 l`aphi mˆauthuˆa˜n. . . - Gia’ su’ Kn−1 l`aphi mˆauthuˆa˜n, nhung Kn l`amˆauthuˆa˜n(n ≥ 1). Khi . . . . . d´onhu ta d˜abiˆe´tmˆo˜imˆo.t cˆongth´uc l`adˆa˜n duo. c trong Kn theo cˆongth´uc dˆo`ng nhˆa´t d´ung A1 → (¬A1 → A2) v`aqui t˘a´cMP.D˘a.cbiˆe.t `K ¬Sn.Dod´o ta c´o Sn `Kn−1 ¬Sn. . V`ı Sn l`acˆongth´uc d´ong,nˆen theo hˆe. qua’ 3.5.1 (b) ta c´o `Kn−1 Sn →¬Sn. . M˘a.t kh´ac,ta c˜ung c´ocˆongth´uc(A1 →¬A1) →¬A1 l`a dˆo`ng nhˆa´t d´ung, nˆen . ´ . ta c´o: `Kn−1 ¬Sn nh`o qui t˘acMP,t´ucl`a `Kn−1 ¬(¬∀xinFn(xin) →¬Fn(bjn)) Theo c´accˆongth´u.c dˆo`ng nhˆa´t d´ung: ¬(A1 → A2) → (A1 ∧¬A2); (A1 ∧ A2) → A1;(A1 ∧ A2) → A2; ¬¬A1 → . . A1, ta nhˆa.n duo.ckˆe´t qua’ sau: `Kn−1 ¬∀xinFn(xin)v`a `Kn−1 Fn(bjn) X´et mˆo.t suy diˆ˜en n`ao d´ocu’a Fn(bjn) trong Kn−1.Tacho.n xp l`amˆo.tbiˆe´n . khˆongc´om˘a.t trong suy diˆ˜en d´o. Ta thay kh˘a´pnoi trong suy diˆe˜n d´ok´y . . . hiˆe.u bjn bo’ i xp, khi d´ota nhˆa.n duo. cmˆo.t suy diˆ˜en trong Kn−1 cu’a F (xp), . t´ucl`a`Kn−1 Fn(xp). ´ ´ . . ’ ` Ap du. ng qui t˘ac GEN ta duo. c: `Kn−1 ∀xpFn(xp), v`atheo bˆo dˆe 3.6.1 ta ` . c´o: `Kn−1 ∀xinFn(xin), v`ı Fn(xin)v`aFn(xp)l`adˆong da.ng v´oi nhau. . . . . Vˆa.ytad˜ach´ung minh duo. cr˘a`ng Kn−1 l`amˆauthuˆa˜n, diˆe` u d´otr´aiv´oi . gia’ thiˆe´t qui na.p. Do d´o Kn l`aphi mˆauthuˆa˜n, v`at`u d´o K∞ c˜ung l`aphi mˆauthuˆa˜n. . Ch´u´yr˘a`ng K∞ l`amo’ rˆo.ng phi mˆauthuˆa˜ncu’a K0, v`atheo di.nh l´y3.6.4 . l´ythuyˆe´t J l`amˆo.tmo’ rˆo.ng phi mˆauthuˆa˜nv`adˆa`y du’ cu’a K∞. . . . . . 3) Bˆaygi`o ta xˆaydu. ng mˆo.t minh hoa. dˆe´m duo. c M cho l´ythuyˆe´t tˆant`u K0 (theo dˆa`y du’ tiˆe´n tr`ınhsau dˆay).
  51. . . . 118 Chuong 3. Hˆe. to´antˆant`u . . . Di.nh ngh˜ıa3.6.6 Mˆo.t term (ha.ng tu’ ) duo. cgo.il`ad´ong,nˆe´u n´okhˆong ch´u.a c´acbiˆe´n. . . . . Minh hoa. M cu’a K0 duo. c xˆaydu. ng nhu sau: . -Tad˘a.t D l`atˆa.pho. ptˆa´tca’ c´acterms d´ongcu’a K0.Tˆa.p n`ayl`a dˆe´m . . . . duo. c theo bˆo’ dˆe` 3.6.2, v`atˆa.p D n`ayl`aTru`ong minh hoa. (hay miˆe` n x´ac di.nh . . dˆo´ituo. ng cu’a M). . . . -Mˆo˜imˆo.tk´yhiˆe.uh˘a`ng c cu’a K th`ın´o duo. c minh hoa. bo’ ich´ınh l`ah˘a`ng . . . d´o(v´oituc´ach l`amˆo.t phˆa`ntu’ cu’a D) trong M. ˜ n . . . n∗ . n -Mˆoimˆo.tk´yhiˆe.ubiˆe´n h`am fj cu’a K duo. c g´anmˆo.t to´antu’ fj t`u D . n v`ao D trong M sao cho dˆo´iv´oimˆo˜imˆo.tbˆo. (t1,t2, , tn)∈ D c´acterm d´ong . . . n∗ tuong ´ung cho ta mˆo.t gi´atri. fj (t1,t2, , tn) l`amˆo.t term d´ongthuˆo.c D cu’a K0. . n . . n∗ . -Mˆo˜imˆo.tk´yhiˆe.u tˆant`u Aj trong K duo. c g´anmˆo.t ´anhxa. Aj t`u n . n D v`ao {T, F} trong M sao cho dˆo´iv´oimˆo.tbˆo. (t1,t2, , tn) ∈ D ta c´o n∗ n Aj (t1,t2, , tn)=T , khi v`achı’ khi `J Aj (t1,t2, , tn). . Mu.c d´ıch cu’atal`ach´ung minh r˘a`ng minh hoa. M l`amˆo.tmˆoh`ınh cu’al´y . thuyˆe´t tˆant`u K0. . . . Dˆe’ ch´ung minh diˆe` u n`ay, ta chı’ cˆa`nch´ung minh r˘a`ng mˆo˜imˆo.t cˆongth´uc d´ong A cu’a K0 l`a d´ung trong M, khi v`achı’ khi `J A,v`ır˘a`ng mo.i di.nh l´y . cu’a K0 dˆe` ul`adi.nh l´ytrong J.Tach´ung minh mˆe.nh dˆe` n`ayb˘a`ng qui na.p . . . . theo sˆo´ ph´epto´anv`aluo. ng t`u trong cˆongth´uc A. . . . . . Tru ´ochˆe´t, gia’ su’ A l`amˆo.t cˆongth´uc d´ongso cˆa´p. Khi d´o,theo di.nh ngh˜ıa A l`a d´ung trong M, khi v`achı’ khi `J A. . . . . Bˆaygi`o bu´oc gia’ thiˆe´t qui na.p: nˆe´u B l`acˆongth´uc d´ongn`ao d´oc´osˆo´ . . . . ph´epto´anv`aluo. ng t`u ´ıthon A,v`aB l`a d´ung trong M khi v`achı’ khi `J B. . . . Ta cˆa`n pha’i x´etc´actru`o ng ho. p sau dˆay: . . . • Tru `ong ho. p1: A l`a ¬B -Nˆe´u A l`a d´ung trong M th`ı B l`asai trong M, v`atheo gia’ thiˆe´t qui . na.p: khˆongc´o `J B.V`ı J l`a dˆa`y du’ v`a B l`acˆongth´uc d´ong,nˆen . `J ¬B,t´ucl`a`J A
  52. 3.6. T´ınh phi mˆauthuˆa˜nv`adˆa`y du’ cu’a logic tˆant`u. 119 - Tr´aila.i, nˆe´u A l`asai trong M th`ı B l`a d´ung trong M.Dod´o `J B.V`ı . . . J l`aphi mˆauthuˆa˜n nˆenta nhˆa.n duo. c: khˆongc´o `J ¬B,t´uc l`akhˆong c´o `J A . . . • Tru `ong ho. p2: A l`a B→C V`ı A l`acˆongth´u.c d´ong,nˆen B v`a C dˆe` u l`acˆongth´u.c d´ong. -Nˆe´u A l`asai trong M th`ı B l`a d´ung v`a C l`asai. Do d´otheo gia’ thiˆe´t qui na.p: `J B v`akhˆongc´o `J C. Theo t´ınh dˆa`y du’ cu’a J: `J ¬C.Do . vˆa.y theo c´accˆongth´uc dˆo`ng nhˆa´t d´ung: A1 → (¬A2 →¬(A1 → A2)) . . nˆenta c´o `J ¬(B→C) nh`o qui t˘a´c Modus Ponens, t´ucl`a`J ¬A,v`a . nhu vˆa.y theo t´ınhphi mˆauthuˆa˜ncu’a J: khˆongc´o `J A. M˘a.t kh´ac,nˆe´u khˆongc´o `J A th`ıtheo t´ınh dˆa`y du’ cu’a J: `J ¬A. Theo c´accˆongth´u.c dˆo`ng nhˆa´t d´ung: ¬(A1 → A2) → A1 v`a ¬(A1 → A2) →¬A2, . . . ta nhˆa.n duo. ckˆe´t qua’: `J B v`a `J ¬C nh`o qui t˘a´c Modus Ponens. Do vˆa.y B l`a d´ung trong M. Theo t´ınhphi mˆauthuˆa˜ncu’a J: khˆongc´o `J C v`ado vˆa.y, C l`asai trong M.Vˆa.y A l`asai trong M. . . . • Tru `ong ho. p3: A l`a ∀xnB . Gia’ su’ B l`a Fk(xik). Ta c´othˆe’ gia’ thiˆe´tr˘a`ng xn l`a xik. Ngo`aira, B l`a . . . . . . cˆongth´uc d´ongv`akhˆongch´ua xn v´oituc´ach l`abiˆe´ntu. do. Nhung . . . trong tru`ong ho. p n`ay, A l`a d´ung khi v`achı’ khi B d´ung, v`a `J A khi v`achı’ khi `J B. Do vˆa.ymˆe.nh dˆe` B d´ung th`ı A c˜ung d´ung. . . . Tru ´o chˆe´t ta gia’ thiˆe´tr˘a`ng A l`a d´ung trong M,nhung khˆongc´o `J A. . . Theo t´ınh dˆa`y du’ cu’a J: `J ¬A,t´ucl`a`J ¬∀xikFk(xik). Nhung `J Sk . . v`ad`ung qui t˘a´c MP ta thu duo. c `J ¬F (bjk). V`ı A = ∀xikFk(xik)l`a d´ung trong M,nˆenFk(bjk)c˜ung d´ung trong M. . Theo gia’ thiˆe´t qui na.p `J Fk(bjk), diˆe` u n`aymˆauthuˆa˜nv´oit´ınh phi mˆau thuˆa˜ncu’a J.Dod´ota pha’i c´o: `J A.
  53. . . . 120 Chuong 3. Hˆe. to´antˆant`u . . - Bˆaygi`o ta gia’ thiˆe´t A l`asai trong M nhung `J A.V`ı ∀xikFk(xik) l`asai . . trong M, nˆentˆo`nta.i ´ıtnhˆa´tmˆo.t phˆa`ntu’ trong D,t´uc l`amˆo.t term d´ongcu’a . K0 sao cho Fk(t) l`asai trong M.V`ı ta gia’ thiˆe´t `J A,t´ucl`a`J ∀xikFk(xik), nˆentheo tiˆen dˆe` (A4) ta c´o `J Fk(t). Do d´o Fk(t)l`ad´ung trong M, diˆe` u . n`aymˆauthuˆa˜nv´oi t´ınhsai cu’a Fk(t) trong M.V`ıvˆa.y khˆongthˆe’ c´o `J A. . . . . Mˆe.nh dˆe` m`ata d`oiho’i ho`anto`an duo. cch´ung minh dˆo´iv´oi A. . . . . . . Nhu vˆa.ytad˜ach´ung minh duo. c M l`amˆo.t mˆoh`ınh dˆe´m duo. c cu’a . . . l´ythuyˆe´t J,v`adod´oc˜ung l`a dˆe´m duo. c dˆo´iv´oi l´ythuyˆe´t K0.V`ımo.i di.nh . . l´ycu’a K l`a di.nh l´ycu’a K0,nˆenM c˜ung l`amˆoh`ınh dˆe´m duo. ccu’al´y thuyˆe´t K.  3.6.4 T´ınh dˆa` y du’ cu’al´y thuyˆe´t tˆant`u. cˆa´p1K . Di.nh l´y3.6.6 Mˆo˜imˆo. t di.nh l´ycu’a l´ythuyˆe´t tˆant`u cˆa´p 1 PP l`alogic dˆo`ng nhˆa´t d´ung. Ch´u.ng minh . . . -Tadˆe˜ d`angkiˆe’m tra duo. cr˘a`ng c´actiˆen dˆe` t`u (A1) dˆe´n (A5) dˆe` ul`a logic dˆo`ng nhˆa´t d´ung. - C´acqui t˘a´cdˆa˜n xuˆa´t MP v`aGEN dˆe` u c´ot´ınhlogic dˆo`ng nhˆa´t d´ung. Do d´omˆo˜imˆo.t di.nh l´yl`alogic dˆo`ng nhˆa´t d´ung.  . . Bˆo’ dˆe` 3.6.3 Mˆo˜imˆo. t cˆongth´uc logic dˆo`ng nhˆa´t d´ung cu’a l´ythuyˆe´ttˆant`u cˆa´p1Kl`amˆo. t di.nh l´ycu’a K. Ch´u.ng minh . . . Ta chı’ cˆa`n x´etc´accˆongth´uc d´ong.Gia’ su’ A l`amˆo.t cˆongth´uc d´ongv`a . logic dˆo`ng nhˆa´t d´ung cu’a K. Gia’ su’ A khˆongpha’il`adi.nh l´ycu’a K. Khi d´o . . . . theo di.nh l´y3.6.3 ta thˆemv`ao K cˆongth´uc ¬A nhu mˆo.t tiˆen dˆe` ,taduo. c 0 0 mˆo.tl´y thuyˆe´t phi mˆauthuˆa˜n K . Theo di.nh l´y3.6.5, K c´omˆo.tmˆoh`ınh M.V`ı ¬A l`atiˆen dˆe` cu’a K 0 ,nˆen¬A d´ung trong M.Ho.nn˜u.a, A l`alogic . . dˆo`ng nhˆa´t d´ung, nˆen A c˜ung d´ung trong M.Nhuvˆa.y cˆongth´uc A dˆo`ng
  54. . . 3.7. Ap´ du. ng trong ch´ung minh di.nh l´ycu’a l´ythuyˆe´t tˆant`u cˆa´p1 121 th`o.iv`u.a d´ung, v`u.a khˆong d´ung trong mˆoh`ınh M. Diˆ`eu n`ayl`amˆauthuˆa˜n. Vˆa.y A l`amˆo.t di.nh l´ycu’a K.  Di.nh l´y3.6.7 (di.nh l´y dˆa`y du’ cu’aGio¨del [1930]) . . . . Trong l´y thuyˆe´t tˆant`u cˆa´p 1PP, l´op c´ac di.nh l´ytr`ungv´oil´op c´accˆong th´u.c logic dˆo`ng nhˆa´t d´ung. Ch´u.ng minh . . . Diˆ`eu n`ay duo. c suy ra t`u di.nh l´y3.6.6 v`abˆo’ dˆe` 3.6.3.  Di.nh l´y3.6.8 (di.nh l´ySkolem-Lo¨wenhim [1919, 1915]) . Nˆe´umˆo. t l´ythuyˆe´t tˆant`u cˆa´p1Kc´omˆo. tmˆoh`ınh n`ao d´oth`ın´oc˜ung c´o . . mˆo. tmˆoh`ınh dˆe´m duo. c. Ch´u.ng minh Ch´u´yr˘a`ng nˆe´u K c´omˆo.tmˆoh`ınh th`ı K l`aphi mˆauthuˆa˜n. Do d´otheo . . di.nh l´y3.6.5, K c´omˆo.tmˆoh`ınh dˆe´m duo. c.  ´ . 3.7 Ap du. ng trong ch´ung minh di.nh l´ycu’a l´y thuyˆe´ttˆan t`u. cˆa´p1 Ch´u.ng minh r˘a`ng: `∀xi(A∨B) → (∃xiA∨∀xiB) Ch´u.ng minh . . . • C´ach1: Ap´ du.ng di.nh l´y suy diˆe˜n trong logic tˆant`u.Tru´o chˆe´tta biˆe´n dˆo’i cˆongth´u.c d˜acho nhu. sau: `∀xi(A∨B) → (∃xiA∨∀xiB) ⇔ `∀xi(A→B) → ((∀xiA) ∨∀xiB) ⇔ `∀xi(A→B) → (∀xiA→∀xiB) . . Ta ch´ung minh b˘a`ng c´ach xˆaydu. ng dˆa˜n xuˆa´t:
  55. . . . 122 Chuong 3. Hˆe. to´antˆant`u 1. ∀xi(A→B) (gia’ thiˆe´t) 2. ∀xiA (gia’ thiˆe´t) 3. A→B (1, A4) 4. A (2, A4) 5. B (3, 4, MP) 6. ∀xiB (5, GEN) . Vˆa.yt`u 1 - 6 ta c´o: ∀xi(A→B), ∀xiA`∀xiB. ’. . . O dˆaytrong khi xˆaydu. ng dˆa˜n xuˆa´t ta khˆongsu’ du.ng qui t˘a´c GEN . . dˆo´iv´oibiˆe´ntu. do cu’a ∀xi(A→B)v`a∀xiA.Dod´otheo di.nh l´y3.5.2, ta dˆ˜e d`ang´apdu. ng 2 lˆa`n di.nh l´y suy diˆe˜n, ta c´o `∀xi(A→B) → (∀xiA→∀xiB)  • C´ach2: Ap´ du.ng di.nh l´y dˆa`y du’ cu’a G¨odelta d˘a.t: C = ∀xi(A∨B) → (∃xiA ∨∀xiB) l`a di.nh l´y,khi v`achı’ khi C l`alogic dˆo`ng nhˆa´t d´ung. . . . Ta x´etmˆo.t minh hoa. v´oi D l`aTru`ong minh hoa. m`atrˆen d´oc´accˆong . . . th´uc A v`a B duo. c x´ac di.nh. . . Gia’ su’ d˜ay s =(b1,b2, , bi, ) ∈ P tu`y´y.Ta s˜ech´ung minh r˘a`ng C . . . . l`athu. chiˆe.n duo. c trˆen s,t´ucl`aC = 1 trˆend˜ay s =(b1,b2, , bi, ). . . . Thˆa.tvˆa.y, ta x´et2 tru`ong ho. p sau dˆay: . . . . . . a) Tru `ong ho. p1: D = ∀xi(A∨B) l`akhˆongthu. chiˆe.n duo. c trˆen s t´u.cl`aD = 0 trˆen s. Khi d´or˜or`angta c´ongay C = 1 trˆend˜ay s. . . . Vˆa.y C thu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, , bi, ).
  56. . . 3.8. B`aitˆa.p chuong 3 123 . . . . . . b) Tru `o ng ho. p2: D = ∀xi(A∨B) l`athu. chiˆe.n duo.c trˆen s = . (b1,b2, , bi, )(t´ucl`aD = 1 trˆend˜ay s). Khi d´otheo di.nh ngh˜ıa . . . D l`athu. chiˆe.n duo. c trˆend˜ay s =(b1,b2, , bi, ) ⇔ (A∨B)l`a . . . 0 thu. chiˆe.n duo. c trˆenmo.i d˜aybˆa´tk`y s kh´ac s khˆongqu´ath`anh . . . . 0 phˆa`nth´u i ⇔ A l`athu. chiˆe.n duo. c trˆenmo.i d˜aybˆa´tk`y s kh´ac . . . . s khˆongqu´ath`anhphˆa`nth´u i (1) ho˘a.c B l`athu. chiˆe.n duo. c trˆen 0 . mo.i d˜aybˆa´tk`y s kh´ac s khˆongqu´ath`anhphˆa`nth´u i (2). . . . . . . T`u (1) suy ra r˘a`ng cˆongth´uc ∃xiA l`athu. chiˆe.n duo. c dˆo´iv´oi´ıt 0 . 0 nhˆa´tmˆo.t d˜ay s kh´ac s khˆongqu´ath`anhphˆa`nth´u i. (3) (s ∈ P). . . . . T`u (2) suy ra r˘a`ng ∀xiB l`athu. chiˆe.n duo. c trˆenmo.i d˜aybˆa´tk`y s0 kh´ac s khˆongqu´ath`anhphˆa`nth´u. i. (4) . . . . Kˆe´tho. p (3) v`a(4) ta c´o: G = ∃xiA∨∀xiB l`athu. chiˆe.n duo. c trˆend˜ay s,t´u.cl`aG = 1 trˆend˜ay s. . . . Vˆa.y C = D→G =1→ 1 = 1, ngh˜ıa l`a C l`athu. chiˆe.n duo. c trˆen . . d˜ay s =(b1,b2, , bi, ) ∈ P.V`ıs duo. ccho.n tu`y´y,nˆen cˆong th´u.c C l`alogic dˆo`ng nhˆa´t d´ung.  . . 3.8 B`ai tˆa. p chuong 3 . 1. H˜ayviˆe´tdˆa´u ngo˘a.c cho c´accˆongth´uc sau: 1 3 1 a) ∀x1¬A1(x1) → A2(x1,x2,x3) ∨∀x1A2(x1) 1 1 2 1 b) ¬∀x1A1(x1) →∃x2A2(x2) → A1(x1,x2) ∨ A1(x2) 1 1 1 c) ∀x1∀x3∀x4A1(x1) → A2(x3) ∧¬A1(x1) 1 2 d) ∃x1∀x2∃x3A1(x1) ∨∃x2¬∀x3A1(x3,x2) . 2. H˜aychı’ ra biˆe´n n`aol`abiˆe´ntu. do, biˆe´n n`aol`abiˆe´n r`angbuˆo.ccu’a c´ac cˆongth´u.c sau: 2 2 a) ∀x3((∀x1A1(x1,x2)) → A1(x3,x1)) 2 2 b) ∀x2A1(x3,x2) →∀x3A1(x3,x2)
  57. . . . 124 Chuong 3. Hˆe. to´antˆant`u 3 2 2 1 c) (∀x2∃x1A1(x1,x2,f1 (x1,x2))) ∨¬∀x1A1(x2,f1 (x1)) 2 . . . 3. C´opha’i t = f1 (x1,x2) l`atu. do dˆo´iv´oi x1 trong cˆongth´uc sau dˆaykhˆong: 2 1 a) A1(x1,x2) →∀x2A1(x2), 2 2 b) (∀x2A1(x2,a1)) ∨∃x2A1(x1,x2). 4. Ch´u.ng minh r˘a`ng c´accˆongth´u.c sau dˆaykhˆonglogic dˆo`ng nhˆa´t d´ung: 2 2 a) ∀x2∃x1A1(x1,x2) →∃x1∀x2A1(x1,x2) 1 1 1 1 b)(∀x1A1(x1) →∀x1A2(x1)) →∀x1(A1(x1) → A2(x1)) 1 1 1 1 c) ∀x1(A1(x1) ∨ A2(x1)) → (∀x1A1(x1) ∨∀x1A2(x1)) 5. Ch´u.ng minh r˘a`ng c´accˆongth´u.c sau dˆayl`alogic dˆo`ng nhˆa´t d´ung: . . a) A(t) →∃x1A(x1), nˆe´u t l`atu. do dˆo´iv´oi x1 trong A(x1) b) ∀xiA→∃xiA c) ∀xi∀xjA≡∀xj∀xiA d)(∀xiA∨∀xiB) →∀xi(A∨B) e) ∃xi∃xjA≡∃xj∃xiA f) ∃xi∀xjA→∀xj∃xiA . . 6. Nˆe´u A l`amˆo.t cˆongth´uc d´ongth`ıkhi d´och´ung minh r˘a`ng A logic k´eo theo B, khi v`achı’ khi B l`a d´ung trong mˆo˜imˆo.t minh hoa. m`ata.i d´o A l`a d´ung. 7. Ch´u.ng minh r˘a`ng cˆongth´u.c sau dˆaykhˆonglogic dˆo`ng nhˆa´t d´ung: 2 2 2 2 a) ∃x∀y(A1(x, y) ∧¬A1(y,x) → [A1(x, x) ↔ A1(y,y)]) 2 2 2 2 b) ∀x¬A1(x, x) ∧∀x∀y∀z(A1(x, y) ∧ A1(y,z) → A1(x, z)) → 2 ∃x∀y¬A1(x, y) 2 2 2 2 2 c) ∀x∀y∀z(A1(x, x)∧(A1(x, z) → A1(x, y)∨A1(y,z))) →∃y∀zA1(y,z)
  58. . . 3.8. B`aitˆa.p chuong 3 125 . . 8. Ch´ung minh r˘a`ng c´accˆongth´uc sau l`a di.nh l´y: a) `∀x1(A→B) → (∀x1A→∀x1B) b) `∀x1(A→B) → (∃x1A→∃x1B) c) `∀x1(A∧B) ≡ (∀x1A∧∀x1B) d) `∀x1∀x2 ∀xnA→A e) `∃x1¬A ≡ ¬∀x1A f) `∀x1A≡¬∃x1¬A g) `∃x1(A∨B) ≡ (∃x1A∨∃x1B) . . 9. Dˆo´iv´oimˆo˜imˆo.tl´y thuyˆe´t tˆant`u cˆa´p1K,nˆe´uΓ`K A v`amˆo˜imˆo.t cˆong . th´uccu’aΓl`ad´ung trong minh hoa. M d˜acho cu’a K th`ı A c˜ung d´ung trong M.