Logika a výpočtová složitost

Z ωικι.matfyz.cz
Přejít na: navigace, hledání

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

  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 \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.