Тази статия съдържа списък с ползвана литература, препоръчана литература или външни препратки, но източниците ѝ остават неясни, защото липсва конкретно посочване на източници за отделните твърдения. |
Теоремата на Гьодел за непълнота описва математически невъзможността за изразяване на цялата истина за дадена предметна област с формални средства (тази формулировка е известна като първа теорема на Гьодел за непълнота).
По-точно:
Нека имаме някаква безкрайна област G от обекти и зависимости между тях и се опитваме да създадем формална теория T, описваща тази област.
Нашата теория T ще позволява с крайни синтактични конструкции (формули, аксиоми, теореми, доказателства) да описваме верните факти за областта G.
Ако теорията T е достатъчно богата, тя не може да изрази чрез теореми всички верни факти за областта G.
Под достатъчно богата се разбира теория, която изразява понятия като алгоритъм или изчислимост в някаква форма.
Доказателството на теоремата е конструктивно – построява се специален обект, наричан Гьоделево твърдение, което нито може да се докаже, нито да се опровергае от формалната теория T, но е вярно в областта G.
Австрийският математик Курт Гьодел формулира и доказва теоремите си през 1931 г. Доказателството му използва техниката на самопозоваване (self-reference), известна още и като диагонален процес на Кантор. Същата математическа техника причинява и известния парадокс на Ръсел в наивната теория на множествата.
Първите доказателства се отнасят до формални аналози на аритметиката, задавана чрез аксиоми на Пеано.
През 1936 г. Алън Тюринг опростява определението на понятието формален метод, свеждайки го до Машина на Тюринг. Той формулира и първите алгоритмично нерешими задачи, като отбелязва връзката им с теоремата на Гьодел. Доказателствата му също използват самопозоваване (за компютърни програми по-точният термин е самоизследване).
Гьоделевото твърдение е подобно на самоизписваща се програма, по-точно то описва поведението на самоизследваща се компютърна програма P, реализираща следния алгоритъм:
Формулата (P се зацикля) е Гьоделево твърдение. То е вярно в нормалния свят на компютърните програми, тъй като единственото поведение на програмата P, което не създава абсурдна ситуация, е тя да търси в т. 3. на алгоритъма доказателство за верността на някоя от двете формули (P спира) и (P се зацикля), без да го намира никога.
Конструкцията на програмата P гарантира, че формулата (P се зацикля) е недоказуема в T, т.е. теорията не е пълна (не съдържа като теореми всички верни твърдения). Думата верни употребяваме в смисъл съдържателно (семантично) верни факти в изследваната област G.
Всички усилия да създадем пълна формална теория за област на изследване, чиято сложност е достатъчна да изрази понятието алгоритъм, са напразни. Можем да добавяме нови аксиоми, но конструкцията на Гьоделево твърдение ще ни даде нова недоказуема формула. Ако добавим всички верни твърдения за G като нови аксиоми ще получим теория, в която нямаме ефективен метод за разпознаване на аксиомите.
Прецизиране на доказателството на първата теорема на Гьодел за непълнота, по-точно провеждането му във формалната теория T, дава като резултат втората теорема на Гьодел за непълнота известна още като теорема на Гьодел за непротиворечивост:
Ако теорията T е непротиворечива, формулата (T е непротиворечива) е недоказуема в T.
Втората теорема обезсмисля усилията да се изгради единна, сигурна и надеждна математическа теория, която да се използва без уговорки като основа или инструмент в останалите науки.
Теоремата на Гьодел (в двете ѝ форми) налага силни ограничения върху формалните математически теории и върху методите на научно изследване изобщо. Прието е научното изследване да се разглежда като комбинация от експериментални методи и теоретични конструкции, като последните използват за основа математически теории.
След като формалните математически теории са съществено семантично непълни (такъв е смисълът на първата теорема) и тяхната непротиворечивост е недоказуема (по втората теорема), възниква изкушението да се обсъждат алтернативни пътища.
Не е наличен друг инструмент за теоретични заключения. Формалните теории са единственият приемлив от гледна точка на представата ни за научен метод инструмент за логично извеждане на следствия от начални предпоставки.
По-разумно е да се примирим с факта, че обитаваме реалност, в която действат закони, които ни ограничават както по отношение на физическите закони (примерно невъзможността физически обект да се движи по-бързо от светлината), така и по отношение на методите ни за натрупване на знания.