Формалізована аксіоматична теорія натуральних чисел

МІНІСТЕРСТВО  ОСВІТИ І НАУКИ, МОЛОДІ ТА СПОРТУ

Бердянський державний педагогічний університет

Інститут фізико-математичної і  технологічної освіти

Кафедра математики та методики викладання математики

Формалізована аксіоматична теорія натуральних чисел

(Курсова робота)

                                           Студентки 5 курсу

денної форми навчання

Науковий керівник:

старший викладач

Бердянськ – 2012

ЗМІСТ

ВСТУП

У безлічі формул виділяється підмножина аксіом, і задається кінцеве число правил виводу - таких правил, за допомогою яких (і тільки за допомогою їх) з аксіом і раніше виведених теорем можна утворити нові теореми. Всі аксіоми також входять до числа теорем. Іноді (наприклад в аксіоматиці Пеано) теорія містить нескінченну кількість аксіом, що задаються за допомогою однієї або декількох схем аксіом. Таким способом задається формальна аксіоматична теорія.

Повнота аксіоматичної теорії - логіко-методологічна вимога до аксіоматично побудованим теоріям і полягає  в тому, що в даній аксіоматичної, формальній системі мають бути доведені (тобто виведені з аксіом) усі  істинні речення цієї теорії. У  зв'язку з розрізненням синтаксичних і семантичних аксіоматичних  теорій вимога повноти диференціюється; виділяється синтаксична повнота  в слабкому сенсі (всі пропозиції, що належать некоректній системі, виводяться або спростовуються в ній) і в  сильному сенсі (після додавання  до аксіомам пропозиції , не виведеного в цій системі, вона стає суперечливою), семантична повнота щодо певної моделі (кожне речення, відповідне істинному  висловом в даній моделі, що виводиться в цій системі).

