Zdroje
Asi nejlepsi zdroj pro tenhle zkusebni okruh jsou skripta Petra Stepanka. Prakticky kapitolu od kapitoly kopiruji pozadavky - nejspis je psal Stepanek podle svych skript. Vyborny dalsi zdroj su Gregorove skripta. Tie maju vyhodu, ze popisuju aj SLD rezoluciu a unifikaciu, co sa zide pri neprocku.
Neformalny nadhlad
Je doelzite si uvedomit, ze ako mame dva strany mince platnost a dokazatelnost - tak ta dolezita vec je platnost. My v matematike stale chceme vediet ci nieco plati v danej strukture.
V konecnych strukturach a v konecnych triedach koencnych sturktur vieme platnost odvodit pomocou "tabulky" (vycet konecneho poctu pripadov). U vacsinou struktur(modelov) to uz take lahke nie je. Preto sme vytvorili kalkulus, ktory dokaze pomocou par syntaktickych pravidiel odvodit veci a sformovat dokaz, ktory je korektny (to, co vieme pomocou tohto syntaktickeho dokazu odvodit, naozaj plati).
Veta o korektnosti teda indukciou podla dlzky dokazu dokazuje, ze co sme odvodili, to fakt plati. Naskyta sa ale aj dalsia otazka: ked nieco plati v nejakom modeli, vieme sformulovat dokaz, ktory to dokazuje? (pripominam, ze dokaz z definicie musi byt konecny, to znamena, ze teoreticky staci geenrovat vsetky konecne stringy a skusat, ci su validnym dokazom tvrdeni). Tu ale naraza kosa na kamen. Casto sa stava, ze nejake tvrdenie v strukture plati, ale neda sa to nijak dokazat (ani prechodom cez vsetky dokazy).
Plati ale aspon pomerne uspokojujuca verzia, tzv. Veta o uplnosti, ktora hovori, ze ked nieco plati VO VSETKYCH MODELOCH, tak sa to da dokazat.
Úplnosť predikátovej logiky
Silná úplnosť predikátovej logiky sa dá formulovať dvomi spôsobmi:
T je bezesporná <=> T má model
<=>
Korektnosť je implikácia sprava doľava a úplnosť zľava doprava. Dokážeme tvrdenie T je bezesporná => T má model.
Idea je jednoduchá, dôkaz, že to funguje je zložitejší.
Bezesporná teória (v jazyku L) sa rozšíri na kompletnú Henkinovksú teóriu (v rozšírenom jazyku L^+)
Ku kompletnej Henkinovskej téorii vezmeme jej kanonickú štruktúru K (platí, že K je model )
Redukt štruktúry K na pôvodný jazyk L je model teórie T
Popíšeme trochu podrobnejšie pojmy a myšlienky, ktoré sme použili.
Kanonická štruktúra
Pre daný jazyk L, ktorý obsahuje aspoň jeden konštantný symbol, môžme uvažovať množinu všetkých jeho konštantných termov K. Napríklad, ak máme v jazyku jednu konštantu c a jeden unárny funkčný symbol f tak K = {c,f(c),f(f(c)),...}. Konštantnú štruktúru K pre téoriu T v jazyku L skonštruujeme tak, že vezmeme množinu konštantných termov K a definujeme realizáciu funkčných a predikátových symbolov nasledovne:
f je funkčný symbol jazyka L: (je dôležité si uvedomiť, že na ľavej strane f predstavuje názov symbolu, ktorý ako argumenty dostáva prvky nosnej množiny, na pravej strane stojí jediný prvok nosnej množiny)
P je predikátový symbol L: <=>
Ak sme v logike bez rovnosti, tak konštantná štruktúra ja rovno kanonickou. V logike s rovnosťou sa ešte konštantná štruktúra musí vyfaktorizovať podľa ekvivalencie .
Platí nasledujúce tvrdenie:
Ak K je kanonická štruktúra pre teóriu T a \varphi je atomická sentencia, tak <=>
Henkinovská teória
Téoria v jazyku L je Henkinovská, ak pre každú formulu s maximálne jednou voľnou premennou existuje konštanta v jazyku L, že
Veta: Každá bezesporná téoria T sa dá rozšíriť na kompletnú Henkinovskú téoriu.
Dôkaz: netriviálny
Veta: Ak T je kompletná Henkinovská teória a K je jej kanonická štruktúra, tak pre každú sentenciu platí <=> .
Dôkaz: Indukciou podľa zložitosti formule. Pre atomické formule to platí pre ľubovoľnú teóriu, v indukčnom kroku sa využíva kompletnosť a Henkinovskosť téorie, nie je to triviálne.
Dôsledok: Kanonická štruktúra pre kompletnú Henkinovskú teóriu T je modelom T.