Obsah

Zadání

10. Základní typy důkazů

Zadání této otázky je poněkud nejasné.

Vypracovanie

Michalův komentář

prof. Zlatuška mi k tejto otázke poradil:

- materiály k Types and Proofs: http://www.paultaylor.eu/stable/prot.pdf - povědomí o různých formálních systémech pro konstrukci důkazů:
- Hilbertův systém (viz Kleeneho metamatematika, ale je v řadě jiných), Gentzenova přirozená dedukce (viz Girard), tabla (viz např Smullyan nebo Nerode), rezoluce, atd. (asi netreba všetky, ale mať o tom povedomie)
- to google: „Proof calculus“ nebo „Proof systems“ (ale vynechte system ve smyslu počítačového systému).

Ešte môžeme tušiť, čo sa vlastne po nás chce odtiaľto: 3. otázka: http://www.fi.muni.cz/studies/szz/mgr_info.xhtml#teoreticka

Tento text předpokládá, že čtenář má nějaké obecné (byť matné) povědomí o výrokové a predikátové logice. Snaží se přitom dát tyto znalosti dohromady a poskytnout souvislosti.

Úvod nemá cenu se učit, spíše jen přečíst – je to úvaha o významu logiky pro matematiku (navíc určitě zkreslená autorovým vnímáním). Celkově je ta teorie kolem matematiky, formální logiky, Hilbertova programu a dalších věcí poměrně značně složitá.

Úvod

Logika studuje způsob vyvozování závěrů z předpokladů. Důkaz je pak popis jednoho konkrétního odvození závěrů z předpokladů. V zásadě by mělo platit, že závěry už jsou obsažené v předpokladech (to, že 5+3=8, je jasně dáno aritmetikou přirozených čísel), jinak je při vyvození použita nějaké dodatečná informace – závěr nevychází z předpokladů. Na druhou stranu to neznamená, že je důkaz jako takový není užitečný – objasňuje, jakým způsobem jsme z předpokladů k závěru došli. Můžeme se na něj taky dívat jako na zkratku – pokaždé, když potřebujeme ověřit, že dané tvrzení platí, můžeme se na něj podívat. Z toho taky vychází základní pravidlo neformálních důkazů (a většinu důkazů provádíme neformálně) – důkaz je tak detailní, aby mu ten, komu je určen, rozuměl.

Formální logika studuje vyvozování jako práci se symboly popisující abstraktní modely založené na matematice. S matematikou je úzce svázána – to je dáno především historicky: formální logika je výsledkem snahy vyjasnit a formalizovat základy matematiky (v jistém smyslu se na ni můžeme dívat jako na normu) – způsob, jakým uvažovat o matematických strukturách. Jedná se především o to, abychom byli schopni pomocí konečného procesu schopni vytvořit platné úsudky o nekonečných strukturách.

Tato snaha probíhala v první polovině dvacátého století. Jejím cílem bylo vytvořit formální jazyk, ve kterém by bylo možné zapsat všechna matematická tvrzení, a definovat způsob, jakým je s ním možné manipulovat tak, aby z malé množiny předpokladů bylo možné odvodit celou matematiku a algoritmicky rozhodnout, jestli dané tvrzení platí (více viz Hilbertův program). Gödel později ukázal, že toto není možné (viz níže), přesto je logika důležitá, protože poskytuje jazyk pro práci s matematickými tvrzeními a návod, jak v něm vyvozovat důsledky.

Formální logické systémy

Pokud definujeme formální logický systém, typicky máme následující (tento popis vychází z predikátové logiky):

  1. Abecedu – konečnou množinu symbolů, které můžeme použít. Typicky je můžeme rozlišit na:
    1. Logické symboly (občas také metajazyk) – symboly, které mají pouze logický význam (výrokové spojky, kvantifikátory).
    2. Mimologické symboly – symboly, které spojují logiku s tím, co modeluje, tj. jsou důležité pro sémantiku. V nich ještě typicky rozlišujeme proměnné, které můžou nabývat různých hodnot.
  2. Syntax – gramatiku určující, co jsou dobře utvořené formule. Typicky požadujeme, aby byla rozhodnutelná. Nejčastěji se proto používají bezkontextové gramatiky, takže formule typicky má svůj syntaktický strom1).
  3. Modely – třídu matematických struktur, které logika popisuje.
  4. Sémantiku – funkci přiřazující logickým formulím pravdivostní hodnotu. Souvisí přitom s interpretací formule na modelu.
  5. Odvozovací systém – soubor pravidel, která popisují, jak manipulovat s dobře utvořenými formulemi tak, abychom dostali formule, které jsou pravdivé.

Sémantika

Sémantika dobře utvořené formule je svázána s modely – matematickými strukturami. Proto, abychom mohli určit její pravdovostní hodnotu, musíme v ní obsažené mimologické symboly nějakým způsobem namapovat na matematické struktury, což bývá součástí modelu. Zvláštní místo mají proměnné, kterým můžou být objekty modelu přiřazeny nezávisle, o což se stará funkce valuace. Rozlišujeme pak tři možnosti:

  1. formule je splněna pro konkrétní model a valuaci,
  2. formule je splněna pro konkrétní model a všechny možné valuace (\mathcal{M}\models\varphi),
  3. formule je splněna pro všechny možné modely a všechny valuace – je tautologie. Píšeme \models\varphi.