У ході досліджень достатньо  багатих аксіоматичних теорій (наприклад, арифметики ) була доведена (Гедел' - 1931 та наступні результати) їх принципова не повнота, тобто наявність таких  пропозицій, які в їх рамках недоведені. Вимога повноти не є абсолютно  неминучою умовою успішної аксіоматизації: неповні теорії можуть мати успішні  практичні додатки.

Дослідженню формалізованої аксіоматичної теорії натуральних  чисел присвяченні роботи таких  вчених як Л. М. Вивальнюк, І. Т.Демидов, О. І. Бородін, А. М. Френкель  та ін.

У 30-і рр.. XX століття Курт Гедель показав, що є цілий клас теорій першого порядку, що є неповними. Більш того, формула, яка стверджує несуперечність теорії, також невиведені засобами самої теорії . Цей висновок мав величезне значення для математики, так як формальна арифметика (а на ній базується теорія дійсних чисел, без якої не можна уявити сучасну математику) є якраз такою теорією першого порядку, а отже, формальна арифметика і всі теорії, що містять її, у тому числі теорія дійсних чисел, є неповними.

Мета дослідження: розкрити елементи формалізованої аксіоматичної теорії натуральних чисел.

Об’єкт дослідження: елементи формалізованої аксіоматичної теорії натуральних чисел.

Предмет дослідження: пошук оптимальних розв’язків задач формалізованої аксіоматичної теорії натуральних чисел.

Завдання дослідження:

1. Вивчити  наукову, психолого-педагогічну та навчальну літературу з предмету дослідження. 
2. Розкрити теоретичні основи формалізованої аксіоматичної теорії натуральних чисел.
3. Систематизувати теоретичні відомості,  розкрити елементи формалізованої аксіоматичної теорії натуральних чисел.

Курсова робота складається  зі вступу, двох розділів, висновків, переліку літератури. Загальний обсяг роботи 28 сторінок.

РОЗДІЛ І. ТЕОРЕТИЧНІ ОСНОВИ ФОРМАЛІЗОВАНОЇ АКСІОМАТИЧНОЇ  ТЕОРІЇ НАТУРАЛЬНИХ ЧИСЕЛ

1. Основні відомості про аксіоматичну теорію натуральних чисел

Аксіоматичний метод — спосіб побудови наукової теорії, при якому в основу теорії кладуться деякі вихідні положення, що їх називають аксіомами теорії, а всі інші положення теорії випливають як логічні наслідки аксіом. Більшість напрямків сучасної математики, теоретична механіка, ряд розділів фізики побудовані на основі аксіоматичного методу. В математиці аксіоматичний метод дає можливість створення закінчених, логічно завершених наукових теорій. Не менше значення має й те, що математична теорія, побудована аксіоматично, часто знаходить застосування в інших науках.

У математиці аксіоматичний метод зародився в роботах давньогрецьких геометрів. Блискучим зразком його застосування аж до XIX ст. була геометрична система, відома під назвою «Начала» Евкліда (бл. 300 до н.е.). Хоча в той час не поставало ще питання про опис логічних засобів, застосовуваних для отримування змістовних наслідків з аксіом, у системі Евкліда вже досить чітко прослідковується ідея отримання всього основного змісту геометричної теорії чисто дедуктивним шляхом, з певного, відносно невеликого, числа тверджень — аксіом, істинність яких уявлялася наочно очевидною.

Відкриття на початку XIX ст. неевклідової геометрії М. І. Лобачевським та Я. Больяї стало поштовхом до подальшого розвитку аксіоматичного методу. Вони встановили, що, замінивши звичний і, здавалося б, єдино «об'єктивно істинний» V постулат Евкліда про паралельні прямі його запереченням, можна розвивати чисто логічним шляхом геометричну теорію, настільки ж струнку і багату змістом, як і геометрія Евкліда. Цей факт змусив математиків XIX ст. звернути особливу увагу на дедуктивний спосіб побудови математичних теорій, що призвело до виникнення зв'язаної із самим поняттям аксіоматичного методу і формальної (аксіоматичної) математичної теорії нової проблематики, на основі якої виросла так звана теорія доведень як основний розділ сучасної математичної логіки.

Розуміння необхідності обґрунтування математики і конкретні задачі в цій області зародилися в більш-менш виразній формі вже в XIX ст. Уточнення основних понять аналізу і зведення складніших понять до найпростішого на точній і логічно усе міцнішій основі, а також відкриття неевклідових геометрій стимулювали розвиток аксіоматичного методу і виникнення проблем загальнішого математичного характеру, таких, як несуперечність, повнота і незалежність тієї чи тієї системи аксіом.

Перші результати в цій області  приніс метод інтерпретацій, який може бути описаний у такий спосіб. Нехай кожному вихідному поняттю і співвідношенню даної аксіоматичної теорії Т поставлений у відповідність певний конкретний математичний об'єкт. Сукупність таких об'єктів називається полем інтерпретації. Усякому твердженню U теорії Т природним чином ставиться у відповідність певне висловлення U* про елементи поля інтерпретації, яке може бути істинним чи помилковим. Тоді говорять, що твердження U теорії Т відповідно істинне або помилкове в даній інтерпретації. Поле інтерпретації і його властивості звичайно самі є об'єктом розгляду певної математичної теорії T₁, яка, зокрема, може бути теж аксіоматичною.

Метод інтерпретацій дозволяє встановлювати факт відносної несуперечливості, тобто довести твердження типу: «якщо теорія T₁ несуперечлива, то несуперечлива і теорія Т». Нехай теорія Т проінтерпретована в теорії T₁ таким чином, що всі аксіоми А_і теорії Т інтерпретуються істинними твердженнями А_і* теорії Т₁. Тоді всяка теорема теорії Т, тобто всяке твердження А, логічно виведене з аксіом А_і в Т, інтерпретується в T₁ певним твердженням А*, яке можна вивести у Т з інтерпретацій А*_і аксіом А_і, і отже істинним. Останнє твердження спирається на ще одне припущення, що робиться неявно нами, певної подібності логічних засобів, застосовуваних у теоріях Т и Т₁. Практично ця умова звичайно виконується. Нехай тепер теорія Т суперечлива, тобто якесь твердження А цієї теорії виведене в ній разом зі своїм запереченням. Тоді з вищесказаного випливає, що твердження А* та «не А*» будуть одночасно істинними твердженнями теорії Т₁, тобто теорія Т₁ суперечлива. Цим методом була, напр., доведена (Ф. Клейн, А. Пуанкаре) несуперечливість неевклідової геометрії Лобачевського в припущенні, що несуперечлива геометрія Евкліда, а питання про несуперечливість гільбертової аксіоматизації евклідової геометрії був зведений (Д. Гільберт) до проблеми несуперечливості арифметики.

Метод інтерпретацій дозволяє також  вирішувати питання про незалежність систем аксіом: для доказу того, що аксіома А теорії Т не виводима з інших аксіом цієї теорії і, отже, істотно необхідна для отримання всього обсягу даної теорії, досить побудувати таку інтерпретацію теорії Т, у якої аксіома А була б помилкова, а всі інші аксіоми цієї теорії істинні. Згадане вище зведення проблеми несуперечливості геометрії Лобачевского до проблеми несуперечливості евклідової геометрії, а цієї останньої — до питання про несуперечливість арифметики має своїм наслідком твердження, що V постулат Евкліда невиводимій з інших аксіом геометрії, якщо тільки несуперечливою є арифметика натуральних чисел.

Слабкий бік методу інтерпретацій  полягає в тому, що в питаннях несуперечливості і незалежності систем аксіом він дає можливість одержувати лише результати, що носять відносний  характер. Важливим досягненням цього  методу став той факт, що з його допомогою  була виявлена особлива роль арифметики як такої математичної теорії, до питання про несуперечності якої зводиться аналогічне питання для цілого ряду інших теорій.

Подальший розвиток — у відомому смислі це була вершина — аксіоматичний метод дістав у роботах Д. Гільберта і його школи. У рамках цього напряму було вироблено подальше уточнення поняття аксіоматичної теорії, а саме поняття формальної системи. У результаті цього уточнення виявилося можливим представляти самі математичні теорії як точні математичні об'єкти і будувати загальну теорію, або метатеорію, таких теорій. При цьому привабливою представлялася перспектива (і Д. Гільберт був у свій час нею захоплений) вирішити на цьому шляху всі головні питання обґрунтування математики. Усяка формальна система будується як точно окреслений клас виразів — формул, у якому певним точним образом виділяється підклас формул, що називають теоремами даної формальної системи. При цьому формули формальної системи самі не несуть у собі ніякого змістовного смислу; їх можна будувати з довільних знаків або елементарних символів, керуючись тільки міркуваннями технічної зручності. Насправді спосіб побудови формул і поняття теореми тієї чи тієї формальної системи вибираються з таким розрахунком, щоб весь цей формальний апарат можна було застосовувати для якомога адекватнішого і повнішого вираження тієї чи тієї конкретної математичної (або не математичної) теорії, точніше, як її фактичного змісту, так і її дедуктивної структури. Усяку конкретну математичну теорію Т можна перекласти на мову придатної формальної системи S таким чином, що кожне осмислене (неправдиве або істинне) висловлювання теорії Т виражається певною формулою системи S.

Природно було сподіватися, що метод  формалізації дозволить будувати весь позитивний зміст математичних теорій на такій точній і, здавалося б, надійній основі, як поняття виведеної формули (теореми формальної системи), а принципові питання типу проблеми несуперечності математичних теорій вирішувати формі  доказів відповідних тверджень  формальних систем, які формалізують ці теорії. Щоб одержати доведення  тверджень про несуперечливість, що не залежать від тих потужних засобів, які в класичних математичних теоріях саме і є причиною ускладнень їх обґрунтування, Д. Гільберт пропонував досліджувати формальні системи  т.зв. фінітними методами (див. Метаматематика).

Однак результати К. Геделя початку 30-х р. XX ст. призвели до краху основних надій, що зв'язувалися з цією програмою. К. Гедель показав наступне.

1. Усяка природна, несуперечлива  формалізація S арифметики або будь-якої іншої математичної теорії, яка містить арифметику (напр., теорії множин), неповна і непоповнювана в тому розумінні, що: а) у S містяться (змістовно істинні нерозв'язні формули, тобто такі формули А, що ні А, ні заперечення А не виводимі у S (неповнота формалізованої аріфметики); б) хоч би якою скінченною множиною додаткових аксіом (напр., нерозв'язними в S формулами) розширювати систему S, у новій, посиленій таким чином формальній системі неминуче з'являться свої нерозв’язні формули (непоповнюваність; див. також Геделя теорема про неповноту).

