Prehľad

Gödelove vety o neúplnosti sú dve ústredné tvrdenia matematickej logiky, ktoré v roku 1931 sformuloval a dokázal rakúsko-švédsky logik Kurt Gödel. Tieto vety sa týkajú formálnych axiomatických systémov, ktoré sú dostatočne silné na to, aby vyjadrovali základné vlastnosti prirodzených čísel (napríklad Peanoovu aritmetiku). V zjednodušenej forme hovoria, že ak je takýto systém konzistentný, potom nie je úplný: v systéme existujú výroky, ktoré sú pravdivé, ale nemajú dôkaz v rámci systému.

Znenie viet a základná myšlienka

Prvá veta hovorí, že v každom konzistentnom, rekurzívne axiomatizovanom a dostatočne výkonnom formálnom systéme existuje aspoň jedno tvrdenie, ktoré systém nedokáže ani dokázať, ani vyvrátiť. Druhá veta dopĺňa, že takýto systém nemôže dokázať svoju vlastnú konzistenciu, ak je skutočne konzistentný. Myšlienka dôkazu spočíva v zakódovaní syntaktických vlastností formálnych výrazov do aritmetiky (tzv. Gödelovo číslenie), čo umožní vytvoriť samoodkazujúce tvrdenie, ktoré v podstate hovorí: "Toto tvrdenie nie je dokázateľné". Podrobnejšie informácie o formálnych aspektoch logiky sú dostupné v literatúre o tejto oblasti.

Dôsledky a význam

Gödelove vety mali hlboký dopad na filozofiu matematiky i na technické smery logiky a informatiky. Medzi najdôležitejšie dôsledky patrí:

  • Nie je možné zostaviť jediný konečný súbor axióm, ktorý by v rámci prirodzenej aritmetiky odôvodnil všetky pravdivé výroky bez toho, aby systém zostal konzistentný.
  • Program Hilberta, ktorý si kládol za cieľ formálne zaručiť bezrozporovosť celej matematiky, nemôže byť dokončený len pomocou vnútorných dôkazov v rámci skúmaného systému.
  • Výrazné prepojenie medzi logikou a teóriou výpočtov: problémy rozhodnuteľnosti a rekurzívnej nerozhodnuteľnosti sú bližšie súvisiace s neúplnosťou.

Aj keď sú tieto výsledky niekedy interpretované populárne ako limit našej schopnosti poznať matematickú pravdu, je dôležité rozlišovať medzi pravdivosťou v modeli (napríklad v štandardnej aritmetike) a formálnou dokázateľnosťou v danom systéme.

Krátka história dôkazu

Gödel predstavil svoje výsledky v rigoróznom článku z roku 1931, kde zaviedol techniku aritmetizácie syntaxe a konštrukciu špeciálneho samoodkazujúceho výroku. Následné práce viedli k zovšeobecneniam a k prepojeniam s ďalšími výsledkami, ako sú práce Tarského o nedefinovateľnosti pravdy alebo Church-Turingova teória rozhodnuteľnosti. O týchto súvislostiach sa často diskutuje v prehľadoch matematiky a teoretickej informatiky venovaných logike.

Príklady, rozšírenia a poznámky

Vo forme príkladu sa ako konkrétne systémy často uvádza Peanoova aritmetika alebo iné systémy obsahujúce základnú aritmetiku prirodzených čísel. Druhá Gödelova veta formálne tvrdí, že ak systém dokáže vyjadriť vlastnú reprezentáciu "nie sú tu žiadne dôkazy vedúce k 0=1", nemôže v ňom byť dôkaz o jeho vlastnej konzistencii bez toho, aby systém bol v skutočnosti nekonzistentný. V diskusiách o axiómoch a ich role v matematike sa preto rozlišuje medzi sémantickou pravdou a formálnou dokazovateľnosťou — túto problematiku ilustrujú aj otázky týkajúce sa voľby axiómov a ich následkov v súvislostiach axióm.