10. Základní typy důkazů

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

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.

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ý strom¹⁾.
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 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 (),
3. formule je splněna pro všechny možné modely a všechny valuace – je tautologie. Píšeme .

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

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ť je množina formulí (teorie). Důkaz formule z předpokladů je konečná posloupnost²⁾ , kde pro každé platí jedno z následujících:

1. ,
2. je jeden z axiomů,
3. vznikne aplikací jednoho z odvozovacích pravidel na některé z formulí .

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

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

• Bezespornost, tedy nelze odvodit spor (neboli – to je nezbytné minimum).
• Úplnost, tedy že jsme schopni odvodit všechny pravdivé formule – tautologie (neboli ).
• Rozhodnutelnost, tedy že existuje algoritmická procedura schopná rozhodnout problém .

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 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í hodnoty³⁾. 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

⁴⁾ Jazykem výrokové logiky jsou konečná množina výrokových proměnných, logické spojky a závorky⁵⁾.

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

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 je pro valuaci pravdivá, pokud , je splnitelná, pokud existuje valuace taková, že a je logicky pravdivá (tautologie, často pouze „pravdivá“), pokud je pravdivá pro libovolnou valuaci. Formule je logickým důsledkem množiny formulí , psáno právě tehdy pokud pro každou valuaci, pro kterou jsou pravdivé všechny formule v je pravdivá .

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 , nebo 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 jsou standardní zápisy formulí. Jsou tvořeny:

1. literály, což je formule nebo její negace,
2. klauzulemi, což je disjunkce () více literálů,
3. duálními klauzulemi, což je konjunkce () 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.

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 (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í(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 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) 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 ).

Abeceda prvořádové logiky obsahuje:

• logické spojky výrokové logiky (zde použijeme pouze a , ale ostatní se dají vyjádřit pomocí nich),
• symbol pro univerzální () a existenciální () kvantifikátor,
• závorky,
• spočetně mnoho znaků pro proměnné ().

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

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 je⁶⁾:

1. proměnná,
2. kde je -ární funkční symbol jazyka a 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 . Uzavřeným termem je například .

Formule

Formule prvořádové logiky jazyka je definována induktivně⁷⁾ jako:

1. ke je -ární predikátový symbol jazyka a jsou termy,
2. , kde je formule,
3. , kde a jsou formule,
4. nebo , kde je proměnná a je formule.

Existenciální kvantifikátor se typicky také definuje pomocí syntaktické zkratky . Pro zpřehlednění zápisů formulí se v praxi další konvence. Například široce rozšířený zápis je zcela formálně zapsán .

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 nebo jsou všechny výskyty proměnné v 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 je proměnná 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 , kde všechny volné proměnné v jsou mezi . Pokud formule neobsahuje volné proměnné, je uzavřená (takovým formulím se také říká sentence⁸⁾), 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 , což zachovává pravdivostní hodnotu formule (viz níže).

Substituce

Zápisem ⁹⁾ značíme formuli , kde jsou všechny volné výskyty proměnné (textově) nahrazeny termem . 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 není substituovatelný za v termu . Typicky používáme vícenásobnou (souběžnou) substituci značenou .

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) jazyka je dána:

1. Neprázdným souborem prvků (individuí) – univerzem (také nosičem).
2. Přiřazením -ární relace každému -árnímu predikátovému symbolu .
3. Přiřazením -ární funkce každému -árnímu funkčnímu symbolu .

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 ().

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

Sémantika prvořádové logiky

Nechť je realizace , valuace a formule prvořádové logiky nad .

Realizace termu je definována induktivně (podle definice termu):

1. ,
2. .

Relace splněnosti formule realizací a valuací je definována induktivně¹⁰⁾:

1. ,
2. ,
3. právě tehdy, když nebo ,
4. právě tehdy, když pro každý .
5. právě tehdy když pro nějaký .

Pokud je jazyk s rovností, platí pouze tehdy, označují-li a stejná individua.

