Метатеория

- совокупность математич. средств и методов, предназначенных для описания и определения нек-рой формальной аксиоматич. теории, а также для исследования ее свойств. М. является важной составной частью метода формализации - одного из центральных методов математич. логики. Суть этого метода можно кратко охарактеризовать следующим образом. Допустим, нас интересует нек-рая содержательная математич. теория T1. Это может быть сложная теория, семантика к-рой недостаточно интуитивно ясна (напр., это может быть теория множеств, математич. анализ, арифметика 2-го порядка и т. п.). Нас интересует, является ли Т 1 непротиворечивой теорией или совместен ли с Т 1 нек-рый математич. принцип (напр., выбора аксиома). С целью выяснения этого вопроса вначале формулируется точный логико-математич. язык Q такой, что все интересующие пас утверждения Т 1 записываются в виде формул языка Q. Затем логич. принципы, употреблявшиеся в теории для получения новых фактов, формализуются в виде аксиом и чисто формальных правил вывода, позволяющих выводить новые формулы языка Qиз аксиом и уже выведенных формул. Таким образом, возникает формальная система (или, иначе, формальная аксиоматическая теория, исчисление) [img: http://localhost:8080/file/031410-152.jpg] точно описывающая нек-рый интересующий, нас фрагмент содержательной теории Т 1. Существенно при этом, что формулировка [img: http://localhost:8080/file/031410-153.jpg] не требует исчерпывающего проникновения в, быть может, весьма сложную семантику Т 1. Исчисление [img: http://localhost:8080/file/031410-154.jpg] строится по простым законам как чисто знаковая система и для понимания устройства этой знаковой системы нет нужды вникать в смысл выводимых в ней формул. Такой подход открывает, во-первых, возможность строго математически сформулировать интересующие нас проблемы, относящиеся к выводимости нек-рых формул в [img: http://localhost:8080/file/031410-155.jpg] и, во-вторых, исследовать [img: http://localhost:8080/file/031410-156.jpg] средствами нек-рой содержательной теории Т 2. В этой ситуации [img: http://localhost:8080/file/031410-157.jpg] наз. предметной теорией, а Т 2- ее метатеорией. С точки зрения оснований математики важно, чтобы Т 2 была в нек-ром отношении более надежной теорией, чем Т 1, так что исследование [img: http://localhost:8080/file/031410-158.jpg] средствами Т 2 можно было бы рассматривать как действительное разъяснение и обоснование неясных деталей семантики Т 1 с помощью более убедительной теории Т 2. В этой связи особенное предпочтение отдается достаточно надежным М., отражающим финитные установки в математике, теориям, построенным в рамках интуиционизма или конструктивной математики. Впрочем, вне оснований математики это ограничение не является обязательным. Если нас интересует не столько вопрос об интуитивной ясности Т 1, сколько просто факт о выводимости или невыводимости нек-рых формул в [img: http://localhost:8080/file/031410-159.jpg] естественно исследовать [img: http://localhost:8080/file/031410-160.jpg] средствами любой исторически сложившейся и убедительной для исследователя математич. теории Т 2, не накладывая никаких априорных ограничений. Можно далее исследовать аналогичным образом и метатеорию Т 2, построив формальную систему [img: http://localhost:8080/file/031410-161.jpg] и изучая уже [img: http://localhost:8080/file/031410-162.jpg] средствами нек-рой метамета-теории Т 3. Такого рода исследования характерны для доказательств теории.