Значення ГЕДЕЛЯ ТЕОРЕМУ ПРО НЕПОВНОТІ в математичній енциклопедії
Значення ГЕДЕЛЯ ТЕОРЕМУ ПРО НЕПОВНОТІ в математичній енциклопедії:
загальна назва двох теорем, встановлених К. Ґеделем [1]. Перша Р. т. про н. стверджує, що в будь-якій несуперечливій формальній системі, що містить мінімум арифметики (знаки та звичайні правила поводження з ними), знайдеться формально нерозв'язне судження, тобто така замкнута формула А, що неА,не є виведеними в системі. Друга Р. т. про н. стверджує, що при виконанні природних додаткових умов як можна взяти твердження про несуперечність аналізованої системи. Ці теореми знаменували невдачу початкового розуміння програми Гільберта в галузі основ математики, яка передбачала повну формалізацію всієї існуючої математики або значної її частини (неможливість цього показала перша Р. т. про н.) і обґрунтування отриманої формальної системи шляхом .фінітного доказу її несуперечності (друга Р. т. про н. показала, що навіть якщо фінітними вважаються всі засоби формалізованої арифметики, цього не вистачить для доказу несуперечності арифметики).
Формально нерозв'язне судження будується методом арифметизації синтаксису, який став одним з основних методів теорії доказів (метаматематики).
Фіксується нумерація основних формальних об'єктів (формул, кінцевих послідовностей формул і т. д.) натуральними числами така, що основні властивості цих об'єктів (бутиаксіомою,бутивисновкомза правилами системи і т.д. д.) виявляються розпізнаваними за номерами з допомогою дуже простих алгоритмів. Так само просто обчислюються за номерами вихідних даних номери результатів комбінаторних перетворень (напр., підстановки терму у формулу замістьзмінної). При цьому можна написати арифметич. формулу В(а,b),має вигляд (f - примітивно рекурсивна функція) і висловлює умову: b є номер формули, яка виходить з формули з номером апутем підстановки натурального числа авместо змінноїх.Якщор -номер формулито формулавиражає свою власну невиводимість. Вона і виявляється формально нерозв'язною. Звідси випливає, що у будь-якій несуперечливій системі з мінімальними виразними арифметичними можливостями є справжнє, але з судження зазначеного виду.
Друга Р. т. про н. виходить шляхом формалізації доказу першої Р. т. про н. Її доказ суттєво використовує особливості арифметизації синтаксису аналізованої системи, а саме - потрібна вивідність у цій системі формул, що виражають судження: 1) система замкнута щодо правила скорочення посилки (модус поненс);2) система замкнута щодо підстановки термів замість предметних змінних; 3) з істинності формули виду , де N - натуральне число, f - примітивно рекурсивна функція, випливає її виведення. Ці умови виконуються для природної арифметизації, але можна, не змінюючи алгоритм. характеристик арифметизації (всі функції та предикати залишаються примітивно рекурсивними), змінити її так, що формула, що виражає несуперечність системи (стосовно нової арифметизації), буде виведена. При цьому для нової арифметизації буде порушено умову 1).
Друга Р. т. про н. дає критерій порівняння формальних систем: якщо в системі Sможна довести несуперечність системиТ,то Sне занурюється в Т(див.Занурювальна операція).Так, доводиться, щоформальний математичний аналізне занурюється варифметику,типів теоріяне занурюється в аналіз, теорія множин Zне занурюється в теорію типів.
Літ. , 2 Aufl., Bd 2, Ст, 1970; [3] Кліні С. К., Введення в метаматематику, пров. з англ., М., 1957.