Říkáme, že je pravdivá v , pokud pro libovolnou valuaci .

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í“).

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

Vezměme si výše zmíněný jazyk teorie grup, symboly 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 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.

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 je dokazatelná z množiny předokladů (teorie) zapisujeme . Teorie je sporná (inkonzistentní), pokud z ní lze dokázat libovolnou formuli jazyka prvořádové logiky.

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

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

Věta o dedukci

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:

• přímý důkaz – dokazujeme implikaci tak jak je,
• nepřímý důkaz – dokazujeme obměněnou implikaci (),
• důkaz sporem – dokazujeme negaci implikace ().

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. pro libovolné ,
2. pro libovolné (distribuce implikace),
3. pro libovolné (obměna implikace),
4. , kde je substituovatelný za v (axiom specifikace),
5. , kde nemá volný výskyt ve (axiom distribuce),

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

• (z odvoď )

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

Pro pohodlí si typicky budeme definovat další schemata axiomů (například ), 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).

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:

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

• zavedení předpokladů a eliminace předpokladů ,
• zavedení konjunkce a eliminiace konjunkce , ,
• zavedení disjunkce a eliminace disjunkce ,
• zavedení implikace , což odpovídá větě o dedukci, a eliminace implikace, neboli modus ponens ,
• zavedení negace a eliminace negace (docházíme ke sporu),
• zavedení dvojí negace a eliminace dvojí negace ,
• zavedení univerzálního kvantifikátoru (pouze pokud není volné v nějaké formuli z ) a eliminace univerzálního kvantifikátoru (pouze pokud je substituovatelné – odpovídá axiomu specifikace),
• zavedení existenčního kvantifikátoru (pouze pokud se nestane vázaným – ano, nahrazujeme term proměnnou) a eliminace existenčního kvantifikátoru (kde je individuová konstanta nevyskytující se nikde jinde).

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

Kde 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 , 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:

• literál je predikát (tedy n-ární predikátový symbol s n termy) nebo jeho negace,
• klauzule je disjunkce literárů, přičemž všechny jejich volné proměnné jsou na jejím začátku univerzálně kvantifikovány (implicitně).

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: , , pokud není volné v (a podobně pro a )¹¹⁾.

Příkladem Skolemizace klauzule je klauzule , kterou píšeme , kde je nová konstanta a 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 a druhá .
2. Provedeme unifikaci predikátů – tzn. snažíme se najít takovou substituci termů za proměnné vyskytující se v , že .
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í.

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:

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

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ň prvků, které splňují “. Požadujeme, aby existovalo prvků, které jsou po dvojicích různé:
Přitom existenci přesně individuí lze zřejmě vyjádřit jako . Není tak ale možné vyjádřit existenci nekonečného počtu predikátů.

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.

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é¹²⁾.

Konkrétně, pokud je takový dokazovací systém bezesporný, není úplný, tedy existuje pravdivé matematické tvrzení, které v něm nelze dokázat.¹³⁾. 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é.

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á).

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 (indukční předpoklad), platí pro .

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 , platí pro . Pak je nutné v základním případě dokázat, že tvrzení platí pro .
2. Silná matematická indukce – indukční krok: pokud tvrzení platí pro , platí i pro – 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 . Pak lze základní princip indukce zapsat následující formulí:
Podobně lze zapsat i upravenou indukci.

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:

• Seznamy:
  1. tvrzení platí pro prázdný seznam (nebo jednoprvkový seznam),
  2. pokud tvrzení platí pro daný seznam (nebo daný seznam a všechny jeho podseznamy bez nějakých prvků na začátku), platí i pokud se na jeho začátek připojí další prvek.
• Stromy:
  1. tvrzení platí pro listy,
  2. tvrzení platí pro uzel, pokud platí pro všechny jeho přímé potomky (nebo celý podstrom).

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.

• MA007 Matematická logika
• IV082 Základní pojmy obecné logiky
• IB013 Logické programování
• IA038 Typy a dukazy