Zavádíme také relaci vyplývání. Formule \varphi je sémantickým důsledkem množiny formulí (teorie) T, psáno T\models\varphi pokud v každém modelu splňujícím všechny formule z T (také model teorie T) je splněna \varphi.

Odvozovací systém

Sémantika svazuje formule s potenciálně nekonečnými matematickými objekty. Navíc udává pravdivostní hodnotu pouze pro jeden model (a jednu konkrétní evaluaci). Matematiku ale zajímají především obecně platné věty, popřípadě věty, které vyplývají z jiných. To však obnáší pravdivost pro velké, často nekonečné množství modelů. Člověk přitom není schopný s aktuálním nekonečnem pracovat.

Odvozovací systém se ideálním, nekonečným strukturám vyhýbá zavedením čistě syntaktické procedury – přepisováním symbolů – která modeluje vyvozování, abstraktní myšlenkovou činnost. Nenechte se mýlit, odvozovací systém musí odpovídat sémantice logiky, jeho operace však neobnáší žádnou práci s modely. Odvozovací systém je tedy nástrojem pro tvorbu důkazů.

Důkaz je posloupnost platných tvrzení (formulí), které končí tvrzením, které chceme dokázat, a dané tvrzení v posloupnosti vždy lze vyvodit z těch nalevo. Vyvozování se děje pomocí odvozovacích pravidel, která určují, jak z jednoho nebo více platných tvrzení odvodit další platné tvrzení. Samozřejmě je třeba od něčeho začít, proto jsou jeho součástí ještě axiomy. Axiomy i odvozovací pravidla jsou přitom závislá na sémantice logiky. Kromě toho mezi axiomy můžeme zahrnout další předpoklady.

Důkaz

Nechť T je množina formulí (teorie). Důkaz formule \psi z předpokladů T je konečná posloupnost2) \varphi_1,\ldots,\varphi_n=\psi, kde pro každé i platí jedno z následujících:
  1. \varphi_i\in T,
  2. \varphi_i je jeden z axiomů,
  3. \varphi_i vznikne aplikací jednoho z odvozovacích pravidel na některé z formulí \varphi_1,\ldots,\varphi_{i-1}.

Pokud existuje důkaz \varphi z T (formule je dokazatelná z T), píšeme T\vdash\varphi.

Požadujeme, aby odvozovací systém splňoval následující vlastnosti:

Poznamenejme, že pokud je odvozovací systém úplný, je částečně rozhodnutelný (rekurzívně vyčíslitelný), protože můžeme generovat platná tvrzení tak dlouho, dokud nenarazíme na vstupní tvrzení.

Bezespornost je poměrně jednoduché dokázat – stačí ukázat, že axiomy jsou platné formule (na základě jejich sémnatiky) a že odvozovací pravidla zachovávají platnost. Dokázat úplnost systému a nebo najít rozhodovací algoritmus už je značně komplikovanější.

Výroková logika

Výroková logika je poměrně jednoduchý systém s omezenou vyjadřovací silou, na kterém jsou ale postaveny všechny ostatní logické systémy. To je dáno dvěmi věcmi:

  1. Má bezesporný, úplný a rozhodnutelný odvozovací systém (což v zásadě vyplývá z druhé vlastnosti).
  2. Zabývá se pouze pravdivostními hodnotami.

Výroková logika nemá jiné mimologické výrazy než proměnné a jejím jediným modelem jsou dvě pravdivostní hodnoty3). To zároveň znamená, že lze použít společně s jakýmikoli jinými logickými konstrukcemi (které mají definovanou sémantiku).

Poznámka: Občas se označení „výroková logika“ používá logiku s predikáty a spojkami výrokové logiky. V tomto případě se nejedná o výrokovou logiku, ale prvořádovou logiku bez kvantifikátorů. Ve výrokové logice nás zajímají pouze pravdivostní hodnoty, nespojeme ji s žádnými soubory prvků a podobnými věcmi.

Syntax výrokové logiky

\varphi::=X \mid \neg\varphi  \mid \varphi_1\lor\varphi_2 \mid \varphi_1\land\varphi_2\mid \varphi_1\to\varphi_24) Jazykem výrokové logiky jsou konečná množina výrokových proměnných, logické spojky a závorky5).

Sémantika výrokové logiky je dána funkcí valuace (také pravdivostního ohodnocení), která každé proměnné přiřadí pravdivostní hodnotu – 0 nebo 1. Ta lze rozšířit na výrokové spojky. Zde toto rozšíření definujeme úplným výčtem:

Sémantika výrokové logiky

\begin{array}{|r|cc|c|} 
\hline 
\psi&v(\varphi_1)&v(\varphi_2)&v(\psi)\\\hline 
\neg\varphi_1&0&&1\\ &1&&0\\\hline 
\varphi_1\lor\varphi_2&0&0&0\\ &0&1&1\\ &1&0&1\\ &1&1&1\\\hline 
\varphi_1\land\varphi_2&0&0&0\\ &0&1&0\\ &1&0&0\\ &1&1&1\\\hline 
\varphi_1\to\varphi_2&0&0&1\\ &0&1&1\\ &1&0&0\\ &1&1&1\\\hline 
\end{array}

Logika vychází z přirozeného jazyka, a logické spojky v zásadě odpovídají svému významu v přirozeném jazyce. Je dobré si ale pamatovat, že pokud je antecendent implikace (formule na levé straně) nepravdivá, implikace je pravdivá.

