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

• $T\models \phi$ <=> $T⊢\phi$

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ší.

1. Bezesporná teória $T$ (v jazyku L) sa rozšíri na kompletnú Henkinovksú teóriu $T^{\prime }$ (v rozšírenom jazyku L^+)

2. Ku kompletnej Henkinovskej téorii $T^{\prime }$ vezmeme jej kanonickú štruktúru K (platí, že K je model $T^{\prime }$)

3. 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: $f^K(t_1,\dots t_n)=f(t_1,\dots t_n)$ (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: $P^K(t_1,\dots t_n)$ <=> $T⊢P(t_1,\dots t_n)$

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 $t_1{t}_2<=>T⊢t1=t2$.

Platí nasledujúce tvrdenie:

Ak K je kanonická štruktúra pre teóriu T a \varphi je atomická sentencia, tak $K\models \phi$ <=> $T⊢\phi$

Henkinovská teória

Téoria $T$ v jazyku L je Henkinovská, ak pre každú formulu $\phi$ s maximálne jednou voľnou premennou existuje konštanta $c_{\phi }$ v jazyku L, že $T⊢\exists x\phi \to \phi (x/c_{\phi })$

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 $\phi$ platí $K\models \phi$ <=> $T⊢\phi$.

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.