Метаматематика — это изучение самой математики с использованием математических методов. Это исследование создает метатеории , которые являются математическими теориями о других математических теориях. Акцент на метаматематике (и, возможно, создание самого термина) обязан попытке Дэвида Гильберта закрепить основы математики в начале 20 века. Метаматематика предоставляет «строгий математический метод для исследования большого разнообразия фундаментальных проблем математики и логики » (Клин, 1952, стр. 59). Важной особенностью метаматематики является ее акцент на различении рассуждений изнутри системы и извне системы. Неформальной иллюстрацией этого является отнесение предложения «2+2=4» к категории математики, а утверждение «2+2=4» действительно» к метаматематике. [1]
Метаматематические метатеоремы о самой математике первоначально отличались от обычных математических теорем в 19 веке, чтобы сосредоточиться на том, что тогда называлось фундаментальным кризисом математики . Парадокс Ричарда (Richard 1905), касающийся некоторых «определений» действительных чисел в английском языке, является примером противоречий, которые легко могут возникнуть, если не удается провести различие между математикой и метаматематикой. Нечто подобное можно сказать и относительно известного парадокса Рассела (Содержит ли множество всех тех множеств, которые не содержат самих себя?).
Метаматематика была тесно связана с математической логикой , так что ранняя история этих двух областей, в конце 19-го и начале 20-го веков, во многом пересекалась. Совсем недавно математическая логика часто включала изучение новой чистой математики, такой как теория множеств , теория категорий , теория рекурсии и чистая теория моделей , которая не имеет прямого отношения к метаматематике .
Серьезные метаматематические размышления начались с работы Готлоба Фреге , особенно с его Begriffsschrift , опубликованного в 1879 году.
Дэвид Гильберт был первым, кто регулярно использовал термин «метаматематика» (см. Программу Гильберта ) в начале 20 века. В его руках это означало что-то вроде современной теории доказательств , в которой финитарные методы используются для изучения различных аксиоматизированных математических теорем (Клин 1952, стр. 55).
Среди других выдающихся фигур в этой области — Бертран Рассел , Торальф Скулем , Эмиль Пост , Алонсо Чёрч , Алан Тьюринг , Стивен Клини , Уиллард Куайн , Пол Бенасерраф , Хилари Патнэм , Грегори Чайтин , Альфред Тарский , Пол Коэн и Курт Гёдель .
Сегодня металогика и метаматематика во многом пересекаются, и обе они в значительной степени включены в состав математической логики в академических кругах.
Открытие гиперболической геометрии имело важные философские последствия для метаматематики. До его открытия существовала только одна геометрия и математика; идея существования другой геометрии считалась маловероятной.
Говорят, что когда Гаусс открыл гиперболическую геометрию, он ничего не опубликовал о ней из страха перед «шумом беотийцев », которое разрушило бы его статус Princeps mathematicorum (лат. «Принц математиков»). [2] «Шум беотийцев» приходил и уходил, давая толчок развитию метаматематики и значительным улучшениям в математической строгости , аналитической философии и логике .
Begriffsschrift (по-немецки примерно «концептуальный сценарий») — это книга Готлоба Фреге пологике , опубликованная в 1879 году, и формальная система , изложенная в этой книге.
Begriffsschrift обычно переводится как написание концепций или обозначение концепций ; полное название книги определяет ее как « язык формул , созданный по образцу языка арифметики и чистого мышления ». Мотивация Фреге для разработки формального подхода к логике напоминала мотивацию Лейбница для его рационализатора исчисления (несмотря на это, в предисловии Фреге явно отрицает, что он достиг этой цели, а также то, что его главной целью было бы построение идеального языка, подобного языку Лейбница, который Фреге объявляет задачу довольно трудной и идеалистической, однако не невыполнимой). Фреге продолжал использовать свое логическое исчисление в своих исследованиях по основам математики , проводившихся в течение следующей четверти века.
Principia Mathematica, или «PM», как его часто сокращают, была попыткой описать набор аксиом и правил вывода в символической логике , на основе которых в принципе можно было доказать все математические истины. По существу, этот амбициозный проект имеет большое значение в истории математики и философии [3] , являясь одним из главных результатов веры в то, что такое предприятие может быть достижимо. Однако в 1931 году теорема Гёделя о неполноте окончательно доказала, что PM, как и любая другая попытка, никогда не сможет достичь этой цели; то есть для любого набора аксиом и правил вывода, предложенных для инкапсулирования математики, на самом деле будут существовать некоторые математические истины, которые невозможно вывести из них.
Одним из главных источников вдохновения и мотивации для ПМ была более ранняя работа Готлоба Фреге по логике, которая, как обнаружил Рассел, позволяла строить парадоксальные множества . Премьер-министр стремился избежать этой проблемы, исключив неограниченное создание произвольных наборов. Это было достигнуто путем замены понятия общего множества понятием иерархии множеств разных « типов », при этом множество определенного типа могло содержать только множества строго более низких типов. Современная математика, однако, избегает парадоксов, подобных парадоксам Рассела, менее громоздкими способами, такими как система теории множеств Цермело-Френкеля .
Теоремы Гёделя о неполноте — это две теоремы математической логики , которые устанавливают внутренние ограничения всех аксиоматических систем, кроме самых тривиальных , способных выполнять арифметические действия . Теоремы, доказанные Куртом Гёделем в 1931 году, важны как в математической логике, так и в философии математики . Эти два результата широко, но не универсально, интерпретируются как показывающие, что программа Гильберта по поиску полного и непротиворечивого набора аксиом для всей математики невозможна, что дает отрицательный ответ на вторую проблему Гильберта .
Первая теорема о неполноте утверждает, что никакая непротиворечивая система аксиом, теоремы которой можно перечислить с помощью « эффективной процедуры » (например, компьютерной программы, но это может быть любой алгоритм), не способна доказать все истины об отношениях естественных явлений . числа ( арифметика ). Для любой такой системы всегда будут утверждения о натуральных числах, которые верны, но недоказуемы внутри системы. Вторая теорема о неполноте, являющаяся расширением первой, показывает, что такая система не может продемонстрировать свою непротиворечивость.
Т-схема или схема истинности (не путать с « Конвенцией Т ») используется для индуктивного определения истины, которая лежит в основе любой реализации семантической теории истины Альфреда Тарского . Некоторые авторы называют ее «схемой эквивалентности» — синонимом, введенным Майклом Дамметом . [4]
Т-схема часто выражается на естественном языке , но ее можно формализовать в многосортной логике предикатов или модальной логике ; такая формализация называется Т-теорией . Т-теории составляют основу многих фундаментальных работ по философской логике , где они применяются в нескольких важных спорах аналитической философии .
Как выражается на полуестественном языке (где «S» — это название предложения, сокращенно S): «S» истинно тогда и только тогда, когда S
Пример: выражение «снег белый» истинно тогда и только тогда, когда снег белый.
Entscheidungsproblem ( по - немецки « проблема решения » ) — это задача , поставленная Дэвидом Гильбертом в 1928 году . обычные аксиомы логики первого порядка) и отвечает «Да» или «Нет» в зависимости от того, является ли утверждение универсально действительным , т. е. действительным в каждой структуре, удовлетворяющей аксиомам. Согласно теореме о полноте логики первого порядка , утверждение является универсально действительным тогда и только тогда, когда оно может быть выведено из аксиом, поэтому проблему Entscheidungsproblem можно также рассматривать как требование алгоритма решить, доказуемо ли данное утверждение на основе аксиом. используя правила логики.
В 1936 году Алонзо Чёрч и Алан Тьюринг опубликовали независимые статьи [6], показывающие , что общее решение проблемы Entscheidungs те, которые выражаются в лямбда-исчислении ). Это предположение теперь известно как тезис Чёрча-Тьюринга .