Formule \varphi je pro valuaci v pravdivá, pokud v(\varphi)=1, je splnitelná, pokud existuje valuace v' taková, že v'(\varphi)=1 a je logicky pravdivá (tautologie, často pouze „pravdivá“), pokud je pravdivá pro libovolnou valuaci. Formule je logickým důsledkem množiny formulí T, psáno T\models\varphi právě tehdy pokud pro každou valuaci, pro kterou jsou pravdivé všechny formule v T je pravdivá \varphi.

Plnohodnotnost systému výrokových funkcí

Pokud máme logickou formuli obsahující n různých proměnných, určuje nární funkci na pravdivostních hodnotách. Triviálně logické spojky určují výrokové funkce. Systém výrokových funkcí je plnohodnotný, pokud pomocí nich lze vyjádřit libovolná výroková funkce, a tedy v zásadě libovolná formule. Lze dokázat, že systémy \mathcal{L}(\neg,\lor), \mathcal{L}(\neg,\land) nebo \mathcal{L}(\neg,\to) jsou plnohodnotné. Proto se často definuje sémantika jen některou z dvojice spojek a ostatní se berou jako zkratky (syntaktický cukr).

Normální formy

Normální formy jsou standardní zápisy formulí. Jsou tvořeny:

  1. literály, což je formule nebo její negace,
  2. klauzulemi, což je disjunkce (\lor) více literálů,
  3. duálními klauzulemi, což je konjunkce (\land) více literálů.

Rozlišujeme:

  1. konjunktivní normální formu (CNF), což je konjunkce více klauzulí,
  2. disjunktivní normální formu (DNF), což je disjunkce více duálních klauzulí.

Přitom platí, že každá formule lze zapsat v každé normální formě (jinak by to nebyla normální forma).

Disjunktivní normální forma je jednoznačná pro danou formuli, až na pořadí klauzulí a literálů uvnitř (duálních) klauzulí. Když ji srovnáme s tabulkami logických funkcí, lze ji zapsat jako disjunkci všech řádků, které dávají za výsledek jedničku. Rozhodnout splnitelnost formule v DNF je lineární – stačí najít (duální) klauzuli, kde není zároveň proměnná a její negace.

Konjunktivní normální forma není jednoznačná a rozhodnout splnitelnost formule v CNF je v NP. To může znít neintuitivně, ale pokud máme formuli v CNF a přepíšeme ji do DNF, může dojít až k exponenciálnímu zvětšení formule.

Odvozovací systém

Výroková logika má jednu zásadní výhodu: je bezesporná, úplná a rozhodnutelná (byť rozhodnutelnost je v NP), respektive, existuje odvozovací systém, který je úplný a bezesporný. Její odvozovací systém je proto použit jako základ odvozovacích systémů pro všechny vyšší logiky (včetně například modálních logik). Proto jej uvedeme až u predikátové logiky.

Predikátová logika prvního řádu

Predikátová logika prvního řádu (nebo také prvořádová logika) rozšiřuje výrokovou logiku o kvantifikaci (která v zásadě vychází z Aristotelových sylogismů). Tím se ale váže na nějaké, potenciálně nekonečné soubory objektů. Predikátová logika je důležitá, protože formalizuje základy jazyka matematiky – pokud chceme nějaké tvrzení zapsat formálně, nejčastěji použijeme jazyk prvořádové logiky (nebo jejích víceřádových variant) – i když sémantika tvrzení nutně nemusí odpovídat sémantice predikátové logiky.

Modelem predikátové logiky je nějaký soubor objektů (množina). Predikátová logika je založena na predikátech, které přiřazují objektům nebo n-ticím objektů pravdivostní hodnoty. Ty tedy odpovídají množinám a relacím((Setkáváme se zde s problémem slepice a vejce – chceme nadefinovat logiku v termínech teorie množin a na druhé straně bychom chtěli nadefinovat teorii množin pomocí axiomů, tedy logických formulí. V zásadě lze říct, že teorie množin a predikátová logika jsou velmi úzce svázány, obojí jsou to základy matematiky.)).

Jazyk

Jazyk \mathcal{L} je systém predikátových a funkčních symbolů, přičemž každému je přiřazena arita – nezáporné celé číslo (můžou tedy existovat i nulární predikátové symboly – true a false – a nulární funkční symboly – konstanty).
Jazyk s rovnostní obsahuje navíc binární predikátový symbol =, který bude mít speciální sémantiku (identitu).

Například jazyk teorie grup jsou symboly (multiplikativní zápis) (\cdot,1,^{-1}) s aritami 2,0,1 (pro znalé: ano, to je definice podle univerzálních algeber – teorie grup ale taky lze zapsat například pouze se symbolem \cdot).

Abeceda prvořádové logiky obsahuje:

Abeceda prvořádové logiky pro jazyk \mathcal{L} dále obsahuje predikátové a funkční symboly jazyka \mathcal{L}.

Syntax prvořádové logiky rozlišuje dva typy struktur:

  1. termy, které se týkají modelů predikátové logiky,
  2. formule, které pracují s pravdivostními hodnotami.

Term

Term jazyka \mathcal{L} je6):
  1. proměnná,
  2. f(t_1,\ldots,t_n) kde f je n-ární funkční symbol jazyka \mathcal{L} a t_1,\ldots,t_n jsou termy.

Term je uzavřený, pokud neobsahuje žádné proměnné (tedy musí obsahovat nějaké nulární funkční symboly – konstanty).