2. Якщо формалізована  арифметика насправді несуперечлива,  то, хоча твердження про її  несуперечливість може бути висловлено  її власною мовою, доведення  цього твердження неможливо провести  засобами, що формалізуються в  ній самій.

Це означає, що вже для арифметики принципово неможливо вичерпати  весь обсяг її змістовно істинних суджень класом виводимих формул хоч якою формальною системою і що немає жодної надії отримати яке-небудь фінітне доведення несуперечливості арифметики, тому що, очевидно, усяке  розумне уточнення поняття фінітного  доведення виявляється формалізуємим  у формальній арифметиці.

Усе це ставить певні границі  можливстям А. м. у тому його вигляді, який він набув у рамках гільбертовського формалізму. Однак і в цих границях він відіграв і продовжує відігравати  важливу роль у основах математики. Так, напр., уже після описаних результатів  К. Геделя ним же в 1938-40 рр., а потім П. Коеном у 1963 р. на основі аксіоматичного підходу із застосуванням методу інтерпретацій були отримані фундаментальні результати про сумісність (тобто відносну несуперечливість) і незалежність аксіоми вибору і континуум-гіпотези в теорії множин. Що стосується такого основного питання основ математики, як проблема несуперечливості, і після результатів К. Геделя стало ясно, що для його розв’язування, очевидно, не обійтися без інших, відмінних від фінітистських, засобів та ідей. Тут виявились можливими різні підходи, з огляду на існування різних поглядів на припустимість тих чи інших логичних засобів.

