Математическая логика — это изучение формальной логики в математике . Основные подразделы включают теорию моделей , теорию доказательств , теорию множеств и теорию рекурсии (также известную как теория вычислимости). Исследования в области математической логики обычно касаются математических свойств формальных систем логики, таких как их выразительная или дедуктивная сила. Однако она также может включать использование логики для характеристики правильных математических рассуждений или для установления основ математики .
С момента своего возникновения математическая логика вносила вклад и была мотивирована изучением оснований математики. Это исследование началось в конце 19 века с разработки аксиоматических рамок для геометрии , арифметики и анализа . В начале 20 века оно было сформировано программой Дэвида Гильберта по доказательству непротиворечивости фундаментальных теорий. Результаты Курта Гёделя , Герхарда Генцена и других обеспечили частичное разрешение программы и прояснили вопросы, связанные с доказательством непротиворечивости. Работа по теории множеств показала, что почти вся обычная математика может быть формализована в терминах множеств, хотя есть некоторые теоремы, которые не могут быть доказаны в общих системах аксиом для теории множеств. Современная работа по основаниям математики часто фокусируется на установлении того, какие части математики могут быть формализованы в конкретных формальных системах (как в обратной математике ), а не на попытках найти теории, в которых может быть развита вся математика.
В « Справочнике по математической логике» [1] 1977 года современная математическая логика грубо делится на четыре области:
Кроме того, иногда область теории вычислительной сложности также включается в состав математической логики. [2] Каждая область имеет отдельную направленность, хотя многие методы и результаты являются общими для нескольких областей. Границы между этими областями и линии, разделяющие математическую логику и другие области математики, не всегда резкие. Теорема Гёделя о неполноте знаменует собой не только веху в теории рекурсии и теории доказательств, но также привела к теореме Лёба в модальной логике. Метод принуждения применяется в теории множеств, теории моделей и теории рекурсии, а также в изучении интуиционистской математики.
Математическая область теории категорий использует множество формальных аксиоматических методов и включает в себя изучение категориальной логики , но теория категорий обычно не считается подобластью математической логики. Из-за ее применимости в различных областях математики, математики, включая Сондерса Маклейна, предложили теорию категорий в качестве основополагающей системы для математики, независимой от теории множеств. Эти основы используют топосы , которые напоминают обобщенные модели теории множеств, которые могут использовать классическую или неклассическую логику.
Математическая логика возникла в середине 19-го века как подраздел математики, отражающий слияние двух традиций: формальной философской логики и математики. [3] Математическая логика, также называемая «логистической», «символической логикой», « алгеброй логики » и, в последнее время, просто «формальной логикой», представляет собой набор логических теорий, разработанных в течение девятнадцатого века с помощью искусственной нотации и строго дедуктивного метода. [4] До этого появления логика изучалась с помощью риторики , с помощью вычислений , [5] через силлогизм и с помощью философии . Первая половина 20-го века ознаменовалась взрывом фундаментальных результатов, сопровождавшимся бурными дебатами по поводу основ математики.
Теории логики разрабатывались во многих культурах в истории, включая Китай , Индию , Грецию и исламский мир . Греческие методы, в частности, аристотелевская логика (или терминологическая логика), изложенная в « Органоне» , на протяжении тысячелетий находили широкое применение и признание в западной науке и математике. [6] Стоики , особенно Хрисипп , начали разработку предикатной логики . В Европе XVIII века попытки трактовать операции формальной логики символическим или алгебраическим способом предпринимались философскими математиками, включая Лейбница и Ламберта , но их труды оставались изолированными и малоизвестными.
В середине девятнадцатого века Джордж Буль , а затем Август Де Морган представили систематические математические трактовки логики. Их работа, основанная на работах таких алгебраистов, как Джордж Пикок , расширила традиционную аристотелевскую доктрину логики до достаточной основы для изучения оснований математики . [7] В 1847 году Ватрослав Бертич проделал значительную работу по алгебраизации логики независимо от Буля. [8] Чарльз Сандерс Пирс позже развил работу Буля, чтобы разработать логическую систему для отношений и квантификаторов, которую он опубликовал в нескольких статьях с 1870 по 1885 год.
Готтлоб Фреге представил независимое развитие логики с кванторами в своем Begriffsschrift , опубликованном в 1879 году, работе, которая обычно рассматривается как поворотный момент в истории логики. Однако работа Фреге оставалась малоизвестной, пока Бертран Рассел не начал продвигать ее на рубеже веков. Двумерная нотация, разработанная Фреге, никогда не была широко принята и не используется в современных текстах.
С 1890 по 1905 год Эрнст Шрёдер опубликовал «Vorlesungen über die Algebra der Logik» в трех томах. Эта работа обобщила и расширила работы Буля, де Моргана и Пирса и стала всеобъемлющим справочником по символической логике, как ее понимали в конце XIX века.
Опасения по поводу того, что математика не построена на надлежащем фундаменте, привели к разработке аксиоматических систем для фундаментальных областей математики, таких как арифметика, анализ и геометрия.
В логике термин арифметика относится к теории натуральных чисел . Джузеппе Пеано [9] опубликовал набор аксиом для арифметики, которые стали носить его имя ( аксиомы Пеано ), используя вариацию логической системы Буля и Шредера, но добавив кванторы. Пеано в то время не знал о работе Фреге. Примерно в то же время Ричард Дедекинд показал, что натуральные числа однозначно характеризуются своими индукционными свойствами. Дедекинд предложил другую характеристику, в которой отсутствовал формальный логический характер аксиом Пеано. [10] Работа Дедекинда, однако, доказала теоремы, недоступные в системе Пеано, включая уникальность множества натуральных чисел (с точностью до изоморфизма) и рекурсивные определения сложения и умножения из функции следования и математической индукции.
В середине 19 века стали известны недостатки аксиом Евклида для геометрии. [11] В дополнение к независимости постулата о параллельных линиях , установленного Николаем Лобачевским в 1826 году, [12] математики обнаружили, что некоторые теоремы, считавшиеся само собой разумеющимися Евклидом, на самом деле не доказуемы из его аксиом. Среди них — теорема о том, что прямая содержит по крайней мере две точки, или что окружности одинакового радиуса, центры которых разделены этим радиусом, должны пересекаться. Гильберт [13] разработал полный набор аксиом для геометрии , основываясь на предыдущих работах Паша. [14] Успех в аксиоматизации геометрии побудил Гильберта искать полные аксиоматизации других областей математики, таких как натуральные числа и действительная прямая . Это оказалось основной областью исследований в первой половине 20 века.
В 19 веке теория действительного анализа достигла больших успехов , включая теории сходимости функций и рядов Фурье . Такие математики, как Карл Вейерштрасс, начали строить функции, которые расширяли интуицию, такие как нигде не дифференцируемые непрерывные функции . Предыдущие концепции функции как правила для вычисления или гладкого графика больше не были адекватными. Вейерштрасс начал отстаивать арифметизацию анализа , которая стремилась аксиоматизировать анализ, используя свойства натуральных чисел. Современное (ε, δ)-определение предельных и непрерывных функций было уже разработано Больцано в 1817 году [15] , но оставалось относительно неизвестным. Коши в 1821 году определил непрерывность в терминах бесконечно малых (см. Cours d'Analyse, стр. 34). В 1858 году Дедекинд предложил определение действительных чисел в терминах дедекиндовых сечений рациональных чисел, определение, которое все еще используется в современных текстах. [16]
Георг Кантор разработал основные концепции теории бесконечных множеств. Его ранние результаты развили теорию мощности и доказали , что действительные и натуральные числа имеют разные мощности. [17] В течение следующих двадцати лет Кантор разработал теорию трансфинитных чисел в серии публикаций. В 1891 году он опубликовал новое доказательство несчетности действительных чисел, которое ввело диагональный аргумент , и использовал этот метод для доказательства теоремы Кантора о том, что ни одно множество не может иметь ту же мощность, что и его супермножество . Кантор считал, что каждое множество может быть вполне упорядоченным , но не смог предоставить доказательство этого результата, оставив его открытой проблемой в 1895 году. [18]
В первые десятилетия 20-го века основными областями исследований были теория множеств и формальная логика. Открытие парадоксов в неформальной теории множеств заставило некоторых задуматься о том, является ли сама математика непоследовательной, и искать доказательства последовательности.
В 1900 году Гильберт сформулировал знаменитый список из 23 проблем для следующего столетия. Первые две из них должны были разрешить континуум-гипотезу и доказать непротиворечивость элементарной арифметики соответственно; десятая заключалась в создании метода, который мог бы определить, имеет ли многомерное полиномиальное уравнение над целыми числами решение. Последующая работа по решению этих проблем сформировала направление математической логики, как и попытка решить Entscheidungsproblem Гильберта , поставленную в 1928 году. Эта проблема требовала процедуры, которая бы решала, учитывая формализованное математическое утверждение, является ли утверждение истинным или ложным.
Эрнст Цермело дал доказательство того, что каждое множество может быть вполне упорядочено , результат, который Георг Кантор не смог получить. [19] Чтобы получить доказательство, Цермело ввел аксиому выбора , которая вызвала жаркие споры и исследования среди математиков и пионеров теории множеств. Немедленная критика метода заставила Цермело опубликовать второе изложение своего результата, напрямую отвечая на критику его доказательства. [20] Эта статья привела к общему принятию аксиомы выбора в математическом сообществе.
Скептицизм относительно аксиомы выбора был усилен недавно обнаруженными парадоксами в наивной теории множеств . Чезаре Бурали-Форти [21] был первым, кто сформулировал парадокс: парадокс Бурали-Форти показывает, что совокупность всех порядковых чисел не может образовывать множество. Вскоре после этого Бертран Рассел открыл парадокс Рассела в 1901 году, а Жюль Ришар открыл парадокс Ришара . [22]
Цермело предоставил первый набор аксиом для теории множеств. [23] Эти аксиомы, вместе с дополнительной аксиомой замены, предложенной Абрахамом Френкелем , теперь называются теорией множеств Цермело–Френкеля (ZF). Аксиомы Цермело включали принцип ограничения размера , чтобы избежать парадокса Рассела.
В 1910 году был опубликован первый том Principia Mathematica Рассела и Альфреда Норта Уайтхеда . Эта основополагающая работа развивала теорию функций и мощности в полностью формальной структуре теории типов , которую Рассел и Уайтхед разработали в попытке избежать парадоксов. Principia Mathematica считается одной из самых влиятельных работ 20-го века, хотя структура теории типов не оказалась популярной в качестве основополагающей теории для математики. [24]
Френкель [25] доказал, что аксиома выбора не может быть доказана из аксиом теории множеств Цермело с урэлементами . Более поздняя работа Пола Коэна [26] показала, что добавление урэлементов не требуется, и аксиома выбора недоказуема в ZF. Доказательство Коэна разработало метод принуждения , который теперь является важным инструментом для установления независимости результатов в теории множеств. [27]
Леопольд Лёвенгейм [28] и Торальф Скулем [29] получили теорему Лёвенгейма–Скулема , которая гласит, что логика первого порядка не может контролировать мощности бесконечных структур. Скулем понял, что эта теорема применима к формализациям первого порядка теории множеств, и что она подразумевает, что любая такая формализация имеет счетную модель . Этот контринтуитивный факт стал известен как парадокс Скулема .
В своей докторской диссертации Курт Гёдель доказал теорему о полноте , которая устанавливает соответствие между синтаксисом и семантикой в логике первого порядка. [30] Гёдель использовал теорему о полноте для доказательства теоремы о компактности , демонстрируя финитную природу логического следования первого порядка . Эти результаты помогли установить логику первого порядка как доминирующую логику, используемую математиками.
В 1931 году Гёдель опубликовал работу «О формально неразрешимых предложениях Principia Mathematica и связанных с ними систем» , в которой была доказана неполнота (в другом значении этого слова) всех достаточно сильных эффективных теорий первого порядка. Этот результат, известный как теорема Гёделя о неполноте , устанавливает серьезные ограничения на аксиоматические основы математики, нанося сильный удар по программе Гильберта. Она показала невозможность предоставить доказательство непротиворечивости арифметики в рамках какой-либо формальной теории арифметики. Однако Гильберт некоторое время не признавал важность теоремы о неполноте. [a]
Теорема Гёделя показывает, что доказательство непротиворечивости любой достаточно сильной, эффективной системы аксиом не может быть получено в самой системе, если система непротиворечива, или в любой более слабой системе. Это оставляет открытой возможность доказательств непротиворечивости, которые не могут быть формализованы в рассматриваемой ими системе. Генцен доказал непротиворечивость арифметики, используя финитную систему вместе с принципом трансфинитной индукции . [31] Результат Генцена ввел идеи устранения сечения и ординалов теории доказательств , которые стали ключевыми инструментами в теории доказательств. Гёдель дал другое доказательство непротиворечивости, которое сводит непротиворечивость классической арифметики к непротиворечивости интуиционистской арифметики в высших типах. [32]
Первый учебник по символической логике для неспециалистов был написан Льюисом Кэрроллом , [33] автором « Приключений Алисы в Стране чудес» , в 1896 году. [34]
Альфред Тарский разработал основы теории моделей .
Начиная с 1935 года группа выдающихся математиков объединилась под псевдонимом Николя Бурбаки , чтобы опубликовать Éléments de mathématique , серию энциклопедических математических текстов. Эти тексты, написанные в строгом и аксиоматическом стиле, подчеркивали строгое изложение и теоретико-множественные основы. Терминология, придуманная этими текстами, такая как слова биекция , инъекция и сюръекция , а также теоретико-множественные основы, используемые в текстах, были широко приняты в математике.
Изучение вычислимости стало известно как теория рекурсии или теория вычислимости , потому что ранние формализации Гёделя и Клини опирались на рекурсивные определения функций. [b] Когда было показано, что эти определения эквивалентны формализации Тьюринга, включающей машины Тьюринга , стало ясно, что было открыто новое понятие — вычислимая функция — и что это определение достаточно надежно, чтобы допускать многочисленные независимые характеризации. В своей работе над теоремами о неполноте в 1931 году Гёделю не хватало строгой концепции эффективной формальной системы; он сразу понял, что новые определения вычислимости могут быть использованы для этой цели, что позволило ему сформулировать теоремы о неполноте в общности, которая могла подразумеваться только в исходной статье.
Многочисленные результаты в теории рекурсии были получены в 1940-х годах Стивеном Коулом Клини и Эмилем Леоном Постом . Клини [35] ввел понятия относительной вычислимости, предвосхищенные Тьюрингом [36], и арифметической иерархии . Позднее Клини обобщил теорию рекурсии на функционалы более высокого порядка. Клини и Георг Крайзель изучали формальные версии интуиционистской математики, особенно в контексте теории доказательств.
По своей сути математическая логика имеет дело с математическими концепциями, выраженными с использованием формальных логических систем . Эти системы, хотя и различаются во многих деталях, имеют общее свойство рассматривать только выражения на фиксированном формальном языке . Системы пропозициональной логики и логики первого порядка являются наиболее широко изучаемыми сегодня из-за их применимости к основаниям математики и из-за их желаемых свойств теории доказательств. [c] Более сильные классические логики, такие как логика второго порядка или бесконечная логика , также изучаются наряду с неклассическими логиками, такими как интуиционистская логика .
Логика первого порядка — это особая формальная система логики . Ее синтаксис включает только конечные выражения в виде правильно сформированных формул , тогда как ее семантика характеризуется ограничением всех квантификаторов фиксированной областью дискурса .
Ранние результаты формальной логики установили ограничения логики первого порядка. Теорема Лёвенгейма–Сколема (1919) показала, что если набор предложений в счетном языке первого порядка имеет бесконечную модель, то он имеет по крайней мере одну модель каждой бесконечной мощности. Это показывает, что набор аксиом первого порядка не может характеризовать натуральные числа, действительные числа или любую другую бесконечную структуру с точностью до изоморфизма . Поскольку целью ранних фундаментальных исследований было создание аксиоматических теорий для всех частей математики, это ограничение было особенно резким.
Теорема о полноте Гёделя установила эквивалентность между семантическими и синтаксическими определениями логического следствия в логике первого порядка. [30] Она показывает, что если конкретное предложение истинно в каждой модели, которая удовлетворяет конкретному набору аксиом, то должно быть конечное выведение предложения из аксиом. Теорема о компактности впервые появилась как лемма в доказательстве теоремы о полноте Гёделя, и потребовалось много лет, прежде чем логики поняли ее значение и начали применять ее повседневно. Она гласит, что набор предложений имеет модель тогда и только тогда, когда каждое конечное подмножество имеет модель, или, другими словами, что несовместимый набор формул должен иметь конечное несовместимое подмножество. Теоремы о полноте и компактности позволяют проводить сложный анализ логического следствия в логике первого порядка и развивать теорию моделей , и они являются ключевой причиной известности логики первого порядка в математике.
Теоремы Гёделя о неполноте устанавливают дополнительные ограничения на аксиоматизации первого порядка. [37] Первая теорема о неполноте утверждает, что для любой непротиворечивой, эффективно заданной (определенной ниже) логической системы, способной интерпретировать арифметику, существует утверждение, которое является истинным (в том смысле, что оно справедливо для натуральных чисел), но не доказуемо в пределах этой логической системы (и которое действительно может не срабатывать в некоторых нестандартных моделях арифметики , которые могут быть совместимы с логической системой). Например, в каждой логической системе, способной выразить аксиомы Пеано , предложение Гёделя справедливо для натуральных чисел, но не может быть доказано.
Здесь говорят, что логическая система эффективно задана, если возможно решить, если задана любая формула на языке системы, является ли эта формула аксиомой, а та, которая может выразить аксиомы Пеано, называется «достаточно сильной». Применительно к логике первого порядка первая теорема о неполноте подразумевает, что любая достаточно сильная, непротиворечивая, эффективная теория первого порядка имеет модели, которые элементарно не эквивалентны , что является более сильным ограничением, чем то, которое установлено теоремой Лёвенгейма–Сколема. Вторая теорема о неполноте утверждает, что никакая достаточно сильная, непротиворечивая, эффективная система аксиом для арифметики не может доказать свою собственную непротиворечивость, что было интерпретировано как доказательство того, что программа Гильберта не может быть достигнута.
Изучаются многие логики, помимо логики первого порядка. К ним относятся бесконечные логики , которые позволяют формулам предоставлять бесконечное количество информации, и логики более высокого порядка , которые включают часть теории множеств непосредственно в свою семантику.
Наиболее изученной бесконечной логикой является . В этой логике квантификаторы могут быть вложены только на конечную глубину, как в логике первого порядка, но формулы могут иметь конечные или счетно бесконечные конъюнкции и дизъюнкции внутри них. Так, например, можно сказать, что объект является целым числом, используя формулу типа
Логики более высокого порядка позволяют квантифицировать не только элементы области дискурса , но и подмножества области дискурса, множества таких подмножеств и другие объекты более высокого типа. Семантика определяется таким образом, что вместо того, чтобы иметь отдельную область для каждого квантификатора более высокого типа, чтобы пробегаться по ней, квантификаторы вместо этого пробегаются по всем объектам соответствующего типа. Логики, изученные до развития логики первого порядка, например логика Фреге, имели схожие аспекты теории множеств. Хотя логики более высокого порядка более выразительны, допуская полную аксиоматизацию структур, таких как натуральные числа, они не удовлетворяют аналогам теорем о полноте и компактности из логики первого порядка и, таким образом, менее поддаются анализу теории доказательств.
Другой тип логики – этоЛогика с фиксированной точкой , допускающаяиндуктивные определения, подобные тем, которые записываются дляпримитивных рекурсивных функций.
Можно формально определить расширение логики первого порядка — понятие, которое охватывает все логики в этом разделе, поскольку они ведут себя как логика первого порядка в некоторых фундаментальных отношениях, но не охватывает все логики в целом, например, оно не охватывает интуиционистскую, модальную или нечеткую логику .
Теорема Линдстрёма подразумевает, что единственным расширением логики первого порядка, удовлетворяющим как теореме компактности , так и нисходящей теореме Лёвенгейма–Скулема, является логика первого порядка.
Модальные логики включают дополнительные модальные операторы, такие как оператор, который утверждает, что конкретная формула не только истинна, но и обязательно истинна. Хотя модальная логика нечасто используется для аксиоматизации математики, она использовалась для изучения свойств доказуемости первого порядка [38] и теоретико-множественного принуждения. [39]
Интуиционистская логика была разработана Гейтингом для изучения программы интуиционизма Брауэра, в которой сам Брауэр избегал формализации. Интуиционистская логика в частности не включает закон исключенного третьего , который гласит, что каждое предложение либо истинно, либо его отрицание истинно. Работа Клини с теорией доказательств интуиционистской логики показала, что конструктивная информация может быть восстановлена из интуиционистских доказательств. Например, любая доказуемо полная функция в интуиционистской арифметике вычислима ; это неверно в классических теориях арифметики, таких как арифметика Пеано .
Алгебраическая логика использует методы абстрактной алгебры для изучения семантики формальных логик. Фундаментальным примером является использование булевых алгебр для представления значений истинности в классической пропозициональной логике и использование алгебр Гейтинга для представления значений истинности в интуиционистской пропозициональной логике. Более сильные логики, такие как логика первого порядка и логика высшего порядка, изучаются с использованием более сложных алгебраических структур, таких как цилиндрические алгебры .
Теория множеств — это изучение множеств , которые являются абстрактными коллекциями объектов. Многие из основных понятий, таких как порядковые и кардинальные числа, были неформально разработаны Кантором до того, как были разработаны формальные аксиоматизации теории множеств. Первая такая аксиоматизация , принадлежащая Цермело, [23] была немного расширена и стала теорией множеств Цермело–Френкеля (ZF), которая в настоящее время является наиболее широко используемой фундаментальной теорией для математики.
Были предложены и другие формализации теории множеств, включая теорию множеств фон Неймана–Бернейса–Гёделя (NBG), теорию множеств Морса–Келли (MK) и Новые основания (NF). Из них ZF, NBG и MK схожи в описании кумулятивной иерархии множеств. Новые основания используют другой подход; они допускают такие объекты, как множество всех множеств, за счет ограничений на аксиомы существования множества. Система теории множеств Крипке–Платека тесно связана с обобщенной теорией рекурсии.
Два известных утверждения в теории множеств — аксиома выбора и гипотеза континуума . Аксиома выбора, впервые сформулированная Цермело [19], была доказана независимо от ZF Френкелем [25] , но стала широко принятой математиками. Она гласит, что для данного набора непустых множеств существует единственное множество C , которое содержит ровно один элемент из каждого набора в наборе. Говорят, что множество C «выбирает» один элемент из каждого набора в наборе. Хотя возможность сделать такой выбор некоторые считают очевидной, поскольку каждое множество в наборе непусто, отсутствие общего, конкретного правила, по которому можно сделать выбор, делает аксиому неконструктивной. Стефан Банах и Альфред Тарский показали, что аксиому выбора можно использовать для разложения сплошного шара на конечное число частей, которые затем можно переставить без масштабирования, чтобы сделать два сплошных шара исходного размера. [40] Эта теорема, известная как парадокс Банаха-Тарского , является одним из многих контринтуитивных результатов аксиомы выбора.
Гипотеза континуума, впервые предложенная как гипотеза Кантором, была указана Дэвидом Гильбертом как одна из его 23 проблем в 1900 году. Гёдель показал, что гипотеза континуума не может быть опровергнута из аксиом теории множеств Цермело–Френкеля (с аксиомой выбора или без нее), разработав конструируемый универсум теории множеств, в котором гипотеза континуума должна быть верна. В 1963 году Пол Коэн показал, что гипотеза континуума не может быть доказана из аксиом теории множеств Цермело–Френкеля. [26] Однако этот результат независимости не полностью разрешил вопрос Гильберта, поскольку возможно, что новые аксиомы для теории множеств могли бы разрешить гипотезу. Недавняя работа в этом направлении была проведена У. Хью Вудином , хотя ее важность пока не ясна. [41]
Современные исследования в теории множеств включают изучение больших кардиналов и определенности . Большие кардиналы — это кардинальные числа с особыми свойствами, настолько сильными, что существование таких кардиналов не может быть доказано в ZFC. Существование наименьшего большого кардинала, обычно изучаемого, недостижимого кардинала , уже подразумевает согласованность ZFC. Несмотря на то, что большие кардиналы имеют чрезвычайно высокую мощность , их существование имеет много последствий для структуры действительной линии. Определенность относится к возможному существованию выигрышных стратегий для определенных игр двух игроков (игры считаются определенными ). Существование этих стратегий подразумевает структурные свойства действительной линии и других польских пространств .
Теория моделей изучает модели различных формальных теорий. Здесь теория — это набор формул в определенной формальной логике и сигнатуре , тогда как модель — это структура, которая дает конкретную интерпретацию теории. Теория моделей тесно связана с универсальной алгеброй и алгебраической геометрией , хотя методы теории моделей больше сосредоточены на логических соображениях, чем на этих областях.
Совокупность всех моделей конкретной теории называется элементарным классом ; классическая теория моделей стремится определить свойства моделей в конкретном элементарном классе или определить, образуют ли определенные классы структур элементарные классы.
Метод исключения кванторов может быть использован для того, чтобы показать, что определимые множества в конкретных теориях не могут быть слишком сложными. Тарский установил исключение кванторов для вещественно-замкнутых полей , результат, который также показывает, что теория поля вещественных чисел разрешима . [42] Он также отметил, что его методы в равной степени применимы к алгебраически замкнутым полям произвольной характеристики. Современная подобласть, развивающаяся из этого, занимается o-минимальными структурами .
Теорема Морли о категоричности , доказанная Майклом Д. Морли [43], утверждает , что если теория первого порядка в счетном языке категорична в некоторой несчетной мощности, т. е. все модели этой мощности изоморфны, то она категорична во всех несчетных мощностях.
Тривиальным следствием гипотезы континуума является то, что полная теория с меньшим, чем континуум, числом неизоморфных счетных моделей может иметь только счетное число. Гипотеза Воота , названная в честь Роберта Лоусона Воота , утверждает, что это верно даже независимо от гипотезы континуума. Было установлено много частных случаев этой гипотезы.
Теория рекурсии , также называемая теорией вычислимости , изучает свойства вычислимых функций и степеней Тьюринга , которые делят невычислимые функции на множества, имеющие одинаковый уровень невычислимости. Теория рекурсии также включает изучение обобщенной вычислимости и определимости. Теория рекурсии выросла из работы Рожи Петера , Алонзо Чёрча и Алана Тьюринга в 1930-х годах, которая была значительно расширена Клини и Постом в 1940-х годах. [44]
Классическая теория рекурсии фокусируется на вычислимости функций от натуральных чисел до натуральных чисел. Фундаментальные результаты устанавливают надежный канонический класс вычислимых функций с многочисленными независимыми эквивалентными характеризациями с использованием машин Тьюринга , λ-исчисления и других систем. Более продвинутые результаты касаются структуры степеней Тьюринга и решетки рекурсивно перечислимых множеств .
Обобщенная теория рекурсии расширяет идеи теории рекурсии на вычисления, которые больше не обязательно являются конечными. Она включает в себя изучение вычислимости в высших типах, а также такие области, как гиперарифметическая теория и теория α-рекурсии .
Современные исследования в области теории рекурсии включают изучение таких приложений, как алгоритмическая случайность , теория вычислимых моделей и обратная математика , а также новых результатов в чистой теории рекурсии.
Важная подобласть теории рекурсии изучает алгоритмическую неразрешимость; проблема принятия решений или проблема функций алгоритмически неразрешима , если не существует возможного вычислимого алгоритма, который возвращает правильный ответ для всех допустимых входных данных задачи. Первые результаты о неразрешимости, полученные независимо Чёрчем и Тьюрингом в 1936 году, показали, что Entscheidungsproblem алгоритмически неразрешима. Тьюринг доказал это, установив неразрешимость проблемы остановки , что имело далеко идущие последствия как для теории рекурсии, так и для компьютерной науки.
Существует множество известных примеров неразрешимых проблем из обычной математики. Алгоритмическая неразрешимость проблемы поиска слов для групп была доказана Петром Новиковым в 1955 году и независимо У. Буном в 1959 году. Задача о занятом бобре , разработанная Тибором Радо в 1962 году, является еще одним известным примером.
Десятая проблема Гильберта требовала алгоритма для определения того, имеет ли многомерное полиномиальное уравнение с целыми коэффициентами решение в целых числах. Частичный прогресс был достигнут Джулией Робинсон , Мартином Дэвисом и Хилари Патнэмом . Алгоритмическая неразрешимость проблемы была доказана Юрием Матиясевичем в 1970 году. [45]
Теория доказательств — это изучение формальных доказательств в различных системах логического вывода. Эти доказательства представляются как формальные математические объекты, что облегчает их анализ математическими методами. Обычно рассматриваются несколько систем вывода, включая системы вывода в стиле Гильберта , системы естественного вывода и секвенциальное исчисление , разработанное Генценом.
Изучение конструктивной математики в контексте математической логики включает изучение систем в неклассической логике, таких как интуиционистская логика, а также изучение предикативных систем. Ранним сторонником предикативизма был Герман Вейль , который показал, что можно развить большую часть реального анализа, используя только предикативные методы. [46]
Поскольку доказательства полностью конечны, тогда как истина в структуре не является таковой, в конструктивной математике принято подчеркивать доказуемость. Связь между доказуемостью в классических (или неконструктивных) системах и доказуемостью в интуиционистских (или конструктивных, соответственно) системах представляет особый интерес. Такие результаты, как отрицательный перевод Гёделя–Гентцена, показывают, что можно встроить (или перевести ) классическую логику в интуиционистскую логику, что позволяет перенести некоторые свойства интуиционистских доказательств обратно в классические доказательства.
Последние разработки в теории доказательств включают исследование добычи доказательств Ульрихом Коленбахом и исследование ординалов теории доказательств Михаэлем Ратьеном.
«Математическая логика успешно применялась не только к математике и ее основаниям ( Г. Фреге , Б. Рассел , Д. Гильберт , П. Бернайс , Г. Шольц , Р. Карнап , С. Лесневский , Т. Скулем ), но и к физике (Р. Карнап, А. Диттрих, Б. Рассел, К. Э. Шеннон , А. Н. Уайтхед , Г. Рейхенбах , П. Феврие), к биологии ( Дж. Х. Вуджер , А. Тарский ), к психологии ( Ф. Б. Фитч , К. Г. Гемпель ), к праву и морали ( К. Менгер , У. Клуг, П. Оппенгейм), к экономике ( Дж. Нойман , О. Моргенштерн ), к практическим вопросам ( Э. К. Беркли , Э. Штамм) и даже к метафизике (Дж. [Ян] Саламуха, Г. Шольц, Дж. М. Бохенский ). Его применение в истории логики оказалось чрезвычайно плодотворным ( J. Lukasiewicz , H. Scholz, B. Mates , A. Becker, E. Moody , J. Salamucha, K. Duerr, Z. Jordan, P. Boehner , JM Bochenski, S. [Stanislaw] T. Schayer, D. Ingalls )». [47] «Применения также были сделаны в теологии (F. Drewnowski, J. Salamucha, I. Thomas)». [47]
Изучение теории вычислимости в информатике тесно связано с изучением вычислимости в математической логике. Однако есть разница в акцентах. Специалисты по информатике часто фокусируются на конкретных языках программирования и возможной вычислимости , в то время как исследователи в математической логике часто фокусируются на вычислимости как теоретической концепции и на невычислимости.
Теория семантики языков программирования связана с теорией моделей , как и верификация программ (в частности, проверка моделей ). Соответствие Карри–Ховарда между доказательствами и программами связано с теорией доказательств , особенно с интуиционистской логикой . Формальные исчисления, такие как лямбда-исчисление и комбинаторная логика, в настоящее время изучаются как идеализированные языки программирования .
Информатика также вносит вклад в математику, разрабатывая методы автоматической проверки или даже поиска доказательств, такие как автоматизированное доказательство теорем и логическое программирование .
Теория описательной сложности связывает логику с вычислительной сложностью . Первый значительный результат в этой области, теорема Фейгина (1974), установила, что NP — это в точности множество языков, выражаемых предложениями экзистенциальной логики второго порядка .
В 19 веке математики осознали логические пробелы и несоответствия в своей области. Было показано, что аксиомы Евклида для геометрии, которые преподавались на протяжении столетий как пример аксиоматического метода, были неполными. Использование бесконечно малых величин и само определение функции стали предметом вопросов в анализе, поскольку были обнаружены патологические примеры, такие как нигде не дифференцируемая непрерывная функция Вейерштрасса.
Изучение Кантором произвольных бесконечных множеств также вызвало критику. Леопольд Кронекер заявил: «Бог создал целые числа; все остальное — дело рук человека», одобрив возвращение к изучению конечных, конкретных объектов в математике. Хотя аргумент Кронекера был продолжен конструктивистами в 20 веке, математическое сообщество в целом отвергло их. Дэвид Гильберт выступал в пользу изучения бесконечности, говоря: «Никто не изгонит нас из Рая, который создал Кантор».
Математики начали искать системы аксиом, которые можно было бы использовать для формализации больших частей математики. Помимо устранения неоднозначности из ранее наивных терминов, таких как функция, надеялись, что эта аксиоматизация позволит проводить доказательства непротиворечивости. В 19 веке основным методом доказательства непротиворечивости набора аксиом было предоставление для него модели. Так, например, непротиворечивость неевклидовой геометрии можно доказать, определив точку как точку на фиксированной сфере, а линию как большую окружность на сфере. Полученная структура, модель эллиптической геометрии , удовлетворяет аксиомам планиметрии, за исключением постулата о параллельности.
С развитием формальной логики Гильберт задался вопросом, возможно ли доказать, что система аксиом непротиворечива, проанализировав структуру возможных доказательств в системе и показав с помощью этого анализа, что невозможно доказать противоречие. Эта идея привела к изучению теории доказательств . Более того, Гильберт предложил, чтобы анализ был полностью конкретным, используя термин финитный для обозначения методов, которые он допускал, но не точно их определяя. Этот проект, известный как программа Гильберта , был серьезно затронут теоремами Гёделя о неполноте, которые показывают, что непротиворечивость формальных теорий арифметики не может быть установлена с помощью методов, формализуемых в этих теориях. Генцен показал, что можно создать доказательство непротиворечивости арифметики в финитной системе, дополненной аксиомами трансфинитной индукции , и методы, которые он разработал для этого, были основополагающими в теории доказательств.
Вторая тема в истории оснований математики включает неклассическую логику и конструктивную математику . Изучение конструктивной математики включает в себя множество различных программ с различными определениями конструктивного . В наиболее удобном конце доказательства в теории множеств ZF, которые не используют аксиому выбора, называются многими математиками конструктивными. Более ограниченные версии конструктивизма ограничиваются натуральными числами , функциями теории чисел и множествами натуральных чисел (которые могут использоваться для представления действительных чисел, облегчая изучение математического анализа ). Распространенная идея заключается в том, что конкретные средства вычисления значений функции должны быть известны, прежде чем можно будет сказать, что сама функция существует.
В начале 20 века Лютцен Эгбертус Ян Брауэр основал интуиционизм как часть философии математики . Эта философия, поначалу плохо понимаемая, утверждала, что для того, чтобы математическое утверждение было истинным для математика, этот человек должен быть способен интуитивно постичь это утверждение, не только поверить в его истинность, но и понять причину его истинности. Следствием этого определения истины стало отвержение закона исключенного третьего , поскольку существуют утверждения, которые, по мнению Брауэра, нельзя назвать истинными, в то время как их отрицания также нельзя назвать истинными. Философия Брауэра была влиятельной и причиной ожесточенных споров среди выдающихся математиков. Клини и Крайзель позже изучают формализованные версии интуиционистской логики (Брауэр отверг формализацию и представил свою работу на неформализованном естественном языке). С появлением интерпретации BHK и моделей Крипке интуиционизм стало легче согласовывать с классической математикой.
Перевод:«Die Ausführung dieses Vorhabens Hat eine Wesentliche Verzögerung Dadurch erfahren, daß in Einem Stadium, in dem die Darstellung Schon ihrem Abschuß nahe War, durch das Erscheinen der Arbeiten von Herbrand und von Gödel eine veränderte Situation im Gebiet der Beweistheorie entstand , welche die Berücksichtigung neuer Einsichten zur Aufgabe machte.
Поэтому Гильберт, несомненно, осознавал важность работы Гёделя к 1934 году. Второй том, опубликованный в 1939 году, включал в себя форму доказательства непротиворечивости Генцена для арифметики.«Осуществление этого плана [Гильберта по изложению теории доказательств для математической логики] столкнулось с существенной задержкой, поскольку на этапе, когда изложение уже приближалось к своему завершению, в области теории доказательств произошла перемена в связи с появлением работ Гербранда и Гёделя, что потребовало рассмотрения новых идей. Таким образом, объем этой книги расширился, так что разделение ее на два тома показалось целесообразным».
{{cite book}}: CS1 maint: location missing publisher (link)Bochenski, Jozef Maria, ред. (1959). A Precis of Mathematical Logic . Synthese Library, Vol. 1. Перевод Отто Берда. Дордрехт : Springer . doi :10.1007/978-94-017-0592-9. ISBN 9789048183296.
Кантор, Георг (1874). «Ueber eine Eigenschaft des Inbegriffes aller reellen алгебраишен Zahlen» (PDF) . Журнал для королевы и математики . 1874 (77): 258–262. дои : 10.1515/crll.1874.77.258. S2CID 199545885.Кэрролл, Льюис (1896). Символическая логика. Переиздания Kessinger Legacy. ISBN 9781163444955.
Soare, Robert Irving (22 декабря 2011 г.). "Computability Theory and Applications: The Art of Classical Computability" (PDF) . Факультет математики . Чикагский университет . Получено 23 августа 2017 г. .Суайнсхед, Ричард (1498 г.). Calculations Suiseth Anglici (на литовском языке). Папье: Per Francisco Gyrardengum.
{{cite book}}: CS1 maint: location missing publisher (link)