Termem teorie grup je například (x\cdot y)^{-1}. Uzavřeným termem je například (1\cdot 1)^{-1}.

Formule

Formule prvořádové logiky jazyka \mathcal{L} je definována induktivně7) jako:
  1. P(t_1,\ldots,t_n) ke P je n-ární predikátový symbol jazyka \mathcal{L} a t_1,\ldots,t_n jsou termy,
  2. \neg\varphi, kde \varphi je formule,
  3. \varphi\to\psi, kde \varphi a \psi jsou formule,
  4. \forall x\varphi nebo \exists x\varphi, kde x je proměnná a \varphi je formule.

Existenciální kvantifikátor se typicky také definuje pomocí syntaktické zkratky \exists x\varphi\equiv\neg\forall x\neg\varphi. Pro zpřehlednění zápisů formulí se v praxi další konvence. Například široce rozšířený zápis \exists x\in Z.\varphi je zcela formálně zapsán \exists x(x\in Z\to\varphi).

Volné a vázané proměnné

Pro definici sémantiky musíme rozlišit volné a vázané proměnné, přičemž vázané proměnné jsou ty, které jsou kvantifikované. Formálně mluvíme o tom, jestli je daný výskyt proměnné ve formuli volný, nebo vázaný (nemůže být obojí):

  1. všechny výskyty proměnných v termech predikátu jsou volné,
  2. ve formuli \forall x\varphi nebo \exists x\varphi jsou všechny výskyty proměnné x v \varphi vázané.

Jinak spojky zachovávají volnost a vázanost. Proměnná je volná (vázaná) ve formuli pokud je nějaký z jejích výskytů ve formuli volný (vázaný) – proměnná tedy může být zároveň volná i vázaná (ale její konkrétní výskyty ne). Například ve formuli Q(x)\to\forall x P(x) je proměnná x volná i vázaná, protože její první výskyt je volný a její druhý výskyt vázaný.

Pro formuli můžeme použít zápis \varphi(x_1,\ldots,x_n), kde všechny volné proměnné v \varphi jsou mezi x_1,\ldots,x_n. Pokud formule neobsahuje volné proměnné, je uzavřená (takovým formulím se také říká sentence8)), jinak je otevřená. Pokud chceme z otevřené formule udělat uzavřenou, typicky se to dělá pomocí univerzálního uzávěru, tedy \forall x_1\ldots\forall x_n\varphi(x_1,\ldots,x_n), což zachovává pravdivostní hodnotu formule (viz níže).

Substituce

Zápisem \varphi[t/x]9) značíme formuli \varphi, kde jsou všechny volné výskyty proměnné x (textově) nahrazeny termem t. Term je substituovatelný za proměnnou, jestliže se žádný výskyt jakékoli proměnné v termu nestane po substituci vázaný.

Tedy například term y+z není substituovatelný za y v termu \forall z(x+y=z). Typicky používáme vícenásobnou (souběžnou) substituci značenou \varphi[t_1/x_1,\ldots,t_n/x_n].

Sémantika

Predikátová logika operuje s množinami (soubory prvků), potřebujeme tedy nějakým způsobem svázat proměnné a daný jazyk s nějakou množinou.

Realizace

Realizace (model, také interpretace) \mathcal{M} jazyka \mathcal{L} je dána:
  1. Neprázdným souborem prvků (individuí) M – univerzem (také nosičem).
  2. Přiřazením n-ární relace P_{\mathcal{M}}\subseteq M^n každému n-árnímu predikátovému symbolu P.
  3. Přiřazením n-ární funkce f_{\mathcal{M}}:M^n\to M každému n-árnímu funkčnímu symbolu f.

Ještě je potřeba přiřadit význam proměnným. V prvořádové logice proměnné zastupují jednotlivé prvky univerza (narozdíl například od druhořádové logiky – viz níže).

Valuace

Pro danou realizaci je valuace (ohodnocení) funkce přiřazující každé proměnné prvek univerza (M).

Sémantika dané formule pak pracuje s těmito pojmy.

Sémantika prvořádové logiky

Nechť \mathcal{M} je realizace \mathcal{L}, e valuace a \varphi formule prvořádové logiky nad \mathcal{L}.

Realizace termu t[e] je definována induktivně (podle definice termu):

  1. x[e]=e(x),
  2. f(t_1,\ldots,t_n)[e]=f(t_1[e],\ldots,t_n[e]).

Relace splněnosti formule realizací a valuací je definována induktivně10):

  1. \mathcal{M}\models P(t_1,\ldots,t_n)[e]\iff(t_1[e],\ldots,t_n[e])\in P_{\mathcal{M}},
  2. \mathcal{M}\models (\neg\varphi)[e]\iff \mathcal{M}\not\models\varphi[e],
  3. \mathcal{M}\models (\varphi\to\psi)[e] právě tehdy, když \mathcal{M}\models\psi[e] nebo \mathcal{M}\not\models\varphi[e],
  4. \mathcal{M}\models (\forall x\varphi)[e] právě tehdy, když \mathcal{M}\models\varphi[e[a/x]] pro každý a\in M.
  5. \mathcal{M}\models (\exists x\varphi)[e] právě tehdy když \mathcal{M}\models\varphi[e[a/x]] pro nějaký a\in M.

Pokud je \mathcal{L} jazyk s rovností, platí \mathcal{M}\models(t_1=t_2)[e] pouze tehdy, označují-li t_1[e] a t_2[e] stejná individua.

