´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
1 / 16
ˇ (o dedukci)
Veta
Bud’ L jazyk, T teorie pro L, ϕ L-sentence a ψ L-formule. Pak
T ` ϕ → ψ ⇔ T ∪ {ϕ} ` ψ.
ˇ (o kompaktnosti)
Veta
´ eˇ kdyˇz kaˇzda´
Bud’ L jazyk, T teorie pro L. Teorie T ma´ model, prav
koneˇcna´ S ⊆ T ma´ model.
ˇ (o korektnosti a uplnosti)
Veta
´
Bud’ L jazyk, T teorie pro L, ϕ L-formule. Pak
T ` ϕ ⇔ T ϕ.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
2 / 16
ˇ (o korektnosti)
Veta
Bud’ L jazyk, T teorie pro L, ϕ L-formule. Pak
T ` ϕ ⇒ T ϕ.
Dukaz.
˚
´
ˇ r´ı se postupneˇ
Indukc´ı dle delky
dukazu.
Oveˇ
˚
T ψ, pro libovoln´y logick´y axiom ψ,
T χ, pro libovoln´y axiom χ ∈ T ,
´ s´ı platnost v T“ (napˇr. pro MP mame:
´
odvozovac´ı pravidla pˇrenaˇ
”
jestliˇze T α a T α → β, pak T β).
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
3 / 16
ˇ (o dedukci)
Veta
Bud’ L jazyk, T teorie pro L, ϕ L-sentence a ψ L-formule. Pak
T ` ϕ → ψ ⇔ T ∪ {ϕ} ` ψ.
Dukaz.
˚
⇒: pouˇzijeme MP
´
⇐: indukc´ı dle delky
dukazu.
˚
Je-li ψ axiom (logick´y, nebo teorie T), plyne T ` ϕ → ψ pomoc´ı MP
´
z v´yrokoveho
axiomu ψ → (ϕ → ψ).
Je-li ψ formule ϕ, pak T ` ϕ → ϕ (pˇr´ıklad z minule´ hodiny).
Je-li ψ odvozena pomoc´ı MP z χ → ψ a χ, pak z indukˇcn´ıho
pˇredpokladu T ` ϕ → (χ → ψ) a T ` ϕ → χ. T ` ϕ → ψ
´
dostaneme pomoc´ı MP z v´yrokoveho
axiomu
(ϕ → (χ → ψ)) → ((ϕ → χ) → (ϕ → ψ)).
Je-li ψ odvozena pomoc´ı generalizace, dukaz
je podobn´y jako pro
˚
´ cnejˇ
ˇ s´ı. (Vynechame
´
pˇr´ıklad MP, pouze technicky naroˇ
ho.)
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
4 / 16
ˇ (o uplnosti)
Veta
´
Bud’ L jazyk, T teorie pro L, ϕ L-formule. Pak
T ϕ ⇒ T ` ϕ.
Lemma
Bud’ ϕ sentence. Jestliˇze (T je bezesporna´ a) T 0 ϕ, pak T ∪ {¬ϕ} je
´
bezesporna.
Dukaz.
˚
ˇ o dedukci a axiomu
Sporem. Z vety
(¬ϕ → ¬ψ) → ((¬ϕ → ψ) → ϕ).
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
5 / 16
ˇ o uplnosti:
Dukaz
vety
˚
´
´
´ pˇr´ıpadeˇ
Staˇc´ı dokazat
pro pˇr´ıpad, kdy ϕ je sentence. V obecnem
´ ım uzav
´ erem.
ˇ
pracujeme m´ısto ϕ s jej´ım generaln´
´ zeme (ekvivalentne)
ˇ T 0 ϕ ⇒ T 2 ϕ.
Ukaˇ
´
´ eˇ T je bezesporna.
´
Pˇredpokladejme
T 0 ϕ. Tedy specialn
´
Z pˇredchoz´ıho lemmatu T ∪ {¬ϕ} je bezesporna.
´ zeme, zˇ e kaˇzda´ bezesporna´ teorie ma´ model.
Ukaˇ
Tedy T ∪ {¬ϕ} ma´ model. Oznaˇcme ho M.
Bezprostˇredneˇ z definic: M T a M ¬ϕ.
Tedy T 2 ϕ.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
6 / 16
Tvrzen´ı (o existenci modelu)
Bezesporna´ teorie ma´ model.
Nav´ıc, pokud T je teorie pro jazyk L a ||L|| definujeme jako
max(ω, |L|), plat´ı, zˇ e existuje model T mohutnosti nejv´ysˇ e ||L||.
(Plyne bezprostˇredneˇ z naˇseho dukazu,
pokud bychom
˚
´
kontrolovali mohutnost jazyka a univerza kanonickeho
modelu.)
Myˇslenky dukazu:
˚
´ materialu.
´
Model, tzv. kanonick´y model, postav´ıme ze syntaktickeho
´
Do jazyka pˇridame
henkinovske´ konstanty - ty se budou chovat jako
ˇ
´ u.
svedci
kvantifikator
˚
´ ım bezespornem
´ henkinovskem
´
Budeme pracovat v maximaln´
´ podaˇr´ı dokazatelnost pˇreloˇzit
rozˇs´ıˇren´ı teorie T - d´ıky tomu se nam
na platnost v modelu.
V pˇr´ıpadeˇ jazyka s rovnost´ı budeme jeˇsteˇ faktorizovat, abychom
zaruˇcili, zˇ e realizac´ı symbolu = je skuteˇcneˇ identita.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
7 / 16
Definice
´ jestliˇze pro kaˇzdou L-formuli ϕ(x)
Teorie T v jazyce L je henkinovska,
ˇ
s nejv´ysˇ e jednou volnou promennnou
x existuj´ı konstantn´ı symboly
´ zˇ e T ` (∃x)ϕ(x) → ϕ(cϕ∃ ) a T ` ϕ(cϕ∀ ) → (∀x)ϕ(x).
cϕ∃ , cϕ∀ ∈ L takove,
Symboly cϕ∃ , cϕ∀ se naz´yvaj´ı henkinovske´ konstanty.
´ ekvivalence (implikace zprava doleva
Pozn.: M´ısto implikac´ı lze psat
´
jsou dokazatelne).
Tvrzen´ı
´ ı
Kaˇzdou bezespornou teorii T v jazyce L lze rozˇs´ırˇit do maximaln´
bezesporne´ henkinovske´ teorie T 0 v jazyce L0 .
Dukaz.
˚
´ ıme.
Technick´y, indukc´ı, neuvad´
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
8 / 16
´ ı bezesporna´ henkinovska´ teorie v jazyce L0 bez
Bud’ T 0 maximaln´
rovnosti. Definujeme kanonickou strukturu A = hA, LA i.
Univerzum A je mnoˇzina vˇsech konstantn´ıch termu˚ (tj. termu˚
ˇ e)
´ jazyka L0 . A je neprazdn
´
´ jelikoˇz
neobsahuj´ıc´ıch promenn
a,
´ eˇ henkinovske´ konstanty.
obsahuje minimaln
Definujme realizace symbolu˚ za jazyka; t0 , . . . , tn−1 jsou konstatn´ı
termy.
Bud’ F funkˇcn´ı symbol: F A (t0 , . . . , tn−1 ) definujeme jako
F (t0 , . . . , tn−1 ).
Bud’ R relaˇcn´ı symbol: definujeme
ht0 , . . . , tn−1 i ∈ R A ⇔ T ` R(t0 , . . . , tn−1 ).
Bud’ c konstantn´ı symbol: definujeme c A = c.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
9 / 16
Lemma
Pro v´ysˇ e uvedene´ T 0 , L0 , A, libovolnou L0 formuli ϕ(x0 , . . . , xn−1 ) a
ohodnocen´ı e plat´ı:
A ϕ(x0 , . . . , xn−1 )[e] ⇔ T 0 ` ϕ(e(x0 ), . . . e(xn−1 )).
Dukaz.
˚
Indukc´ı dle sloˇzitosti formule.
Dusledek
˚
A T 0.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
10 / 16
Dokonˇcen´ı dukazu
– existence modelu pro jazyk bez rovnosti
˚
Zaˇcneme s bezespornou teori´ı T pro jazyk L.
´ ı bezesporne´ henkinovske´ teorie T 0 pro
Rozˇs´ırˇ´ıme ji do maximaln´
jazyk L0 .
Sestroj´ıme kanonick´y model A. Plat´ı A T 0 .
´
My ovˇsem hledame
model teorie T v L, nikoli T 0 v L0 – vezmeme
´
tzv. redukt modelu A do jazyka L (zachovame
univerzum,
´
zachovame
realizace symbolu˚ z L, zapomeneme na realizace
symbolu˚ z L0 − L).
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
11 / 16
Kanonick´y model K = hK , LK i pro jazyk s rovnost´ı
Stejna´ definice jako pro jazyk bez rovnosti, jen nav´ıc celou
strukturu vyfaktorizujeme.
Definujeme relaci ∼ na mnoˇzineˇ A vˇsech konstantn´ıch termu˚
´
ˇ t ∼ s ⇔ T ` t = s.
nasledovn
e:
Relace je zˇrejmeˇ ekvivalence (d´ıky axiomum
˚ rovnosti).
´
Univerzem kanonickeho
modelu bude K = A/ ∼= {[t]; t ∈ A}.
´
Realizace funkˇcn´ıch a relaˇcn´ıch symbolu˚ definujeme na tˇr´ıdach
ekvivalence pomoc´ı reprezentantu˚ (korektn´ı definice d´ıky
axiomum
˚ rovnosti):
h[t0 ], . . . , [tn−1 ]i ∈ R K ⇔ T ` R(t0 , . . . , tn−1 ),
F K ([t0 ], . . . , [tn−1 ]) = [F (t0 , . . . , tn−1 )],
c K = [c].
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
12 / 16
Dukaz
existence modelu pro jazyk s rovnost´ı
˚
ˇ enou
ˇ
Obdobneˇ jako pro jazyk bez rovnosti, jen se zmen
definic´ı
´
kanonickeho
modelu.
ˇ o uplnosti
Konec dukazu
vety
˚
´
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
13 / 16
Lemma
´ eˇ tehdy kdyˇz T je bezesporna´ (= nen´ı sporna).
´
T ma´ model, prav
Dukaz.
˚
´ eˇ dokazan
´
⇐: Prav
e´ tvrzen´ı o existenci modelu.
ˇ
⇒: Sporem. Bud’ T ` ϕ ∧ ¬ϕ pro nejakou
ϕ. Z korektnosti
´ modelu T plat´ı ϕ ∧ ¬ϕ, tedy T nema´
T ϕ ∧ ¬ϕ. Tedy v kaˇzdem
model.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
14 / 16
ˇ (o kompaktnosti)
Veta
´ eˇ kdyˇz kaˇzda´
Bud’ L jazyk, T teorie pro L. Teorie T ma´ model, prav
koneˇcna´ S ⊆ T ma´ model.
Dukaz.
˚
´
´ prav
´ eˇ tehdy kdyˇz
Ekvivalentneˇ staˇc´ı dokazat:
Teorie T je bezesporna,
´
kaˇzda´ koneˇcna´ S ⊆ T je bezesporna.
⇒: Bezprostˇredneˇ z definice.
´
´ tedy T ` ϕ ∧ ¬ϕ pro
⇐: Sporem. Pˇredpokladejme,
zˇ e T je sporna,
’
ˇ
ˇ y.
nejakou
ϕ. Bud d pˇr´ısluˇsn´y dukaz.
Z definice je d konecn
´ Tedy
˚
ˇ
´
je dukazem
v S, pro nejakou
koneˇcnnou S ⊆ T . Tedy S je sporna.
˚
Pˇr´ıklad
´ T libovolneˇ velke´ koneˇcne´ modely, ma´ i nekoneˇcn´y model.
Ma-li
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
15 / 16
Nestandardn´ı pˇrirozena´ cˇ ´ısla
´
Pˇredpokladejme,
zˇ e ZFC je bezesporna´ teorie. Bud’ M jej´ı model.
Pˇridejme do jazyka teorie mnoˇzin novou konstantu L.
Uvaˇzujme teorii T = ZFC ∪ {L ∈ ω} ∪ {L > n; n ∈ N}. (Tato teorie
ˇ s´ı neˇz vˇsechna standardn´ı
o L tvrd´ı, zˇ e je to pˇrirozene´ cˇ ´ıslo vetˇ
pˇrirozena´ cˇ ´ısla.)
´ Zˇrejmeˇ muˇ
Bud’ S ⊆ T koneˇcna.
˚ zeme ve struktuˇre M realizovat
ˇ e´ dostateˇcneˇ
konstantu L tak, aby M S. (Realizac´ı bude nejak
velke´ pˇrirozene´ cˇ ´ıslo – prvek ω.)
Z kompaktnosti existuje model teorie T . Realizac´ı konstanty L v
tomto modelu je nestandardn´ı pˇrirozene´ cˇ ´ıslo.
()
´ a´ logika - pˇrednaˇ
´ ska 3
Predikatov
6. 1. 2015
16 / 16
Download

Predikátová logika