Математическая логика - Mathematical logic

Относительно теории Куайна, иногда называемой «математической логикой», см. Новые основы.

Математическая логика является подполем математика изучение применения формальных логика к математике. Он имеет тесные связи с метаматематика, то основы математики, и теоретическая информатика.[1] Объединяющие темы в математической логике включают изучение выразительной силы формальные системы и дедуктивный сила формального доказательство системы.

Математическая логика часто делится на области теория множеств, теория моделей, теория рекурсии, и теория доказательств. Эти области имеют общие результаты по логике, в частности логика первого порядка, и определимость. В информатике (особенно в Классификация ACM ) математическая логика включает в себя дополнительные темы, не раскрытые в этой статье; видеть Логика в информатике для тех.

С момента своего создания математическая логика способствовала изучению основ математики и мотивировалась им. Это исследование началось в конце 19 века с развитием аксиоматический рамки для геометрия, арифметика, и анализ. В начале 20 века его сформировали Дэвид Гильберт с программа доказать непротиворечивость основополагающих теорий. Результаты Курт Гёдель, Герхард Гентцен, и другие предоставили частичное решение программы и прояснили вопросы, связанные с доказательством согласованности. Работа в области теории множеств показала, что почти всю обычную математику можно формализовать в терминах множеств, хотя есть некоторые теоремы, которые нельзя доказать в общих системах аксиом для теории множеств. Современные работы по основам математики часто сосредоточены на установлении того, какие части математики могут быть формализованы в конкретных формальных системах (как в обратная математика ) вместо того, чтобы пытаться найти теории, в которых можно развить всю математику.

Подполя и область действия

В Справочник по математической логике[2] в 1977 г. делает грубое разделение современной математической логики на четыре области:

  1. теория множеств
  2. теория моделей
  3. теория рекурсии, и
  4. теория доказательств и конструктивная математика (рассматриваются как части единой территории).

Каждая область имеет определенную направленность, хотя многие методы и результаты используются во многих областях. Границы между этими областями и линии, разделяющие математическую логику и другие области математики, не всегда четкие. Теорема Гёделя о неполноте знаменует собой не только веху в теории рекурсии и теории доказательств, но также привел к Теорема Лёба в модальной логике. Методика принуждение используется в теории множеств, теории моделей и теории рекурсии, а также при изучении интуиционистской математики.

Математическое поле теория категорий использует множество формальных аксиоматических методов и включает изучение категориальная логика, но теория категорий обычно не считается подразделом математической логики. Из-за его применимости в различных областях математики, математики, в том числе Saunders Mac Lane предложили теорию категорий как основную систему математики, независимую от теории множеств. Эти фонды используют топы, которые напоминают обобщенные модели теории множеств, которые могут использовать классическую или неклассическую логику.

История

Математическая логика возникла в середине XIX века как раздел математики, отражающий слияние двух традиций: формальной философской логики и математики (Феррейрос 2001, п. 443). «Математическая логика, также называемая« логистической »,« символической логикой »,алгебра логики «, а в последнее время просто« формальная логика »- это набор логических теорий, разработанных в течение последнего [девятнадцатого] века с помощью искусственной записи и строго дедуктивного метода».[3] До этого появления логика изучалась с помощью риторика, с расчеты,[4] сквозь силлогизм, и с философия. В первой половине 20-го века произошел взрыв фундаментальных результатов, сопровождавшийся энергичными дебатами об основах математики.

Ранняя история

Дальнейшая информация: История логики

Теории логики были разработаны во многих культурах в истории, в том числе Китай, Индия, Греция и Исламский мир. Греческие методы, особенно Аристотелевская логика (или логика термина), как указано в Органон, нашла широкое применение и признание в западной науке и математике на протяжении тысячелетий.[5] В Стоики, особенно Хрисипп, начали разработку логика предикатов. В Европе XVIII века попытки трактовать операции формальной логики символическим или алгебраическим образом предпринимались философскими математиками, в том числе Лейбниц и Ламберт, но их труды оставались изолированными и малоизвестными.

19 век

В середине девятнадцатого века Джордж Буль а потом Огастес Де Морган представлены систематические математические трактовки логики. Их работа, основанная на трудах алгебраистов, таких как Джордж Пикок, расширил традиционную аристотелевскую доктрину логики в достаточную основу для изучения основы математики  (Кац 1998, п. 686).

Чарльз Сандерс Пирс основанный на работе Буля по разработке логической системы отношений и кванторов, которую он опубликовал в нескольких статьях с 1870 по 1885 год.Готтлоб Фреге представил независимое развитие логики с кванторами в своей Begriffsschrift, опубликованный в 1879 году, труд, который считается поворотным моментом в истории логики. Однако работа Фреге оставалась неясной до тех пор, пока Бертран Рассел начали продвигать его на рубеже веков. Двумерная нотация, разработанная Фреге, никогда не получила широкого распространения и не используется в современных текстах.

С 1890 по 1905 год Эрнст Шредер опубликовано Vorlesungen über die Algebra der Logik в трех томах. Эта работа обобщила и расширила работы Буля, Де Моргана и Пирса и была исчерпывающей ссылкой на символическую логику, как она понималась в конце XIX века.

Основополагающие теории

Опасения по поводу того, что математика не была построена на должном основании, привели к развитию аксиоматических систем для фундаментальных областей математики, таких как арифметика, анализ и геометрия.