Říkáme, že \varphi je pravdivá v \mathcal{M}, pokud \mathcal{M}\models\varphi[e] pro libovolnou valuaci e.

Všimněme si několika věcí. Zaprvé, formule je pravdivá v dané realizaci, pokud je pravdivá pro všechna možná ohodnocení. To se podobá sémantice univerzálního kvantifikátoru, a tedy univerzální uzávěr (viz výše) zachovává pravdivostní hodnotu. Za druhé, je třeba si všimnout role valuace v definici kvantifikátorů. Zatřetí, vezměme na vědomí jazyk, kterým sémantiku prvořádové logiky definujeme. Na rozdíl od výrokové logiky ji nemůžeme definovat úplným výčtem možností, a tedy musíme použít přirozený jazyk, protože nemáme žádný jiný formalismus pomocí kterého bychom sémantiku definovali. To v zásadě posiluje význam logiky jako standardu – stále ještě musíme vysvětlit v přirozeném jazyce, co tím myslíme. Na druhou stranu, odvozovací systém je vyloženě syntaktická záležitost, kterou lze vysvětlit pouze přepisováním slov (samozřejmě musíme v přirozeném jazyce vysvětlit, co to je „přepisování“).

Teorie

Pro relaci sémantického vyplývání je důležitý pojem teorie. Pro jazyk \mathcal{L} (všechny predikátové formule se musí vztahovat k nějakému jazyku, narozdíl od výrokových) je teorie T soubor formulí (i nekonečný) – axiomů teorie. Realizace \mathcal{M} je modelem teorie T jestliže \mathcal{M}\models\varphi pro každou \varphi\in T. Pokud pro danou teorii model existuje, říkáme, že je splnitelná. Formule \varphi je sémantickým důsledkem teorie T, psáno T\models\varphi právě tehdy, když je \varphi pravdivá v každém modelu teorie.

Vezměme si výše zmíněný jazyk teorie grup, symboly (\cdot,1,^{-1}) s aritami 2,0,1. Axiomy této teorie jsou (zřejmě používáme jazyk s rovností):

Jakákoli (číselná) množina s vhodným přiřazením operací je modelem teorie grup právě tehdy, když splňuje výše uvedené axiomy. Příkladem může být množina celých čísel s operací sčítání, nulou přiřazenou symbolu 1 a změnou znaménka místo operace </math>^{-1}</math>. Existují ale i jiné modely této teorie (i konečné – modulární aritmetika).

Pojem teorie má v matematice zásadní význam. Typicky máme nějakou soustavu axiomů (například axiomatická teorie množin), ze které se snažíme odvodit další tvrzení. Samozřejmě, problém je, že nestačí ukázat, že tvrzení platí jen na jednom konkrétním modelu dané teorie. Je nutné ukázat, že platí pro všechny možné modely, kterých může být nekonečně mnoho. Proto existují odvozovací systémy.

Odvozovací systémy prvořádové logiky

Jak už bylo zmíněno výše, odvozovací systém se skládá z:

  1. axiomů, což jsou logicky platné formule (tj. platné na všech modelech),
  2. odvozovacích pravidel, která převádějí platné formule na platné formule.

Důkaz je pak řetěz platných tvrzení, kde začínáme z axiomů nebo předpokladů a aplikujeme na ně odvozovací pravidla dokud nedostaneme formuli, kterou chceme. Většina odvozovací systémů prvořádové logiky vychází z odvozovacích systémů výrokové logiky, které rozšiřují o pravidla (nebo axiomy) pro práci s kvantifikátory. To je logické, protože dokázat bezespornost odvozovacích systémů výrokové logiky je velmi jednoduché (výroková logika je rozhodnutelná – úplným výčtem pravdivostních hodnot) a tato bezespornost se přenáší do vyšších logik. Odvozovací systémy výrokové logiky tedy vypadají stejně jako níže uvedené, pouze se vypustí axiomy a pravidla pracující s kvantifikátory.

To, že formule \varphi je dokazatelná z množiny předokladů T (teorie) zapisujeme T\vdash\varphi. Teorie je sporná (inkonzistentní), pokud z ní lze dokázat libovolnou formuli jazyka prvořádové logiky.

Modus Ponens

Existuje celá řada odvozovacích systémů. Většina z nich obsahuje odvozovací pravidlo modus ponens (také eliminace implikace), které vychází z jednoduchého principu: Pokud z A vyplývá B a A platí, platí také B.

Modus Ponens

\{\varphi\to\psi,\varphi\}\vdash\psi

Typicky pro odvozovací systémy platí důležitá věta, věta o dedukci.

Věta o dedukci

T,\varphi\vdash\psi\iff T\vdash\varphi\to\psi

Tato věta formalizuje princip, jakým se běžně vede většina důkazů, kdy vybereme jeden předpoklad a dokazujeme implikaci. Podle toho, jakým způsobem se postupuje, rozlišujeme:

Hilbertovský odvozovací systém

