Jazyk prvnÍho UÁdu Jazyk obsahuje (i) PromEnnÉ x, y, z , x1 , x2 , 4 y, y, 4 neomezenE mnoho (ii) Funk7nÍ symboly f , g , h, 4 , f 1 , f 2 4 kaŞdÝ mÁ svou 7etnost (po7et argument]) n 0. (iii)PredikÁtovÉ symboly p, q, r , 4 p1 , p2 , 4 kaŞdÝ mÁ svou
PredikÁtovÁ logika
7etnost n 0. (iv) Symboly pro logickÉ spojky negace, disjunkce, & konjunkce, implikace, ekvivalence. (v) Symboly pro kvantifikÁtory univerzÁlnÍ existen7nÍ.
1
2
Definice - Termy Termy a formule (i) KaŞdÁ promEnnÁ je term. jsou vÝrazy jazyka prvnÍho UÁdu, kterÉ majÍ sv]j vÝznam. (ii) Je-li f n-ÁrnÍ funk7nÍ symbol a vÝrazy termy, potom vÝraz
Termy popisujÍ (nEkterÁ) individua.
t1 , t 2 , 4 t n jsou
f (t1 , t 2 , 4 t n )
Formule jsou tvrzenÍmi o individuÍch.
je term.
Definujeme je induktivnE.
Termy jsou definovÁny kone7nÝm po7tem uŞitÍ pravidel (i) a (ii). Tedy jsou to kone7nÁ slova. 3
4
Formule.
PUÍklad.
(i) Je-li p n-ÁrnÍ predikÁtovÝ symbol, potom vÝraz p(t1 , t 2 , 4 t n ), kde t1 , t 2 , 4 t n jsou termy, je (atomickÁ) formule.
V jazyce aritmetiky jsou nÁsledujÍcÍ vÝrazy termy x
x 0
y S ( x)
y S ( S (0 ))
x y
S (0 ) S ( S (0 ))
(ii) Jsou-li vÝrazy A, B formule, potom vÝrazy A, ( A & B ), ( A B ), ( A B ), a ( A
Podle definice bychom mEli psÁt x
( x, 0 ) ( y, S ( x)) ( y, S ( S (0 ))) ( x, y ) ( S (0 ), S ( S (0 )))
B)
jsou takÉ formule.
ale u binÁrnÍch symbol] se pUidrŞujeme zavedenÉ praxe infixnÍho zÁpisu.
(iii) Je-li x promEnnÁ a A formule, potom vÝrazy ( x) A a ( x) A jsou formule.
5
6
Formule a podformule.
PUÍklady.
Formule
x e
e x
x e
x ( x)( y )( x y
e) e e
e
x e e x x e x e e e jsou atomickÉ. Vznikly podle pravidla (i) Formule
x
S ( x)
x x
S ( S 0) x
x
y
x S ( y)
( x)( y )( x y
vznikla z formulÍ x 0 K
( y )( x
S ( y ))
k|x
( y )(k y
(y | z
k | z )))
x)
x 0
(k | x
(x | y
(1)
e)
(x y
e)
(i )
( y )( x y ( x)( y )( x y
e) e)
(iii ) (iii )
(2)
TÍkÁme, Şe formule (2) jsou podformule formule (1). 7
8
Podtermy, podformule, volnÉ a vÁzanÉ promEnnÉ. (iii) TÍkÁme, Şe promEnnÁ x je volnÁ ve formuli A, mÁ-li tam volnÝ vÝskyt. PromEnnÁ x je vÁzanÁ v A, mÁ-li tam vÁzanÝ vÝskyt.
Nech[ t je term a A je formule. (i) Podslovo s termu t, kterÉ je samo termem nazveme podtermem termu t.
(iv) Formule A je otevUenÁ, pokud neobsahuje ŞÁdnou vÁzan ou promEnnou. A je uzavUenÁ, neobsahuje-li ŞÁdnou volnou promEnnou,
Podslovo B formule A, kterÉ je samo formulÍ nazveme podformulÍ formule A. (ii) DanÝ vÝskyt promEnnÉ x ve formuli A je vÁzanÝ, je-li sou7ÁstÍ nEjakÉ podformule tvaru ( x) B nebo ( x) B. NenÍ-li danÝ vÝskyt promEnnÉ x vÁzanÝ, UÍkÁme, Şe je volnÝ.
Je zUejmÉ, Şe otevUenÁ formule neobsahuje ŞÁdnÝ kvantifikÁtor zatÍm co uzavUenÁ formule vÁŞe kaŞdou promEnnou nEjakÝm kvantifikÁtorem .
9
10
SÉmantika predikÁtovÉ logiky PUÍklad. PromEnnÁ m]Şe bÝt v tÉŞe formuli sou7asnE volnÁ i vÁzanÁ.
( x)(( x e) ^ ^
x) ^
((e x) #
Interpretace jazyka je definovÁna mnoŞinovou (rela7nÍ) strukturou M kterÁ ke kaŞdÉmu symbolu jazyka a k mnoŞinE promEnnÝch pUiUadÍ mnoŞinu individuÍ. Rela7nÍ struktura M obsahuje
x) #
• neprÁzdnou mnoŞinu M pro individua. (x
z)
( x)( x
z)
• zobrazenÍ f M : M n • relaci 11
M pro n-ÁrnÍ funk7nÍ symbol f
pro kaŞdÝ n-ÁrnÍ predikÁt p 12
Interpretace term].
PUÍklady. a) M = (M = {a, b, c},
M
MEjme jazyk L a strukturu M, kterÁ ho interpretuje. Chceme kaŞdÉmu termu pUiUadit jeho hodnotu v domÉnE M struktury M.
{ a, b } )
je interpretacÍ jazyka L = { }, je to (orientovanÝ) graf se tUemi vrcholy a jednou hranou.
a) PromEnnÉ, v termech musÍme ohodnotit nejdUÍve. PouŞijeme zobrazenÍ e, kterÉ kaŞdÉ promEnnÉ x pUiUadÍ hodnotu e(x) z domÉny M. TakovÉmu zobrazenÍ UÍkÁme ohodnocenÍ promEnnÝch.
2
b) E = ({e}, e, E ), kde E : {e} {e} je interpretacÍ jazyka L = {e, } teorie grup. Je to jednoprvkovÁ grupa.
b) Interpretaci termu t pUi ohodnocenÍ e ozna7Íme t[e].
c) N = (N, 0N , S N , , ) , kde 0N je interpretace konstanty 0, S N interpretuje funkci nÁslednÍka a a , interpretujÍ operace sou7tu a sou7inu, je interpretacÍ jazyka aritmetiky.
Definujeme
t[e] = e(x)
t[ e ]
je-li t promEnnÁ x
f M (t1[e], 4 t n [e]), je-li t tvaru
f (t1 4 t n ). 13
Je zUejmÉ, Şe ohodnocenÍ promEnnÝch nenÍ absolutnÍ pojem, ale Şe zÁvisÍ na struktuUe M. MEli bychom proto psÁt t[e, M]. Je-li struktura M dÁna, pÍŁeme krÁtce t[e].
14
TarskÉho definice pravdy Nech[ L je jazyk, M jeho interpretace, e pravdivostnÍ ohodnocenÍ a A je formule jazyka L.
Interpretace termu pUi ohodnocenÍ e zÁvisÍ jenom na kone7nE hodnotÁch e.
(i) TÍkÁme, Şe A je splnEna v M pUi ohodnocenÍ e a pÍŁeme
Lemma.
M | A [e]
Jsou-li vŁechny promEnnÉ termu t mezi promEnnÝmi
jestliŞe (indukcÍ podle sloŞitosti A)
x1 , x2 , 4 xn
a e, e dvE ohodnocenÍ takovÁ, Şe e( xi ) e(xi ) pro i, 1 i n, potom t[e] = t[e]. D]kaz indukcÍ podle sloŞitosti termu t. 15
a) A je atomickÁ A Potom
M | A [e] ,
p (t1 , 4 t n ) , kde p nenÍ rovnost.
jestliŞe (t1[e], 4 t n [e])
pM 16
b) A je atomickÁ, A t1 c) A je tvaru
t2
a t1[e] t 2 [e].
B a M | B [e].
d) A je tvaru B
C
e) A je tvaru ( x) B a M | B [e( x / m)] pro kaŞdÉ m M.
a M | B [e] nebo M | C [e]. f) A je tvaru ( x) B a M | B [e( x / m)] pro nEjakÉ m M.
Je-li e ohodnocenÍ promEnnÝch, x je promEnnÁ a m je prvek z domÉny M, pozmEnEnÉ ohodnocenÍ e(x/m) definujeme e( x / m)( y )
m
je li y
x
e( y )
je li y
x
(ii) TÍkÁme, Şe formule A je pravdivÁ v M a pÍŁeme M| A
je-li A splnEna v M pUi kaŞdÉm ohodnocenÍ promEnnÝch.
17
18
• PodobnE jako u term], splnEnÍ formule pUi nEjakÉm ohodnocenÍ e zÁvisÍ jen na ohodnocenÍ e(x) kone7nE mnoha promEnnÝch. • z e) a f) vyplÝvÁ, Şe pokud mÁ promEnnÁ jen vÁzanÉ vÝskyty, potom splnEnÍ formule nezÁvisÍ na ohodnocenÍ tÉto formule. • Je-li formule uzavUenÁ, potom jejÍ splnEnÍ je pro vŁechna ohodnocenÍ stejnÉ. Sta7Í ovEUit zda je splnEna, 7i nesplnEna pUi jednom ohodnocenÍ.
TÍkÁme, Şe formule je validnÍ (platnÁ) nebo logicky pravdivÁ a pÍŁeme | A, jestliŞe je pravdivÁ pUi kaŞdÉ interpretaci danÉho jazyka. Tedy
| A
prÁvE kdyŞ
M| A
pro kaŞdou interpretaci M
•JinÝmi slovy, je-li uzavUenÁ formule splnEna pUi alespoO jednom ohodnocenÍ, je pravdivÁ.
19
20
Substituce term] do term] za promEnnÉ
Jsou-li x1 , 4 xn r]znÉ promEnnÉ a t , t1 , 4 t n jsou termy, potom symbolicky
PUÍklady.
t
(x
y) s
( x x) r
t x [ s ] (( x x)
( z y) q
w
t x1 , 4 , xn [t1 , 4 t n ]
y ) t y [r ] ( x ( z y ))
ozna7Íme vÝraz, kterÝ vznikne z t sou7asnÝm nahrazenÍm kaŞdÉho vÝskytu promEnnÉ xi termem ti pro i, i n.
t xy [ s, r ] (( x x) ( z y ))
rz [ s ] (( x x) y ) ry [q ] ( z w) rzy [t x [ s ], s x [q ]] ((( x x)
IndukcÍ podle sloŞitosti termu t se snadno ovEUÍ, tÍmto zp]sobem vznikne term.
y ) ( w w))
21
Substituce term] do formulÍ A sin 2 ( ) cos 2 ( ) 1 B
t
( / 3) s
q
2
a
2
2
( z )( x 2 u
x
y2 2
Jsou-li x1 , 4 xn r]znÉ promEnnÉ A formule a t1 , 4 t n jsou termy, potom symbolicky
z)
Ax1 , 4 , xn [t1 , 4 t n ]
1
A [t ] sin ( / 3) cos ( / 3) 1
Bxy [ s, u ] ( z )(( 2
2
y2 )
(1)
ozna7Íme vÝraz, kterÝ vznikne z A nahrazenÍm kaŞdÉho volnÉho vÝskytu promEnnÉ xi termem ti pro i, i n.
2
Bx [q ] ( z )(((a 2 ) 2
22
z) 2
x2 1 )
IndukcÍ podle sloŞitosti formule A se snadno ovEUÍ, tÍmto zp]sobem vznikne formule. TÉto formuli UÍkÁme instance formule A.
z)
23
24
Substituovatelnost termu do formule Co se stalo? Intuice: formule vypovÍdÁ o substituovanÝch termech „totÉŞ“, co vypovÍdÁ o promEnnÝch, za kterÉ bylo substituovÁno. VarovnÝ pUÍklad. MEjme formuli
A ( y )( x a term t
(y
y ))
(1)
( y 1). Potom instance Ax [t ] formule (1)
Ax [t ] ( y )( y 1
y
VolnÁ promEnnÁ x, za kterou bylo substituovÁno, byla v podformuli kvantifikÁtoru, kterÝ svÁzal promEnnou y v termu t. TÍkÁme, Şe term t je substituovatelnÝ do formule A za promEnnou x, jestliŞe pro kaŞdou promEnnou y vyskytujÍcÍ se v t ŞÁdnÁ podformule ( y ) B, ( y ) B formule A neobsahuje (z hlediska formule A ) volnÝ vÝskyt promEnnÉ x. Ve dvou pUÍpadech je snadnÉ substituovatelnost rozpoznat
y)
• je-li formule A otevUenÁ
vypovÍdÁ nEco jinÉho o termu (y + 1) neŞ vypovÍdala formule (1) o x.
• ŞÁdnÁ promEnnÁ substituovanÝch term] nenÍ vÁzanÁ v A. 25
26
A (x PUUÍklady.
A (x B
B
0)
( x)( y )( z )((u
(( x)( y )((( y u )
( x u ))
z)
(x
y ))
0)
( x)( y )( z )((u
(( x)( y )((( y u )
(u / v w) s
Au [t ] ( x 0 )
(v 2
( y )( x )( y
z2 ) r
( x u )))
d
( x)( y )( z )((u
z)
y2
x y e u Au [d ]
(v x )
( x)( y )( z )(((u / v w) z )
Ax [r ] ((v x) 0 )
( x u ))
(x
y ))
( y )( x )( y
( x u )))
b) nesubstitu ovatelnÉ
a) substituovatelnÉ termy
t
z)
(x
(x
Bu [d ]
y ))
y ))
PUitom
Ax [d ]
f
( z v w)
Au [e]
Bu [e] Ax [e]
Bu [ f ]
Ax [ f ]
Au [ f ]
Spo7Ítejte
Au [ s ]
Bu [t ]
jsou substituovatelnÉ.
Bu [ s ] 27
28
Lemma.
ºmluva. VÝraz Ax , y , z ,4[t , s, r 4] budeme pouŞÍvat jen kdyŞ jsou termy t , s, r 4 substituovatelnÉ za promEnnÉ x, y, z, ... do formule A.
L je jazyk, M jeho interpretace, x1 , 4 xn promEnnÉ, t , t1 , 4 t n termy a e je ohodnocenÍ promEnnÝch takovÉ, Şe ti [e] mi pro nEjakÉ individuum z M. Potom (i ) t x1 , x2 ,4, xn [t1 , t 2 , 4 , t n ][e] t[(e / m1 ), 4 , (e / mn )] (ii ) M | Ax1 , 4 , xn [t1 , 4 t n ][e] prÁvE kdyŞ
M | A[(e / m1 ), 4 (e / mn )]
29
30
Redukce jazyka. • Z logickÝch spojek pracujeme jen s negacÍ a implikacÍ. OstatnÍ spojky jsou z nich odvozenÉ.
FormÁlnÍ systÉm predikÁtovÉ logiky Dokazatelnost
• UniverzÁlnÍ kvantifikÁtor je zÁkladnÍ. •Existen7nÍ kvantifikÁtor je z nEj odvozen vztahem ( x) A
31
je zkratka za formuli
( x)
A.
32
Axiomy pro logickÉ spojky Je-li L jazyk 1. UÁdu a A, B, C jsou formule jazyka L, potom kaŞdÁ formule tvaru (A1)
A
(B
A)
(A
(B
C ))
( B
A)
[( A
(A
B)
(A
C )]
Vezmeme-li v Úvahu, Şe pravidlo modus ponens je takÉ odvozovacÍ pravidlo predikÁtovÉ logiky, dostÁvÁme Je-li A vEtou vÝrokovÉ logiky a A vznikne z A dosazenÍm libovolnÝch formulÍ predikÁtovÉ logiky za vÝrokovÉ promEnnÉ formule A, potom A je vEtou predikÁtovÉ logiky.
(A2) (A3)
B)
Axiomy predikÁtovÉ logiky pro spojky jsou „instancemi“ schemat (A1), (A2) a (A3), kterÉ vzniknou z axiom] vÝrokovÉ logiky dosazenÍm libovolnÝch formulÍ predikÁtovÉ logiky za vÝrokovÉ promEnnÉ.
je axiom. 33
34
Axiomy pro kvantifikÁtory.
OdvozovacÍ pravidla.
Schema specifikace. Je-li A formule, x promEnnÁ a t je term, potom formule ( x) A Ax [t ]
Modus ponens A
A
B
B
je axiom specifikace predikÁtovÉ logiky. Pravidlo generalizace Schema „pUeskoku“. Jsou-li A, B formule a je-li x promEnnÁ, kterÁ nemÁ volnÝ vÝskyt ve formuli A, potom formule ( x)( A
B)
(A
A ( x) A
pro libovolnou promEnnou x.
( x) B)
je axiom predikÁtovÉ logiky. 35
36
ZÁkladnÍ vEty o kvantifikÁtorech. UvedenÉ axiomy axiomy a odvozovacÍ pravidla tvoUÍ formÁlnÍ systÉm predikÁtovÉ logiky bez rovnosti.
.
Pravidlo zavedenÍ
NemÁ-li promEnnÁ x volnÝ vÝskyt ve formuli A a |
Pojem d]kazu, d]kazu z pUedpoklad] a vEt je stejnÝ jako ve vÝrokovÉ logice.
A
B potom |
A
( x) B
Pravidlo substituce, Pravidlo zavedenÍ . (i )
FormÁlnÍ systÉm predikÁtovÉ logiky s rovnostÍ vznikne z tohoto systÉmu rozŁÍUenÍm jazyka o predikÁtovÝ symbol rovnosti = a tUi schema axiom] rovnosti.
|
Ax [t ]
(ii) Je-li |
A
( x) A
B a x nenÍ volnÁ v B, potom
| ( x) A
takÉ
B.
37
38
V GentzenovE stylu m]Şeme tato pravidla zapsat A
B
x nenÍ volnÁ v A A ( x) B
Ax [t ]
A
B
( x) A
x nenÍ volnÁ v B ( x) A B
D]kazy.
Pravidlo zavedenÍ .
Pravidlo zavedenÍ
|
Pravidlo substituce
Pravidlo zavedenÍ .
A
39
pUedpoklad
B
| ( x)( A
B)
| ( x)( A
B)
| (A
.
( x) B)
generalizace
(A
( x) B)
schema pUeskoku MP
40
Pravidlo substituce. | ( x) A |
( x) A (+)+*
Instance formulÍ.
schema specifikace
Ax [t ] Ax [t ]
(v3), zkratka
Ax1 , 4 , xn [t1 , 4 t n ]
( x) A
|
Ax [t ]
(A3), MP
( x) A
je instance formule A . x1 , 4 xn jsou navzÁjem r]znÉ promEnnÉ, t1 , 4 t n jsou (substituovatelnÉ) termy.
Pravidlo zavedenÍ . |
A
pUedpoklad
B
(v5), MP
|
B
A
|
B
( x) A ( +)+ *
pravidlo
, (v4)
Instance vyjadUuje nEjakÝ zvlÁŁtnÍ pUÍpad tvrzenÍ formule. Do formule dosazujeme vsechny termy sou7asnE (paralelnE).
( x)
| ( x) A
B
( y )( x
(A3)
y)
( y )(1
y)
41
VarovnÝ pUÍklad.
A
x
VEta o instancÍch.
y
Axy [ s, t ]
42
t y
x
s
y
Je-li A’ instance A, potom platÍ
x
| Ax [ s ] Ay [t ]
y x
y x
(( Ax [ s ]) y [t ]) (( Ay [t ]) x [ s ])
x y
A implikuje |
A'
x
Je-li dokazatelnÁ formule A, potom je dokazatelnÁ kaŞdÁ jejÍ instance.
y
43
44
Je-li n > 1, nech[ z1 , 4 z n jsou novÉ promEnnÉ, kterÉ se nevyskytujÍ ani ve formuli A ani v termech t1 , 4 t n . Potom pUedpoklad
D]kaz. IndukcÍ podle po7tu substituovanÝch term]. A Ax1 , 4 , xn [t1 , 4 t n ]
Nech[
Je-li n = 1 a A Ax [t ] potom |
|
|
Ax1 [ z1 ]
generalizace
| ( x) A
| ( x) A
A
Ax [t ]
Ax [t ]
zÁklad indukce
| ( Ax1 [ z1 ]) x2 [ z 2 ]
pUedpoklad
A
|
Ax1 x2 [ z1 , z 2 ]
iterace
6
axiom specifikace
|
celkem
A , 4 , n [ z1 , 4 z n ] (x1+++x) +++ * B
MP 45
46
NynÍ Co nÁs pUekvapilo?
|
B
mezivÝsledek
|
Bz1 [t1 ]
zÁklad indukce
| ( Bz1 [t1 ]) z2 [t 2 ]
Bz1 z2 [t1 , t 2 ]
iterace
6 |
B , 4 , zn [t1 , 4 t n ] (x1++ +)+++ *
celkem
A[ t1 ,4,t n ]
Tedy
|
Je-li
A
x
0
potom
A
Kdyby
|
A
potom
|
A 3 0
t
3
Ax [t ] 3 0
A Ax1 , 4 , xn [t1 , 4 t n ]
Jak ukÁŞeme pozdEji formule dokazatelnÁ. 47
A
x
0
nenÍ 48
D]kaz. (i) Z axiomu specifikace pro libovolnou formuli C dostÁvÁme | ( x)C C ( C x [ x])
Specifikace a substituce. Je-li A formule, x1 , 4 xn promEnnÉ a termy, potom platÍ
t1 , 4 t n
iteracÍ
| ( xn ) A
A
| ( xn 1 )( xn ) A
(i ) (ii )
( x1 ), 4 , ( xn ) A Ax1 , 4 , xn [t1 , 4 t n ]
( xn ) A
6
Ax1 , 4 , xn [t1 , 4 t n ]
| ( x1 ), 4 , ( xn ) A
( x2 ), 4 , ( xn ) A
SloŞenÍm vŁech implikacÍ dostaneme | ( x1 ), 4 , ( xn ) A A
( x1 ), 4 , ( xn ) A
TvrzenÍ (i) je instancÍ tÉto formule. (ii) se dokÁŞe obdobnE iteracÍ Substitu7nÍho lemmatu. 49
50
UzÁvEr formule Cvi7enÍ.
Jsou-li x1 , 4 xn vŁechny promEnnÉ s volnÝm vÝskytem ve formuli A v nEjakÉm poUadÍ, potom formuli ( x1 ) 4 ( xn ) A
a) JestliŞe formule A neobsahuje volnE promEnnou x, potom platÍ | A ( x) A |
nazveme uzÁvErem formule A.
b)
Podle tÉto definice mÁ formule vÍce uzÁvEr], podle toho jakÉ zvolÍme poUadÍ promEnnÝch. PomocÍ lemmatu o specifikaci a pravidla zavedenÍ univerzÁlnÍho kvantifikÁtoru se dokÁŞe, Şe vŁechny uzÁvEry jsou ekvivalentnÍ.
A
( x) A
| ( x )( y ) A
( y )( x ) A
| ( x )( y ) A
( y )( x) A
c) Je-li ヾ permutace 7Ísel {1, …, n}, potom
51
| ( x1 )( x2 ) 4 ( xn ) A
( x
( 1)
)( x
(2)
)4( x
(n)
)A
| ( x1 )( x2 ) 4 ( xn ) A
( x
( 1)
)( x
(2)
)4( x
(n)
)A 52
VEta o uzÁvEru.
Lemma o distribuci kvantifikÁtor] Je-li | A
Je-li A uzÁvEr formule A, potom platÍ |
A prÁvE kdyŞ |
B , potom
| ( x) A
A
D]kaz.
( x) B a | ( x) A
( x) B
D]kaz. pUedpoklad
a) Je-li dokazatelnÉ A, potom pravidlem generalizace odvodÍme A .
|
| ( x) A
A
axiom specifikace
b) Je-li dokazatelnÉ A, pouŞijeme lemma o specifikaci a substituci a A odvodÍme pravidlem modus ponens.
| ( x) A
B
sloŞenÍ implikacÍ
| ( x) A
( x) B
zavedenÍ
53
VEta o ekvivalenci.
B1 4 |
B1
Bn
A
DruhÉ tvrzenÍ se dokazuje obdobnE pomocÍ substitu7nÍho 54 lemmatu a pravidla .
Postupujeme indukcÍ podle sloŞitosti formule A stejnE jako u obdobnÉ vEty vÝrokovÉho po7tu. NavÍc je jen pUÍpad, kdy A je tvaru ( x) B nebo ( x)B. Potom A je tvaru ( x) B nebo ( x)B. DostÁvÁme induk7nÍ pUedpoklad | B B zkratka ekvivalence | B B a | B B distribuce kvantifikator] | A A a | A A
Bn
potom
|
B
D]kaz.
Nech[ formule A vznikne z formule A nahrazenÍm nEkterÝch vÝskyt] podformulÍ B1 , 4, Bn po UadE formulemi B1, 4, Bn . Je-li |
A
A
Tedy 55
|
A
A. 56
TÍkÁme, Şe formule A je variantou formule A, jestliŞe A vznikne z A postupnÝm nahrazenÍm podformulÍ (Qx)B formulemi (Qy ) Bx [ y ], kde y nenÍ volnÁ ve formuli B a Q je univerzÁlnÍ nebo existen7nÍ kvantifikÁtor.
ZÁmEna vÁzanÝch promEnnÝch VÁzanÉ promEnnÉ se pouŞÍvajÍ v bEŞnÉ matematickÉ praxi. n 0
1 / n2
k 0
PUÍklad.
1/ k 2
A ( x)( y )( z )( x y z ) (++)++*
C < ( w)( x
y
w)
C
sin( )d 0
A1
sin( )d
( x)( y )( w)( x y w) (+++)+++*
C1 < ( v)( w)( x
v
w)
C1
0
A2
( x)( v)( w)( x v w) (++++)++++*
C2 < A
C2
Na obou stranÁch rovnosti je stejnÉ 7Íslo.
A ( u )( v )( w)(u
v
w)
57
58
D]kaz. Podle VEty o ekvivalenci sta7Í dokÁzat
VEta o variantÁch
| (Qx) B
za pUedpoklad] uvedenÝch v definici varianty. D]kaz . provedeme pro Q
Je-li A variantou formule A, potom
|
A
(Qy ) Bx [ y ]
A
a)
59
| ( x) B
Bx [ y ]
| ( x) B
( y ) Bx [ y ]
axiom specifikace pravidlo
60
VEta o dedukci
b) Ozna7me formuli Bx [ y ] symbolem C. Potom | ( y )C
C y [ x]
axiom specifikace
| ( y )C
( x)C y [ x]
pravidlo
Nech[ T je mnoŞina formulÍ, A je uzavUenÁ formule a B je libovolnÁ formule. Potom
T|
A
B
prÁvE kdyŞ T , A |
B
protoŞe promEnnÁ x nenÍ volnÁ v C a je substituovatelnÁ do C za y. Ale C y [x] je formule B. tÍm je dokÁzÁna i opa7nÁ implikace.
61
62
To znamenÁ, Şe Bi je tvaru ( x) B j . Z induk7nÍho pUedpokladu
D]kaz. Implikace zleva do prava se dokazuje zcela stejnE jako ve vÝrokovÉ logice. PUi d]kazu zprava do leva, mEjme d]kaz B1 , 4, Bn formule B z pUedpoklad] T, A. IndukcÍ podle dÉlky d]kazu dokÁŞeme T | B j pro vŁechna j. Ve vÝrokovÉ logice jsme rozebrali vŁechny pUÍpady aŞ na ten, kdy je formule Bi odvozena z formule B j , j i pravidlem generalizace.
T|
A
Bj
T|
A
( x) B j ()*
odvodÍme Bi
pravidlem zavedenÍ univerzÁlnÍho kvantifikÁtoru, protoŞe promEnnÁ x nenÍ volnÁ ve formuli A.
TÍm je d]kaz dokon7en. 63
64
Ve vEtE o dedukci je pUedpoklad uzavUenosti formule A pUÍliŁ omezujÍcÍ. Sta7ilo by, kdybychom vEdEli, Şe v d]kazu formule B z T, A nebylo pouŞito pravidlo generalizace na ŞÁdnou promEnnou, kterÁ je volnÁ v A. JinÝmi slovy, kdybychom vEdEli, Şe ŞÁdnÁ volnÁ promEnnÁ z A nebyla v d]kazu vyuŞita.
VEta o konstantÁch Nech[ T je mnoŞina formulÍ jazyka L a A je formule jazyka L. Nech[ x1 , 4 xn jsou promEnnÉ. Nech[ jazyk L vznikne rozŁÍUenÍm L o novÉ symboly c1 , 4 cn pro konstanty. Potom platÍ T|
To by znamenalo, Şe se takovÁ promEnnÁ chovala v pr]bEhu d]kazu jako konstanta. DokÁŞeme vEtu, Şe promEnnÉ lze za ur7itÝch pUedpoklad] nahradit konstantami a pozdEji se k tEmto promEnnÝm vrÁtit.
L
Ax1 , 4 , xn [c1 , 4 cn ] prÁvE kdyŞ T |
L
A
(PUidali jsme novÉ symboly pro konstanty ale nepUidali jsme o nich ŞÁdnÉ axiomy.)
65
D]kaz.
Nech[ pro kaŞdÉ i , formule Ai vznikne z formule Ai nahrazenÍm kaŞdÉho vÝskytu konstanty c j promEnnou y j .
Ozna7me A formuli Ax1 , 4 , xn [c1 , 4 cn ]. a) je-li T | instancÍ A.
L
A potom T |
L
66
A, protoŞe A je
b) je-li T | L A, nech[ A1 , 4, An je d]kaz A z T. Nech[ y1 , 4 yn jsou novÉ promEnnÉ, kterÉ se nevyskytujÍ v d]kazu A ani v A. D]kaz A1 , 4, An formule A pUemEnÍme na d]kaz A1 , 4, An formule Ax1 , 4 , xn [ y1 , 4 yn ]. Formule Ax1 , 4 , xn [c1 , 4 cn ] bude jejÍ instancÍ. 67
Snadno se pUesvEd7Íme, Şe A1 , 4, An je d]kazem formule Ax1 , 4 , xn [ y1 , 4 yn ] z T. Je-li Ai axiom predikÁtovÉ logiky, potom Ai je takÉ axiom predikÁtovÉ logiky stejnÉho druhu. Je-li Ai prvek T, potom Ai je Ai , protoŞe tato formule neobsahuje novÉ konstanty. Je-li Ai odvozena pravidlem modus ponens nebo generalizace, pak Ai je odvozena stejnÝm pravidlem.
68
Odtud
T|
L
Ax1 , 4 , xn [ y1 , 4 yn ]
a formule A je jejÍ instancÍ. TÍm je d]kaz vEty dokon7en. Konstanty a VEta o dedukci. Chceme-li dokÁzat implikaci A B z T a A mÁ volnÉ promEnnÉ x1 , 4 xn , rozŁÍUÍme jazyk o novÉ konstanty c1 , 4 cn .
D]sledek. Je-li A uzÁvEr formule A a T je mnoŞina formulÍ, potom T|
A, prÁvE kdyŞ T
{ A} je spornÁ
Sta7Í dokÁzat T , Ax1 , 4 , xn [c1 , 4 cn ] | Bx1 , 4 , xn [c1 , 4 cn ] a z VEty o dedukci a VEty o konstantÁch dostaneme T|
A
B. 69
Cvi7enÍ.
D]kaz. a) je-li T | Proto je T
70
A, z vEty o uzÁvEru dostÁvÁme T |
a) JestliŞe formule A neobsahuje promEnnou x volnE, potom
A.
{ A} spornÁ.
|
A
( x) A
|
A
( x) A
| ( x) A
b) Je-li T { A} je spornÁ, potom z nÍ lze dokÁzat libovolnou formuli, tedy i formuli A. Podle VEty o dedukci dostÁvÁme T | A A podle vEty (v7) vÝrokovÉ logiky T | A.
( x) A
b) a
71
| (Qx)(Qy ) A
(Qy )(Qx) A
c) | ( x)( y ) A
( y )( x) A
72
d) | ( x) A
f) ( x)( A
B)
| (Q1 x1 ) 4 (Qi 1 xi 1 )(Qi xi ) (Q i 1 xi 1 ) 4 (Q j xi ) 4 (Qn xn )
| ( x) A ( x)( A B ) | ( x) A
( x)( A
(Q1 x1 ) 4 (Qi 1 xi 1 ) (Q i 1 xi 1 ) 4 (Q j xi ) 4 (Qn xn )
B)
e) | ( x)( A & B )
(( x)( A) & ( x)( B ))
| (( x)( A) ( x)( B ))
( x)( A B )
| ( x)( A B )
(( x)( A) ( x)( B ))
| ( x)( A & B )
(( x)( A) & ( x)( B ))
73
74
Ve vÝrokovÉ logice jsme pomocÍ logickÝch spojek sestrojili konjunktivnÍ a disjunktivnÍ normÁlnÍ tvary formulÍ. V predikÁtovÉ logice sestrojÍme prenexnÍ normÁlnÍ tvary, kterÉ jsou v jistÉm smyslu jejich nadstavbou.
PrenexnÍ tvary formulÍ. Rovnost.
Budeme poŞadovat, aby pUi sestrojenÍ formule, byly kvantifikÁtory pouŞity aŞ na konec. To znamenÁ, Şe za UetEzcem kvantifikÁtor] bude nÁsledovat podformule sestrojenÁ jen z vÝrokovÝch spojek.Chceme-li, ta m]Şe bÝt v konjunktivnÍm nebo disjunktivnÍm tvaru.
1
PrenexnÍ tvar formule.
2
PUÍklady.
Formule A je v prenexnÍm tvaru, jeli
a ) ( x)( y )( z )( z
(x
b) ( x)(( x | p
1)
y ) / 2)
A (Q1 x1 )(Q2 x2 ) 4 (Qn xn ) B
kde
(i ) n 0 a pro kaŞdÉ i, 1 i
n je Qi
nebo
x
p je prvo7Íslo )
. c) ( F )( x)( y )(( x
(ii) B je otevUenÁ formule a kvantifikovanÉ promEnnÉ jsou navzÁjem r]znÉ.
y) F
(x F
d ) ( F )( G )( C )( D )( E )[( F : C
Formule B se nazÝvÁ otevUenÉ jÁdro A a posloupnost kvantifikacÍ pUed B se nazÝvÁ prefix.
y F ))
D)
((G : D
E)
(F C G : C 3
E ))] 4
Zna7enÍ. Je-li Q kvantifikÁtor, potom zna7Íme
VEta o prenexnÍch tvarech
je li Q
Q
Ke kaŞdÉ formuli A lze sestrojit formuli A, v prenexnÍm tvaru, kterÁ je s nÍ ekvivalentnÍ.
je li Q
Konstrukce ekvivalentnÍ formule v prenexnÍm tvaru postupuje indukcÍ podle sloŞitosti danÉ formule pomocÍ prenexnÍch operacÍ. Jejich Úkolem je vyvÉst kvantifikÁtory zevnitU podformulÍ ven. AŞ tento proces skon7Í, mÁme hledanou prenexnÍ formuli.
5
D]kaz.
Lemma. PrenexnÍ operace.
b) Je-li Q
a) v pUÍpadE potUeby nahradÍme nEjakou podformuli jejÍ variantou (ta je s nÍ ekvivalentnÍ).
(Qx ) B
c) | ( B
protoŞe B a B jsou ekvivalentnÍ c) Je-li Q
(Qx )( B
C ) , pokud x nenÍ vo ln Á v B.
(Q x)( B
C ) , pokud x nenÍ vo ln Á v C.
a promEnnÁ x nenÍ volnÁ v B, implikace
| ( x)( B d ) | ((Qx ) B
C)
e) | ((Qx ) B C ) Symbol
( x) B ( +)+ * ( x)
(Q x) B
(Qx )C )
dostÁvÁme ( x) B
|
Pro libovolnÉ formule B, C , kvantifikÁtor Q a promEnnou x platÍ b) |
6
(Qx )( B C ) , pokud x nenÍ vo ln Á v C.
(B
( x)C )
je axiom. Abychom dokÁzali obrÁcenou implikaci uŞijeme | (B
zastupuje konjunkci nebo disjunkci.
C)
( x)C )
[(( x)C C ) (+ +)++ *
(B
C )]
axiom specifikace
7
8
c) Je-li Q
Abychom dokÁzali tvrzenÍ pro Q zavedenÍ disjunkce plyne
a promEnnÁ x nenÍ volnÁ v B, implikace
| ( x)( B
C)
(B
| (B
( x)C )
je axiom. Abychom dokÁzali obrÁcenou implikaci uŞijeme | (B
( x)C )
[(( x)C C ) (+ +)++ *
(B
( x)C )
(B
C )]
MÁme tedy dokÁzat | ( B ( x)C )
( B ( x)C )
(1)
( x)( B
(2)
C)
C )]
Podle vEty o d]kazu rozborem pUÍpad] mÁme dokÁzat
axiom specifikace
| (B
( x)C )
uvEdomme si, Şe ze
MP
| ( x)C
( x)( B
C)
(3)
a Na konec pravidlem zavedenÍ dostaneme druhou implikaci protoŞe B neobsahuje x volnE.
|
B
( x)( B
(4)
C)
9
TÍm, Şe jsme dokÁzali (3) a (4), jsme podle vEty o d]kazu rozborem pUÍpad] dokÁzali (2) a podle (1) i jednu implikaci pUÍpadu c). DokÁŞeme opa7nou implikaci.
D]kaz (3). | C
(B
axiom (A1)
C)
| ( x) C
( x) ( B
C)
10
distribuce kvantifikÁtor]
| C | (B
substitu7nÍ lemma
xC C)
[(C
x C)
(B
D]kaz (4). | (B
C)
( x)( B
|
B
(B
|
B
( x)( B
C)
| (B
substitu7nÍ lemma
| ( x) ( B
(v2)
C) C)
C)
sloŞenÍ implikacÍ, MP 11
(B C)
( x)C ) (B
( x)C )
( x)C )]
sklÁdÁnÍ implikacÍ MP pravidlo
protoŞe B neobsahuje x volnE. TÍm je pUÍpad c) dokÁzÁn pro oba kvantifikÁtory. 12
d) Q PUi d]kazu tvrzenÍ c) pro existen7nÍ kvantifikÁtor, byla pouŞita vEta o d]kazu rozborem pUÍpad]. Ale ta byla dokÁzÁna jen ve vÝrokovÉ logice. V jejÍm d]kazu se pouŞÍvÁ vEta o dedukci, a to v obou smErech.
| (( x) B
C)
PUi pe7livÉm provedenÍ d]kazu c) je tUeba poŞadovat, aby
( C
( x) B)
( C
( x)
( C
( x) B)
( x)( C
B a ( x)C
( x)( B
byly uzavUenÉ formule. Tohoto poŞadavku lze dosÁhnou pouŞitÍm vEty o konstantÁch.
Pro Q
tautologie B)
B)
ekvivalence operace b) operace c)
C)
tautologie
se d]kaz dElÁ obdobnE.
13
14
D]kaz VEty se provÁdÍ indukcÍ podle sloŞitosti formule A. (i) je-li A atomickÁ, pak je v prenexnÍm tvaru a A je A. e) d]kaz prenexnÍ operace pro konjunkci a disjunkci se pUevede na pUedchozÍ operace a) - d) rozepsÁnÍm zkratek.
(ii) je-li A tvaru B a B je prenexnÍ tvar B, A se sestrojÍ pomocÍ operace b). (iii) je-li A tvaru B C a B,C jsou prenexnÍ tvary B a C, potom podle vEty o variantÁch (operace a)), pUejmenujeme vÁzanÉ promEnnÉ tak, aby ŞÁdnÁ volnÁ promEnnÁ B nebyla vÁzanÁ v C a naopak. PlatÍ
|
A
( B
C)
a A se sestrojÍ pomocÍ c) a d). 15
16
PUÍklady.
b) PrenexnÍ tvar v aritmetice.
Nech[ promEnnÁ x nenÍ volnÁ ve formuli B a promEnnÁ y se nevyskytuje v B ani v C. a) PrenexnÍ operace pro ekvivalenci (B
( x)C )
(B
( x)C ) & (( y )C x [ y ]
( x)( B
C ) & ( y )(C x [ y ]
( x)( y )[( B
C ) & (C x [ y ]
B)
ekvivalence, varianta
B)
operace e)
B)]
( x)( x
y)
( x)( x
0
( y )( y 0 ))
(o)
( x)( x
y)
( u )(u
0
( v)(v 0 ))
(a)
( x)( x
y)
( u )(u
0 ( v) (v 0 ))
(b)
( x)( x
y)
( u )( v)(u
( x)( u )( v)[( x
y)
0
(u
(v 0 )) 0
(v 0 ))]
(e) (c), (d)
PoUadÍ prenexnÍch operacÍ nenÍ deterministickÉ, toto je jinÝ prenexnÍ tvar formule (o).
operace c), d)
( u )( x)( v)[( x
y)
(u
0
17
(v 0 ))] 18
Schema axiom] identity.
PredikÁtovÁ logika s rovnostÍ. Je-li x promEnnÁ, pak nÁsledujicÍ formule je axiom identity
x
x
(R1)
{Leibnitz]v axiom} 19
20
Schema axiom] rovnosti pro predikÁty. Schema axiom] rovnosti pro funkce. Je-li f n-ÁrnÍ funk7nÍ symbol, x1 , x2 , 4, xn a y1 , y2 , 4, yn jsou promEnnÉ, potom nÁsledujÍcÍ formule je axiom rovnosti pro funkce.
x1
y1
4 xn
yn
f ( x1 , 4 , xn )
f ( y1 , 4 , yn )
(R2)
Je-li p n-ÁrnÍ predikÁtovÝ symbol, x1 , x2 , 4, xn a y1 , y2 , 4, yn jsou promEnnÉ, potom nÁsledujÍcÍ formule je axiom rovnosti pro predikÁty.
x1
y1
4 xn
yn
p ( x1 , 4 , xn )
(R3)
p ( y1 , 4 , yn )
21
ElementÁrnÍ vlastnosti rovnosti.
Tranzitivnost
x
O rovnosti se pUedpoklÁdÁ, Şe je reflexivnÍ, symetrickÁ
|
x1
|
x
y
x y1
y
x x2
y
x
x y2
x
y
|
x1
x2
y1
x
x1
y1 |
(2)
x
y
y
y
z
z
x
z
z
y
z
y2
x1
x2
z
x
(3)
x
z
(R3)
Pro kontrolu
pro libovolnÉ promEnnÉ x, y.
x
|
a tranzitivnÍ.
Reflexivnost je dÁna axiomem (R1). DokÁŞeme nejprve symetrii, tedy (1) y x | x y
|
22
y2 (R3)
(2),(R1),MP
x2 y
x
y
y1 z
y2 (R3) (R1),(R3), MP
Formule (3) se odvodÍ sloŞenÍm poslednÍ implikace s implikacÍ (1).
TÍm je dokÁzÁno (1). 23
24
ZÁkladnÍ vEta o rovnosti.
D]kaz.
Nech[ T je mnoŞina formulÍ a t1 , 4 , t n , jsou termy pro, kterÉ platÍ
(i) IndukcÍ podle sloŞitosti termu t. Je-li t promEnnÁ nebo nEkterÝ z term] ti a term s vznikne zÁmEnou celÉho termu t termem s, potom (6) je jednÍm z pUedpoklad] (5).
T | t1
s1 , 4 , | t n
sn
s1 , 4 , sn (5)
(i) Je-li t term a term s z nEj vznikne zÁmEnou nEkterÝch vÝskyt] term] ti odpovÍdajÍcÍmi termy si , potom (6) T| t s (ii) Je-li A formule, kterÁ vznikne z formule A zÁmEnou nEkterÝch vÝskyt] term] ti odpovÍdajÍcÍmi termy si , ne vŁak bezprostUednE za kvantifikÁtorem, potom
T|
A A
(7) 25
D]sledek. Jsou-li t , t1 , 4 , t n , s1 , 4 , sn termy, A formule, potom platÍ (i ) | t1 s1 4 t n sn t[t1 , 4 , t n ] t[ s1 , 4 , sn ]
(ii ) | t1
s1
4 tn
sn
( A[t1 , 4 , t n ]
A[ s1 , 4 , sn ])
Je-li navÍc x promEnnÁ, kterÁ nenÍ obsaŞena v termu t, potom
(iii ) |
Ax [t ]
( x)( x
t
A)
(iv) |
Ax [t ]
( x)( x
t & A) 27
Je-li term t tvaru f (r1 , 4 , rk ) a term s tvaru f (r1 , 4, rk ) z induk7nÍho pUedpokladu dostÁvÁme
T | r1 | r1
r1
4 rk
rk
r1 , 4 , | rn
rn
f ( x1 , 4 , xk ) (+) + +* +
f (r1 , 4 , rk ) (R2) (+ +)++ *
t
(8)
s
odkud tvrzenÍ (i) odvodÍme pravidlem modus ponens. TvrzenÍ (ii) se dokazuje obdobnE. 26
Teorie prvnÍho UÁdu. Je-li L jazyk prvnÍho UÁdu a T mnoŞina jeho formulÍ, UÍkÁme, Şe T je teorie prvnÍho UÁdu s jazykem L.
Pravdivost a dokazatelnost Vztah formÁlnÍho systÉmu a sÉmantiky predikÁtovÉ logiky
FormulÍm z mnoŞiny T UÍkÁme speciÁlnÍ axiomy teorie T. PredikÁtovÁ logika je zvlÁŁtnÍm pUÍpadem teorie prvnÍho UÁdu, kterÁ nemÁ ŞÁdnÉ speciÁlnÍ axiomy.
1
2
Modely teoriÍ.
PUÍklady.
(i) Je-li T teorie s jazykem L a M je interpretace jazyka L, UÍkÁme, Şe M je modelem teorie T a pÍŁeme M | T , jestliŞe kaŞdÝ speciÁlnÍ axiom teorie T , tedy kaŞdÁ formule z T je pravdivÁ v M.
(a) Teorie (ostrÉho) uspoUÁdÁnÍ mÁ jazyk s rovnostÍ, kterÝ obsahuje jedinÝ speciÁlnÍ symbol, binÁrnÍ predikÁt a dva speciÁlnÍ axiomy ( x x) x y (y z x z)
(ii) TÍkÁme, Şe formule A je sÉmantickÝm d]sledkem teorie (mnoŞiny) T a pÍŁeme T | A, jestliŞe A je pravdivÁ v kaŞdÉm modelu teorie T .
kaŞdÝ model tÉto teorie je 7Áste7nE uspoUÁdanÁ mnoŞina. (b) pUidÁme-li jeŁtE axiom x y x y y x, dostaneme teorii (ostrÉho) lineÁrnÍho uspoUÁdÁnÍ. KaŞdÝ model tÉto teorie je lineÁrnE uspoUÁdanÁ mnoŞina.
3
4
(c) Teorie okruh], obor] integrity a tEles. Nech[
a pro nÁsobenÍ
L {0, 1, , }
1 x
je jazyk s rovnostÍ, kde 0, 1 jsou konstanty a , jsou binÁrnÍ funk7nÍ symboly pro operace s7ÍtÁnÍ a nÁsobenÍ.
x
y
y x
x 1
(o5)
x
(o6)
x ( y z) ( x y) z x y y x
Teorie komutativnÍch okruh] s jednotkou mÁ tyto speciÁlnÍ axiomy pro s7ÍtÁnÍ
x ( y z) ( x y) z x 0 x 0 x x ( y )( x y 0 & y x 0 )
x
x ( y z)
(o7)
( x y) ( x z)
pUidÁme-li axiom x y 0 ( x 0 y 0) dostaneme Teorii obor] integrity. PUidÁme-li k teorii okruh] dva axiomy 0 1
(o1) (o2) (o3) (o4)
x 0
(o8) (i1)
(t1) (t2)
( y )( y x 1)
dostaneme Teorii tEles. 5
6
ElementÁrnÍ aritmetika mÁ tyto speciÁlnÍ axiomy
(d) Jazyk elementÁrnÍ aritmetiky obsahuje rovnost a speciÁlnÍ symboly 0, S , , kde
S ( x) 0 S ( x)
• 0 je konstanta pro nejmenŁÍ pUirozene 7Íslo,
x
• S je unÁrnÍ funk7nÍ symbol pro nÁsledujÍcÍ pUirozenÉ 7Íslo S ( x) x 1,
0
x 0
a jsou binÁrnÍ funk7nÍ symboly pro operace • s7ÍtÁnÍ a nÁsobenÍ.
S ( y)
x)
x S(x
y)
0
x S ( y)
7
y
( y )( S ( y )
x S ( y) x 0
x
( x y) x
8
VEta o korektnosti.
Interpretace N , jejÍŞ domÉnou jsou pUirozenÁ 7Ísla, 0N
Je-li T teorie, A formule T, potom platÍ
0
S N ( x)
x 1 (x
{x})
T|
x
N
y
x
y
(x
y)
ordinÁlnÍ sou7et
x
N
y
x y
(x
y)
ordinÁlnÍ sou7in
T| A
A
SpeciÁlnE
|
Se nazÝvÁ standardnÍ model aritmetiky.
{
A
| A
nenÍ implikace v jazyku T , zastupuje slova
" jestliŞe ... potom "...} 9
10
(b1) A je pUÍpad axiomu specifikace tvaru ( x) B Bx [t ]. Je-li M | ( x) B[e], potom implikace A je pravdivÁ.
Lemma. Axiomy predikÁtovÉ logiky jsou validnÍ formule. D]kaz. Nech[ L je jazyk predikÁtovÉ logiky a A jeho formule. Nech[ M je libovolnÁ interpretace jazyka L , e je pravdivostnÍ ohodnocenÍ v M. Probereme jednotlivÉ axiomy. (a) A je pUÍpad axiomu A vÝrokovÉ logiky. Podle vEty o Úplnosti vÝrokovÉ logiky je A tautologie. Jsou-li p1 , 4 , pn vŁechny vÝrokovÉ promEnnÉ fomule A a A1 , 4 , An jsou formule, kterÉ v A vystupujÍ na jejich mÍstE, pak M | A[e] nezÁvisle na pravdivosti M | Ai [e] i,1 i n. 11
Naopak, je-li M | ( x) B[e], potom M | ( x) B[e( x / m)], pro libovolnÝ prvek m z domÉny M, speciÁlnE pro t[e]. potom M | ( Bx [t ])[e]. Axiom specifikace je pravdivÝ v M. (b2) A je pUÍpad axiomu pUeskoku tvaru ( x)( B
C)
(B
( x)C )
(1)
kde promEnnÁ x nenÍ volnÁ v B. Jako v pUedchozÍm pUÍpadE, nenÍ-li pravdivÝ pUedpoklad implikace, potom A je pravdivÁ v M pUi ohodnocenÍ e.
12
PUedpoklÁdejme, Şe M | ( x)( B C )[e], tedy pro libovolnÉ m z domÉny M podle definice splOovÁnÍ platÍ M | (B
(c) Nech[ A je axiom rovnosti pro funkce
x1
C )[e( x / m)].
to znamenÁ, Şe bu@ je formule B pravdivÁ pUi ohodnocenÍ e(x/m) nebo totÉŞ musÍ platit pro formuli C. ProtoŞe formule B neobsahuje promEnnou x volnE, je pravdivÁ pUi ohodnocenÍ e(x/m) prÁvE kdyŞ je pravdivÁ pUi ohodnocenÍ e. PUitom M | C[e( x / m)] to znamenÁ, Şe M | ( x)C[e], a tedy M | ( B ( x)C )[e].
y1
4 xn
f ( x1 , 4 , xn )
f ( y1 , 4 , yn )
Je zUejmÉ, Şe nebude-li nEkterÁ z rovnostÍ xi yi nEkterÁ splnEna pUi ohodnocenÍ e, potom nebude splnEn axiom (2). PUedpoklÁdejme, Şe tom u tak nenÍ, to znamenÁ,Şe e( x1 ) e( y1 ) 4 e( xn ) e( yn ) Potom M | ( f ( x1 ,5 xn )
(2)
(3)
f ( y1 , 5 yn ))[e]
f M (e( x1 ),5 e( xn ))
a z (3) plyne
TÍm je pravdivost (a validnost) (1) dokÁzÁna.
yn
f M (e( y1 ),5 e( yn ))
M | A[e]
Validnost axiomu rovnosti pro predikÁty se dokazuje podobnE. 13
14
(a) Ai je axiom predikÁtovÉ logiky. Pak je to validnÍ formule a (1) platÍ.
D]kaz vEty o korektnosti. PUedpoklÁdejme, Şe T | A a Şe A1 , 4 , An A je d]kaz A v teorii T. Nech[ M je libovolnÝ model T.
(b) Ai je axiom T. Potom (1) platÍ protoŞe M je model T.
Budeme postupovat indukcÍ podle d]kazu formule A. PUedpoklÁdejme, Şe Ai je takovÁ, Şe pro vŁechny formule A j , 1 j i jiŞ bylo dokÁzÁno M | A j .
(c) Ai je odvozena z formulÍ A j , Ak 1 j , k i pravidlem modus ponens. PUedpoklÁdejme, Şe platÍ Ak A j Ai .
DokÁŞeme
Z induk7nÍho pUedpokladu dostÁvÁme M | A j a M | Ak . M | Ai .
(1)
Z korektnosti pravidla modus ponens takÉ
M | Ai .
Rozebereme nEkolik pUÍpad] 15
16
(c) Ai je odvozena z formule A j , 1 j i pravidlem generalizace. Tedy Ai ( x) A j nEjakou promEnnou x.
pro
ValidnÍ formule
nech[ e je li bovolnÉ ohodnocenÍ. Z i nduk7nÍho pUed pokladu plyne M | A j , tedy takÉ M | A j [e]. SpeciÁlnE
VEty T
Axiomy T
M | A j [e( x / m)]
odkud
M | (( x) A j )[e] ( +)+ * Ai
protoŞe e bylo libovolnÉ ohodnocenÍ, dostÁvÁme M | Ai .
TÍm je vEta o korektnosti dokÁzÁna. 17
18
VEta o Úplnosti. (GÖdel 1930) Nech[ T je teorie s jazykem L.
VEta o Úplnosti.
(i) je-li A libovolnÁ formule jazyka L, potom platÍ
T|
A
prÁvE kdyŞ T | A
(ii) Teorie T je bezespornÁ, prÁvE kdyŞ mÁ model.
1
PozorovÁnÍ.
2
Lemma.
VEta o korektnosti dÁvÁ polovinu z kaŞdÉho tvrzenÍ VEty o Úplnosti. SamotnÁ vEta o korektnosti je implikacÍ zleva doprava v tvrzenÍ (i),
Ve VEtE o Úplnosti druhÉ tvrzenÍ implikuje prvnÍ. D]kaz. PUedpoklÁdejme, Şe platÍ (ii). Nech[ T je teorie, A formule jazyka teorie T. VÍme
T|
zatÍm co
A
prÁvE kdyŞ T
{ uzÁvEr ( A)} je spornÁ
Podle (ii) to znamenÁ, Şe teorie T { uzÁvEr ( A)} nemÁ model. Tedy v kaŞdÉm modelu teorie T je pravdivÁ (uzavUenÁ) formule uzÁvEr ( A) a takÉ A.
jejÍ d]sledek je implikacÍ zprava doleva v tvrzenÍ (ii).
TÍm je tvrzenÍ (i) dokÁzÁno. 3
4
VEtu o Úplnosti dokÁŞeme, podaUÍ-li se nÁm dokÁzat, Şe kaŞdÁ bezespornÁ teorie mÁ model. Metoda, kterou pouŞijeme nenÍ p]vodnÍ GÖdelova, ale pochÁzÍ od L. Henkina.
KanonickÁ struktura M .
MEjme bezespornou teorii T s jazykem L. NaŁÍm Úkolem je sestrojit jejÍ model, tedy strukturu M , kterÁ mÁ neprÁzdnÉ universum M a kterÁ v nEm interpretuje vŁechny funk7nÍ a predikÁtovÉ symboly teorie T . PUitom T nÁm poskytuje jenom syntaktickÝ materiÁl v podobE jazyka, axiom] a vEt. Z nEj musÍme strukturu M vytvoUit. NavÍc mÁme uŞite7nÝ pUedpoklad, Şe T je bezespornÁ teorie.
• Universum M = {t | t je term bez promEnnÝch} • Funk7nÍ symboly (nepotUebujeme ohodnocenÍ promEnnÝch). Je-li t1 , 4, t n M a f je n-ÁrnÍ funk7nÍ symbol, jeho realizaci f M definujeme nÁsledovnE f M (t1 , 4 , t n ) f (t1 , 4 , t n ) M • PredikÁtovÉ symboly. Je-li p n-ÁrnÍ predikÁtovÝ symbol, jeho interpretace pM se definuje takto (t1 , 4 , t n )
pM
p (t1 , 4 , t n )
prÁvE kdyŞ T |
5
Pokud jazyk L neobsahuje predikÁt rovnosti, je lehkÉ ovEUit indukcÍ podle sloŞitosti termu, Şe t [e] = t pro kaŞdÝ prvek t univerza a kaŞdÉ ohodnocenÍ promEnnÝch e.
M| A[e] (t1 , 4 , t n ) pM T|
SÉmantika se trochu zkomplikuje, pokud jazyk L obsahuje predikÁt rovnosti. Je-li napUÍklad T aritmetika, m]Şe se stÁt, Şe T|
Potom pro kaŞdou atomickou formuli A p(t1 , 4, t n ) bez promEnnÝch (a kaŞdÉ ohodnocenÍ e) platÍ M| A
6
S (0 ) S (0 ) (+)+*
S ( S (0 )) ( +)+ *
t
s
ale M | S (0 ) S (0 ) (+)+*
(1)
t
S ( S (0 )) ( +)+ *
protoŞe t
s
s
A
Struktura M povaŞuje termy t, s za dvE r]znÁ individua.
SÉmantika atomickÝch formulÍ bez promEnnÝch je tedy dÁna vEtami teorie T. 7
8
Zde pom]Şe faktorizace. VÍme, Şe predikÁt rovnosti definuje na mnoŞinE vŁech term], tedy i na univerzu M, struktury M, reflexivnÍ, symetrickou a tranzitivnÍ relaci, tedy relaci ekvivalence, ozna7me ji a definujme
t
s
prÁvE kdyŞ T | t
M| t
[t ] [ s ] T| t s
(2)
f M ([t1 ], 4 , [t n ]) [ f (t1 , 4 , t n )]
a ostatnÍ predikÁty p, pM
Potom hodnotou termu t ve struktuUe M je [t].
([t1 ], 4, [t n ])
PlatÍ
prÁvE kdyŞ T | t
s
definujeme-li pro funk7nÍ symboly f
s
MÍsto term] samotnÝch pracujeme s tUÍdami ekvivalence [t ] {s M | s t} a s univerzem M / .
[t ] [ s ]
Tedy
pM
(M/ ) n pUedpisem
prÁvE kdyŞ T |
p (t1 , 4 , t n )
(3)
dostÁvÁme nÁsledujÍcÍ tvrzenÍ.
s 9
10
D]kaz
Lemma.
probÍhÁ ÚplnE stejnE, jako u pUedchozÍho tvrzenÍ (1), jenom je tUeba ovEUit, Şe definice f M a pM jsou korektnÍ, tedy Şe (2) a (3) nezÁvisÍ na volbE term]
Nech[ M je kanonickÁ struktura pro L. Nech[ A je atomickÁ formule bez promEnnÝch jazyka L. Potom platÍ M| A
T|
A
si
[ti ].
Interpretaci f M funk7nÍho symbolu f jsme definovali pUedpisem (2).
(4)
Nech[ s1 [t1 ], 4, sn [t n ] pro libovolnÉ platÍ
si
[ti ]
si T|
11
i, 1 i
n (5)
ti si
(6)
ti 12
z (5) a (6) dostÁvÁme
T | si
pro
ti
i, 1 i
(7)
n
vezmEme axiom rovnosti pro f .
s1
t1
4
sn
T|
f ( s1 , 4, sn )
tn
f ( s1 , 4, sn )
f (t1 , 4, t n )
NaŁÍm cÍlem je dokÁzat stejnou vEtu (4) pro kaŞdou uzavUenou formuli A . Potom struktura M bude modelem teorie T .
Potom
f (t1 , 4, t n )
MP, (7)
Tedy
[ f ( s1 , 4, sn )] [ f (t1 , 4, t n )]
Pro libovolnÝ axiom B teorie T a jeho uzÁvEr A , dostÁvÁme T | A a podle (4) takÉ M | A. Z definice splOovÁnÍ potom M | B.
a definice f M je korektnÍ. StejnÝm zp]sobem bychom dokÁzali, Şe korektnÍ je i definice pM . 13
14
DvE definice. DalŁÍ postup
Nech[ T je teorie s jazykem L . (i) TÍkÁme, Şe T je ÚplnÁ teorie, je-li bezespornÁ a pro libovolnou uzavUenou formuli A jazyka L je jedna z formulÍ A a A dokazatelnÁ v T .
• VEtu o Úplnosti dokÁŞeme jen pro nEkterÉ teorie (ÚplnÉ a Henkinovy) • UkÁŞeme, Şe kaŞdou bezespornou teorii lze rozŁÍUit do teorie s poŞadovanÝmi vlastnostmi. • UkÁŞeme, Şe model rozŁÍUenÍ nEjakÉ teorie lze redukovat do modelu vÝchozÍ teorie. • TÍm sestrojÍme model libovolnÉ bezespornÉ teorie.
(ii) TÍkÁme, Şe T je Henkinova teorie, jestliŞe pro libovolnou uzavUenou formuli tvaru ( x) B existuje konstanta c , takovÁ, Şe T | ( x) B
15
Bx [c ]
16
D]kaz. Pro kaŞdou uzavUenou formuli A ukÁŞeme M| A
VEta o kanonickÉm modelu.
T|
(4)
A
a) pro uzavUenÉ atomickÉ formule jsme to jiŞ dokÁzali. Je-li T ÚplnÁ a Henkinova teorie, potom kanonickÁ struktura M pro T je modelem T .
b) je-li A tvaru B , potom M| A
M| B T| T| T|
B B
induk7nÍ pUedpoklad Úplnost T
A
17
c) je-li A tvaru B M| A
C , potom
18
d) Je-li A uzavUenÁ formule tvaru ( x) B, potom
M | B nebo M | C M| A T|
B nebo T | C
T| T|
B nebo T | C A
induk7nÍ pUedpoklad Úplnost T
M | B ( x /[t ]) pro nEjakÝ term t bez promEnnÝch
M | Bx [t ]
pro nEjakÝ term t bez promEnnÝch
T|
Bx [t ]
pro nEjakÝ term t bez promEnnÝch
T|
A
{cvi7enÍ}
19
20
Rozeberme jeŁtE podrobnEji poslednÍ ekvivalenci.
Co jsme jiŞ dosÁhli
A ( x) B
T je Henkinova, existuje tedy konstanta c , takovÁ, Şe T | ( x) B
Bx [c ]
• VEtu o Úplnosti dokÁŞeme jen pro nEkterÉ teorie (ÚplnÉ a Henkinovy) • UkÁŞeme, Şe kaŞdou bezespornou teorii lze rozŁÍUit do teorie s poŞadovanÝmi vlastnostmi. • UkÁŞeme, Şe model rozŁÍUenÍ nEjakÉ teorie lze redukovat do modelu vÝchozÍ teorie. • TÍm sestrojÍme model libovolnÉ bezespornÉ teorie.
(5)
TÍm je implikace zdola nahoru dokÁzÁna. ObrÁcenÁ implikace je instancÍ lemmatu o substituci. TÍm je vEta o kanonickÉm modelu dokÁzÁna a prvnÍ krok na cestE k d]kazu vEty o Úplnosti mÁme za sebou. 21
Jak rozŁÍUit teorii: dva zp]soby
22
PozorovÁnÍ.
• Nech[ L a L jsou jazyky, nech[ T je teorie s jazykem L a T je teorie s jazykem L. • Definice. TÍkÁme, Şe jazyk L je rozŁÍUenÍm jazyka L, jestliŞe kaŞdÝ symbol jazyka L je symbolem jazyka L stejnÉho vÝznamu a stejnÉ 7etnosti. • Definice. TÍkÁme, Şe teorie T je rozŁÍUenÍm teorie T , jestliŞe L je rozŁÍUenÍm L a kaŞdÝ axiom teorie T je vEtou teorie T. • Definice. TÍkÁme, Şe T je konzervativnÍ rozŁÍUenÍ T, je-li to rozŁÍUenÍ a pro kaŞdou formuli A jazyka L platÍ T | A T | A. 23
(i) je-li T rozŁÍUenÍm teorie T a T je bezespornÁ, potom T je takÉ bezespornÁ.
(ii) je-li T konzervativnÍ rozŁÍUenÍ T, potom T je bezespornÁ, prÁvE kdyŞ je bezespornÁ teorie T.
24
D]kaz. Teorii TH sestrojÍme postupnÝm pUidÁvÁnÍm axiom] tak, aby byla splnEna podmÍnka (5) z definice Henkinovy teorie.
VEta. (Henkin)
PoloŞme T formuli
Ke kaŞdÉ teorii T lze sestrojit konzervativnÍ rozŁÍUenÍ .TH , kterÉ je Henkinovou teoriÍ.
L0 a pro libovolnou uzavUenou
T0 , L
( x) B
pUidejme do jazyka L0 novou speciÁlnÍ konstantu c( x ) B (6) a do teorie T0 axiom ( x) B
B x [ c(
x) B
]
(7)
Budeme UÍkat, Şe konstanta (6) pUÍsluŁÍ k axiomu (7). 25
Tak vytvoUÍme rozŁÍUenÍ L1 jazyka L0 a rozŁÍUenÍ T1 teorie T0 .
PostupnE vytvoUÍme posloupnost rozŁÍUenÍ jazyk]
Tento postup je tUeba iterovat. Formule ( x) B jazyka teorie T1 m]Şe obsahovat konstantu c( x ) B z T1 k nÍŞ nepatUÍ ŞÁdnÝ axiom ( x) B
B x [ c(
x) B
26
L
L0
L1
4
Ln
Ln
1
4
T
T0
T1
4
Tn
Tn
1
4
LH
:L
a teoriÍ PoloŞÍme-li
].
Proto konstanty (6) teorie T1 nazveme HenkinovÝmi konstantami prvnÍho UÁdu a k nim pUÍsluŁnÉ axiomy (7) takÉ nazveme HenkinovÝmi axiomy prvnÍho UÁdu. Opakujeme-li stejnÝ postup s uzavUenÝmi existen7nÍmi formulemi teorie T1 sestrojÍme rozŁÍUenÍ L2 jazyka L1 a rozŁÍUenÍ T2 teorie T1 . Tak zÍskÁme Henkinovy konstanty a axiomy druhÉho UÁdu.
n
n 0
TH
:T
n
n 0
potom jazyk LH obsahuje Henkinovy konstanty vŁech UÁd] a v teorii TH jsou vŁechny k nim pUÍsluŁnÉ axiomy. Tedy TH je Henkinova teorie. ZbÝvÁ dokÁzat, Şe je to konzervativnÍ rozŁÍUenÍ teorie T .
27
28
TH .
Nech[ A je formule jazyka L , kterÁ je vEtou Nech[
(8)
B1 , B2 , 4 , Bn
Tedy UÁd konstanty pUÍsluŁejÍcÍ k axiomu B1 je vEtŁÍ nebo roven UÁd]m vŁech konstant pUÍsluŁejÍcÍch k formulÍm B2 , 4, Bn
jsou vŁechny Henkinovy axiomy z d]kazu A. Potom PUedpoklÁdejme, Şe B1 je tvaru T , B1 , B2 , 4, Bn |
A ( x) D
protoŞe (8) jsou uzavUenÉ formule, z VEty o dedukci dostÁvÁme T|
B1
B2
4
Bn
(9)
A
Bez Újmy na obecnosti m]Şeme pUedpoklÁdat, Şe B1 je axiom pUÍsluŁnÝ k HenkinovE konstantE maximÁlnÍho UÁdu.
D x [ c(
x) D
].
Podle pUedpokladu o UÁdech HenkinovÝch konstant, c( x ) D nenÍ obsaŞena ve formulÍch B2 , 4, Bn a tÍm mÉnE v teorii T. M]Şeme pouŞÍt vEtu o konstantÁch a nahradÍme uvedenou Henkinovu konstantu novou promEnnou w.
29
30
Z (9) dostaneme ( B2 4 ( Bn A) 4) (++++)++++*
T | (( x) D Dx [ w]) pravidlem zavedenÍ
T | ( w)(( x) D ()*
neobsahuje w
Dx [ w])
( B2
4
( Bn
A) 4)
nenÍ w
VEta (Lindenbaum)
prenexnÍ operacÍ T | (( x) D
( w) Dx [ w])
( B2
4
( Bn
A) 4)
KaŞdnou bezespornou teorii T lze rozŁÍUit do ÚplnÉ teorie S se stejnÝm jazykem jako T .
z VEty o variantÁch plyne | (( x) D T|
B2
4
( w) Dx [ w])) Bn
A
MP
6 T|
A
dostaneme opakovÁnÍm stejnÉho postupu 31
32
D]kaz. Je-li dÁna bezespornÁ teorie T s jazykem L , podle VEty o uzÁvEru m]Şeme pUedpoklÁdat, Şe vŁechny axiomy T jsou uzavUenÉ formule. ºplnÉ rozŁÍUenÍ TU teorie T sestrojÍme jako maximÁlnÍ bezespornÉ rozŁÍUenÍ T s jazykem L.
Postupujeme stejnÝm zp]sobem jako u obdobnÉ vEty VÝrokovÉ logiky, jenom mÍsto vŁech formulÍ o7Íslujeme jen formule uzavUenÉ.
UspoUÁdejme vŁechny uzavUenÉ formule jazyka L do posloupnosti A0 , A1 , A2 , 4 , An , 4
na uspoUÁdÁnÍ formulÍ nezÁleŞÍ, d]leŞitÉ je, aby posloupnost byla prostÁ. VytvoUÍme neklesajÍcÍ posloupnost teoriÍ se stejnÝm jazykem T
T0
T1
4 Tn
4
nÁsledujÍcÍm postupem.
33
UkÁŞeme, Şe TU je ÚplnÁ teorie. Postupujeme sporem. Nech[ TU nenÍ ÚplnÁ a existuje uzavUenÁ formule A takovÁ, Şe TU | A a TU | A
Je-li T { A0 } bezespornÁ, definujeme T1 T { A0 }, jinak poloŞÍme T1 T. V g-tÉm kroku poloŞÍme T
1
T
{A } je-li to bezespornÁ teorie, jinak T
Je-li g limitnÍ ordinÁl poloŞÍme T
:
1
34
T .
ProtoŞe A nenÍ vEtou TU , nem]Şe bÝt ani prvkem TU . NavÍc A takÉ nenÍ dokazatelnÁ v TU , to znamenÁ, Şe
T.
Nech[ TU je sjednocenÍ vŁech teoriÍ T .
TU
StejnÝm zp]sobem jako v LindenbaumovE vEtE ve VÝrokovÉ logice se ovEUÍ, Şe S je bezespornÁ maximÁlnÍ mnoŞina uzavUenÝch formulÍ teorie T .
{ A}
je bezespornÁ a TU je jejÍ vlastnÍ podmnoŞinou. To je ve sporu s maximalitou mnoŞiny TU . Teorie TU je tedy ÚplnÁ. 35
36
Redukce a expanze struktur Definice. Je-li L rozŁÍUenÍ jazyka L, potom (i) je-li M je interpretace jazyka L, redukce struktury M do jazyka L, kterou ozna7Íme M| L, vznikne z M vynechÁnÍm tEch zobrazenÍ a relacÍ, kterÉ interpretujÍ funk7nÍ a predikÁtovÉ symboly, kterÉ nejsou v jazyce L.
Lemma. Nech[ T je rozŁÍUenÍ teorie T, kterÁ mÁ jazyk L. Je-li M model teorie T potom redukt M = M| L je model teorie T.
(ii) je-li M interpretace jazyka L a M interpretace L, UÍkÁme, Şe M je expanzÍ M, jestliŞe M = M| L. Po vŁimnEme si, Şe redukce a expanze majÍ stejnÉ univerzum. 37
38
(ii) je-li A formule jazyka L, potom se indukcÍ podle sloŞitosti formule A dokÁŞe pro kaŞdÉ ohodnocenÍ e
D]kaz lemmatu. M je redukt M, majÍ tedy stejnÉ univerzum a takÉ stejnou mnoŞinu ohodnocenÍ promEnnÝch. ObE struktury interpretujÍ stejnE vŁechny funk7nÍ a predikÁtovÉ symboly jazyka L.
tedy takÉ
(i) Nech[ t je libovolnÝ term jazyka L. IndukcÍ podle sloŞitosti termu t se pro kaŞdÉ ohodnocenÍ e dokÁŞe, Şe interpretace (hodnota) t[e] je stejnÁ v obou strukturÁch.
(iii) je-li A axiom teorie T, pak je vEtou teorie T a podle vEty o korektnosti je M| A tedy takÉ M | A. To znamenÁ, Şe M je model T.
M | A[e]
M| A
39
M | A[e]
M | A
40
DosavadnÍ vÝsledky m]Şeme shrnout takto • Je-li dÁna bezespornÁ teorie T , • umÍme sestrojit konservativnÍ rozŁÍUenÍ T* teorie T, kterÉ je Henkinovou teoriÍ. • ProtoŞe T je podle pUedpokladu bezespornÁ a T* je jejÍ konzervativnÍ rozŁÍUenÍ, je takÉ T* bezespornÁ. • M]Şeme, tedy sestrojit ÚplnÉ rozŁÍUenÍ T** teorie T* • PUitom T** mÁ stejnÝ jazyk jako T* je tedy Henkinova. • MÁme tedy Úplnou Henkinovu teorii T** , kterÁ je rozŁÍUenÍm teorie T. Podle VEty o kanonickÉm modelu mÁ model M. • redukt M = M| L je model teorie T .
VEta o kompaktnosti. Teorie T mÁ model, prÁvE kdyŞ kaŞdÝ jejÍ kone7nÝ fragment T T mÁ model.
{spolu s VEtou o Úplnosti patUÍ k nEkolika vEtÁm, kterÉ charakterizujÍ logiku prvnÍho UÁdu.}
41
42
D]kaz. Podle VEty o Úplnosti mÁ libovolnÁ teorie S model, prÁvE kdyŞ je bezespornÁ. (i) je-li bezespornÁ T pak je bezespornÝ kaŞdÝ jejÍ fragment a mÁ tedy model.
D]sledek. Je-li T teorie s jazykem L, A je libovolnÁ formule jazyka L, potom
T| A
T | A
pro nEjakÝ kone7nÝ fragment T T . (ii) je-li naopak bezespornÝ kaŞdÝ kone7nÝ fragment T T pak je bezespornÁ i teorie T, protoŞe d]kaz sporu by se odehrÁl v nEjakÉm kone7nÉm fragmentu T. To znamenÁ, Şe mÁ-li kaŞdÝ kone7nÝ fragment teorie T model, pak T mÁ takÉ model. 43
44
Dva pUÍklady. a) Je nutnÉ v logice prvnÍho UÁdu popisovat teorii tEles charakteristiky 0 nekone7nÝm po7tem axiom]?
D]kaz. Podle vEty o Úplnosti T| A
T|
Nech[ T je teorie tEles s jazykem L = {0, 1,+, • } s rovnostÍ. Je-li x promEnnÁ, termy
A
a d]kaz formule A pouŞÍvÁ jen kone7nE mnoho axiom] teorie T.
x ( x ( x 4 ( x x) 4 ))) , ... x, (x+x), (x+(x+x)), … , (( ++++ +)+++++ * n krÁt x
budeme ozna7ovat zkratkami
1 x, 2 x, 3 x 4 n x, 4 a budeme jim UÍkat pUirozenÉ nÁsobky x. 45
Pokud pro ŞÁdnÉ nenulovÉ p neplatÍ (1), UÍkÁme, Şe tEleso mÁ charakteristiku 0.
PUipomeOme, Şe pUirozenÁ 7Ísla nemusÍ bÝt prvky kaŞdÉho tElesa a pUirozenÝ nÁsobek imituje sou7in jako opakovanÉ pUi7ÍtÁnÍ. VÝraz
p x
PUidÁme-li k teorii tEles axiomy
p 1 0
m]Şe zastupovat term zna7nÉ dÉlky.
(2)
pro vŁechna nenulovÁ p, dostaneme rozŁÍUenÍ T, kterÉ axiomatizuje tElesa charakteristiky nula.
Pokud v nEjakÉm tElese platÍ formule
p 1 0
46
(1)
pro nEjakÉ nenulovÉ p UÍkÁme, Şe tEleso mÁ kone7nou charakteristiku a nejmenŁÍ nenulovÉ p, pro kterÉ platÍ (1) nazveme charakteristikou tElesa. 47
Je pUirozenÉ poloŞit si otÁzku, zda je moŞnÉ nekone7nou mnoŞinu axiom] (2) nahradit kone7nE mnoha, a tedy jednÍm axiomem. OdpovE@ je negativnÍ. 48
PUitom T obsahuje jenom kone7nE mnoho axiom] (2). Je-li r nejvEtŁÍ z 7Ísel v tEchto axiomech, A platÍ v kaŞdÉm tElese kone7nÉ charakteristiky vEtŁÍ neŞ r.
PUedpoklÁdejme, Şe by nekone7nÉ schema axiom] (2) bylo moŞnÉ nahradit jedinou formulÍ A jazyka L. Potom A je pravdivÁ ve vŁech tElesech charakteristiky 0 a v ŞÁdnÉm tElese kone7nÉ charakteristiky.
To je spor, protoŞe algebra ukazuje, Şe existujÍ tElesa libovolnE velkÉ kone7nÉ charakteristiky.
DostÁvÁme T| A a podle d]sledku VEty o kompaktnosti existuje kone7nÝ fragment T teorie T takovÝ, Şe T | A.
Nekone7nou mnoŞinu axiom] (2) nelze v logice prvnÍho UÁdu nahradit jednÍm axiomem.
49
50
b) Je standardnÍ model aritmetiky N jedinÝm modelem aritmetiky (aŞ na isomorfismus) ?
Snad nejvÍce se obE teorie liŁÍ ve vyjÁdUenÍ principu indukce.
V PeanovE aritmetice druhÉho UÁdu ANO.
Peanova aritmetika prvnÍho UÁdu vznikne z ElementÁrnÍ aritmetiky pUidÁnÍm schematu axiom] indukce:
V PeanovE aritmetice prvnÍho UÁdu NE.
pro kaŞdou formuli A a promEnnou x je nÁsledujÍcÍ formule axiom indukce.
ObE aritmetiky se liŁÍ celkovÝm rÁmcem, do kterÉho jsou zasazeny. Aritmetika druhÉho UÁdu je teorie v logice druhÉho UÁdu.
Ax [0 ]
(( x)( A
Ax [ S ( x)])
( x) A)
(3)
Snadno se ovEUÍ, Şe standardnÍ model (elementÁrnÍ) aritmetiky je takÉ modelem Peanovy aritmetiky prvnÍho UÁdu.
Aritmetika prvnÍho UÁdu je teorie v logice prvnÍho UÁdu. 51
52
Peanova aritmetika druhÉho UÁdu (nÁznak) x, y, z, …
promEnnÉ pro 7Ísla
X, Y, Z, …
promEnnÉ pro mnoŞiny
UkÁŞeme, Şe z VEty o kompaktnosti plyne, Şe existujÍ modely Peanovy aritmetiky prvnÍho UÁdu, kterÉ nejsou izomorfnÍ se standardnÍm modelem N. TakovÉ modely nazÝvÁme nestandardnÍ. Pro kaŞdÉ pUirozenÉ 7Íslo n budeme definovat term n nÁsledovnE.
predikÁt nÁleŞenÍ Axiom indukce ( X )[0
X
(( x)( x
X
S ( x)
X)
( x)( x
X ))]
0
0
1
S (0 )
6 n 1 S ( S ( S (4 S (0 ) 4)) (++ +)+++ *
Schema indukce (3) zachycuje jen spo7etnE mnoho instancÍ Axiomu indukce pro mnoŞiny, kterÉ jsou definovatelnÉ pomocÍ formulÍ prvnÍho UÁdu.
n 1 krÁt
Tyto termy se nazÝvajÍ numerÁly. KaŞdÉ individuum standardnÍho modelu je interpretacÍ nEjakÉho numerÁlu. 53
K jazyku Peanovy aritmetiky pUidÁme novou konstantu c a axiomy 0 c 1
c
6
(4)
54
Podle VEty o kompaktnosti mÁ teorie Pc model M. Jeho redukcÍ do jazyka Peanovy aritmetiky dostaneme model M Peanovy aritmetiky, kterÝ nenÍ izomorfnÍ se standardnÍm modelem N.
n 1 c 6
M obsahuje individuum, kterÉ nenÍ interpretacÍ ŞÁdnÉho numerÁlu. ProtoŞe individua, kterÁ odpovÍdajÍ numerÁl]m tvoUÍ po7Áte7nÍ Úsek M, takovÉ individuum mÁ nekone7nE pUedch]dc] jako ŞÁdnÉ individuum v N.
Tak vznikne rozŁÍUenÍ Pc Peanovy aritmetiky P. PUitom kaŞdÝ kone7nÝ fragment T Pc mÁ model, kterÝ vznikne expanzÍ standardnÍho modelu N. T obsahuje jen kone7nE mnoho axiom] (4), konstantu c interpretujeme za vŁemi numerÁly z fragmentu T.
Proto N a M nejsou izomorfnÍ.
55
56
Nech[ T T S . pomocÍ vEty o kompaktnosti ukaŞte, Şe T mÁ nEjakÝ model M . Jeho redukt do T je potom nekone7nÝ model T.]
Cvi7enÍ. a) UkaŞte, Şe ŞÁdnÁ teorie prvnÍho UÁdu T necharakterizuje tUÍdu vŁech kone7nÝch interpretacÍ svÉho jazyka. To znamenÁ, Şe pro ŞÁdnou teorii T neplatÍ M| T
b) UkaŞte, Şe ŞÁdnÁ teorie prvnÍho UÁdu necharakterizuje tUÍdu vŁech dobrÝch uspoUÁdÁnÍ.
M je kone7nÁ struktura pro T
[NÁvod. Sporem. PUedpoklÁdejte, Şe T mÁ u vedenou vlastnost.
[NÁvod. Sporem. PUedpoklÁdejte, Şe T mÁ uvedenou vlastnost.
PodobnE jako v a) pUidejte spo7etnE mnoho konstant a k nim axiomy, kterÉ postulujÍ nekone7nou klesajÍcÍ posloupnost. PomocÍ vEty o kompaktnosti ukaŞte, Şe takovÉ rozŁÍUenÍ mÁ nEjakÝ model. Jeho reduktem je model T , kterÝ nenÍ dobrÝm uspoUÁdÁnÍm.]
RozŁiUte jazyk o spo7etnE mnoho konstant c0 , c1 , c2 , 4 , cn , 4
n 0
a pUidejte mnoŞinu S axiom] tvaru ci
c j pro i
j. 57
58
Teorie majÍ svou historii. • Jejich formÁlnÍ systÉmy za7ÍnajÍ axiomy. • Ty jsou formulovÁny ÚspornE a v co nejjednoduŁŁÍm jazyku. • S rozvÍjenÍm teorie pUibÝvajÍ novÉ pojmy. • Konstanty, operace, predikÁty. • Ty jsou zavÁdEny pomocÍ formulÍ. • UkÁŞeme, Şe novÉ pojmy majÍ pomocnÝ charakter. • Jejich definovÁnÍm vznikne konzervativnÍ rozŁÍUenÍ. • DefinovanÉ symboly lze eliminovat a tak se vrÁtit k p]vodnÍmu jazyku.
VÝvoj teoriÍ prvnÍho UÁdu
RozŁiUovÁnÍ teoriÍ
1
UŞite7nÉ lemma
2
D]kaz.
Nech[ L je rozŁÍUenÍm jazyka L a nech[ T je teorie s jazykem L a T teorie s jazykem L.
(i) Je-li T rozŁÍUenÍm T, potom podle lemmatu o redukci a expanzi je redukt kaŞdÉho modelu teorie T do L modelem teorie T.
(i) T je rozŁÍUenÍm T, prÁvE kdyŞ redukt M|L kaŞdÉho modelu M teorie T je modelem T.
Naopak nech[ redukt kaŞdÉho modelu teorie T do L je modelem teorie T.
(ii) Je-li T rozŁÍUenÍm T a kaŞdÝ model M teorie T lze expandovat do modelu M teorie T, potom T je konzervativnÍ rozŁÍUenÍ T.
Nech[ A je axiom T a M je libovolnÝ model T. ProtoŞe M| L je modelem T , M | L | A a tedy M | A. Formule A je tedy pravdivÁ v kaŞdÉm modelu teorie T. Podle vEty o Úplnosti je A vEtou T. To znamenÁ, Şe teorie T je rozŁÍUenÍm T.
3
4
(ii) Nech[ T je rozŁÍUenÍm T a A je formule jazyka L , kterÁ je vEtou teorie T. Nech[ M je libovolnÝ model teorie T a M je jeho expanze do modelu teorie T. Potom podle VEty o korektnosti
M| A
RozŁÍUenÍ teorie o definici predikÁtu. Motivace. V aritmetice m]Şeme definovat predikÁt dElitelnosti
odkud takÉ
M
k|n
M | L | A
UkÁzali jsme, Şe formule A je pravdivÁ v kaŞdÉm modelu M teorie T. Podle VEty o Úplnosti je A takÉ vEtou T .
( s )( s k
n)
VÝraz k | n 7teme „k dElÍ n“ nebo „k je dElitelem n“. Na levÉ stranE ekvivalence je definovanÝ predikÁt a na pravÉ stranE je definujÍcÍ formule.
To znamenÁ, Şe T je konzervativnÍ rozŁÍUenÍ T . 5
6
VEta o definici predikÁtu. D]kaz.
Nech[ T je teorie s jazykem L , nech[ x1 , 4, xn jsou promEnnÉ. Nech[ D je formule jazyka L , takovÁ, Şe vŁechny jejÍ volnÉ promEnnÉ jsou mezi x1 , 4, xn .
Nejprve ukÁŞeme, Şe definovanÝ symbol lze eliminovat. Nech[ B je libovolnÁ formule jazyka L. Zvolme variantu D definujÍcÍ formule z (1) takovou, Şe ŞÁdnÁ promEnnÁ formule B nenÍ vÁzanÁ v D. Potom podle vEty o variantÁch v definici (1) m]Şeme zamEnit D za D.
Nech[ jazyk L vznikne z L pUidÁnÍm novÉho n-ÁrnÍho predikÁtovÉho symbolu p a nech[ rozŁÍUenÍ T teorie T vznikne pUidÁnÍm axiomu (1) p ( x1 , 4 , xn ) D
Ve formuli B nahradÍme kaŞdou podformuli
Potom T je konzervativnÍ rozŁÍUenÍ T a novE definovanÝ symbol lze z kaŞdÉ formule B jazyka L eliminovat tak, Şe pro upravenou formuli B platÍ T | B B 7
p (t1 , 4 , t n )
formulÍ potom
Dx1 x2 4xn [t1 , t 2 , 4 t n ] T |
p (t1 , t 2 , 4 t n )
Dx1 x2 4xn [t1 , t 2 , 4 t n ]
(2) 8
K d]kazu konzervativnosti T sta7Í pro libovolnou formuli B jazyka L ukÁzat
PoslednÍ ekvivalence je instancÍ varianty definujÍcÍho axiomu (1).
T | B
Ve formuli B jsme nahrazovali nEkterÉ atomickÉ formule ekvivalentnÍmi formulemi. Pro vÝslednou formuli B podle VEty o ekvivalenci platÍ
T | B
T|
B
(3)
kde B vznikla z B eliminovÁnÍm definovanÉho predikÁtu. SpeciÁlnE, je-li B z jazyka L, pak B a B jsou totoŞnÉ formule a (3) mÁ tvar
B
T | B
TÍm je moŞnost eliminace dokÁzÁna.
T|
B
TÍm bude konzervativnost dokÁzÁna.
9
Nech[ B1 , 4, Bm je d]kaz B z T. Nech[ pro kaŞdÉ i formule Bi vznikne z Bi eliminacÍ definovanÉho predikÁtu. UkÁŞeme, Şe kaŞdÁ formule Bi je vEtou teorie T. Postupujeme indukcÍ podle d]kazu. UvaŞujeme tyto pUÍpady. a) Bi je axiom predikÁtovÉ logiky kromE axiomu rovnosti pro p . Potom Bi je axiom stejnÉho druhu. b) Bi je axiom rovnosti pro p , tedy x1 y1 4 xn yn p( x1 , 4 , xn ) potom Bi je tvaru x1 y1 4 xn yn D[x1 , 4 , xn ]
p ( y1 , 4 , yn )
10
c) Je-li Bi axiom z T pak je bu@ z T a nenÍ co dokazovat, nebo je to definujÍcÍ axiom (1). V tomto pUÍpadE je Bi tvaru D D a to je instance VEty o variantÁch. d) Je-li Bi odvozena pravidlem modus ponens nebo pravidlem generalizace, pak Bi je odvozena stejnÝm pravidlem z odpovÍdajÍcÍch formulÍ. UkÁzali jsme, Şe kaŞdÁ formule Bi a tedy i formule B je vEtou T . TÍm je (3) dokÁzÁno a d]kaz je uzavUen.
D[ y1 , 4 , yn ]
a to je d]sledek VEty o rovnosti. 11
12
RozŁÍUenÍ teorie o funk7nÍ symboly. Dva zp]soby rozŁÍUenÍ teorie o novÝ funk7nÍ symbol, podle toho s jakou ur7itostÍ jsou dÁny funk7nÍ hodnoty.
Oba postupy majÍ svÉ oprÁvnEnÍ.
PUÍklad. a) Tekneme-li „nech[ p je nEjakÉ prvo7Íslo p > x“, zavÁdÍme funkci f(x), formulÍ, kterÁ ur7Í mnoŞinu moŞnÝch hodnot a f(x) vyberere jednu z nich, ale nÁm nezÁleŞÍ na tom, kterou.
ZavedenÍ funk7nÍho symbolu je jedinou moŞnostÍ v situaci, kdy umÍme dokÁzat, Şe pro kaŞdou hodnotu argumentu je mnoŞina moŞnÝch hodnot neprÁzdnÁ, ale neumÍme z nich ŞÁdnou jednozna7nE definovat.
b) Tekneme-li „nech[ p je nejmenŁÍ prvo7Íslo p, p > x“, definujeme hodnotu p jednozna7nE. V takovÉm pUÍpadE definujeme funkci f(x) = p formulÍ, kterÁ definuje hodnotu funkce jednozna7nE.
Definice funk7nÍho symbolu odpovÍdÁ situaci, kdy se nÁm to podaUÍ.
13
14
VEta o zavedenÍ funk7nÍho symbolu. Nech[ T je teorie s jazykem L , nech[ formule (4) ( y) A jazyka L mÁ vŁechny volnÉ promEnnÉ mezi x1 , 4, xn . Nech[ T vznikne z T rozŁÍUenÍm jazyka o novÝ funk7nÍ n-ÁrnÍ symbol f a pUidÁnÍm axiomu
Ay [ f ( x1 , 4 , xn )]
(5)
K d]kazu vEty pouŞijeme jeden d]sledek axiomu vÝbEru z teorie mnoŞin: VEtu o dobrÉm uspoUÁdÁnÍ. PUipomeOme, Şe mnoŞina m je dobUe uspoUÁdanÁ relacÍ < jestliŞe kaŞdÁ neprÁznÁ podmnoŞina m mÁ nejmenŁÍ prvek vzhledem k < . VEta o dobrÉm uspoUÁdÁnÍ. Na kaŞdÉ mnoŞinE existuje relace dobrÉho uspoUÁdÁnÍ.
Potom T je konzervativnÍm rozŁÍUenÍm teorie T . 15
16
Podle definice splOovÁnÍ existuje alespoO jedno individuum m takovÉ, Şe M | A[e( y / m)]. pUitom m zÁvisÍ na individuÍch m1 , 4, mn . mnoŞinu vŁech takovÝch m ozna7me F (m1 , 4 , mn ) {m | M | A[e( y / m)]}
D]kaz VEty o zavedenÍ funk7nÍho symbolu. T je rozŁÍUenÍ T, konzervativnost dokÁŞeme tÍm, Şe libovolnÝ model T budeme expandovat do modelu T. Nech[ M je libovolnÝ model T, nech[ < je relace dobrÉho uspoUÁdÁnÍ na jeho univerzu M.
min( F (m1 , 4 , mn ))
Podle pUedpokladu je formule (4) vEtou teorie T, to znamenÁ, Şe je pravdivÁ v M pUi kaŞdÉm ohodnocenÍ promEnnÝch e . MEjme takovÉ ohodnocenÍ e, nech[ e( x1 )
m1 , 4 , e( xn )
je to neprÁzdnÁ mnoŞina individuÍ a protoŞe uspoUÁdÁnÍ < je dobrÉ, mÁ tato mnoŞina nejmenŁÍ prvek
NynÍ m]Şeme definovat interpretaci f M novÉho funk7nÍho symbolu f pUedpisem f M (m1 , 4 , mn )
mn
(min( F (m1 , 4 , mn ))
17
Je-li M expanze modelu M pUidÁnÍm interpretace f M funk7nÍho symbolu f , je zUejmÉ, Şe axiom (5) je pravdivÝ v M.
18
Aplikace: Skolemova vEta. TÍkÁme, Şe T je otevUenÁ teorie, jestliŞe vŁechny axiomy z T jsou otevUenÉ formule.
KaŞdÝ model T jsme expandovali do modelu T, tedy T je konzervativnÍ rozŁÍUenÍ T . PoznÁmka. D]kaz vEty se opÍral o charakteristiku konzervativnÍho rozŁÍUenÍ pomocÍ model]. Modely teoriÍ jsou mnoŞinovÉ struktury, vEtŁinou nekone7nÉ. Proto se takovÝm d]kaz]m UÍkÁ nefinitnÍ.
VEta (Skolem) K libovolnÉ teorii T lze sestrojit otevUenou teorii T, kterÁ je konzervativnÍm rozŁÍUenÍm T .
FinitnÍ d]kaz tÉto vEty se opÍrÁ o Herbrandovu vEtu, kterÁ je mimo rÁmec tÉto pUednÁŁky. 19
20
Idea d]kazu. VEta o zavedenÍ funk7nÍho symbolu ukazuje, Şe pomocÍ zavedenÝch funk7nÍch symbol] lze eliminovat existen7nÍ kvantifikÁtory. {s univerzÁlnÍmi si poradÍme podle vEty o uzÁvEru}
Podle VEty o Úplnosti jsou dvE teorie ekvivalentnÍ, prÁvE kdyŞ majÍ stejnÉ modely.
NEkolik definic. (i) UÍkÁme, Şe formule A je univerzÁlnÍ (existen7nÍ), je-li v prenexnÍm tvaru a vŁechny kvantifikÁtory jsou univerzÁlnÍ (existen7nÍ).
Teorie T a S jsou ekvivalentnÍ, prÁvE kdyŞ kaŞdÝ axiom z T je vEtou S a naopak.
(ii) Teorie T a S se stejnÝm jazykem jsou ekvivalentnÍ, jestliŞe majÍ stejnÉ vEty. PÍŁeme T S . 21
22
Skolemova varianta formule. Je-li A uzavUenÁ formule v prenexnÍm tvaru, indukcÍ podle po7tu existen7nÍch kvantifikÁtor] sestrojÍme uzavUenou univerzÁlnÍ formuli AS takovou, Şe | AS A. (i) je-li A univerzÁlnÍ, AS je A.
K sestrojenÍ Skolemovy varianty potUebujeme rozŁÍUit jazyk o kone7nE mnoho novÝch funk7nÍch symbol].
(ii) je-li A tvaru ( x1 ) 4 ( xn )( y ) B
Pokud formule A nenÍ otevUenÁ, stejnÝm postupem sestrojÍme formuli A ... aŞ po kone7nÉm po7tu krok] sestrojÍme formuli AS .
n 0
Podle substitu7nÍho lemmatu platÍ
nech[ f je novÝ n-ÁrnÍ funk7nÍ symbol, definujeme formuli A ( x1 ) 4 ( xn ) B y [ f ( x1 , 4 , xn )]
|
23
AC
A a tedy |
AS
A
(7)
24
T2 vznikne z T1 tak, Şe ke kaŞdÉmu axiomu A z T pUidÁme jeho Skolemovu variantu AS . Potom T2 je konzervativnÍ rozŁÍUenÍ T1 . Je-li A axiom z T1 ,potom pUidÁnÍm axiomu A vznikne podle vEty o zavedenÍ funk7nÍho symbolu konzervativnÍ rozŁÍUenÍ T1 . OpakovÁnÍm tohoto postupu dostaneme konzervativnÍ rozŁÍUenÍ pUidÁnÍm AS .
K d]kazu Skolemovy vEty zavedeme 7tyUi teorie, z nichŞ ta poslednÍ bude otevUenÝm konzervativnÍm rozŁÍUenÍm T .
T1 je teorie se stejnÝm jazykem jako T a jejÍ axiomy jsou uzÁvEry prenexnÍch tvar] formulÍ z T . Z vEty o prenexnÍm tvaru a vEty o uzÁvEru plyne, Şe teorie T a T1 jsou ekvivalentnÍ.
T3 vznikne z T2 vynechÁnÍm vŁech axiom] teorie T2 . Podle (7) jsou obE teorie ekvivalentnÍ. T4 vznikne z T3 nahrazenÍm kaŞdÉho axiomu (je to univerzÁlnÍ formule) jeho otevUenÝm jÁdrem. Podle vEty o uzÁvEru jsou obE teorie ekvivalentnÍ. 25
26
VEta o definici funk7nÍho symbolu. VytvoUili jsme nÁsledujÍcÍ situaci
T
T1
T2
T3
Nech[ L je jazyk, x1 , 4, xn , y r]znÉ promEnnÉ. Nech[ T je teorie s jazykem L a D formule jazyka L s volnÝmi promEnnÝmi mezi x1 , 4, xn , y.
T4
Nech[ platÍ kde T4 je otevUenÁ teorie a je konzervativnÍm rozŁÍUenÍm teorie T .
(8)
T | ( y) D T|
D
( D y [t ]
y
t)
(9)
Nech[ T vznikne z T pUidÁnÍm novÉho n-ÁrnÍho funk7nÍho symbolu f a definujÍcÍho axiomu
TÍm je Skolemova vEta dokÁzÁna.
y 27
f ( x1 , 4 , xn )
D
(10) 28
a) eliminovatelnost. VŁechny vÝskyty symbolu f najdeme uŞ v atomickÝch podformulÍch. Sta7Í dokÁzat (11) jen pro atomickÉ formule a obecnÝ pUÍpad plyne z vEty o ekvivalenci.
Potom T je konzervativnÍ rozŁÍUenÍ teorie T a definovanÝ symbol lze eliminovat. To znamenÁ, Şe ke kaŞdÉ formuli A jazyka teorie T lze sestrojit formuli A jazyka L , takovou, Şe
T |
A
A
(11)
Nech[ A je formule jazyka teorie T. PUi eliminaci postupujeme indukcÍ podle po7tu vÝskyt] symbolu f v A. Pokud f nemÁ vÝskyt v A pak A je A. V opa7nÉm pUÍpadE uvaŞujeme nEkterÝ z nejvnitUnEjŁÍch vÝskyt] f v A, tedy term
D]kaz je rozdElen do dvou krok] • Nejprve dokÁŞeme eliminovatelnost symbolu f
f (t1 , 4 , t n )
• potom konzervativnost rozŁÍUenÍ T
kde t1 , 4 , t n jiŞ neobsahujÍ f . 29
30
NynÍ m]Şeme A definovat takto
Potom A je tvaru
A ( z )( Dx1 x2 4xn y [t1 , 4 , t n , z ] & B )
Bz [ f (t1 , 4, t n )]
kde B mÁ o jeden vÝskyt f mÉnE neŞ A. M]Şeme pUedpoklÁdat, Şe promEnnÁ z se nevyskytuje ani v A ani v definujÍcÍ formuli D . Podle induk7nÍho pUedpokladu jiŞ umÍme sestrojit formuli B jazyka L (tedy bez symbolu f ) takovou, Şe
T | B
B
(11)
Pro definici formule A nech[ D je varianta definujÍcÍ formule D , kterÁ nevÁŞe ŞÁdnou promEnnou formule A. 31
Potom A je formule teorie T a ukÁŞeme, Şe platÍ ekvivalence (11). Z definujÍcÍho axiomu a vEty o variantÁch dostÁvÁme
T | z
f (t1 , 4 , t n )
Dx1 x2 4xn y [t1 , 4 , t n , z ]
a z (11) a vEty o ekvivalenci dostaneme
T | ( z )( z
f (t1 , 4 , t n ) & B)
odkud pomocÍ vEt o rovnosti T | Bz [ f (t1 , 4, t n )] (++)++* A TÍm je (11) dokÁzÁno.
A
A
32
a) (12) je vEtou T. VezmEme instanci definujÍcÍho axiomu (10) a dostÁvÁme
ZbÝvÁ dokÁzat konzervativnost rozŁÍUenÍ. UŞijeme vEtu o zavedenÍ funk7nÍho symbolu.
T |
Nech[ S je teorie, kterÁ vznikne z T pUidÁnÍm stejnÉho funk7nÍho symbolu f a axiomu
f ( x1 , 4 , xn )
D y [ f ( x1 , 4 , xn )]
PouŞitÍm axiomu identity a pravidla MP, potom
T | D y [ f ( x1 , 4 , xn )] (++)++*
(12)
D y [ f ( x1 , 4 , xn )]
f ( x1 , 4 , xn )
( 12 )
S je konzervativnÍm rozŁÍUenÍm T, protoŞe vznikla zavedenÍm funk7nÍho symbolu. UkÁŞeme, Şe S a T jsou ekvivalentnÍ.
b) (10) je vEtou S. Vyjdeme z tÉto vEty o rovnosti
K tomu sta7Í ukÁzat, Şe (12) je vEtou T a definujÍcÍ axiom (10) je vEtou S.
odkud prostUedky vÝrokovÉ logiky
|
|
y
f ( x1 , 4 , xn )
D y [ f ( x1 , 4 , xn )]
(D
(y
D y [ f ( x1 , 4 , xn )])
f ( x1 , 4 , xn )
D)
33
34
Z axiomu (12) a MP pak
S| y
f ( x1 , 4 , xn )
Cvi7enÍ.
D
Opa7nou implikaci odvodÍme z axiomu jednozna7nosti (9). UvEdomme si, Şe S je rozŁÍUenÍm T . ZÁmEnou prvnÍch dvou 7len] implikace odvodÍme S|
D y [ f ( x1 , 4 , xn )]
(D
y
Jeli-li T rozŁÍUenÍ teorie T o definice, pak ke kaŞdÉmu modelu M teorie T existuje jednozna7nE ur7enÁ expanze M modelu M, kterÁ je modelem T.
f ( x1 , 4 , xn ))
Z axiomu (12) a MP pak S|
D
y
f ( x1 , 4 , xn )
UkÁzali jsem, Şe T a S jsou ekvivalentnÍ teorie, tedy T je konzervativnÍ rozŁÍUenÍ T . 35
36
Definice funk7nÍho symbolu termem.
PUirozenÉ nÁsobky a numerÁly byly zavedeny pomocÍ term]. M]Şeme se na nE dÍvat nejen jako na zkratky, ale jako na definovanÉ funk7nÍ symboly.
6astÝm pUÍpademdefinice funk7nÍho symbolu je definice „pUedpisem“ v podobE termu.
Definice.
DefinujÍcÍ formule D je tvaru y = t , kde vŁechny promEnnÉ termu t jsou mezi x1 , 4, xn . V takovÉm pUÍpadE jsou podmÍnky existence a jednozna7nosti snadno dokazatelnÉ jen v predikÁtovÉ logice. Existence | D y [t ] ()*
TÍkÁme, Şe T je rozŁÍUenÍm teorie T o definice jestliŞe T vznikne z T kone7nÝm po7tem rozŁÍUenÍ o definice funkcÍ a a predikÁt].
( y ) D tedy | ( y ) D.
t t
Jednozna7nost | y t t t symetrie a tranzitivnosti rovnosti.
y
t je d]sledkem
37
V takovÉm pUÍpadE je T konzervativnÍm rozŁÍUenÍm T a ke kaŞdÉ formuli A teorie T existuje formule A teorie T tako vÁ, Şe T | A A 38
V nÁsledujÍcÍm vÝkladu nebudeme mÍt k disposici vŁechny prostUedky nutnÉ k provedenÍ d]kaz], pokusÍme se je alespoO pUiblÍŞit.
Nerozhodnutelnost, neÚplnost
VÝsledky, kterÉ chceme uvÉst jsou natolik d]leŞitÉ, Şe patUÍ k zÁkladnÍmu kurzu predikÁtovÉ logiky, uvedeme je alespoO bez d]kaz].
Meze formÁlnÍ metody
Nejprve uvedeme nEkterÉ pojmy.
1
MnoŞina k-tic pUirozenÝch 7Ísel je rekurzivnÍ, kdyŞ je rekurzivnÍ jejÍ charakteristickÁ funkce. Pokud mÁ takovÁ mnoŞina nEjakÝ vztah k logice, UÍkÁme takÉ, Şe takovÁ mnoŞina je rozhodnutelnÁ.
(6Áste7nÉ) rekursivnÍ funkce tvoUÍ tUÍdu „efektivnE (algoritmicky) vy7ÍslitelnÝch“ funkcÍ
f : Nk
N
k
2
1
PUibliŞnE Ue7eno, mnoŞina A je rekurzivnÍ, kdyŞ umÍme algoritmicky rozpoznat jejÍ prvky.
zobrazujÍcÍ (podmnoŞiny) mnoŞiny uspoUÁdanÝch k-tic pUirozenÝch 7Ísel do mnoŞiny pUirozenÝch 7Ísel pro nEjakÉ k.
Budeme pracovat s jazyky, kterÉ majÍ kone7nE, nebo spo7etnE speciÁlnÍch symbol], nej7astEji s jazykem aritmetiky. TakovÉ jazyky budeme nazÝvat spo7etnÉ.
Tato tUÍda mÁ pUesnou definici v teorii rekurze.
3
4
Nerozhodnutelnost predikÁtovÉ logiky.
PUedpoklÁdejme, Şe L je spo7etnÝ jazyk a Şe jeho speciÁlnÍ symboly umÍme efektivnE o7Íslovat pUirozenÝmi 7Ísly.
VEta (Church) Nech[ L je spo7etnÝ jazyk prvnÍho UÁdu takovÝ, Şe
PouŞÍvÁme slovo efektivnE mÍsto rekurzivnE, protoŞe jsme rekurzivnÍ funkce zavedli na pUirozenÝch 7Íslech a ne na symbolech.
• obsahuje alespoO jednu konstantu a alespoO jeden funk7nÍ symbol 7etnosti k > 0.
Ve vEtŁinE pUÍpad] budeme uvaŞovat jen jazyky s kone7nE mnoha speciÁlnÍmi symboly.
• pro kaŞdÉ pUirozenÉ 7Íslo n obsahuje spo7etnE mnoho predikÁtovÝch symbol]. Potom mnoŞina
DÁ se ukÁzat, Şe v takovÉm pUÍpadE lze kaŞdÉ formuli A efektivnE pUiUadit pUirozenÉ 7Íslo #A, jejÍ kÓd.
{ #A | A je uzavUenÁ formule a L|= A } nenÍ rozhodnutelnÁ. 5
6
TUi axiomatizace aritmetiky PUedchozÍ vEta byla formulovÁna k ur7itÉmu d]kazu, k nerozhodnutelnosti sta7Í daleko mÉnE speciÁlnÍch symbol].
Jazyk L {0, S , , , } Robinsonova aritmetika Q.
VEta.
Q1 S ( x ) 0
Nech[ L je jazyk prvnÍho UÁdu bez rovnosti, kterÝ obsahuje alespoO dva binÁrnÍ predikÁty,
Q 2 S ( x) Q3 x
potom predikÁtovÁ logika s jazykem L je nerozhodnutelnÁ.
7
S ( y)
0
( y )( x
Q4
x 0
Q5
x S ( y)
x
y
Q6
x 0
Q7
x S ( y)
S ( y )) Q 8
x
0
y
( x y) x ( z )( z
x
y)
x S(x
y) 8
Peanova aritmetika P (prvnÍho UÁdu)
ºplnÁ aritmetika.
MÁ axiomy Q1, Q2, Q4 - Q8 a schema indukce
Je-li N standardnÍ model aritmetiky, ºplnÁ aritmetika mÁ za axiomy vŁechny uzavUenÉ formule pravdivÉ v N.
Pro kaŞdou formuli A a kaŞdou promEnnou x je nÁsledujÍcÍ formule axiom indukce. Ax [0 ]
{( x)( A
Ax [ S ( x)])
Th( N ) { A | A je uzavUenÁ formule
( x) A}
N | A}
TÉto teorii se takÉ UÍkÁ PravdivÁ aritmetika, protoŞe je axiomatizovanÁ vŁemi formulemi, kterÉ jsou pravdivÉ ve standardnÍm modelu N.
DÁ se ukÁzat, Şe v PeanovE aritmetice je dokazatelnÝ axiom Q3, takŞe Peanova aritmetika je rozŁÍUenÍm Robinsonovy aritmetiky.
MnoŞinE formulÍ Th(N) se UÍkÁ teorie modelu N.
DÁ se takÉ dokÁzat, Şe axiomatika Peanovy aritmetiky je rekursivnÍ. 9
MÁme tUi axiomatizace aritmetiky Q , P, Th(N), vŁechny v jazyku L {0, S , , , }. Je zUejmÉ, Şe
Q
P
10
Je-li T teorie s jazykem aritmetiky, m]Şeme definovat mnoŞinu kÓd] vEt teorie T
Th(N )
kde inkluze znamenÁ rozŁÍUenÍ.
Thm (T) = { #A | A je uzavUenÁ formule, T |- A }
• Q mÁ kone7nE mnoho axiom], je tedy rekursivnE axiomatizovatelnÁ.
Podle vEty o uzÁvEru sta7Í se omezit na uzavUenÉ formule.
• P mÁ spo7etnE axiom]. DÁ se ukÁzat, Şe kÓdy axiom] schematu indukce tvoUÍ rekurzivnÍ mnoŞinu, spolu s dalŁÍmi kone7nE mnoha axiomy je P rekurzivnE axiomatizovatelnÁ.
Definice. TÍkÁme, Şe teorie T je rozhodnutelnÁ, je-li mnoŞina Thm(T) (kÓd]) vEt rekurzivnÍ. Jinak je teorie nerozhodnutelnÁ.
• Th(N) podle d]kazu nenÍ rekurzivnE axiomatizovatelnÁ. 11
12
VEta o neÚplnosti aritmetiky. (GÖdel, Rosser)
VEta o nerozhodnutelnosti aritmetiky (Church)
Je-li T bezespornÉ, rekurzivnE axiomatizovatelnÉ rozŁÍUenÍ Robinsonovy aritmetiky Q , potom T nenÍ ÚplnÁ teorie.
Je-li T bezespornÉ rozŁÍUenÍ Robinsonovy aritmetiky Q, potom T je nerozhodnutelnÁ teorie.
13
14
Ozna7enÍ. DruhÁ vEta o neÚplnosti. Je-li T bezespornÉ, rekurzivnE axiomatizovatelnÉ rozŁÍUenÍ Peanovy aritmetiky P a A formule, pÍŁeme
Nech[ T je bezespornÉ rekurzivnE axiomatizovatelnÉ rozŁÍUenÍ Peanovy aritmetiky P , potom
A jako zkratku za formuli Thm(T)(#A)
T | Con (T )
Con(T) jako zkratku za formuli (0=1) Con(T) 7teme T je bezespornÁ (konzistentnÍ).
15
16
Shepherdsonova hUÍ7ka aneb kouzlo nestandardnÍch d]kaz].
PoznÁmka. PUedpoklÁdejme, Şe Peanova aritmetika je bezespornÁ. ProtoŞe
PUedpoklÁdejme, Şe jsme v nEjakÉm nestandardnÍm modelu P , kde existuje nestandardnÍ 7Íslo.
P | Con ( P )
Nech[ A je libovolnÁ formule, potom posloupnost podle vEty o Úplnosti existuje model M |= P, takovÝ, Şe M |= Proof(d, # 0=1) , kde d je 7Íslo d]kazu formule 0 = 1. TakovÉ 7Íslo musÍ bÝt nestandardnÍ.
A
(A
A), A
(A
A) 4 ; 4 ( A
A), A, ( A
A), A, 4
vypadÁ jako d]kaz (libovolnÉ) formule A . Ale nenÍ to d]kaz, protoŞe takovou posloupnost formulÍ nelze kÓdovat ŞÁdnÝm pUirozenÝm 7Íslem danÉho modelu. 17
Zermelo-Fraenkelova teorie mnoŞin ZF mÁ jazyk prvnÍho UÁdu s rovnostÍ, obsahuje Peanovu aritmetiku, mÁ rekuzivnÍ mnoŞinu axiom], tedy je-li ZF bezespornÁ, pak ZF | Con( ZF )
M]Şeme, proto o7ekÁvat jen d]kazy relativnÍ bezespornosti Con ( ZF )
Con ( ZFC )
19
18
