Метаматематика , теорія доказів, теорія доказу, в широкому сенсі слова — метатеорія математики, що не передбачає жодних спеціальних обмежень на характер використовуваних метатеоретічеських методів, на спосіб завдання і об'єм досліджуваної в М. «математики». Поширенішим і історично ранішим (тим паче, що М. взагалі була першим прикладом «метанауки») є наступне, більш спеціальне розуміння терміну «М-коду.», що йде від Д. Гильберта . Відкриття парадоксів (антиномій ) в логіці і безлічі теорії висунуло на початку 20 ст завдання перебудови підстав математики і логіки на деякій основі, що виключає появу протиріч. Програма логіцизму передбачала для цієї мети «зведення» математики до логіки за допомогою аксіоматичного методу, але незалежно від успішності такого «зведення» для перебудованої т.ч. математики (або лежачої в її основі логіки) відсутність відомих і неможливість появи нових антиномій могла гарантувати лише доказ їх несуперечності . Представники математичного інтуїционізма пропонували настільки радикально переглянути вміст самого поняття «математика», щоб повинні (і навіть лише підозрювані) в появі антиномій абстракції класичної математики (як, наприклад, абстракція актуальної нескінченність) були раз і назавжди вигнані з неї. Висунута Гільбертом концепція математичного формалізму, з одного боку, відмовлялася від логицистічеських ілюзій про можливість обгрунтування математики шляхом «зведення» її до логіки, але з іншої — рішуче не розділяла і інтуїционістського скепсису по відношенню до можливостей аксіоматичної побудови задовільною в логічному відношенні математики. Приймаючи значну частину інтуїционістськой критики за адресою традиційної класичної математики, Гільберт в той же час вирішив «реабілітовувати» аксіоматичну установку: «Ніщо не може вигнати нас з раю, який створив нам Кантора», — говорив він. Для цього перш за все потрібна була послідовна формалізація математичних теорій, що підлягають обгрунтуванню (аксіоматичній теорії безлічі, аксіоматичної арифметики), тобто вистава їх у вигляді числень (формальних систем ) , для яких «чисто формально» слід визначити поняття аксіоми (формули деякого спеціального вигляду), виводу (послідовності формул, кожна з яких виходить з попередніх по строго фіксованих правилах виводу), докази (виводу з аксіом) і теореми (формули, завершальною формулою деякого доказу, що є), щоб потім, користуючись деякими «абсолютно об'єктивними» і «стовідсотково надійними» змістовними методами міркувань, показати недоказовність в даній формальній теорії протиріччя (тобто неможливість ситуації, при якій її теоремами виявлялася б яка-небудь формула і її заперечення). Сукупність таких «об'єктивних» і «надійних» (в усякому разі, невразливих з боку інтуїционістського критицизму) методів і повинна була скласти М. (теорію математичного доказу). Комплекс обмежень, що накладаються на допустимі в М. методи, Гільберт охарактеризував як фінітізм: у ще радикальнішій формі, ніж інтуїционізм, ця «фінітна установка» забороняє використання яких би то не було «метафізичних» заслань на безконечних («інфінітниє») сукупності. Обмеженням цим не задовольняють, наприклад, такі важливі метатеоретічеськие результати, як теорема До. Геделя про облиште числення предикатів і теорема Л. Льовенхейма — Т. Ськолема про інтерпретується будь-якої несуперечливої теорії на області натуральних чисел, оскільки використовуване в них поняття загальнозначущої формули числення предикатів визначається за допомогою «нефінітного» уявлення про «сукупність всіх можливих інтерпретацій» (тому ці метатеореми, строго кажучи, не належать до М., у зв'язку з чим їх часто відносять до металогике або до т.з. теоретико-множинній логіці предикатів). Проте (мета) теореми про несуперечність числення висловів і числення предикатів удалося отримати в руслі «фінітної установки», тобто строго метаматематичним дорогою. Та все ж гильбертовськая програма в її повному вигляді виявилася нездійсненною: Гедель (1931) показав, що жодна несуперечлива формалізація математики не може охопити всієї класичної математики (і навіть всієї формальної арифметики) — в ній неодмінно знайдуться т.з. нерозв'язні, т. е. виразимі на її мові, але не доказові і не спростовні її засобами (хоча і змістовно достеменні) формули. Прикладом такої формули є формула, що затверджує свою власну недоказовність; задати формулу з настільки парадоксальною на вигляд інтерпретацією Геделю удалося за допомогою придуманого їм дотепного прийому — свого роду арифметичного кодування («гедельовськой нумерації») символів, формул і послідовностей формул формальної системи, однозначно що приписує кожному елементу системи «гедельовський номер». Завдяки такій «арифметизації синтаксису» Геделю удалося представити не лише предикати даної формальної системи, але і метаматематичні предикати («бути формулою», «бути доказом», «бути теоремою» і т.п.), що відносяться до неї, за допомогою деяких арифметичних предикатів. Твердження цій т.з. першої теореми Геделя доводиться тепер за допомогою міркування, надзвичайно близького до т.з. парадоксу Рішара і взагалі до парадоксів типа «Брехуна» («я брешу») і варіантів антиномії Б. Рассела («цирульник, бриючий всіх тих і лише тих жителів села, які не голяться самі» і т.п.). Як слідство з цієї теореми виходить друга теорема Геделя, згідно якої несуперечність будь-якої несуперечливої формальної системи, що містить арифметику натуральних чисел, не може бути доведена засобами, що формалізуються в цій системі. У цих теоремах Геделя говориться, т. о., не лише про властивості даної формальної системи, але і про деякі метаматематичні властивості, так що вони є навіть не метатеоремамі, а, строго кажучи, метаметатеоремамі. З них витікає нездійсненність «фінітістськой» програми Гільберта: не лише вся математика, але навіть арифметики натуральних чисел не допускають формалізації, яка була б одночасно повною і несуперечливою; до того ж весь апарат фінітізма виразимо засобами інтуїционістськой арифметики, з чого, через другу теорему Геделя, слідує неможливість фінітістського доказу несуперечності арифметики. (Ще один фундаментальний результат М. — т.з. теорема А. Черча про нерозв'зність арифметики і числення предикатів, згідно якої не існує алгоритму розпізнавання довідності для формул відповідних числень.)
В деякому сенсі теореми Геделя можна було сприймати як «кінець М.», але, свідчивши про обмеженість фінітізма, формалізму і пов'язаною з ними гильбертовськой програми, а також аксіоматичного методу в цілому, ці теореми в той же час послужили потужною стимул-реакцією пошуку засобів доказів (зокрема, доказів несуперечності) сильніших, ніж фінітні, але і в певному значенні конструктивних. Одним з таких методів з'явилася т.з. трансфінітна індукція до першого недосяжного конструктивного трансфініта; ця дорога дозволила отримати доказ несуперечності арифметики (Р. Генцен, Ст Аккерман, П. С. Новіков, До. Шютте, П. Лоренцен і ін.). Ін.(Древн) прикладом може служити т.з. ультраїнтуїционістськая програма обгрунтування математики, що дозволила отримати абсолютний (що не користується редукцією до якої-небудь ін. системі) доказ несуперечності теоретико-множинної системи аксіом Цермела — Френкель.
Літ.: Гільберт Д., Підстави геометрії, пер.(переведення) з йому.(німецький), М-код.—Л., 1948, добавл. 6—10; Кліні С. До., Введення в метаматематику, пер.(переведення) з англ.(англійський), М., 1957; його ж, Математична логіка, пер.(переведення) з англ.(англійський), М., 1973; Каррі Х. Би., Підстави математичної логіки, пер.(переведення) з англ.(англійський), М., 1969, гл.(глав) 2—3; Генцен Р., Несуперечність чистої теорії чисел, пер.(переведення) з йому.(німецький), у кн.: Математична теорія логічного виводу, М., 1967, с. 77—153; Нагель Е., Ньюмен Дж., Теорема Геделя, пер.(переведення) з англ.(англійський), М., 1970; Тарський А., Введення в логіку і методологію дедуктивних наук, пер.(переведення) з англ.(англійський), М., 1948; Gödel K., Über formal unent scheidbare Sätze der Principia Mathematica und verwander System. I, «Monatshefte Mathematic Physik», 1931, Bd 38, S. 173—98; Rosser Ст, Extensions of some theorems of Gödel and Church, «Journal Symbolic Logic», 1936, v. 1 № 3; Tarski A., Logic, semantics, metamathematics, Oxf., 1956.