Tento odvozovací systém má především teoretický význam – typicky se používá k důkazům (meta)tvrzení o prvořádové logice. Má relativně malé množství axiomů – respektive, používá relativně malé množství schemat axiomů (axiomů jako takových je nekonečně mnoho), a malé množství odvozovacích pravidel. Prakticky se k vytváření důkazů používá poměrně špatně, protože je obtížné z axiomů dojít k požadovanému tvrzení. Skládá se z následujících axiomatických schemat:

  1. \varphi\to(\psi\to\varphi)\quad pro libovolné \varphi,\psi,
  2. (\varphi\to(\psi\to\xi))\to((\varphi\to\psi)\to(\varphi\to\xi))\quad pro libovolné \varphi,\psi,\xi (distribuce implikace),
  3. (\neg\varphi\to\neg\psi)\to(\psi\to\varphi)\quad pro libovolné \varphi,\psi (obměna implikace),
  4. \forall x\varphi\to\varphi[t/x]\quad, kde t je substituovatelný za x v \varphi (axiom specifikace),
  5. (\forall x(\varphi\to\psi))\to(\varphi\to\forall x\psi)\quad, kde x nemá volný výskyt ve \varphi (axiom distribuce),

a dvou odvozovacích pravidel, modu ponens a pravidla generalizace:

Navíc, pokud jazyk obsahuje rovnost, přidávají se ještě axiomy rovnosti (existuje více možných formulací):

  1. x=x
  2. (x=y)\to(\varphi[x/z]\to\varphi[y/z])

Pro pohodlí si typicky budeme definovat další schemata axiomů (například \varphi\to\neg\neg\varphi), které odvodíme už z existujících axiomů.

Tento odvozovací systém je bezesporný (což lze ověřit jednoduše) a úplný (což poprvé dokázal Gödel).

Přirozená dedukce

Systémy přirozené dedukce se oproti velmi formálnímu Hilbertovskému systému (se kterým je problém v praxi něco dokázat) snaží důkaz přiblížit tomu, jak přirozeně usuzujeme. Mívají minimum axiomů a oproti tomu hodně odvozovacích pravidel. Je také typické, že pro každou logickou spojku mají pravidlo, které ji zavádí a pravidlo, které ji eliminuje.

Následuje zjednodušený model Gentzenova sekvenčního kalkulu. Používá pouze jeden axiom:

T,\varphi\vdash\varphi

a velké množství odvozovacích pravidel:

Rezoluce

Problémem výše uvedených odvozovacích systémů je, že existuje mnoho různých axiomů nebo odvozovacích pravidel. Rezoluce používá pouze jedno pravidlo – rezoluční pravidlo, založené na odvození \frac{\varphi\lor\psi,\neg\varphi\lor\xi}{\psi\lor\xi}. Vyžaduje přitom, aby formule (jak teorie, tak dokazovaná formule) byly zapsány v CNF. Rezoluce je široce používaná především v logickém programování a automatickém dokazování.

Rezoluční pravidlo

\frac{a_1\lor\ldots\lor a_n\lor c, b_1\lor\ldots\lor b_m\lor \neg c}{a_1\lor\ldots\lor a_n\lor b_1\lor\ldots\lor b_m} Kde a_1,\ldots,a_n,b_1,\ldots,b_m,c jsou literály. Důsledku dvou klauzulí (nahoře) se říká rezolventa (dole).

Rezoluční důkaz – nebo spíše vyvrácení – je založené na důkazu sporem. Nejprve je nutné převést všechny axiomy teorie a negaci cílové formule do CNF. Protože \varphi_1,\ldots,\varphi_n\models\psi\iff\varphi_1\land\ldots\land\varphi_n\models\psi, bereme teorii (a negaci cílové formule) jako množinu klauzulí – té se v kontextu logického programování říká znalostní báze. Rezoluční vyvrácení je pak konečná posloupnost klauzulí, přičemž každý její prvek je buď klauzule ze znalostní báze, nebo klauzule cílové formule, nebo rezolventa dvou předcházejících prvků. Posloupnost končí prázdnou klauzulí, která je vždy nepravdivá – sporem.

Výše uvedený důkaz funguje dobře pro výrokovou logiku. Predikátová logika přináší problém ve formě univerza, predikátu a kvantifikátorů. Klauzule je nutné definovat trochu jinak CNF:

Ne všechny formule jdou do převést na konjunkci klauzulí, konkrétně je problém s existenčními kvantifikátory (ty nelze vždy přepsat na univerzální kvůli přesunutí negace k literálům). Proto se provádí tak zvaná Skolemizace, kdy se formule převádí na jinou formuli, která je splněna za stejných podmínek. Při ní se existenčně kvantifikovaná proměnná nahrazuje:

  1. konstantou (která ještě nebyla použita)
  2. pokud je existenční kvantifikátor pod jedním (nebo více) univerzálním kvantifikátorem, novou funkcí, která závisí na univerzálně kvantifikované proměnné (proměnných).

Využívá se přitom následujících identit: \exists x\varphi\equiv\neg\forall x\neg\varphi, \forall x(\varphi\land\psi)\equiv (\forall x\varphi)\land(\forall x\psi), \forall x(\varphi\land\psi)\equiv(\forall x\varphi)\land\psi pokud x není volné v \psi (a podobně pro \lor a \exists)11).