З результатів про несуперечливість формальних систем варто вказати  на доведення несуперечливості формалізованої арифметики, яке спирається на нескінченну  індукцію до певного зліченого трансфінітного числа.

2. Поняття про формалізовану аксіоматичну теорію натуральних чисел

Загальна схема  побудови формальної системи  .

Розглянемо коротко відомості  про формальну систему , яка є формалізованою аксіоматичною теорією натуральних чисел. Формальна система відрізняється від змістовної аксіоматичної теорії натуральних чисел рядом особливостей. По-перше, в явно представлені і використовуються засоби логічних доведень теорем арифметики. По-друге, аксіома індукції в не повністю відповідатиме аксіомі індукції в змістовній аксіоматиці натуральних чисел. Крім того, сам процес побудови теорії має більш формальну, абстрактну (і значно громіздкішу) форму.

Побудову формальної системи  здійснюватимемо засобами мови  L. Для нього в алфавіті  А мови  L здійснимо такі зміни: вилучимо всі предикатні і функціональні символи, замість них введемо один предикатний індивідуальний символ «» («менше»), три індивідуальні символи алгебраїчних операцій: «'» (унарна операція «слідування»), «+» (бінарна операція додавання), «•» (бінарна операція множення), залишимо одну індивідуальну константу «1 ».  В результаті цих змін дістали алфавіт системи .

Далі до множини и    аксіом мови  L приєднуємо множину аксіом Пеано (позначимо її через ) і множину аксіом порядку (позначимо її через ).

Аксіоми Пеано формулюються так, як і в змістовній аксіоматиці, аксіома індукції подається такою  формулою: , де - одномісний предикат.

Аксіоми порядку

або ((x<y)(y<z)⇒(x<z) )

