´ Ulohy - predik´atov´a logika (pˇrepis) Martin Vˇsetiˇcka 7. ledna 2009, 17:12
Z´ asadn´ı informace pro n´ asledn´ eˇ cten´ı pˇ r´ıklad˚ u Tvrzen´ı: Pravidlo tautologie (PTT) Pravidlo o rozboru pˇr´ıpad˚ u (PR) Pravidlo konjunkce (PK)
Kaˇzd´a tautologie je dokazateln´a v predik´atov´e logice. T $ pA _ B q Ñ C ô pT $ A Ñ C q a pT $ B Ñ C q T $AaT $BôT $A & B
Pravidlo tranzitivity implikace (PTI)
T
$AÑB aT $BÑCñT $AÑC
D˚ ukaz. 1. PTT plyne z toho, ˇze predik´atov´a logika 1. ˇr´adu v sobˇe pˇrirozenˇe obsahuje v´ yrokovou logiku (tj. kaˇzd´a formule je v´ yrok nad prvov´ yroky, kter´e pˇredstavuj´ı atomick´e formule a formule zaˇc´ınaj´ıc´ı kvantifik´atorem). 2. PR plyne z PTT a z faktu, ˇze pA _ B q Ñ C 3. PK plyne z toho, ˇze A Ñ pB 4.
Ø ppA Ñ B q
& pB
Ñ C qq je tautologie.
Ñ pA & B qq je tautologie, z PTT a z definice symbolu $. PTI plyne z toho, ˇze pA Ñ B q Ñ ppB Ñ C q Ñ pA Ñ C qq je tautologie.
Dalˇ s´ı z´ akladn´ı pouˇ cky, pravidla, vˇ ety a axiomy a jejich symbolick´ e oznaˇ cen´ı Pouˇ cka, pravidlo, axiom Pravidlo Modus Ponens Pravidlo Generalizace Axiom Specifikace Axiom Pˇreskoku Pravidlo Zaveden´ı @ Pravidlo Zaveden´ı D Vˇeta o uz´avˇeru Vˇeta o Instanci Vˇeta o Substituci
Symbol MP PG AxS AxP PZ@ PZD VU VI VS
Vˇeta o Konstant´ach
VK
Vˇeta o Dedukci D˚ ukaz sporem Pravidlo Distribuce Q Vˇeta o Ekvivalenci
VD DS PDQ VE
Vˇeta o Variant´ach
VV
Formulace Odvod’ B z A a A Ñ B Odvod’ p@xqA z A p@xqA Ñ Ax rts; Ax rts Ñ pDxqA (”du´aln´ı verze”) p@xqpA Ñ B q Ñ pA Ñ p@xqB q, nen´ı-li x voln´a v A. T $ A Ñ B ñ T $ A Ñ p@xqB, nen´ı-li x voln´a v A. T $ A Ñ B ñ T $ pDxqA Ñ B, nen´ı-li x voln´a v B. T $ A ô T $ A1 , je-li A1 uz´avˇer A. T $ A ñ T $ A1 , je-li A1 instance A. a) $ p@x1 , . . . , xn qA Ñ Ax1 ,...,xn rt1 , . . . , tn s b) $ Ax1 ,...,xn rt1 , . . . , tn s Ñ pDx1 , . . . , xn qA T $ A ô T 1 $ Ax1 ,...,xn rc1 , . . . , cn s, je-li T 1 rozˇs´ıˇren´ı o nov´e konstantn´ı symboly ci , 1 ¤ i ¤ n. Je-li A sentence, tak T, A $ B ô T $ A Ñ B. Je-li A sentence, tak T, A je sporn´a ô T $ A. T $ A Ñ B ñ T $ pQxqA Ñ pQxqB. Necht’ formule A1 vznikne z formule A nahrazen´ım nˇekter´ ych v´ yskyt˚ u podformul´ı A1 , A2 , . . . , An po ˇradˇe formulemi A11 , A12 , . . . , A1n , kde pro @i P t1, . . . , nu je $ Ai Ø A1i . Potom: $ A Ø A1 . $ A Ø A1 , je-li A1 varianta A. 1
Dalˇs´ı bˇeˇznˇe uˇz´ıvan´a symbolick´a oznaˇcen´ı: • Q . . . oznaˇcen´ı pro kvantifik´ator (@, D) • • • • • •
ñ . . . znaˇc´ı ˇcesk´e ”implikuje”. ô . . . znaˇc´ı ˇcesk´e ”je ekvivalentn´ı”. Ñ . . . symbol pro implikaci ve form´aln´ım jazyce Ø . . . symbol pro ekvivalenci ve form´aln´ım jazyce Pro formule A, B symbol A B znaˇc´ı ”formule A je B”; obdobnˇe o termech t, s m˚ uˇzeme prohl´asit t s Je-li A formule resp. t je term, symbol Apxq resp. tpxq znaˇc´ı, ˇze x je nˇejak´a n-tice x1 , . . . , xn
navz´ ajem r˚ uzn´ ych promˇenn´ ych, mezi kter´ ymi jsou vˇsechny voln´e promˇenn´e A resp. vˇsechny promˇenn´e termu t.
F.1.0 Substituce, instance F.1.0.1 Vlastnosti substituc´ı a instanc´ı 1. Dokaˇzte: $ p@xqA Ø p@y qAx ry s, pokud y nen´ı voln´a v A a je substituovateln´a za x do A. Speci´alnˇe tedy plat´ı: p@xqA Ø p@y qAx ry s, nem´a-li y v´ yskyt v A. ˇ sen´ı: Oznaˇcme Ax ry s jako A1 . Oba pˇredpoklady o x, y v A zaruˇcuj´ı, ˇze voln´ Reˇ y v´ yskyt y v A1 je pr´avˇe tam, kde je voln´ y v´ yskyt x v A. Tedy x je substituovateln´e za y do A1 a A1y rxs je A. (1) (2) (3) (4) (5) (6)
$p@yqA1 Ñ Ay rxs $p@yqA1 Ñ A $p@xqA Ñ A1 $p@yqA1 Ñ p@xqA $p@xqA Ñ p@yqA1 $p@xqA Ø p@yqAx rys
(AxS) (pˇrepis) (AxS) (PZ@ na (2)) (PZ@ na (3)) (PK na (4) a (5))
Pˇ r´ıpisek: Ukaˇzme si ty substituce na pˇr´ıkladu, mˇejme formuli: Ax0Ñ
pDyqpy 0q
M´ame splnˇen´e oba pˇredpoklady (y nen´ı voln´a v A a y je substituovateln´a za x). A1 je tedy tvaru: A1 y 0 Ñ pDy qpy 0q Promˇenn´a x je zˇrejmˇe substituovateln´a za y, ˇc´ımˇz dostaneme: Ax0Ñ 2. Dokaˇzte:
pDyqpy 0q
$ p@x1 , . . . , xn qA Ñ Ax ,...,x rt1 , . . . , tn s 1
n
ˇ sen´ı: Pro kaˇzd´e i 1, 2, . . . , n plat´ı Reˇ (*)
$ p@xi , xi
1 , . . . , xn
2
qA Ñ A
Toto tvrzen´ı dok´aˇzeme pomoc´ı indukce:
$ p@xi , xi 1 , . . . , xn qA Ñ p@xi $ p@xi 1 , . . . , xn qA Ñ A $ p@xi , xi 1 , . . . , xn qA Ñ A
(7) (8) (9)
1 , . . . , xn
qA
(AxS) (indukˇcn´ı pˇredpoklad) (PTI na (1) a (2))
Dokazovan´e tvrzen´ı plyne z (*) pomoc´ı vˇety o instanc´ıch:
$(p@x1 , . . . , xn qA Ñ A)x ,...,x rt1 , . . . , tn s $p@x1 , . . . , xn qA Ñ Ax ,...,x rt1 , . . . , tn s
(1)
1
(2)
1
(VI na (*))
n
n
(viz vysvˇetlen´ı n´ıˇze)
Pˇrechod od (1) k (2) je moˇzn´ y proto, ˇze premisa implikace v (1) neobsahuje ˇz´adnou z promˇenn´ ych x1 , . . . , xn volnˇe - vych´az´ıme tedy z definice substituovatelnosti termu do formule. Pˇ r´ıpisek: Zad´an´ı je vˇeta o substituci, jak je uvedeno v u ´vodn´ı tabulce. 3. Dokaˇzte:
M ( Ax1 ,...,xn rt1 , . . . , tn sres ô M ( Are1 s,
kde e1 px1 {t1 res, . . . , xn {tn resq.
ˇ sen´ı: Indukc´ı podle sloˇzitosti A. Pro A atomickou a spojky Reˇ krok pro A tvaru p@xqB:
ô ô ô ô ô
M ( Ax1 ,...,xn rt1 , . . . , tn sres M ( Bx1 ,...,xn rt1 , . . . , tn srepx{aqs pro kaˇzd´e a P M M ( B repx{aq1 s pro kaˇzd´e a P M M ( B re1 px{aqs pro kaˇzd´e a P M M ( p@xqB re1 s M ( Are1 s
a
Ñ to je jasn´e. Indukˇcn´ı
(definice splˇ nov´an´ı) (indukˇcn´ı pˇredpoklad) (viz vysvˇetlen´ı n´ıˇze) (definice splˇ nov´an´ı) (pˇrepis)
Tˇret´ı ekvivalence plyne z e1 px{aq epx{aq1 , coˇz plat´ı v d˚ usledku toho, ˇze x nen´ı v ti d´ıky substituovatelnosti1 ti za xi do A. Pˇ r´ıpisek: Kompletn´ı d˚ ukaz je moˇzno naj´ıt ve skriptech Jana Pelce, str. 28, lemma 8.12
F.1.0.2 Vlastnosti instanc´ı - protipˇ r´ıklady 1.
& p@xqA Ñ Atx , je-li Atx v´ ysledek nahrazen´ı kaˇzd´eho voln´eho v´ yskytu x v A termem t. ˇ sen´ı: Podle vˇety o u Reˇ ´plnosti predik´atov´e logiky staˇc´ı: xM, P M y * p@xqA Ñ Atx , kde:
pDyqP px, yq M ta, bu P M txa, by, xb, ayu vol´ıme t y
• A je • • •
Pˇ r´ıpisek: Atx nen´ı to sam´e, co substituovatelnost termu t za promˇennou x do formule A. 1 Protoˇ ze
A je tvaru
p@xqB. 3
2. kde e1
M ( Atx res ø M ( Are1 s,
epx{tresq a Atx je v´ysledek nahrazen´ı kaˇzd´eho voln´eho v´yskytu x v A termem t.
ˇ sen´ı: Protipˇr´ıklad je n´asleduj´ıc´ı: Reˇ • A bud’ pDy qP px, y q • t bud’ y; tedy Atx je
pDyqP py, yq
ta, bu • P txa, by, xb, ayu Mˇejme epxq a, epy q b a e1 pxq b e1 py q. Pak xM, P M y ( Are1 s, ale xM, P M y * Ayx res. • M
M
3.
$ Ax rts ÷ T $ A, je jist´a teorie v jazyce xM, P, cy - P je un´arn´ı predik´at, c konstanta. T
kde T
ˇ sen´ı: Protipˇr´ıklad je n´asleduj´ıc´ı: Reˇ • Bud’ T tP pcqu • Bud’ M xM, P M , cM y ( T , kde P M • Bud’ A P pxq
tcM u
• Bud’ t c
Pak M ( P pcq, ale M * P pxq
F.1.1 Varianta F.1.1.1 ˇ ık´ame, ˇze formule A1 je variantou formule A, jestliˇze A1 vznikne z A postupn´ ym Definice: R´ nahrazen´ım podformul´ı tvaru pQxqB formulemi pQy qBx ry s, kde y nen´ı voln´a promˇenn´a ve formuli pQxqB. Bud’te x, y, z, u r˚ uzn´e promˇenn´e, Q kvantifik´ator. Odpovˇezte a uved’te d˚ uvod, zda plat´ı: B je varianta A. 1. A pQxqpx y _ pDz qpz
y
& z
xqq, B pQzqpz y _ pDzqpz y
& z
zqq
ˇ sen´ı: Ne. z nen´ı substitovateln´e za x do A. Reˇ Pˇ r´ıpisek: Protoˇze existuje podformule A ve tvaru pDz qC takov´a, ˇze x m´a v C voln´ y v´ yskyt.
2. A pQxqpx y _ p@z qpz
y
& z
xqq, B pQyqpy y _ p@zqpz y
& z
yqq
& z
xqq, B pQuqpu y _ pDzqpz y
& z
uqq
ˇ sen´ı: Ne. y je voln´a v A. Reˇ 3. A pQxqpx y _ pDz qpz
y
ˇ sen´ı: Ano. u nen´ı voln´a v A a je substituovateln´a za x do A. Reˇ
4
F.1.2 Dokazateln´ e, vyvratiteln´ e a nez´ avisl´ e formule F.1.2.1 Dokazatelnost jednoduch´ ych formul´ı Bud’te P, R r˚ uzn´e un´arn´ı predik´atov´e symboly. Odpovˇezte, zda uveden´a formule je: dokazateln´a (D) / vyvratiteln´a (V) / nez´avisl´a (NZ) a uved’te d˚ uvod. 1. P ˇ sen´ı: NZ. x1, 0y ( Reˇ
P, x1, 1y ( P
x1, 0y zde znaˇc´ı model jehoˇz interpretace (realizace) je: 1 t0u . . . jednoprvkov´a mnoˇzina, ˇze je jej´ım prvkem zrovna nula nen´ı pˇr´ıliˇs
Pˇ r´ıpisek:
• M podstatn´e • PM 2. P
ÑR
H
ˇ sen´ı: NZ. Reˇ • x2, 0, 2y ( P
3.
Ñ R . . . Premisa (P) je vˇzdy nesplnˇen´a. • x2, 2, 0y ( pP Ñ Rq . . . Premisa (P) je vˇzdy splnˇen´a, z´avˇer (R) je vˇsak vˇzdy nesplˇ nen. Pˇ r´ıpisek: x2, 0, 2y zde znaˇc´ı model jehoˇz interpretace (realizace) je: • M 2 t0, 1u • PM H • RM tt0u, t1uu P Ñ pR Ñ P q ˇ sen´ı: D. Je to tautologie (instance axiomu A1). Reˇ
4.
pDxqP pxq ˇ sen´ı: NZ. Reˇ • x1, 0y (
5.
pDxqP • x1, 1y ( pDxqP P pxq _ pDxq P pxq ˇ sen´ı: D. Formule je logicky ekvivalentn´ı s Reˇ
p@xqP Ñ P , coˇz je axiom substituce.
Pˇ r´ıpisek: (1) (2)
ô
P pxq _ pDxq P pxq P pxq Ñ pDxq P pxq
(zkratky)
Formule (2) nen´ı nic jin´eho neˇz instance ”du´aln´ı verze”axiomu specifikace (viz tabulka v prvn´ı kapitole).
5
F.1.2.2 Nez´ avisl´ e formule v modelu 1. Bud’ A formule P Ñ p@xqP , kde P je un´arn´ı relaˇcn´ı symbol. V pr´avˇe kter´ ych modelech2 M xM, P y, neplat´ı A ani A? ˇ sen´ı: Pr´avˇe, kdyˇz 0 P M Reˇ
2.
M. Pˇ r´ıpisek: Pokud bude splnˇeno 0 P M M , pak pro danou realizaci jazyka (pojem model mi zde obsahovˇe nesed´ı) budou vˇzdy existovat ohodnocen´ı e a e1 takov´a, ˇze xM, P M y ( Ares ale xM, P M y * Are1 s. Bud’ A formule x c, kde c je konstantn´ı symbol. V pr´avˇe kter´ ych modelech xM, cM y, neplat´ı A ani
A?
ˇ sen´ı: Pr´avˇe kdyˇz |M | ¡ 1. Reˇ Pˇ r´ıpisek: Pokud bude |M | ¡ 1, pak bude existovat pr´avˇe jedno ohodnocen´ı e, pro kter´e bude platit epxq cM , pro jedno ohodnocen´ı bude tedy formule splnˇena pro zb´ yvaj´ıc´ı ne, tedy formule je nez´avisl´a. 3. Bud’ A formule P Ñ p@xqR, kde P, R jsou r˚ uzn´e un´arn´ı predik´atov´e symboly. V pr´avˇe kter´ ych modelech M xM, P M , RM y, neplat´ı A ani A? ˇ sen´ı: Pr´avˇe, kdyˇz 0 P M Reˇ
M RM .
Pˇ r´ıpisek: Zˇrejmˇe plat´ı: M • M * A ô looomooon PM 0 a R M, loooomoooon #1
• M*
#2
M A ô loooomoooon P M nebo R M. loooomoooon M
#3
#4
Aby byla formule A nez´avisl´a, mus´ıme spojit podm´ınky #1, #2 a #3 (viz 3 ).
F.1.3 Protipˇ r´ıklady F.1.3.1 K vˇ etˇ e o dedukci a o d˚ ukazu sporem 1.
T, A $ B
kde T
÷ T $ A Ñ B,
tpDxqP u je teorie v jazyce xP y s un´arn´ım predik´atem P, A je P pxq a B vhodn´e.
ˇ sen´ı: Reˇ
p@xqP pxq. Je dokazateln´e T, A $ B: T, P pxq $ P pxq (1) (2) T, P pxq $ p@xqP pxq • Bud’ B formule
Plat´ı vˇsak T
(PG)
& A Ñ B, nebot’ xM, P M y * P pxq Ñ p@xqP pxq, kdyˇz 0 P M M .
2 Pouˇ zil bych radˇ eji pojem interpretace jazyka, jelikoˇ z model je definov´ an jako interpretace jazyka L, pˇri kter´ e je formule pravdiv´ a. 3 Podm´ ınky #1, #2 a #4 se vyluˇ cuj´ı, pro jich nelze pouˇ z´ıt.
6
Pˇ r´ıpisek: V dokumentu [1], 3.44 je uvedeno kter´e jin´e formule lze pouˇz´ıt pro dok´az´an´ı naˇseho tvrzen´ı. Jsou to formule, jejichˇz d˚ ukaz z´avis´ı na pouˇz´ıt´ı pravidla generalizace (coˇz se d´ale napˇr. vyuˇzije pro pouˇzit´ı pravidla zaveden´ı @). 2. T, A je sporn´a teorie
kde T
÷ T $ A,
tpDxqP u je teorie v jazyce xP y s un´arn´ım predik´atem P
a A je vhodn´e.
ˇ sen´ı: Reˇ • Bud’ A rovno P . T, A je sporn´a, nebot’ dokazuje
pDxqP
&
pDxqP :
$ P (pˇredpoklad) $ p@xq P (PG) $ pDxqP (pˇredpoklad) $ pDxqP & p@xq P (Pravidlo konjunkce na (2) a (3)) T, P $ pDxqP & pDxqP (Prenex (i) + VE) D´ıky tautologii pB & B q Ñ C dost´av´ame T, A $ C. Na druh´e stranˇe T & A, nebot’ pDxqP & P , o ˇcemˇz svˇedˇc´ı model x2, 1y * P . (1) (2) (3) (4) (5)
T, T, T, T,
P P P P
F.1.4 Tvrzen´ı o kvantifik´ atorech F.1.4.1 Vyt´ yk´ an´ı kvantifik´ ator˚ u 1 Necht’ Q znaˇc´ı kvantifik´ator, Q kvantifik´ator ”du´aln´ı”ke Q. 1.
p@xqpA Ñ B q Ø pA Ñ p@xqB q, nem´a-li x voln´y v´yskyt v A. ˇ sen´ı: Reˇ ”Ñ” Instance axiomu pˇreskoku. ”Д Dokazujeme takto:
$pA Ñ p@xqB q Ñ ppp@xqB Ñ B q Ñ pA Ñ B qq (tautologie PTI) (2) $pp@xqB Ñ B q Ñ ppA Ñ p@xqB q Ñ pA Ñ B qq (vˇeta o z´amˇenˇe pˇredpoklad˚ u3 ) (3) $p@xqB Ñ B q (AxS) (4) $pA Ñ p@xqB q Ñ pA Ñ B q ((2), (3) MP) (5) $pA Ñ p@xqB q Ñ p@xqpA Ñ B q (PZ@) pDxqpA Ñ B q Ñ pA Ñ pDxqB q, nem´a-li x voln´y v´yskyt v A. (1)
2.
ˇ sen´ı: Reˇ ”Ñ” Dokazujeme: (1) (2) (3) (4) (5) 3 viz
$pA Ñ B q Ñ ppB Ñ pDxqB q Ñ pA Ñ pDxqB qq $pB Ñ pDxqB q Ñ ppA Ñ B q Ñ pA Ñ pDxqB qq $B Ñ pDxqB $pA Ñ B q Ñ pA Ñ pDxqB q $pDxqpA Ñ B q Ñ pA Ñ pDxqB q
skripta Jana Pelce, vˇ eta 3.14
7
(tautologie PTI) (vˇeta o z´amˇenˇe pˇredpoklad˚ u3 ) (”du´aln´ı”verze AxS) ((2), (3) MP) (PZD)
3. pA Ñ pDxqB q Ñ pDxqpA Ñ B q ˇ sen´ı: Reˇ ”Ñ” Dokazujeme: (1) (2) (3) (4) (5) (6) (7) (8)
$pA Ñ B q Ñ pDxqppA Ñ B q $ A Ñ pA Ñ B q $ A Ñ pDxqpA Ñ B q $B Ñ pA Ñ B q $pDxqB Ñ pDxqpA Ñ B q $p A _ pDxqB q Ñ pDxqpA Ñ B q $p A _ pDxqB q Ø pA Ñ pDxqB q $pA Ñ pDxqB q Ñ pDxqpA Ñ B q
(”du´aln´ı”verze AxS) (V2) ((1), (2) PTI) (A1) (DK4 ) ((3), (5) PR) (zkratky) (VE na (6) se (7))
4. pQxqpA Ñ B q Ø ppQ1 xqA Ñ B q, nem´a-li x voln´ y v´ yskyt v B. N´ avod: Uˇzijte tvrzen´ı o vyt´ yk´ an´ı kvantifik´ator˚ u z konsekventu implikace. ˇ sen´ı: Reˇ
$ pQxqpA Ñ B q Ø pQxqp B Ñ Aq Ø p B Ñ pQxq Aq Ø p pQxq A Ñ B q Ø ppQ1 xqA Ñ B q
(1) (2) (3) (4)
(V5) (Prenex (ii)) (V5 a V3,V4) (vztah mezi
5. pQxqpA ♦ B q Ø pA ♦ pQxqB q, nem´a-li x voln´ y v´ yskyt v A, ♦ je
@ a D)
_ nebo &.
N´ avod: Uˇzijte tvrzen´ı o vyt´ yk´ an´ı kvantifik´ator˚ u z konsekventu implikace. ˇ sen´ı: Reˇ (a) Q je @, ♦ je (1) (2) (3)
_. Jsou dokazateln´e ekvivalence: $ p@xqpA _ B q Ø p@xqp A Ñ B q Ø p A Ñ p@xqB q Ø pA _ p@xqB q
(b) Ostatn´ı vztahy plynou z (a) uˇzit´ım $ ganov´ ych pravidel a vˇety o ekvivalenci.
pDxqC Ø p@xq
(zkratky) (Prenex (ii)) (zkratky) C,
$
C
F.1.4.2 Vyt´ yk´ an´ı kvantifik´ ator˚ u - protipˇ r´ıklady 1 Necht’ Q znaˇc´ı kvantifik´ator, Q kvantifik´ator ”du´aln´ı”ke Q. 1.
& p@xqpA Ñ B q Ñ pA Ñ p@xqB q. ˇ sen´ı: Reˇ • Bud’ M xM, P M , RM y, kde P, R jsou un´arn´ı predik´atov´e symboly. • Bud’ a P P .
4 Distribuce
D
Kvantifik´ ator˚ u, Jan Pelc, lemma 9.9; d˚ usledek PZ
8
Ø
C, deMor-
• Necht’ plat´ı 0 P M
2.
RM M . Pak M ( p@xqpP Ñ Rq, M * pP Ñ p@xqRqras. Tedy M * p@xqpP Ñ Rq Ñ pP Ñ p@xqRq. & pA Ñ p@xqB q Ñ p@xqpA Ñ B q. ˇ sen´ı: Reˇ • Bud’ M xM, P M , RM y, kde P, R jsou un´arn´ı predik´atov´e symboly. • Bud’ a P M zP M . • Necht’ plat´ı 0 P M RM . Pak • M ( pP
Ñ p@xqRqras . . . jelikoˇz nen´ı splnˇena premisa Ñ Rq Tedy M * pP Ñ p@xqRq Ñ p@xqpP Ñ Rq. & pDxqpA Ñ B q Ñ pA Ñ pDxqB q. • M * p@xqpP
3.
ˇ sen´ı: Reˇ • Bud’ M xM, P M , RM y, kde P, R jsou un´arn´ı predik´atov´e symboly. • Bud’ a P P M . • Necht’ plat´ı 0 P M M, R 0. Pak • M ( pDxqpP
Ñ Rq . . . protoˇze existuje a P M zP M • M * pP Ñ pDxqRqras . . . protoˇze je a P P M Tedy M * pDxqpP Ñ Rq Ñ pP Ñ pDxqRq. F.1.4.3 Vlastnosti kvantifik´ ator˚ u 1. Dokaˇzte syntakticky, pˇriˇcemˇz Q znaˇc´ı kvantifik´ator:
$ pQxqpA
& B q Ñ pQxqA & pQxqB
ˇ sen´ı: Necht’ vˇsechny voln´e promˇenn´e formul´ı A, B kromˇe x jsou mezi x1 , . . . , xn , necht’ Reˇ c1 , . . . , cn jsou nov´e konstantn´ı symboly, A1 je Ax1 ,...,xn rc1 , . . . , cn s, B 1 je Bx1 ,...,xn rc1 , . . . , cn s. (1) (2) (3) (4) (5) (6) (7) (8) (9)
pQxqpA1 pQxqpA1 pQxqpA1
& & &
$pA1 & B 1 q Ñ A1 $pA1 & B 1 q Ñ B 1 $pQxqpA1 & B 1 q Ñ pQxqA1 $pQxqpA1 & B 1 q Ñ pQxqB 1 B 1 q $pQxqA1 B 1 q $pQxqB 1 B 1 q $pQxqA1 & pQxqB 1 $pQxqpA1 & B 1 q Ñ pQxqA1 & pQxqB 1 $pQxqpA & B q Ñ pQxqA & pQxqB
2. Dokaˇzte syntakticky, pˇriˇcemˇz Q znaˇc´ı kvantifik´ator:
$ p@xqA
&
p@xqB Ñ p@xqpA 9
& Bq
(PK (tautologie)) (PK (tautologie)) (PDQ na (1)) (PDQ na (2)) ((3) VD) ((4) VD) (PK na (5), (6)) ((7) VD) ((8) VK)
ˇ sen´ı: Necht’ vˇsechny voln´e promˇenn´e formul´ı A, B kromˇe x jsou mezi x1 , . . . , xn , necht’ Reˇ c1 , . . . , cn jsou nov´e konstantn´ı symboly, A1 je Ax1 ,...,xn rc1 , . . . , cn s, B 1 je Bx1 ,...,xn rc1 , . . . , cn s. (1) (2) (3) (4) (5) (6)
p@xqA1 p@xqA1 p@xqA1 p@xqA1
& & & &
p@xqB 1 $A1 p@xqB 1 $B 1 p@xqB 1 $A1 & B 1 p@xqB 1 $p@xqpA1 & B 1 q $p@xqA1 & p@xqB 1 Ñ p@xqpA1 & B 1 q $p@xqA & p@xqB Ñ p@xqpA & B q
(AxS + MP) (AxS + MP) (PK na (1) a (2)) (PG) (VD) (VK)
3. Dokaˇzte syntakticky:
N´ avod:
$ p@xqpA & B q Ø p@xqA & p@xqB, $ pDxqpA _ B q Ø pDxqA _ pDxqB i) $ pQxqpA & B q Ñ pQxqA & pQxqB, ii) $ p@xqA & p@xqB Ñ p@xqpA
& Bq
ˇ sen´ı: Reˇ (a) Prvn´ı formule: (1) (2) (3)
$p@xqpA & B q Ñ p@xqA & p@xqB $p@xqA & p@xqB Ñ p@xqpA & B q $p@xqpA & B q Ø p@xqA & p@xqB
(pˇr´ıklad 1., tj. hint i) ) (pˇr´ıklad 2., tj. hint ii) ) (PK (1) a (2))
(b) Druh´a formule plyne z prvn´ı uˇzit´ım (Negace Implikace (NI)): T $ C Ñ C 1 ô T $ C 1 Ñ C (coˇz plyne z PTT) a VE. (1) (2) (3) (4) (5) (6)
$ p@xqpA $ p@xqpA
& Bq Ø & Bq Ø
pp@xqA & p@xqB q p@xq p A _ B q Ø pDxqp A _ B q $ pp@xqA & p@xqB q Ø p@xqA _ p@xqB Ø pDxq A _ pDxq B $ pDxqp A _ B q Ø pDxq A _ pDxq B
(NI) (deMorgan) (zkratky) (deMorgan) (zkratky)
Formule (6) plyne z toho, ˇze jsme dok´azali ekvivalentn´ımi u ´pravami obˇe strany formule (6) z jiˇz dok´azan´eho tvrzen´ı. Formuli (6) si nav´ıc m˚ uˇzeme pozmˇenit5 , tak ˇze podformule tvaru B zamˇen´ıme za B, ˇc´ımˇz dostaneme ˇz´ad´an´e. 4. Dokaˇzte syntakticky:
N´ avod:
$ pDxqpA & B q Ñ pDxqA & pDxqB, $ p@xqA _ p@xqB Ñ p@xqpA _ B q i) $ pQxqpA & B q Ñ pQxqA & pQxqB, ii) $ p@xqA & p@xqB Ñ p@xqpA
ˇ sen´ı: Reˇ (a) Prvn´ı formule: Pˇr´ımo plyne z hintu i) (b) Druh´a formule plyne z prvn´ı uˇzit´ım (Negace Implikace (NI)): T $ C Ñ C 1 ô T $ C 1 Ñ C (coˇz plyne z PTT) a VE. 5. Dokaˇzte syntakticky:
$ p@xqp@yqA Ø p@yqp@xqA, $ pDxqpDyqA Ø pDyqpDxqA
ˇ sen´ı: Reˇ 5 T´ ım
vlastnˇ e vytv´ aˇr´ıme instanci dan´ e tautologie.
10
& Bq
(a) Prvn´ı formule:
$p@xqp@yqA Ñ p@yqA $p@yqA Ñ A $p@xqp@yqA Ñ A $p@xqp@yqA Ñ p@xqA $p@xqp@yqA Ñ p@yqp@xqA
(1) (2) (3) (4) (5)
(AxS) (AxS) (PTI na (1) a (2)) (PZ@) (PZ@)
Ze symetrie plyne druh´a implikace. Pomoc´ı PK pak plyne tvrzen´ı. (b) Druh´a formule plyne z prvn´ı formule uˇzit´ım NI a VE: (1) (2) (3) (4)
$ p@xqp@yqA Ø p@yqp@xqA ô ô ô ô
$ p@xqp@yqA Ø p@yqp@xqA $ pDxq p@yqA Ø pDyq p@xqA $ pDxqpDyq A Ø pDyqpDxq A $ pDxqpDyqA Ø pDyqpDxqA
(NI) (Prenex (i)) (Prenex (i))
V kroku (4) jsme provedli stejnou u ´vahu jako v pˇr´ıkladu 3. 6. Dokaˇzte syntakticky, pˇriˇcemˇz Q znaˇc´ı kvantifik´ator: $ pDxqp@yqA Ñ p@yqpDxqA, $ pQxqA Ø A, nen´ı-li x voln´a v A. ˇ sen´ı: Reˇ (a) Prvn´ı formule:
$A Ñ pDxqA $p@yqA Ñ p@yqpDxqA $pDxqp@yqA Ñ p@yqpDxqA
(1) (2) (3)
(VS) (PD@) (PZD)
(b) Druh´a formule. Q bud’ @.
$p@xqA Ñ A $A Ñ p@xqA $p@xqA Ø A
(1) (2) (3) Pro Q rovno
(AxS) (PZ@) (PK na (1) a (2))
D plyne tvrzen´ı z dok´azan´eho uˇzit´ım NI a VE.
7. Dokaˇzte:
Ax rts Ø p@xqpx t Ñ Aq,
nen´ı-li x obsaˇzeno v termu t. ˇ sen´ı: Reˇ ” Ñ” (1) (2) (3) (4)
6 Pˇ redpokl´ ad´ a
$p@xqpx t Ñ Aq Ñ pt t Ñ Ax rtsq $t t Ñ pp@xqpx t Ñ Aq Ñ Ax rtsq $t t $p@xqpx t Ñ Aq Ñ Ax rts se substituovatelnost t za x do A
11
(AxS6 ) (Z´amˇena pˇredpoklad˚ u) (Axiom identity) (MP)
” Д (1) (2) (3) (4)
$t1 s1 Ñ t2 s2 Ñ Ñ tn sn Ñ pArt1 , . . . , tn s Ø Ars1 , . . . , sn sq $x t Ñ pA Ø Ax rtsq $Ax rts Ñ px t Ñ Aq $Ax rts Ñ p@xqpx t Ñ Aq
(VR7 ) (z (1)) (ZP) (PZ@)
V kroku (4) jsme vyuˇzili pˇredpokladu, ze kter´eho plyne, ˇze x nen´ı voln´a v Ax rts. 8. Dokaˇzte:
Ax rts Ø pDxqpx t & Aq,
nen´ı-li x obsaˇzeno v termu t. ˇ sen´ı: Reˇ ”Ñ” PT bude znaˇcit pˇredpoklad tvrzen´ı.
$pt t & Ax rtsq Ñ pDxqpx t $t t $Ax rts Ñ pDxqpx t & Aq
(1) (2) (3)
& Aq
(AxS a PT) (Axiom identity) (z PT a (2))
” Д (1) (2) (3) (4)
$t1 s1 Ñ t2 s2 Ñ Ñ tn sn Ñ pArt1 , . . . , tn s Ø Ars1 , . . . , sn sq $x t Ñ pA Ø Ax rtsq $px t & Aq Ñ Ax rts $pDxqpx t & Aq Ñ Ax rts
(VR) (z (1)) (z (2)) (PZD)
V kroku (4) jsme vyuˇzili pˇredpokladu, ze kter´eho plyne, ˇze x nen´ı voln´a v Ax rts.
Pˇ r´ıklady odjinud 1. Dokaˇzte syntakticky v predik´atov´e logice:
pDxqpDyqpP pxq _
P py qq
ˇ sen´ı: Reˇ (1) (2) (3) (4) (5) (6) (7) (8) (9)
$p@xqP pxq Ñ P pxqx rys p@xqP pxq $P pxqx rys $P pxqx rys Ñ pDxqP pxq $p@xqP pxq Ñ pDxqP pxq $pDxqP pxq Ñ pDyqP pxqx rys $p@xqP pxq Ñ pDyqP pyq $pDxq(P pxq Ñ pDyqP pyq) $pDxqpDyq(P pxq Ñ P pyq) $pDxqpDyq( P pxq _ P pyq)
(AxS) (VD) (PS) ((2),(3) MP, VD) (VV) ((4) VD + (5) MP, VD) (Prenex (iii)) (Prenex (ii)) (zkratky)
Reference ˇ ep´anek. [1] DrSc. prof. RNDr. Petr Stˇ (AIL023). Praha, 2000. 7 Vˇ eta
Skripta pro pˇredn´ aˇsku V´yrokov´ a a predik´ atov´ a logika
o rovnosti
12