Příkladem Skolemizace klauzule \exists xP(x)\lor\forall x\exists yQ(x,y) je klauzule \forall x(P(c)\lor Q(x,f(x)), kterou píšeme P(c)\lor Q(x,f(x)), kde c je nová konstanta a f je nová unární funkce.

Na takových klauzulích můžeme provádět rezoluci. Ta probíhá následovně:

  1. Vybereme dvě klauzule, přičemž jedna obsahuje literál P(t_1,\ldots,t_n) a druhá \neg P(u_1,\ldots,u_n).
  2. Provedeme unifikaci predikátů – tzn. snažíme se najít takovou substituci termů za proměnné vyskytující se v t_1,\ldots,t_n,u_1,\ldots,u_n, že t_1=u_1,\ldots,t_n=u_n.
  3. Pokud se predikáty dají unifikovat, provedeme rezoluci, jinak musíme vybrat jiné predikáty.

Více o rezoluci a zefektivnění dokazovacího procesu se lze dočíst v materiálech předmětu IB013 Logické programování.

Vlastnosti prvořádové logiky

Prvořádová logika je bezesporná a úplná (a tedy i částečně rozhodnutelná), ale není rozhodnutelná (existuje spojitost s nerozhodnutelností problému zastavení). Dále pro ni platí následující věty:

Kompaktnost

Množina prvořádových formulí (teorie) má model právě tehdy, když každá její konečná podmnožina má model.

To ve výsledku znamená, že pokud je formule logickým důsledkem teorie, je logickým důsledkem konečně mnoha jejích axiomů.

Löwenheimova-Skolemova věta

Pokud má formule nekonečný model, má model libovolné kardinality.

Což mimojiné znamená, že pomocí prvořádové logiky nelze sformulovat teorii přirozených čísel (respektive teorii, kterou by splňovala pouze přirozená čísla).

Pokud pracujeme s jazykem s rovností, můžeme definovat numerický kvantifikátor „existuje alespoň n prvků, které splňují \varphi“. Požadujeme, aby existovalo n prvků, které jsou po dvojicích různé:
\exists^{\ge n}x\varphi(x)\equiv\exists x_1\ldots\exists x_n(\varphi[x_1/x]\land\ldots\land\varphi[x_n/x]\land 'x_1\neq x_2)\land\ldots\land (x_1\neq x_n)\land\ldots\land (x_{n-1}\neq x_n)) Přitom existenci přesně n individuí lze zřejmě vyjádřit jako \exists^{\ge n}x\varphi(x)\land\neg\exists^{\ge n+1}x\varphi(x). Není tak ale možné vyjádřit existenci nekonečného počtu predikátů.

Druhořádová logika

Vyjadřovací možnosti prvořádové logiky jsou omezené – kvantifikátory se totiž mohou vztahovat pouze k prvkům univerza. Například tvrzení „každá neprázdná omezená množina má supremum“, není možné vyjádřit v prvořádové logice. Proto byla zavedena logika druhého řádu. Ta kromě individuí umožňuje kvantifikovat i predikáty a funkce (tedy proměnné jsou predikáty i funkce).

Druhořádová logika nemá odvozovací systém, který by byl zároveň bezesporný a úplný (jinak by byla prvořádová logika rozhodnutelná). Existuje několik různých odvozovacích systémů.

Zajímavou podtřídou druhořádové logiky je monadická druhořádová logika (MSOL), která umožňuje kvantifikaci pouze individuí a množin. Není bez zajímavosti, že formule MSOL se dají převádět na Büchiho automaty, avšak za cenu exponenciálního nárustu velikosti.

Neúplnost

Predikátová logika vznikla na základě snahy vytvořit formální systém pro celou matematiku, tak že by mohl být použit k důkazu všech tvrzení (tak zvaný Hilbertův program). Následující dvě věty dokázané Gödelem ukázaly, že toto není možné12).

Gödelova první věta o neúplnosti

Každý dokazovací systém zahrnující Peanovu aritmetiku přirozených čísel nemůže být zároveň bezesporný a úplný.

Konkrétně, pokud je takový dokazovací systém bezesporný, není úplný, tedy existuje pravdivé matematické tvrzení, které v něm nelze dokázat.13). Samozřejmě, pokud toto tvrzení přidáme jako axiom, opět najdeme jiné pravdivé nedokazatelné tvrzení. Jiná formulace této věty (možná bližší informatikům) je, že jazyk platných formulí pracující s Peanovou aritmetikou není rekurzívně vyčíslitelný (přitom víme, že jazyk generovaný libovolným dokazovacím systémem je rekurzívně vyčíslitelný).

Poznámka: Peanova aritmetika je relativně silná – obsahuje sčítání, násobení a indukci. Některé slabší teorie (například pouze se sčítáním) jsou úplné.

Gödelova druhá věta o neúplnosti

Žádný bezesporný dokazovací systém zahrnující Peanovu aritmetiku přirozených čísel nelze použít k důkazu vlastní bezespornosti.

Pokud tedy chceme dokázat bezespornost teorie, musíme k tomu použít nějakou silnější teorii – o jejíž bezespornosti ovšem nemáme důkaz. V bezespornost tedy musíme věřit – respektive ji předpokládat.

Přes všechny tyto výsledky má prvořádová logika svůj význam. Ačkoliv nelze formalizovat veškerá matematika, jsou velké oblasti které jsou formalizovány. Zermelova-Fraenkelova teorie množin spolu s prvořádovou logikou je považována za základní formalismus pro většinu matematiky.

Existují netriviální teorie, které jsou rozhodnutelné – například existuje algoritmus pro teorii analytické geometrie (respektive, teorie uzavřených reálných komutativních těles je rozhodnutelná).

Důkaz indukcí

Matematická indukce je způsob jak dokázat, že nějaké tvrzení platí pro všechna přirozená čísla. Vždy se skládá ze

  1. základní krok – tvrzení platí pro nulu (nebo jedničku),
  2. indukční krok – pokud tvrzení platí pro k (indukční předpoklad), platí pro k+1.

