Logika a výpočtová složitost
Obsah
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 \vDash \varphi $ <=> $ T \vdash \varphi $
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 $ T $ (v jazyku L) sa rozšíri na kompletnú Henkinovksú teóriu $ T^\prime $ (v rozšírenom jazyku L^+)
- Ku kompletnej Henkinovskej téorii $ T^\prime $ vezmeme jej kanonickú štruktúru K (platí, že K je model $ T^\prime $)
- 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 \vdash 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 \vdash t1 = t2 $.
Platí nasledujúce tvrdenie: Ak K je kanonická štruktúra pre teóriu T a \varphi je atomická sentencia, tak $ K \vDash \varphi $ <=> $ T \vdash \varphi $
Henkinovská teória
Téoria $ T $ v jazyku L je Henkinovská, ak pre každú formulu $ \varphi $ s maximálne jednou voľnou premennou existuje konštanta $ c_\varphi $ v jazyku L, že $ T \vdash \exists x \varphi \rightarrow \varphi(x/c_\varphi) $
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 $ \varphi $ platí $ K \vDash \varphi $ <=> $ T \vdash \varphi $.
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.