3. ((x<y)
4. .

Таким чином, формальна система    містить 13  логічних аксіом і 15  спеціальних, а саме: 4 аксіоми рівності, 7 аксіом Пеано і 4 аксіоми порядку, разом 28 аксіом. Правила виведення такі самі, що й у мові L.

Приклад доведення  в  системі .

Домовимось про такі позначення. Вираз  «А В» читатимемо:  «А позначає (є назвою для)  В». Наприклад, вираз означає: «буквою F позначаємо формулу ». Символом підстановку елемента  b замість a. В дужках подаватимемо коротке обґрунтування утворених вивідних формул.

Зміст теорем К. Геделя

У 1931 р. у статті «Про формально  нерозв’язні твердження Principia Mathematica і споріднених систем» австрійський математик К. Гедель вміщує дві свої відомі теореми, які займають центральне місце в основах математики. Ці теореми були новими і несподіваними щодо математичних висновків, оригінальним був і метод доведення їх.

Перш ніж описати зміст  і значення теорем Геделя, розглянемо деякі поняття, які фігурують  у цих теоремах.

По-перше, в цих теоремах йдеться про формальні аксіоматичні теорії, які інтуїтивно вважаються досить багатими (або досить змістовними), тобто такими, що їхніми засобами можна  виразити арифметику натуральних чисел і, тим більше, теорію множин.

По-друге, у цих теоремах фігурує поняття формально нерозв’язної формули, тобто такої (як правило, замкненої) формули Ф даної формальної системи, яку засобами цієї системи не можна  ні довести, ні спростувати (тобто, довести ). Якщо засобами даної ф. а. т. можна довести формулу Ф або , то таку формулу називають формально розв’язною (скорочено ф. р. ф.).

По-третє, у своїх теоремах Гедель вводить поняття . Ф. а. т., яка містить арифметику натуральних чисел, називають , якщо в ній немає жодної такої формули , яка виражає певну властивість натуральних чисел, що всі формули одночасно є теоремами. Якщо ф. а. т. містить хоча б одну таку формулу, то її називають . З випливає формальна несуперечливість, але не навпаки. Ф. а. т. називають формально несуперечливою, якщо не кожне її твердження можна довести засобами цієї системи.

Ф. а. т. називають формально  повною, якщо кожна її  формула  є ф. р. ф., і формально неповною в противному випадку.

Сформулюємо теореми Геделя. Позначимо через  ф. а. т., яка містить арифметику натуральних чисел.

Теорема (1) .  Якщо , то вона формально неповна.

У 1936 р. американський математик  Д. Б. Россер показав, що в цій теоремі  можна обійтися без поняття .

Теорема (у формі  Россера). Якщо ф. а. т. формально несуперечлива, то вона формально неповна.

Формальна нерозв'язність  якої-небудь формули ф. а. т. не означає, що ця теорія неспроможна виявити (певними  засобами) змістовну істинність чи хибність цієї формули. Наприклад, формула, яку будує Гедель у процесі  доведення теореми (1), формально  нерозв’язна, але змістовно істинна.

Йдеться про те, що не кожне  змістовно істинне твердження, виражене формулою у ф. а. т., може бути в ній  доведене.

Теорема (1) має принципове гносеологічне і методологічне  значення: з неї випливає, що дедуктивні можливості будь-якої досить багатої  ф. а. т. обмежені, зокрема змістовну  арифметику повністю формалізувати  не можна.

Було також доведено, що система аксіом формальної арифметики не поповнювана: якщо до даної системи  аксіом приєднати нерозв’язну (але  змістовно істинну) формулу, то в арифметиці з поповненою системою аксіом знову знайдеться нерозв’язна (і змістовно істинна) формула і т. д.

Отже, в будь-якій досить багатій ф. а. т. існує безліч змістовно  істинних тверджень, які не можна  дістати формалізованими засобами цієї теорії. Процес математичного  доведення не можна повністю звести до застосування аксіоматичного методу, без елементів математичної винахідливості не обійтися. Математична творчість  настільки багатогранна і глибока, що її не можна втиснути в рамки  будь - якої ф. а. т.

Теорема (2). Якщо ф. а. т. несуперечлива, то довести її несуперечливість засобами, які можна в ній формалізувати, неможливо.

Ця теорема є наслідком  теореми (1) про неповноту. Її іноді  називають теоремою про несуперечливість. З теореми (2) випливає, що довести  несуперечливість формалізованої класичної  математики принципово неможливо, і  план Гільберта щодо обґрунтування  основ математики на шляху повної формалізації аксіоматичного методу не можна повністю реалізувати. З цієї теореми також випливає, що для  доведення несуперечливості системи  формалізованої арифметики треба використати інші засоби, які не можна формалізувати в самій ф, а. т. . Так, німецький математик Г. Генцен у 1936 р., використовуючи так званій метод трансфінітної індукції, довів несуперечливість ф. а. т.. Проте не всі математики визнають це доведення. Згодом аналогічно виконали доведення несуперечливості Аккерман (1940), Лоренц (1951), Шютте (1951), Хлодовський (1959).

Хоч ці доведення проведено  не повністю в рамках ф, а. т. , вони мають велику пізнавальну цінність, сприяють глибшому розумінню природи основ математики.

Аксіома індукції у формальній 1 змістовній теоріях  натуральних чисел. Підсумки.

Система аксіом формалізованої арифметики натуральних чисел (системи ) містить два індивідуальних предикати «=» і «<» і невизначений предикат в аксіомі індукції.

У цьому відношенні вона відрізняється від інших аксіом, оскільки аксіома в звичайному розумінні  описує властивості індивідуального  предиката, а аксіома індукції е  класом аксіом. За зовнішнім виглядом аксіома індукції в змістовній  і  формалізованій арифметиці однакова. Але між ними значна відмінність. У змістовій теорії натуральних  чисел предикатів можна утворити стільки, скільки існує підмножин у множині натуральних чисел, тобто континуум предикатів. В той же  час у системі в аксіомі індукції може брати участь лише зчисленна множина предикатів  (так званих арифметичних предикатів), які визначаються формулами цієї системи.

Підведемо короткий підсумок про властивості аксіом у змістовній і формалізованій аксіоматичних  теоріях натуральних чисел.

Змістовна теорія. Система  аксіом цієї теорії категорична і  незалежна. Несуперечливість не може бути доведена за методом моделей, бо при  цьому доведеться користуватися  моделями складнішої природи, в несуперечливості яких менше впевненості, ніж у  несуперечливості арифметики. Абсолютне  доведення несуперечливості в цій  теорії також неможливе, бо тут немає  поняття формального доведення, Отже, впевненість у несуперечливості змістовної теорії має науково-природничий, досвідний характер, такий, як скажімо, наукові гіпотези у фізиці або  хімії, які не можна вивести формально. В цій теорії ми не маємо повної гарантії від суперечностей, але  є досить велика практична впевненість  в її несуперечливості.

З несуперечливості і категоричності змістовної аксіоматичної теорії випливає її повнота в тому розумінні, що всі  істинні твердження інтуїтивної  арифметики можна мати в змістовній аксіоматичній теорії.

Формалізована теорія,  як уже зазначалося раніше, неповна, і провести абсолютне доведення  її несуперечливості принципово неможливо.

Шведський математик Т. Сколем довів, що формальна система  некатегорична. Водночас змістовна аксіоматична теорія натуральних чисел, як відомо, категорична. Ця розбіжність пояснюється відмінністю аксіом індукції в змістовній і формальній теоріях.

1.3. Можливості і межі формалізації

Можливості  і межі формалізації (філософський зміст теорем Геделя, Тарського)

У розумінні основних проблем формалізації - її суті, пізнавальної цінності, умов і меж застосування - серед філософів, логіків і істориків науки  відсутня єдина думка. Нерідко висловлюються  прямо протилежні погляди - перебільшення  ролі формалізації і формалізованого  мови і недооцінка значення формалізованих методів дослідження.

Давид Гільберт (1862-1943), засновник формалістичної школи в математики, припускав, що все наше знання, і перш за все математичне, може бути повністю формалізовано.Ідеї Гільберта взяли багато талановитих математики, серед яких П. Бернайс (1888-1977), Дж. Гербрандта (1908-1931), В. Аккерман (1898-1962), Дж. фон Нейман (1903-1957).

Однак у 1931 р. Курт Гедел у статті «Про формально нерозвязних пропозиціях« Principia Mathematica »і споріднених систем» довів відому теорему про неповноту формалізованої арифметики. Він довів, що в системі «Principia Mathematica» і в будь-який інший формальної системи, здатної виразити арифметику натуральних чисел, є нерозвязні (тобто недоведені і разом з тим незаперечні в даній системі) пропозиції. Теорема Геделя свідчить про те, що арифметика натуральних чисел включає зміст, який не може бути виражена виключно на основі логічних правил освіти і перетворення відповідної формальної системи. Більш того, формула логічного числення, здатного формалізувати елементарну арифметику, бездоказова як формула, що виражає її послідовність. Таким чином, несуперечності не можна досягти, використовуючи інструменти, що належать до тієї ж формальної системі. Це було справжнє поразку програми Гільберта.

Неповнота формалізованих систем, що містять арифметику, означає, що у  змістовній математичної теорії завжди можна знайти справжнє пропозиція, яку не можна довести за допомогою  аксіом формальної теорії, формалізує змістовну цю теорію. Крім того, у більш багатої формальної системі, до якої недоведені пропозиція приєднано як аксіоми, його можна тривіально довести, але тим не менше і в новій системі є можливість побудувати аналогічне недоказово пропозицію і, таким чином, завжди залишається певний «формалізації залишок». Ця теорема показала неможливість дати у рамках формальної побудови підставу всій як сьогоднішній, так і майбутньої математіке251. Гедель показав нездійсненність в цілому програми Гільберта, яка передбачала повну формалізацію істотної частини математики. Вона обмежила саму ідею, яка виходить від робіт Лейбніца, про формалізацію всій раціональної думки у вигляді синтаксичних структур і розумінні мислення як ігри символів безвідносно їх значення. Тому теорема Геделя часто розглядається як досить суворе обгрунтування принципову неможливість повної формалізації наукових міркувань і наукового знання в цілому.