b'\n_START_ARTICLE_\nTwierdzenie G\xc3\xb6dla\n_START_SECTION_\nKontekst\n_START_PARAGRAPH_\nTwierdzenie G\xc3\xb6dla by\xc5\x82o odpowiedzi\xc4\x85 na pr\xc3\xb3b\xc4\x99 przedstawienia wszystkich aksjomat\xc3\xb3w i twierdze\xc5\x84 matematycznych w postaci czysto symbolicznej (syntaktycznej), tzn. bez odwo\xc5\x82ywania si\xc4\x99 do ich znaczenia (czyli w oderwaniu od semantyki; por. logicyzm, formalizm). Pr\xc3\xb3by takiej podj\xc4\x85\xc5\x82 si\xc4\x99 m.in. David Hilbert._NEWLINE_J\xc4\x99zyk \xe2\x80\x93 zbi\xc3\xb3r term\xc3\xb3w (zda\xc5\x84) tworzonych wed\xc5\x82ug pewnych regu\xc5\x82._NEWLINE_Teoria matematyczna nad pewnym j\xc4\x99zykiem \xe2\x80\x93 przyporz\xc4\x85dkowanie zdaniom w okre\xc5\x9blonym j\xc4\x99zyku w\xc5\x82asno\xc5\x9bci prawdy lub fa\xc5\x82szu. Teoria nadaje j\xc4\x99zykowi znaczenie i opisuje pewn\xc4\x85 matematyczn\xc4\x85 rzeczywisto\xc5\x9b\xc4\x87. Teoria pozwala odpowiedzie\xc4\x87, czy dane zdanie jest prawdziwe._NEWLINE_System formalny \xe2\x80\x93 zbi\xc3\xb3r aksjomat\xc3\xb3w (zda\xc5\x84) wraz z regu\xc5\x82ami wnioskowania (algorytmem), generuj\xc4\x85cy pewien podzbi\xc3\xb3r zda\xc5\x84 j\xc4\x99zyka. System formalny jest \xe2\x80\x9eprzybli\xc5\xbceniem\xe2\x80\x9d teorii matematycznej. Pozwala odpowiedzie\xc4\x87, czy dane zdanie jest dowodliwe. Dla jednej teorii mo\xc5\xbce istnie\xc4\x87 wiele r\xc3\xb3\xc5\xbcnych system\xc3\xb3w formalnych (aksjomatyzacji), przybli\xc5\xbcaj\xc4\x85cych j\xc4\x85 lepiej lub gorzej. Je\xc5\xbceli zdanie jest dowodliwe, to musi by\xc4\x87 ono prawdziwe (ale niekoniecznie na odwr\xc3\xb3t)._NEWLINE_System formalny niesprzeczny \xe2\x80\x93 system, w kt\xc3\xb3rym nie da si\xc4\x99 udowodni\xc4\x87 jednocze\xc5\x9bnie pewnego zdania i jego zaprzeczenia._NEWLINE_System formalny zupe\xc5\x82ny \xe2\x80\x93 system, w kt\xc3\xb3rym mo\xc5\xbcliwe jest przeprowadzenie dowodu dowolnego prawid\xc5\x82owo zapisanego zdania tego systemu lub jego zaprzeczenia. W systemie zupe\xc5\x82nym ka\xc5\xbcde prawdziwe zdanie jest dowodliwe._NEWLINE_System formalny pierwszego rz\xc4\x99du \xe2\x80\x93 system, w kt\xc3\xb3rym u\xc5\xbcyto wy\xc5\x82\xc4\x85cznie standardowych regu\xc5\x82 wnioskowania oraz wszystkie jego aksjomaty s\xc4\x85 wyra\xc5\xbcone w logice pierwszego rz\xc4\x99du, czyli nie dopuszcza si\xc4\x99 kwantyfikator\xc3\xb3w po zmiennych przebiegaj\xc4\x85cych zbiory._NEWLINE_System formalny rozstrzygalny (efektywny) \xe2\x80\x93 taki system, kt\xc3\xb3rego algorytm wnioskowania da si\xc4\x99 zaprogramowa\xc4\x87 na maszynie Turinga. \xc5\xbbeby system by\xc5\x82 rozstrzygalny, potrzeba i wystarcza, \xc5\xbceby istnia\xc5\x82a tylko jedna (ale odpowiednia) regu\xc5\x82a wnioskowania (najcz\xc4\x99\xc5\x9bciej przyjmuje si\xc4\x99 modus ponens) oraz \xc5\xbceby jego zbi\xc3\xb3r aksjomat\xc3\xb3w da\xc5\x82 si\xc4\x99 wygenerowa\xc4\x87 za pomoc\xc4\x85 maszyny Turinga._NEWLINE_Aksjomatyka Peana \xe2\x80\x93 pewien system formalny pierwszego rz\xc4\x99du, opisuj\xc4\x85cy liczby naturalne.\n_START_SECTION_\nPierwsze, o niezupe\xc5\x82no\xc5\x9bci\n_START_PARAGRAPH_\nKa\xc5\xbcdy niesprzeczny rozstrzygalny system formalny pierwszego rz\xc4\x99du, zawieraj\xc4\x85cy w sobie aksjomaty Peana, musi by\xc4\x87 niezupe\xc5\x82ny._NEWLINE_Oznacza to, \xc5\xbce \xc5\xbcaden system formalny pierwszego rz\xc4\x99du nigdy nie \xe2\x80\x9epokryje\xe2\x80\x9d w ca\xc5\x82o\xc5\x9bci zbioru wszystkich twierdze\xc5\x84 arytmetyki. Nie oznacza to, \xc5\xbce zbi\xc3\xb3r wszystkich twierdze\xc5\x84 arytmetyki nie istnieje, a jedynie, \xc5\xbce nie mo\xc5\xbce on by\xc4\x87 wygenerowany przez \xc5\xbcaden system formalny. Inaczej m\xc3\xb3wi\xc4\x85c, dowodliwo\xc5\x9b\xc4\x87 jest zawsze s\xc5\x82absza od prawdziwo\xc5\x9bci \xe2\x80\x93 zbi\xc3\xb3r zda\xc5\x84 generowanych (dowodzonych) przez system formalny nigdy nie b\xc4\x99dzie r\xc3\xb3wny ze zbiorem zda\xc5\x84 prawdziwych teorii. Mo\xc5\xbce on by\xc4\x87 albo mniejszy od zbioru zda\xc5\x84 prawdziwych (system niesprzeczny, ale niezupe\xc5\x82ny), albo wi\xc4\x99kszy od niego (system zupe\xc5\x82ny, ale sprzeczny)._NEWLINE_Twierdzenie G\xc3\xb6dla zachodzi tak\xc5\xbce dla ka\xc5\xbcdej teorii silniejszej od arytmetyki Peana (zawieraj\xc4\x85cej w sobie t\xc4\x99 arytmetyk\xc4\x99). Oryginalne twierdzenie nic nie m\xc3\xb3wi o teoriach s\xc5\x82abszych od arytmetyki, ale odkryto ju\xc5\xbc s\xc5\x82absze teorie, kt\xc3\xb3re wystarczaj\xc4\x85 do zachodzenia podobnych twierdze\xc5\x84._NEWLINE_Mo\xc5\xbcna rozszerzy\xc4\x87 definicj\xc4\x99 system\xc3\xb3w formalnych tak, \xc5\xbce twierdzenie G\xc3\xb6dla nie b\xc4\x99dzie dla nich zachodzi\xc4\x87. Jednak takie niestandardowe systemy nigdy nie b\xc4\x99d\xc4\x85 rozstrzygalne, tzn. ich algorytm wnioskowania nie da\xc5\x82by si\xc4\x99 zaprogramowa\xc4\x87 na maszynie Turinga lub ich zbi\xc3\xb3r aksjomat\xc3\xb3w nie da\xc5\x82by si\xc4\x99 tak\xc4\x85 maszyn\xc4\x85 wygenerowa\xc4\x87. Poniewa\xc5\xbc ka\xc5\xbcdy zbi\xc3\xb3r sko\xc5\x84czony jest rozstrzygalny, dlatego twierdzenie G\xc3\xb6dla m\xc3\xb3wi, \xc5\xbce nie istnieje \xc5\xbcadna zupe\xc5\x82na niesprzeczna, sko\xc5\x84czona aksjomatyzacja arytmetyki, ani nawet taka niesko\xc5\x84czona, kt\xc3\xb3ra da si\xc4\x99 wygenerowa\xc4\x87 ze sko\xc5\x84czonej.\n_START_SECTION_\nDrugie, o niedowodliwo\xc5\x9bci niesprzeczno\xc5\x9bci\n_START_PARAGRAPH_\nTo twierdzenie jest konsekwencj\xc4\x85 poprzedniego. G\xc5\x82osi ono, \xc5\xbce w ramach \xc5\xbcadnego rozstrzygalnego systemu formalnego pierwszego rz\xc4\x99du zawieraj\xc4\x85cego w sobie aksjomaty Peana nie da si\xc4\x99 dowie\xc5\x9b\xc4\x87 niesprzeczno\xc5\x9bci jego samego. Aby taki dow\xc3\xb3d przeprowadzi\xc4\x87, niezb\xc4\x99dny jest szerszy system, kt\xc3\xb3rego niesprzeczno\xc5\x9bci w ramach niego samego r\xc3\xb3wnie\xc5\xbc nie da si\xc4\x99 dowie\xc5\x9b\xc4\x87 \xe2\x80\x93 i tak ad infinitum.\n_START_SECTION_\nWnioski\n_START_PARAGRAPH_\nObydwa twierdzenia G\xc3\xb6dla mo\xc5\xbcna uog\xc3\xb3lni\xc4\x87 na dowolne systemy formalne zawieraj\xc4\x85ce sko\xc5\x84czon\xc4\x85 lub rekurencyjnie przeliczaln\xc4\x85 liczb\xc4\x99 aksjomat\xc3\xb3w. Warunkiem jest, aby w sk\xc5\x82ad takiego systemu wchodzi\xc5\x82a arytmetyka liczb naturalnych lub zawiera\xc5\x82 on sko\xc5\x84czon\xc4\x85 liczb\xc4\x99 aksjomat\xc3\xb3w umo\xc5\xbcliwiaj\xc4\x85c\xc4\x85 przeprowadzenie tzw. arytmetyzacji twierdze\xc5\x84._NEWLINE_Mo\xc5\xbcna oznaczy\xc4\x87 G\xe2\x82\x80=P\xe2\x82\x96(k) i doda\xc4\x87 to zdanie do aksjomat\xc3\xb3w systemu. Wtedy r\xc3\xb3wnie\xc5\xbc b\xc4\x99dzie istnia\xc5\x82o zdanie G\xe2\x82\x81 niezale\xc5\xbcne od poszerzonych aksjomat\xc3\xb3w. W ten spos\xc3\xb3b mo\xc5\xbcna doda\xc4\x87 G\xe2\x82\x82, G\xe2\x82\x83..., a nawet G, G, G..., G, G..., G, G... i G.\n_START_SECTION_\nPokrewne zagadnienia\n_START_PARAGRAPH_\nIstniej\xc4\x85 r\xc3\xb3wnie\xc5\xbc alternatywne formy twierdze\xc5\x84 G\xc3\xb6dla pos\xc5\x82uguj\xc4\x85ce si\xc4\x99 poj\xc4\x99ciami m.in. z zakresu tak zwanych zbior\xc3\xb3w rekurencyjnych. Mo\xc5\xbcna pokaza\xc4\x87 \xc5\xbce twierdzenie G\xc3\xb6dla jest r\xc3\xb3wnowa\xc5\xbcne twierdzeniu Turinga o problemie stopu.'