Pokud platí tyto dva kroky, tvrzení platí pro všechna přirozená čísla.

Toto základní schéma má více variant:

  1. Přeskakování – indukční krok je upraven: pokud tvrzení platí pro k, platí pro k+n. Pak je nutné v základním případě dokázat, že tvrzení platí pro 0,\ldots,n-1.
  2. Silná matematická indukce – indukční krok: pokud tvrzení platí pro 0,\ldots,k, platí i pro k+1 – tato indkuce je silnější a nevyžaduje úpravu základního kroku.

Na matematickou indukci lze také pohlížet z trochu jiného pohledu – jako rozhodování o platností výroků indexovaných přirozenými čísly V_0,\ldots. Pak lze základní princip indukce zapsat následující formulí:
(V_0\land(\forall k\in\mathbb{N}_0.(V_k\to V_{k+1})))\to(\forall k\in\mathbb{N}_0.V_k) Podobně lze zapsat i upravenou indukci.

Strukturální indukce

Strukturní indukce je zobecnění matematické indukce, které lze použít pro libovolnou fundovanou uspořádanou množinu. Uspořádaná množina je fundovaná, pokud pro každou její neprázdnou podmnožinu existuje minimální prvek. Pak aby tvrzení platilo pro všechny prvky takové množiny stačí dokázat:

  1. tvrzení platí pro minimální prvky množiny,
  2. tvrzení platí pro daný prvek pokud platí pro maximální menší prvky (slabá indukce) nebo pro všechny menší prvky (silná indukce).

Typicky se setkáváme se strukturální indukcí u definic pomocí indukce – což je nejčastější konstruktivní způsob definice potenciálně nekonečných struktur. Konkrétně většinou půjde o:

Občas se říká, že indukce probíhá vzhledem k délce seznamu a výšce stromu.

Protože důkazy jsou v zásadě seznamy a formule jsou v zásadě stromy (abstraktní syntaktické stromy), tento typ důkazu se typicky používá i pro tyto struktury. Tímto způsobem se dokazuje úplnost dokazovacího systému (axiomy jsou platné a odvozovací pravidla zachovávají platnost). Pro formule typicky dokazujeme, že tvrzení platí pro predikáty (nebo výroky) a že se zachovává aplikací logických spojek.

Předměty

1)
V předmětu MA007 Matematická logika prof. Kučera definuje něco jako vytvořující posloupnost, což je v zásadě syntaktický strom zapsaný v jednom řádku od listů po kořen. Prakticky je to velmi podobná konstrukce jako důkaz (viz níže). Pokud dostanete do komise jeho nebo někoho, kdo pod ním cvičí, pravděpodobně to bude chtít vědět. Já jsem se ale s tímhle způsobem nikde nesetkal (pokud zadám do googlu `vytvořující posloupnost formule', vypadnou mi na prvním místě materiály k tomuto předmětu nebo cvičení a to je všechno k logice) a popravdě ho považuju za poněkud neobratný (zatímco důkaz se běžně bere jako lineární záležitost). – tomvej
2)
Nebo se na něj můžeme dívat jako na strom.
3)
Alespoň pokud ji srovnáme s tím, jak je definována predikátová logika.
4)
Pro účely tohoto textu je implikace zapsána \to. Občas se také používá značka \subset. Celkově ale logici často odlišují implikaci od textové zkratky „a z toho plyne“ \implies. Podobně pro \leftrightarrow a \iff.
5)
Abstraktní syntaktická rovnice uvedená výše závorky nepotřebuje, ale pro zápis formule v řádku jsou nutné.
6)
Prof. Kučera term definuje pomocí vytvořující posloupnosti.
7)
Nebo s pomocí vytvořovací posloupnosti.
8)
Například v angličtině neexistuje nic takového jako „closed formula“ – je to „a sentence“.
9)
Mnemotechnická pomůcka „nahradím t za x“. Také se používá zápis \varphi[x/t] nebo dokonce \varphi(x/t) – podle autora.
10)
Symbol \iff je použit jako zkratka „právě tehdy když“. Všimnětě si, že tato definice prakticky používá jazyk teorie množin.
11)
Jak bych postupoval? Nejdříve bych přesunul všechny negace k predikátům. Pak bych přepsal logické spojky tak, abych byl v CNF, až na kvantifikátory (které můžou být všude). Pak bych přesunul všechny univerzální kvantifikátory na začátek klauzulí, přičemž pokud by hrozilo, že univerzální kvantifikátor „přeskočí“ přes existenční, posunul bych i existenční. Když potřebuju upravit \forall x\varphi(x)\lor\psi(x), nahradím x v \psi novou proměnnou x' a přepíšu na \forall x(\varphi(x)\lor\psi(x')). Když už mám klauzule ve správném tvaru, zbavím se existenčních kvantifikátorů Skolemizací.
12)
Důkaz první věty je například v materiálech k předmětu MA007 Matematická logika, kde je rovněž osnov důkazu druhé věty.
13)
K tomu se váže vtipná historka: Když Alonzo Church navrhoval λ-kalkulus a doslechl se o této větě, myslel si, že se teorie λ-kalkulu (tj. λ-kalkulus a predikátovou logiku) neúplnost netýká. Ve finále měl pravdu, protože se ukázalo, že teorie λ-kalkulu je sporná. Není to ale asi úplně to, co chtěl.