MATEMATICKÝ DŮKAZ A „VĚČNÁ JISTOTA“: CO V MATEMATICE ZNAMENÁ DOKÁZAT PRAVDU
ÚVOD
Matematický důkaz má ve veřejné debatě zvláštní postavení. V experimentální vědě může nový přístroj změnit naměřenou hodnotu. V právu mohou nový svědek nebo nový dokument změnit závěr soudu. V matematice se zdá, že jednou dokázaná Pythagorova věta zůstane pravdivá navždy.
V určitém smyslu to platí. Důkaz je konečná logická cesta od definic a přijatých axiomů k závěru. Pokud je každý krok správný, nové měření jej nemůže vyvrátit. Jenže 20. století ukázalo, že i tato jistota má hlubší vrstvy: závisí na axiomech, formálním systému a našem přesvědčení, že v důkazu není chyba. Gödel navíc dokázal, že dostatečně silný konzistentní formální systém nemůže rozhodnout všechny aritmetické pravdy uvnitř sebe sama.
1. DŮKAZ NENÍ MĚŘENÍ
Představme si tvrzení, že součet prvních n lichých čísel je n². Můžeme otestovat tisíc případů. To je silná evidence, ale stále pouze tisíc případů.
Důkaz ukáže, proč vztah platí pro všechna přirozená n. Může použít algebraickou transformaci, geometrickou konstrukci nebo matematickou indukci. Počet možných n je nekonečný, ale důkaz je konečný.
Právě tato komprese nekonečně mnoha případů do logické struktury je jednou z největších sil matematiky.
2. AXIOMY: KDE DŮKAZ ZAČÍNÁ
Žádný důkaz nezačíná z absolutního ničeho. Matematická teorie pracuje s definicemi, logickými pravidly a axiomy – tvrzeními přijatými jako výchozí.
V eukleidovské geometrii se například pracuje s určitými postuláty o bodech, přímkách a rovnoběžkách. V 19. století matematici zjistili, že změnou postulátu o rovnoběžkách lze vytvořit konzistentní neeukleidovské geometrie.
To neznamenalo, že Eukleidés byl „vyvrácen“. Znamenalo to, že jeho geometrie popisuje jeden axiomatický systém. Jiný soubor axiomů vytváří jinou geometrii.
3. KDY JE VĚTA „PRAVDIVÁ“
Je užitečné rozlišit syntaktický a sémantický pohled.
Syntakticky je věta dokazatelná, pokud existuje formální posloupnost kroků podle pravidel systému. Sémanticky je pravdivá v určitém modelu, pokud odpovídá významu symbolů v tomto modelu.
V běžné matematické praxi se rozdíl často skrývá, protože pracujeme s ustálenými strukturami. V matematické logice je však zásadní.
4. HILBERTŮV SEN
Na přelomu 19. a 20. století existovala silná naděje, že matematiku bude možné kompletně formalizovat: zvolit přesné axiomy a mechanická pravidla, dokázat konzistenci systému a v principu rozhodnout každou dobře formulovanou matematickou otázku.
David Hilbert byl jedním z hlavních představitelů tohoto programu. Jeho slavný optimismus bývá shrnován mottem „Musíme vědět. Budeme vědět.“
Pak přišel Kurt Gödel.
5. GÖDELOVA PRVNÍ VĚTA O NEÚPLNOSTI
Gödel v roce 1931 ukázal, že každý dostatečně expresivní, efektivně axiomatizovaný a konzistentní formální systém schopný popsat základní aritmetiku obsahuje výroky, které v rámci tohoto systému nelze ani dokázat, ani vyvrátit.
Intuitivně vytvořil způsob, jak aritmetice umožnit mluvit o vlastních důkazech, a sestavil tvrzení analogické větě „toto tvrzení není v tomto systému dokazatelné“.
Pokud by konzistentní systém takovou větu dokázal, dostal by se do rozporu. Pokud je systém konzistentní, věta proto zůstane nedokazatelná – a právě tím je v zamýšleném smyslu pravdivá.
6. DRUHÁ VĚTA: SYSTÉM NEDOKÁŽE ZEVNITŘ GARANTOVAT VLASTNÍ KONZISTENCI
Gödelova druhá věta jde dál. Dostatečně silný konzistentní systém nemůže standardními prostředky dokázat vlastní konzistenci.
To neznamená, že matematika je nespolehlivá nebo že „nic nelze vědět“. Znamená to, že absolutní uzavřený základ, který by zevnitř sám sobě vystavil definitivní certifikát bezespornosti, naráží na logickou mez.
Můžeme konzistenci jednoho systému dokazovat v silnějším systému. Pak se ale přirozeně zeptáme na konzistenci toho silnějšího.
7. NEÚPLNOST NENÍ TOTÉŽ CO PARADOX
Častý omyl říká: „Gödel dokázal, že matematika si odporuje.“ Právě naopak. Jeho slavný výsledek je podmíněný konzistencí: pokud je systém konzistentní, existují v něm nerozhodnutelné věty.
Neúplnost znamená meze dokazatelnosti, ne univerzální chaos.
8. NEZÁVISLOST CONTINUUM HYPOTHESIS
Výrazným příkladem je hypotéza kontinua. Gödel a později Paul Cohen ukázali, že v běžně používané teorii množin ZFC nelze hypotézu kontinua ani dokázat, ani vyvrátit, pokud je ZFC konzistentní.
Matematici pak mohou zkoumat rozšíření axiomatického systému, v nichž je hypotéza pravdivá, i systémy, v nichž je nepravdivá.
Tady je dobře vidět, že „jaká je správná odpověď?“ může záviset na tom, které axiomy chceme považovat za základ.
9. FERMATOVA VĚTA: 350 LET MEZI TVRZENÍM A DŮKAZEM
Pierre de Fermat si v 17. století poznamenal, že rovnice x^n + y^n = z^n nemá pro n > 2 kladná celočíselná řešení, a tvrdil, že má „skutečně podivuhodný důkaz“, pro který je okraj knihy příliš malý.
Po více než tři století nikdo obecný důkaz neznal. Andrew Wiles v 90. letech prokázal Fermatovu poslední větu prostřednictvím hlubokého spojení eliptických křivek a modulárních forem.
Zajímavé je, že první verze Wilesova důkazu obsahovala mezeru. Ta byla objevena při odborné kontrole a následně opravena. Příběh ukazuje, že „publikovaný důkaz“ není automaticky totéž co bezchybný důkaz. Lidská komunita musí logickou strukturu zkontrolovat.
10. POČÍTAČEM PODPOROVANÉ DŮKAZY
Věta o čtyřech barvách byla v roce 1976 dokázána pomocí počítačové kontroly velkého množství případů. To vyvolalo filozofickou debatu: je důkaz, který žádný člověk nedokáže celý ručně projít, stejným druhem matematického poznání?
Dnes je použití výpočetní techniky běžnější. Rozlišujeme však mezi programem, který něco numericky otestuje, a formálně ověřeným důkazem, jehož každý krok kontroluje malé důvěryhodné jádro proof assistantu.
11. PROOF ASSISTANTS: LEAN, COQ, ISABELLE
Systémy jako Lean, Coq a Isabelle umožňují zapisovat definice a důkazy v přesném formálním jazyce. Počítač kontroluje, že každý krok odpovídá pravidlům logiky.
To je důležitý posun. U velmi dlouhých nebo technicky složitých důkazů lze část lidské nejistoty přenést na malý ověřovací kernel. Pokud kernel pracuje správně a formální tvrzení skutečně odpovídá matematické větě, získáme mimořádně silnou kontrolu.
12. FORMÁLNĚ OVĚŘENÝ SOFTWARE
Stejná logika má praktický dopad v informatice. Místo testování programu na milionu vstupů lze u některých vlastností matematicky dokázat, že program nikdy neporuší daný invariant.
Formální verifikace se používá u mikrojader operačních systémů, kryptografických protokolů, kompilátorů a hardwaru. Známý projekt seL4 například vytvořil strojově kontrolovaný důkaz důležitých vlastností mikrojádra.
Důkaz samozřejmě nepokrývá vše. Pokud je vadný hardware, špatná specifikace nebo fyzická implementace, formální korektnost zdrojového modelu nemusí zachránit celý systém. Matematika garantuje přesně to, co jsme formulovali – nic víc.
13. DŮKAZ V MATEMATICE A „DŮKAZ“ U SOUDU
V běžném jazyce používáme stejné slovo pro dva odlišné koncepty.
U soudu je důkaz informace, která zvyšuje či snižuje pravděpodobnost skutkového tvrzení. Svědek může lhát, DNA může být kontaminována a dokument může být padělaný. Soud rozhoduje podle standardu dokazování a dostupných faktů.
Matematický důkaz není statistická evidence. Je to dedukce: pokud platí předpoklady, závěr musí platit. Proto v matematice nedává smysl říci, že je věta po správném důkazu „na 99,9 % pravdivá“.
14. DŮKAZ VE FYZICE
Fyzika používá matematiku, ale fyzikální teorie se potvrzuje experimentem. Rovnice mohou být bezchybně odvozeny z teorie a přesto může být teorie špatným modelem přírody.
Newtonova mechanika je matematicky konzistentní a mimořádně užitečná, ale při vysokých rychlostech a silné gravitaci ji nahrazuje přesnější relativistický popis. Nešlo o vyvrácení algebraického důkazu, nýbrž o zjištění, že fyzický svět nesplňuje Newtonovy předpoklady ve všech režimech.
15. JE MATEMATICKÝ DŮKAZ „VĚČNÝ“?
Pokud máme korektní důkaz věty z explicitně daných axiomů a pravidel, jeho platnost se nezmění tím, že zítra změříme jinou hodnotu fyzikální konstanty. V tomto smyslu je matematická nutnost mimořádně stabilní.
Může se však změnit naše hodnocení konkrétního textu jako důkazu, pokud objevíme skrytou chybu. Můžeme také přejít do jiného axiomatického systému, v němž má analogická otázka jiné vlastnosti.
„Věčná jistota“ tedy není mystická absolutnost. Je to podmíněná logická nutnost: jsou-li předpoklady a pravidla správně stanoveny a odvození je korektní, závěr z nich nutně plyne.
16. CO NÁM GÖDEL NEVZAL
Gödelova neúplnost matematiku nezničila. Matematici dál dokazují miliony vět, budují teorie a používají je v technice. Neúplnost pouze ukázala, že žádný dostatečně bohatý mechanický formální systém není zároveň úplným univerzem všech aritmetických pravd a vlastním definitivním certifikátem.
Je to spíše rozšíření našeho chápání matematiky než její porážka.
ZÁVĚR
Matematický důkaz je pravděpodobně nejpřísnější forma zdůvodnění, kterou lidstvo vytvořilo. Jeho síla spočívá v tom, že závěr není závislý na budoucím měření, názoru autority ani většinovém hlasování.
Současně právě matematická logika ukázala vlastní hranice formálních systémů. A moderní proof assistants připomínají ještě jednu praktickou hranici: dokonalá logika musí být správně zapsána a kontrolována nedokonalými lidmi a stroji.
Nejpřesnější formulace této teze proto zní: správný matematický důkaz poskytuje trvalou logickou jistotu vzhledem k daným axiomům a pravidlům – ale matematika sama nás učí být velmi přesní v tom, co přesně jsme dokázali.
17. ČTYŘBAREVNÁ VĚTA A OTÁZKA „VIDĚL ČLOVĚK CELÝ DŮKAZ?“
Čtyřbarevná věta tvrdí, že každou rovinnou mapu lze obarvit nejvýše čtyřmi barvami tak, aby sousední oblasti neměly stejnou barvu. První obecně přijatý důkaz Appela a Hakena z roku 1976 použil počítač k ověření velkého množství konfigurací.
Část matematiků byla zpočátku nespokojená, protože jednotlivý člověk nemohl všechny výpočty ručně projít. Spor odhalil, že matematická jistota má i sociální vrstvu: důvěřujeme nejen logice, ale kompilátoru, procesoru, programu a postupu kontroly.
Pozdější formální verifikace čtyřbarevné věty v proof assistantu Coq tento problém výrazně zmenšila. Velký výpočet je redukován na objekt, který kontroluje malé logické jádro.
18. POINCARÉHO DOMNĚNKA: DŮKAZ, KTERÝ KOMUNITA KONTROLOVALA ROKY
Grigorij Perelman zveřejnil v letech 2002–2003 preprinty řešící Poincarého domněnku pomocí Ricciho toku. Text nebyl okamžitě přijat pouze proto, že jej napsal geniální matematik. Několik týmů strávilo roky doplňováním detailů a kontrolou argumentu.
Příklad ukazuje, že matematická komunita má vlastní obdobu replikace: jiní odborníci musí být schopni rekonstrukci pochopit a nezávisle potvrdit. Rozdíl od experimentu je v tom, že nereplikují přírodní jev, ale logické odvození.
19. KDY POČÍTAČ NAJDE DŮKAZ SÁM
Automated theorem provers mohou vyhledávat důkaz bez toho, aby člověk předem znal cestu. Moderní systémy kombinují symbolickou logiku, SAT/SMT řešiče a stále častěji strojové učení.
Tím vzniká nová otázka: pokud stroj najde formálně správný důkaz o milionu kroků, kterému žádný člověk intuitivně nerozumí, máme matematické poznání, nebo pouze certifikát pravdivosti? Z hlediska formální správnosti může být certifikát perfektní. Z hlediska matematiky jako porozumění může stále chybět vysvětlující idea.
20. DŮKAZ A VYSVĚTLENÍ NEJSOU VŽDY TOTÉŽ
Dva důkazy mohou být stejně správné a přitom mít úplně jinou intelektuální hodnotu. Jeden může být dlouhý výpočet, druhý krátká konstrukce, která odhalí, proč věta musí platit.
Matematici proto hledají nejen „Q.E.D.“, ale i elegantní důkazy, nové souvislosti a generalizace. Věčný certifikát pravdy je pouze jedna část matematické práce; druhou je struktura porozumění, kterou důkaz vytvoří.
21. CO ZNAMENÁ CHYBA V AXIOMU
Axiom není empirické tvrzení, které by se „pokazilo“ novým měřením. Je součástí definice teorie. Může se ale ukázat, že zvolený systém je nekonzistentní nebo že není vhodným modelem jevu, který jsme chtěli popsat.
Proto je vždy důležité uvést, v jakém systému věta platí. V běžné matematice se kontext často předpokládá, ale u základů matematiky je explicitní uvedení axiomatického rámce součástí přesnosti.
ZDROJE A DALŠÍ ČTENÍ
[1] Stanford Encyclopedia of Philosophy — Gödel's Incompleteness Theorems.
plato.stanford.edu
https://plato.stanford.edu/entries/goedel-incompleteness/
[2] Lean theorem prover.
lean-lang.org
https://lean-lang.org/
[3] Coq Proof Assistant.
coq.inria.fr
https://coq.inria.fr/
[4] Isabelle theorem prover.
isabelle.in.tum.de
https://isabelle.in.tum.de/
[5] seL4 — formally verified microkernel.
sel4.systems
https://sel4.systems/
[6] MacTutor History of Mathematics — Andrew Wiles and Fermat's Last Theorem.
mathshistory.st-andrews.ac.uk
https://mathshistory.st-andrews.ac.uk/Biographies/Wiles/