В логике термин арифметика относится к теории натуральные числа. Джузеппе Пеано (1889 ) опубликовал набор аксиом для арифметики, получивший его имя (Аксиомы Пеано ), используя вариант логической системы Буля и Шредера, но добавляя кванторы. В то время Пеано не знал о работе Фреге. Примерно в то же время Ричард Дедекинд показали, что натуральные числа однозначно характеризуются своим индукция характеристики. Дедекинд (1888 ) предложил другую характеристику, в которой отсутствовал формально-логический характер аксиом Пеано. Однако работа Дедекинда доказала теоремы, недоступные в системе Пеано, включая единственность множества натуральных чисел (с точностью до изоморфизма) и рекурсивные определения сложения и умножения из функция преемника и математическая индукция.

В середине XIX века стали известны недостатки геометрических аксиом Евклида (Кац 1998, п. 774). Помимо независимости параллельный постулат, установленный Николай Лобачевский в 1826 г. (Лобачевский 1840 ) математики обнаружили, что некоторые теоремы, которые Евклид считал само собой разумеющимися, на самом деле нельзя было доказать на основе его аксиом. Среди них - теорема о том, что линия содержит по крайней мере две точки или что круги одного радиуса, центры которых разделены этим радиусом, должны пересекаться. Гильберт (1899 ) разработан полный комплект аксиомы геометрии, опираясь на Предыдущая работа по Pasch (1882 ). Успех аксиоматизации геометрии побудил Гильберта искать полную аксиоматизацию других областей математики, таких как натуральные числа и реальная линия. Это окажется основным направлением исследований в первой половине 20 века.

