[Метаматематика]
аЧ раздел математической логики, изучаюнщий основания математики, структуру математических доказательств и математических теорий с помощью формальных методов. М. рассматривает формализованную теорию как множество ненкоторых конечных последовательностей символов, называемых фор- мулами и термами, к которым добавляется множество операций, производимых над этими последовательностями. Формулы и тернмы, получаемые с помощью простых правил, служат заменой преднложениям и функциям содержательной математической теории. Операции над формулами соответствуют элементарным шагам дендукции в математических рассуждениях. Формулы, соответствуюнщие аксиомам содержательной теории, выступают в качестве акнсиом формализованной теории. Формулы, которые могут быть выведены из аксиом посредством принятых операций, соответнствуют теоремам содержательной теории. Множество формул и множество термов, рассматриваемые как множества конечных последовательностей с операциями, в свою очередь, могут быть объектами математического исследования. В ранний период развития математической логики использовались в основном простые методы, исключались все нефинитные. Лиденром этого направления был Д. Гильберт, полагавший, что с понмощью простых методов М. удастся доказать непротиворенчивость фундаментальных математических теорий. Однако теонремы К. Гёделя показали, что программа Гильберта неосуществинма. Использование финитных методов для исследования форманлизованных теорий является естественным в силу их очевидного финитного характера. Но на практике ограничение методов доканзательства элементарными методами значительно усложняет мантематические исследования. Поэтому для более глубокого проникнновения в сущность формализованных теорий современная М. широко использует более сложные, нефинитные методы. Множество термов любой формализованной теории является алнгеброй, и множество всех формул также является алгеброй. После естественного отождествления эквивалентных формул множество всех формул становится решеткой (структурой), а именно: булевой алнгеброй, псевдобулевой алгеброй, топологической булевой алгеброй и т. п. - в зависимости от типа логики, принимаемой в теории. Эти алгебры, в свою очередь, связаны с понятием поля множеств и тонпологического пространства. С этой точки зрения представляется еснтественным применение в М. методов алгебры, теории решеток (струкнтур), теории множеств и топологии. В М. широко используется также гёделевский метод арифметизации и теория рекурсивных функций. М. исследует вопросы непротиворечивости и полноты форманлизованных теорий; независимость аксиом; проблему разрешинмости; вопросы определимости и погружения одних теорий в друнгие; дает точное определение понятия доказательства для различнных формализованных теорий и доказывает теоремы о дедукции; изучает проблемы интерпретации формальных систем и их разнличные модели; устанавливает разнообразные отношения между формализованными теориями и т. п.