XIX век ознаменовался большими успехами в теории реальный анализ, включая теории сходимости функций и Ряд Фурье. Математики, такие как Карл Вейерштрасс начал создавать функции, расширяющие интуицию, такие как нигде не дифференцируемые непрерывные функции. Предыдущие концепции функции как правила вычисления или гладкого графика больше не подходили. Вейерштрасс начал защищать арифметизация анализа, который пытался аксиоматизировать анализ, используя свойства натуральных чисел. Современный (ε, δ) -определение предела и непрерывные функции уже был разработан Больцано в 1817 г. (Фельшер 2000 ), но оставался относительно неизвестным.Коши в 1821 г. определил преемственность с точки зрения бесконечно малые (см. Cours d'Analyse, стр. 34). В 1858 году Дедекинд предложил определение действительных чисел в терминах Дедекинд сокращает рациональных чисел (Дедекинд 1872 г.), определение, которое до сих пор используется в современных текстах.

Георг Кантор разработал основные концепции теории бесконечных множеств. Его первые результаты развили теорию мощность и доказано что действительные и натуральные числа имеют разную мощность (Cantor 1874). В течение следующих двадцати лет Кантор разработал теорию трансфинитные числа в серии публикаций. В 1891 году он опубликовал новое доказательство несчетности действительных чисел, которое ввело диагональный аргумент, и использовал этот метод для доказательства Теорема кантора что ни один набор не может иметь такую ​​же мощность, как его powerset. Кантор считал, что каждый набор может быть хорошо организованный, но не смог предоставить доказательства этого результата, оставив его открытой проблемой в 1895 г. (Кац 1998, стр. 807 ).

20 век

В первые десятилетия 20 века основными областями исследований были теория множеств и формальная логика. Открытие парадоксов в неформальной теории множеств заставило некоторых задуматься, не противоречит ли сама математика, и искать доказательства непротиворечивости.

В 1900 г. Гильберта представил знаменитый список 23 задачи на следующий век. Первые два из них должны были решить гипотеза континуума и доказать непротиворечивость элементарной арифметики соответственно; Десятый заключался в создании метода, который мог бы решить, является ли многомерное полиномиальное уравнение над целые числа есть решение. Последующая работа по разрешению этих проблем сформировала направление математической логики, как и попытки решить проблему Гильберта. Entscheidungsproblem, поставленная в 1928 году. Эта проблема требовала процедуры, которая решала бы, учитывая формализованное математическое утверждение, является ли утверждение истинным или ложным.

Теория множеств и парадоксы

Эрнст Цермело (1904 ) дал доказательство того, что каждый набор может быть хорошо заказан, результат Георг Кантор не удалось получить. Чтобы добиться доказательства, Цермело ввел аксиома выбора, который вызвал жаркие споры и исследования среди математиков и пионеров теории множеств. Непосредственная критика метода побудила Цермело опубликовать второе изложение своего результата, прямо обращаясь к критике его доказательства (Цермело 1908a ). Эта статья привела к всеобщему принятию аксиомы выбора в математическом сообществе.

Скептицизм по поводу аксиомы выбора был усилен недавно обнаруженными парадоксами в наивная теория множеств. Чезаре Бурали-Форти (1897 ) был первым, кто сформулировал парадокс: Парадокс Бурали-Форти показывает, что совокупность всех порядковые номера не может составить набор. Очень скоро после этого, Бертран Рассел обнаруженный Парадокс Рассела в 1901 г. и Жюль Ричард (1905 ) обнаруженный Парадокс ричарда.

Цермело (1908b ) предоставил первый набор аксиом теории множеств. Эти аксиомы вместе с дополнительными аксиома замены предложено Авраам Френкель, теперь называются Теория множеств Цермело – Френкеля (ZF). Аксиомы Цермело включали принцип ограничение размера чтобы избежать парадокса Рассела.

В 1910 г. вышел первый том Principia Mathematica Расселом и Альфред Норт Уайтхед был опубликован. Эта основополагающая работа развила теорию функций и мощности в полностью формальных рамках теория типов, который Рассел и Уайтхед разработали, чтобы избежать парадоксов. Principia Mathematica считается одной из самых влиятельных работ 20-го века, хотя рамки теории типов не оказались популярными в качестве фундаментальной теории математики (Феррейрос 2001, п. 445).

Френкель (1922 ) доказал, что аксиома выбора не может быть доказана из аксиом теории множеств Цермело с урэлементы. Позже работа Пол Коэн (1966 ) показал, что добавление мурэлементов не требуется, а выбранная аксиома недоказуема в ZF. Доказательство Коэна развило метод принуждение, который сейчас является важным инструментом для создания результаты независимости в теории множеств.[6]

Символическая логика

Леопольд Левенхайм (1915 ) и Торальф Сколем (1920 ) получил Теорема Лёвенгейма – Сколема, который говорит, что логика первого порядка не может контролировать мощности бесконечных структур. Сколем понял, что эта теорема применима к формализации первого порядка теории множеств, и что из нее следует, что любая такая формализация имеет счетный модель. Этот парадоксальный факт стал известен как Парадокс Сколема.

В своей докторской диссертации Курт Гёдель (1929 ) доказал теорема полноты, который устанавливает соответствие между синтаксисом и семантикой в ​​логике первого порядка. Гёдель использовал теорему о полноте для доказательства теорема компактности, демонстрируя финитарную природу первого порядка логическое следствие. Эти результаты помогли установить логику первого порядка как доминирующую логику, используемую математиками.

В 1931 году Гёдель опубликовал О формально неразрешимых предложениях Principia Mathematica и родственных систем, который доказал неполноту (в другом смысле этого слова) всех достаточно сильных и эффективных теорий первого порядка. Этот результат, известный как Теорема Гёделя о неполноте, устанавливает серьезные ограничения на аксиоматические основы математики, нанося сильный удар по программе Гильберта. Он показал невозможность обеспечить непротиворечивость арифметики в рамках какой-либо формальной теории арифметики. Гильберт, однако, некоторое время не признавал важности теоремы о неполноте.[7]

Теорема Гёделя показывает, что последовательность Доказательство какой-либо достаточно сильной и эффективной системы аксиом не может быть получено ни в самой системе, если она непротиворечива, ни в какой-либо более слабой системе. Это оставляет открытой возможность доказательств непротиворечивости, которые не могут быть формализованы в рамках рассматриваемой системы. Генцен (1936 ) доказал непротиворечивость арифметики, используя финитистическую систему вместе с принципом трансфинитная индукция. Результат Гентцена представил идеи вырезать устранение и ординалы теории доказательств, которые стали ключевыми инструментами теории доказательств. Гёдель (1958 ) дал другое доказательство непротиворечивости, которое снижает непротиворечивость классической арифметики до интуиционистской арифметики в высших типах.

Начало других ветвей

Альфред Тарский разработал основы теория моделей.

Начиная с 1935 г. группа выдающихся математиков сотрудничала под псевдонимом Николя Бурбаки чтобы публиковать Éléments de mathématique, серия текстов по энциклопедической математике. Эти тексты, написанные в строгом и аксиоматическом стиле, подчеркивали строгость изложения и теоретико-множественные основы. Терминология, придуманная этими текстами, например, слова биекция, инъекция, и сюрприз и теоретико-множественные основы использованных текстов получили широкое распространение в математике.

Изучение вычислимости стало известно как теория рекурсии или теория вычислимости, потому что ранние формализации Гёделя и Клини основывались на рекурсивных определениях функций.[8] Когда эти определения были показаны эквивалентными формализации Тьюринга, включающей Машины Тьюринга стало ясно, что новая концепция - вычислимая функция - было обнаружено, и что это определение было достаточно надежным, чтобы допускать многочисленные независимые характеристики. В своей работе над теоремами о неполноте в 1931 году Гёделю не хватало строгой концепции эффективной формальной системы; он сразу понял, что для этой цели можно использовать новые определения вычислимости, что позволило ему сформулировать теоремы о неполноте в общих чертах, которые могли подразумеваться только в исходной статье.

Многочисленные результаты в теории рекурсии были получены в 1940-х гг. Стивен Коул Клини и Эмиль Леон Пост. Клини (1943 ) ввел концепции относительной вычислимости, предвосхищенные Тьюрингом (1939 ), а арифметическая иерархия. Позже Клини обобщил теорию рекурсии на функционалы более высокого порядка. Клини и Георг Крайзель изучал формальные версии интуиционистской математики, особенно в контексте теории доказательств.

Формальные логические системы

По своей сути математическая логика имеет дело с математическими концепциями, выраженными с помощью формальных логические системы. Эти системы, хотя и отличаются во многих деталях, имеют общее свойство рассматривать только выражения на фиксированном формальном языке. Системы логика высказываний и логика первого порядка сегодня наиболее широко изучаются из-за их применимости к основы математики и из-за их желательных теоретико-доказательственных свойств.[9] Более сильные классические логики, такие как логика второго порядка или же бесконечная логика также изучаются вместе с Неклассические логики Такие как интуиционистская логика.

Логика первого порядка

Основная статья: Логика первого порядка

Логика первого порядка особый формальная система логики. Его синтаксис включает только конечные выражения как правильные формулы, а его семантика характеризуются ограничением всех кванторы к фиксированному область дискурса.

Первые результаты формальной логики установили ограничения логики первого порядка. В Теорема Лёвенгейма – Сколема (1919) показали, что если набор предложений в счетном языке первого порядка имеет бесконечную модель, то он имеет по крайней мере одну модель каждой бесконечной мощности. Это показывает, что набор аксиом первого порядка не может характеризовать натуральные числа, действительные числа или любую другую бесконечную структуру вплоть до изоморфизм. Поскольку целью ранних фундаментальных исследований было создание аксиоматических теорий для всех разделов математики, это ограничение было особенно суровым.

Теорема Гёделя о полноте (Гёдель 1929 ) установил эквивалентность семантического и синтаксического определения логическое следствие в логике первого порядка. Это показывает, что если конкретное предложение истинно в каждой модели, которая удовлетворяет определенному набору аксиом, то должно быть конечное выведение предложения из аксиом. В теорема компактности впервые появилась в виде леммы в доказательстве теоремы Гёделя о полноте, и потребовалось много лет, прежде чем логики осознали ее значение и начали регулярно ее применять. Он говорит, что набор предложений имеет модель тогда и только тогда, когда каждое конечное подмножество имеет модель, или, другими словами, несовместимый набор формул должен иметь конечное несовместимое подмножество. Теоремы о полноте и компактности позволяют провести сложный анализ логических следствий в логике первого порядка и разработать теория моделей, и они являются ключевой причиной выдающегося положения логики первого порядка в математике.

Теоремы Гёделя о неполноте (Гёдель 1931 ) устанавливают дополнительные ограничения на аксиоматизацию первого порядка. В первая теорема о неполноте утверждает, что для любой непротиворечивой, эффективно заданной (определенной ниже) логической системы, способной интерпретировать арифметику, существует утверждение, которое является истинным (в том смысле, что оно справедливо для натуральных чисел), но не доказуемо в рамках этой логической системы (и которое действительно может потерпеть неудачу в некоторых нестандартные модели арифметики что может быть согласовано с логической системой). Например, в любой логической системе, способной выразить Аксиомы Пеано, предложение Гёделя верно для натуральных чисел, но не может быть доказано.

Здесь говорят, что логическая система эффективно задана, если по любой формуле на языке системы можно решить, является ли формула аксиомой, а та, которая может выражать аксиомы Пеано, называется «достаточно сильной». Применительно к логике первого порядка первая теорема о неполноте означает, что любая достаточно сильная, последовательная и эффективная теория первого порядка имеет модели, которые не являются элементарно эквивалентный, более сильное ограничение, чем ограничение, установленное теоремой Левенгейма – Сколема. В вторая теорема о неполноте утверждает, что никакая достаточно сильная, непротиворечивая, эффективная система аксиом для арифметики не может доказать свою собственную непротиворечивость, которая была интерпретирована, чтобы показать, что Программа Гильберта недоступен.

Другая классическая логика

Изучаются многие логики, помимо логики первого порядка. К ним относятся инфинитарная логика, которые позволяют формулам предоставлять бесконечное количество информации, и логика высшего порядка, которые включают часть теории множеств непосредственно в свою семантику.

Самая хорошо изученная инфинитарная логика - это . В этой логике кванторы могут быть вложены только на конечную глубину, как в логике первого порядка, но формулы могут иметь в себе конечные или счетно бесконечные союзы и дизъюнкции. Так, например, можно сказать, что объект представляет собой целое число, используя формулу Такие как

Логики более высокого порядка позволяют количественно определять не только элементы область дискурса, но подмножества области дискурса, множества таких подмножеств и другие объекты более высокого типа. Семантика определена таким образом, что вместо того, чтобы иметь отдельный домен для каждого квантификатора более высокого типа, в котором должен быть диапазон, квантификаторы вместо этого охватывают все объекты соответствующего типа. Логики, изучаемые до развития логики первого порядка, например логика Фреге, имели аналогичные теоретико-множественные аспекты. Хотя логики более высокого порядка более выразительны и допускают полную аксиоматизацию структур, таких как натуральные числа, они не удовлетворяют аналогам теорем о полноте и компактности из логики первого порядка и, таким образом, менее поддаются теоретическому анализу.

Другой тип логики логика с фиксированной точкойs что позволяет индуктивные определения, как пишут для примитивные рекурсивные функции.

Можно формально определить расширение логики первого порядка - понятие, которое охватывает все логики в этом разделе, потому что они ведут себя как логика первого порядка в определенных фундаментальных отношениях, но не охватывает всю логику в целом, например он не включает интуиционистский, модальный или нечеткая логика.

Теорема Линдстрема означает, что единственное расширение логики первого порядка, удовлетворяющее как теорема компактности и вниз теорема Левенгейма – Сколема логика первого порядка.

Неклассическая и модальная логика

Основная статья: Неклассическая логика

Модальная логика включить дополнительные модальные операторы, такие как оператор, который утверждает, что конкретная формула не только истинна, но и обязательно истинна. Хотя модальная логика не часто используется для аксиоматизации математики, она использовалась для изучения свойств доказуемости первого порядка (Соловей 1976 ) и теоретико-множественное форсирование (Хэмкинс и Лёве 2007 ).

Интуиционистская логика был разработан Гейтингом для изучения программы интуиционизма Брауэра, в которой сам Брауэр избегал формализации. Интуиционистская логика специально не включает закон исключенного среднего, в котором говорится, что каждое предложение истинно или его отрицание истинно. Работа Клини с теорией доказательств интуиционистской логики показала, что конструктивная информация может быть получена из интуиционистских доказательств. Например, любая доказуемо полная функция в интуиционистской арифметике есть вычислимый; это неверно в классических теориях арифметики, таких как Арифметика Пеано.

Алгебраическая логика

Алгебраическая логика использует методы абстрактная алгебра изучить семантику формальных логик. Основополагающий пример - использование Булевы алгебры представлять ценности истины в классической логике высказываний, и использование Гейтинговые алгебры представлять ценности истины в интуиционистской логике высказываний. Более сильные логики, такие как логика первого порядка и логика высшего порядка, изучаются с использованием более сложных алгебраических структур, таких как цилиндрические алгебры.

Теория множеств

Основная статья: Теория множеств

Теория множеств это изучение наборы, которые представляют собой абстрактные коллекции объектов. Многие из основных понятий, таких как порядковые и кардинальные числа, были разработаны Кантором неформально до того, как были разработаны формальные аксиоматизации теории множеств. В первая такая аксиоматизация, благодаря Цермело (1908b ), был немного расширен, чтобы стать Теория множеств Цермело – Френкеля (ZF), которая в настоящее время является наиболее широко используемой фундаментальной теорией математики.

Были предложены другие формализации теории множеств, в том числе теория множеств фон Неймана – Бернейса – Гёделя (NBG), Теория множеств Морса – Келли (МК), и Новые основы (NF). Из них ZF, NBG и MK похожи в описании совокупная иерархия наборов. New Foundations использует другой подход; он позволяет использовать такие объекты, как набор всех множеств, за счет ограничений на его аксиомы существования множеств. Система Теория множеств Крипке – Платека тесно связана с обобщенной теорией рекурсии.

Два известных утверждения в теории множеств: аксиома выбора и гипотеза континуума. Аксиома выбора, впервые сформулированная Цермело (1904 ), независимость от ZF была доказана Френкелем (1922 ), но получил широкое признание среди математиков. В нем говорится, что для данной коллекции непустых наборов существует единственный набор C который содержит ровно один элемент из каждого набора в коллекции. Набор C Говорят, что он «выбирает» один элемент из каждого набора в коллекции. Хотя некоторые считают возможность сделать такой выбор очевидной, поскольку каждое множество в коллекции непусто, отсутствие общего, конкретного правила, по которому может быть сделан выбор, делает аксиому неконструктивной. Стефан Банах и Альфред Тарский (1924[цитата не найдена ]) показал, что выбранная аксиома может быть использована для разложения твердого шара на конечное число частей, которые затем могут быть перегруппированы без масштабирования, чтобы сделать два твердых шара исходного размера. Эта теорема, известная как Парадокс Банаха – Тарского, является одним из многих противоречивых результатов аксиомы выбора.

Гипотеза континуума, впервые предложенная в качестве гипотезы Кантором, была перечислена Дэвид Гильберт в качестве одной из своих 23 проблем в 1900 году. Гедель показал, что гипотеза континуума не может быть опровергнута аксиомами теории множеств Цермело – Френкеля (с аксиомой выбора или без нее), развивая конструируемая вселенная теории множеств, в которой должна выполняться гипотеза континуума. В 1963 г. Пол Коэн показал, что гипотеза континуума не может быть доказана из аксиом теории множеств Цермело – Френкеля (Коэн 1966 ). Однако этот результат независимости не разрешил полностью вопрос Гильберта, поскольку вполне возможно, что новые аксиомы теории множеств могли разрешить гипотезу. Недавняя работа в этом направлении была проведена В. Хью Вудин, хотя его важность пока не ясна (Вудин 2001 ).

Современные исследования в области теории множеств включают изучение большие кардиналы и определенность. Крупные кардиналы Количественные числительные с частными свойствами, настолько сильными, что существование таких кардиналов не может быть доказано в ZFC. Существование наименьшего большого кардинала обычно изучается, недоступный кардинал, уже подразумевает непротиворечивость ZFC. Несмотря на то, что у крупных кардиналов чрезвычайно высокий мощность, их существование имеет много разветвлений для структуры реальной линии. Решительность относится к возможному существованию выигрышных стратегий для некоторых игр для двух игроков (игры называются определенный). Существование этих стратегий предполагает структурные свойства реальной линии и других Польские просторы.

Теория моделей

Основная статья: Теория моделей

Теория моделей изучает модели различных формальных теорий. Здесь теория набор формул в определенной формальной логике и подпись, а модель представляет собой структуру, дающую конкретную интерпретацию теории. Теория моделей тесно связана с универсальная алгебра и алгебраическая геометрия, хотя методы теории моделей сосредоточены больше на логических соображениях, чем на этих областях.

Множество всех моделей конкретной теории называется начальный класс; Классическая теория моделей стремится определить свойства моделей в конкретном элементарном классе или определить, образуют ли определенные классы структур элементарные классы.

Методика исключение квантора может использоваться, чтобы показать, что определимые множества в конкретных теориях не могут быть слишком сложными. Тарский (1948 ) установленное исключение квантора для реально закрытые поля, результат, который также показывает, что теория поля действительных чисел разрешимый. (Он также отметил, что его методы в равной степени применимы к алгебраически замкнутым полям произвольной характеристики.) Современное подполе, развивающееся из этого, связано с о-минимальные конструкции.

Теорема Морли о категоричности, доказано Майкл Д. Морли (1965 ), утверждает, что если теория первого порядка в счетном языке категорична в некоторой несчетной мощности, т.е. все модели этой мощности изоморфны, то она категорична во всех бесчисленных мощностях.

Тривиальное следствие гипотеза континуума состоит в том, что полная теория с меньшим, чем континуум, множеством неизоморфных счетных моделей может иметь только счетное число. Гипотеза воота, названный в честь Роберт Лоусон Воот, говорит, что это верно даже независимо от гипотезы континуума. Установлено множество частных случаев этой гипотезы.

Теория рекурсии

Основная статья: Теория рекурсии

Теория рекурсии, также называемый теория вычислимости, изучает свойства вычислимые функции и Степени Тьюринга, которые делят невычислимые функции на множества с одинаковым уровнем невычислимости. Теория рекурсии также включает изучение обобщенной вычислимости и определимости. Теория рекурсии выросла из работ Рожа Петер, Церковь Алонсо и Алан Тьюринг в 1930-х годах, который был значительно расширен Клини и Почтовый в 1940-е гг.[10]

Классическая теория рекурсии фокусируется на вычислимости функций от натуральных чисел до натуральных чисел. Фундаментальные результаты устанавливают устойчивый канонический класс вычислимых функций с многочисленными независимыми эквивалентными характеризациями с использованием Машины Тьюринга, λ исчисление, и другие системы. Более продвинутые результаты касаются структуры степеней Тьюринга и решетка из рекурсивно перечислимые множества.

Обобщенная теория рекурсии расширяет идеи теории рекурсии на вычисления, которые больше не обязательно являются конечными. Он включает в себя изучение вычислимости в высших типах, а также в таких областях, как гиперарифметическая теория и теория α-рекурсии.

Современные исследования в области теории рекурсии включают изучение таких приложений, как алгоритмическая случайность, теория вычислимых моделей, и обратная математика, а также новые результаты в чистой теории рекурсии.

Алгоритмически неразрешимые проблемы

Важное подразделение теории рекурсии изучает алгоритмическую неразрешимость; а проблема решения или же функциональная проблема является алгоритмически неразрешимый если нет возможного вычислимого алгоритма, который возвращает правильный ответ для всех допустимых входных данных проблемы. Первые результаты о неразрешимости, полученные независимо Черчем и Тьюрингом в 1936 г., показали, что Entscheidungsproblem алгоритмически неразрешима. Тьюринг доказал это, установив неразрешимость проблема остановки, результат с далеко идущими последствиями как в теории рекурсии, так и в информатике.

Есть много известных примеров неразрешимых задач из обычной математики. В проблема слов для групп было доказано алгоритмически неразрешимым Петр Новиков в 1955 г. и независимо У. Бун в 1959 г. занятой бобер проблема, разработанная Тибор Радо в 1962 году - еще один известный пример.

Десятая проблема Гильберта попросили алгоритм, чтобы определить, имеет ли многомерное полиномиальное уравнение с целыми коэффициентами решение в целых числах. Частичный прогресс был достигнут Джулия Робинсон, Мартин Дэвис и Хилари Патнэм. Алгоритмическая неразрешимость проблемы доказана Юрий Матиясевич в 1970 г. (Дэвис 1973 ).

Теория доказательств и конструктивная математика

Основная статья: Теория доказательств

Теория доказательств это изучение формальных доказательств в различных системах логического вывода. Эти доказательства представлены в виде формальных математических объектов, что упрощает их анализ математическими методами. Обычно рассматриваются несколько систем удержания, в том числе Системы дедукции в стиле Гильберта, системы естественный вычет, а последовательное исчисление разработан Gentzen.

Изучение конструктивная математикав контексте математической логики включает изучение систем в неклассической логике, такой как интуиционистская логика, а также изучение предикативный системы. Один из первых сторонников предикативизма был Герман Вейль, который показал, что можно разработать большую часть реального анализа, используя только методы прогнозирования (Вейль 1918 )[цитата не найдена ].

Поскольку доказательства полностью окончательны, а истина в структуре - нет, в конструктивной математике обычно делается упор на доказуемость. Особый интерес представляет связь между доказуемостью в классических (или неконструктивных) системах и доказуемостью в интуиционистских (или конструктивных, соответственно) системах. Такие результаты, как Негативный перевод Гёделя – Гентцена показать, что можно встраивать (или переведите) классическая логика в интуиционистскую логику, что позволяет перенести некоторые свойства интуиционистских доказательств обратно в классические доказательства.

Последние разработки в теории доказательств включают изучение доказательная добыча к Ульрих Коленбах и изучение ординалы теории доказательств к Майкл Ратьен.

Приложения

«Математическая логика успешно применяется не только к математике и ее основам (Г. Фреге, Б. Рассел, Д. Гильберт, П. Бернейс, Х. Шольц, Р. Карнап, С. Лесневски, Т. Сколем ), но и в физику (Р. Карнап, А. Диттрих, Б. Рассел, К. Э. Шеннон, А. Н. Уайтхед, Х. Райхенбах, П. Февриер), биологии (Дж. Х. Вудгер, А. Тарский ), психологии (Ф. Б. Фитч, К. Г. Хемпель ), закону и морали (К. Менгер, У. Клуг, П. Оппенгейм), к экономике (Дж. Нойман, О. Моргенштерн ), на практические вопросы (Э. К. Беркли, Э. Штамм) и даже к метафизике (Дж. [Ян] Саламуча, Х. Шольц, Я. М. Боченски ). Его приложения к истории логики оказались чрезвычайно плодотворными (Я. Лукасевич, Х. Шольц, Б. Товарищи, А. Беккер, Э. Муди, Дж. Саламуча, К. Дуэрр, З. Джордан, П. Бонер, Дж. М. Боченски, С. [Станислав] Т. Шайер, Д. Ингаллс )."[11] «Применения были также сделаны в теологии (Ф. Древновски, Дж. Саламуча, И. Томас)».[12]

Связь с информатикой

Основная статья: Логика в информатике

Изучение теория вычислимости в информатике тесно связано с изучением вычислимости в математической логике. Однако есть разница в акцентах. Компьютерные ученые часто сосредотачиваются на конкретных языках программирования и допустимая вычислимость, в то время как исследователи математической логики часто сосредотачиваются на вычислимости как теоретической концепции и на невычислимости.

Теория семантика языков программирования относится к теория моделей, как есть проверка программы (особенно, проверка модели ). В Изоморфизм Карри – Ховарда между доказательствами и программами относится к теория доказательств, особенно интуиционистская логика. Формальные исчисления, такие как лямбда-исчисление и комбинаторная логика теперь рассматриваются как идеализированные языки программирования.

Информатика также вносит свой вклад в математику, разрабатывая методы автоматической проверки или даже нахождения доказательств, такие как автоматическое доказательство теорем и логическое программирование.

Описательная теория сложности связывает логику с вычислительная сложность. Первый значительный результат в этой области, Теорема Феджина (1974) установил, что НП это как раз набор языков, выражаемых предложениями экзистенциального логика второго порядка.

Основы математики

Основная статья: Основы математики

В 19 веке математики осознали логические пробелы и несоответствия в своей области. Было показано, что Евклид Аксиомы России для геометрии, которые веками преподавались как пример аксиоматического метода, были неполными. Использование бесконечно малые, и само определение функция, ставились под сомнение при анализе, поскольку такие патологические примеры, как «нигде» Вейерштрасса.дифференцируемый были открыты непрерывные функции.

Исследования Кантора произвольных бесконечных множеств также вызвали критику. Леопольд Кронекер известное высказывание «Бог создал целые числа; все остальное - дело рук человека», поддерживая возвращение к изучению конечных конкретных объектов в математике. Хотя аргумент Кронекера был поддержан конструктивистами в 20 веке, математическое сообщество в целом отвергло их. Дэвид Гильберт выступал за изучение бесконечного, говоря: «Никто не изгонит нас из рая, созданного Кантором».

Математики начали поиск систем аксиом, которые можно было бы использовать для формализации больших частей математики. Помимо устранения двусмысленности из ранее наивных терминов, таких как функция, была надежда, что эта аксиоматизация позволит получить доказательства непротиворечивости. В XIX веке основным методом доказательства непротиворечивости набора аксиом было создание модели для него. Так, например, неевклидова геометрия можно доказать непротиворечивость, определив точка означать точку на фиксированной сфере и линия означать большой круг на сфере. Полученная структура, модель эллиптическая геометрия, удовлетворяет аксиомам плоской геометрии, за исключением постулата параллельности.

С развитием формальной логики Гильберт спросил, можно ли доказать, что система аксиом непротиворечива, анализируя структуру возможных доказательств в системе и показывая этим анализом невозможность доказательства противоречия. Эта идея привела к изучению теория доказательств. Более того, Гильберт предложил, чтобы анализ был полностью конкретным, используя термин финишный сослаться на методы, которые он позволил бы, но не определив их точно. Этот проект, известный как Программа Гильберта, серьезно повлияли теоремы Гёделя о неполноте, которые показывают, что непротиворечивость формальных теорий арифметики не может быть установлена ​​с помощью методов, формализуемых в этих теориях. Генцен показал, что можно получить доказательство непротиворечивости арифметики в финитарной системе, дополненной аксиомами трансфинитная индукция, и методы, которые он разработал для этого, были основополагающими в теории доказательств.

Вторая нить в истории основ математики связана с неклассическая логика и конструктивная математика. Изучение конструктивной математики включает в себя множество различных программ с различными определениями конструктивный. В большинстве случаев доказательства в теории множеств ZF, не использующие аксиому выбора, многие математики называют конструктивными. Более ограниченные версии конструктивизма ограничиваются натуральные числа, теоретико-числовые функции, и наборы натуральных чисел (которые могут использоваться для представления действительных чисел, облегчая изучение математический анализ ). Распространенная идея состоит в том, что конкретные средства вычисления значений функции должны быть известны, прежде чем можно будет сказать, что сама функция существует.

В начале 20 века Луитцен Эгбертус Ян Брауэр основанный интуиционизм в составе философия математики . Эта философия, сначала плохо понимаемая, утверждала, что для того, чтобы математическое утверждение было верным для математика, этот человек должен уметь интуиция утверждение, чтобы не только поверить в его истинность, но и понять причину его истинности. Следствием этого определения истины стало отрицание закон исключенного среднего, поскольку есть утверждения, которые, согласно Брауэру, нельзя назвать истинными, в то время как их отрицания также не могут быть заявлены как истинные. Философия Брауэра оказала влияние и стала причиной ожесточенных споров среди выдающихся математиков. Позже Клини и Крайзель изучили формализованные версии интуиционистской логики (Брауэр отверг формализацию и представил свою работу на неформализованном естественном языке). С появлением Толкование BHK и Крипке модели интуиционизм стало легче примириться с классическая математика.

Смотрите также

Примечания

  1. ^ Тексты для студентов бакалавриата включают Boolos, Burgess и Jeffrey. (2002), Enderton (2001), и Мендельсон (1997). Классический выпускной текст Шенфилда (2001) впервые появился в 1967 году.
  2. ^ Видеть (Барвайз 1989 )
  3. ^ Юзеф Мария Боченски, Точность математической логики (1959), ред. и пер., Альберт Менне, изд. и пер., Отто Берд, Дордрехт, Южная Голландия: Reidel, Sec. 0.1, п. 1.
  4. ^ Ричард Свинсхед (1498), Calculationes Suiseth Anglici, Папи: Per Franciscum Gyrardengum.
  5. ^ Boehner p. xiv
  6. ^ Смотрите также Коэн 2008.
  7. ^ В предисловии к первому изданию журнала 1934 г.Grundlagen der Mathematik " (Гильберт и Бернейс, 1934 г. ), Бернейс написал следующее, напоминающее знаменитую записку Фреге когда ему сообщили о парадоксе Рассела.

    «Die Ausführung Dieses Vorhabens шляпу Eine wesentliche Verzögerung dadurch erfahren, Дас в Эйнем стадионе, в деме фильеров Darstellung Schon ihrem Abschuß нах война, Дурх дас Erscheinen дер Arbeiten фон Эрбраны унд фон гёделевской Eine veränderte Ситуация им-Gebiet дера Beweistheorie entstand, Welche умереть Berücksichtigung Нойера Einsichten zur Aufgabe machte. Dabei ist der Umfang des Buches angewachsen, so daß eine Teilung in zwei Bände angezeigt erschien ".

    Перевод:

    «Осуществление этого плана [Гильберта по изложению теории доказательств для математической логики] столкнулось с существенной задержкой, потому что на этапе, на котором изложение было уже близко к завершению, произошла изменившаяся ситуация в области теории доказательств. в связи с появлением работ Хербранда и Гёделя, которые потребовали рассмотрения новых идей. Таким образом, объем этой книги вырос, так что разделение на два тома казалось целесообразным ».

    Так что, конечно, Гильберт осознавал важность работы Гёделя к 1934 году. Второй том 1939 года включал форму доказательства непротиворечивости Гентцена для арифметики.
  8. ^ Подробное изучение этой терминологии дано Соаре (1996 ).
  9. ^ Феррейрос (2001 ) рассматривает рост логики первого порядка над другими формальными логиками в начале 20 века.
  10. ^ Соаре, Роберт Ирвинг (22 декабря 2011 г.). «Теория вычислимости и приложения: искусство классической вычислимости» (PDF). Кафедра математики. Чикагский университет. Получено 23 августа 2017.
  11. ^ Юзеф Мария Боченски, Точность математической логики, ред. и пер., Альберт Менне, изд. и пер., Отто Берд, Дордрехт, Южная Голландия: Reidel, Sec. 0.3, п. 2.
  12. ^ Юзеф Мария Боченски, Точность математической логики, ред. и пер., Альберт Менне, изд. и пер., Отто Берд, Дордрехт, Южная Голландия: Reidel, Sec. 0.3, п. 2.

Рекомендации

Тексты для студентов

Тексты для выпускников

Научные статьи, монографии, тексты и обзоры

Классические статьи, тексты и сборники

  • Бурали-Форти, Чезаре (1897), Вопрос о трансфинитных числах, перепечатано в van Heijenoort 1976, pp. 104–111.
  • Дедекинд, Ричард (1872), Stetigkeit und Irrationale Zahlen. Английский перевод названия: «Непротиворечивость и иррациональные числа».
  • Дедекинд, Ричард (1888), Was sind und was sollen die Zahlen? Два английских перевода:
    • 1963 (1901). Очерки теории чисел. Беман, У. У., изд. и транс. Дувр.
    • 1996. В От Канта до Гильберта: Справочник по основам математики, 2 тома, Эвальд, Уильям Б., изд., Oxford University Press: 787–832.
  • Френкель, Абрахам А. (1922), "Der Begriff 'Definit' und die Unabhängigkeit des Auswahlsaxioms", Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-Mathematische Klasse, стр. 253–257 (Немецкий), перепечатано в английском переводе как «Понятие« определенный »и независимость аксиомы выбора», van Heijenoort 1976, стр. 284–289.

внешняя ссылка