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

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

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

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

Справочник по математической логике в 1977 году делает грубое деление современной математической логики в четырех областях:

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

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

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

История

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

История ранних веков

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

19 век

В середине девятнадцатого века Джордж Буль, а затем Август де Морган представили систематические математические трактовки логики. Их работа, основанная на трудах таких алгебраистов, как Джордж Пикок , расширила традиционную аристотелевскую доктрину логики до достаточной основы для изучения основ математики . Чарльз Сандерс Пирс позже основал работу Буля для разработки логической системы отношений и кванторов, которую он опубликовал в нескольких статьях с 1870 по 1885 год.

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

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

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

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

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

В середине 19 века стали известны недостатки геометрических аксиом Евклида. Помимо независимости постулата параллельности , установленного Николаем Лобачевским в 1826 году, математики обнаружили, что некоторые теоремы, которые Евклид считал само собой разумеющимися, на самом деле нельзя было доказать на основе его аксиом. Среди них - теорема о том, что прямая содержит как минимум две точки или что круги одного радиуса, центры которых разделены этим радиусом, должны пересекаться. Гильберт разработал полный набор аксиом геометрии , основываясь на предыдущей работе Паша. Успех аксиоматизации геометрии побудил Гильберта искать полную аксиоматизацию других областей математики, таких как натуральные числа и действительная прямая . Это могло стать основным направлением исследований в первой половине 20-го века.

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

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

20 век

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

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

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

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

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

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

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

Френкель доказал, что аксиома выбора не может быть доказана с помощью аксиом теории множеств Цермело с элементами . Более поздняя работа Пола Коэна показала, что добавление мочеточников не требуется, а аксиома выбора недоказуема в ZF. Доказательство Коэна развило метод принуждения , который теперь является важным инструментом для установления результатов независимости в теории множеств.

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

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

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

В 1931 году Гёдель опубликовал « Формально неразрешимые предложения принципов математики и связанных систем» , в котором доказал неполноту (в другом значении этого слова) всех достаточно сильных и эффективных теорий первого порядка. Этот результат, известный как теорема Гёделя о неполноте , устанавливает серьезные ограничения на аксиоматические основы математики, нанося сильный удар по программе Гильберта. Это показало невозможность предоставить доказательство непротиворечивости арифметики в рамках какой-либо формальной теории арифметики. Гильберт, однако, некоторое время не признавал важности теоремы о неполноте.

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

Первый учебник по символической логике для обывателя был написан Льюисом Кэрроллом, автором книги «Алиса в стране чудес», в 1896 году.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Последние разработки в области теории доказательств включают в себя изучение доказательств добычи по Ульриху Коленбаха и изучение доказательства теоретико-порядковых по Michael Rathjen .

Приложения

«Математическая логика успешно применяется не только к математике и ее основам ( Г. Фреге , Б. Рассел , Д. Гильберт , П. Бернейс , Х. Шольц , Р. Карнап , С. Лесневски , Т. Сколем ), но и к физике (Р. Карнап, А. Диттрих, Б. Рассел, К. Э. Шеннон , А. Н. Уайтхед , Х. Райхенбах , П. Февриер), к биологии ( Дж. Х. Вудгер , А. Тарски ), к психологии ( Ф. Б. Фитч , К. Г. Хемпель ) , закону и морали ( К. Менгер , У. Клуг, П. Оппенгейм), экономике ( Дж. Нойман , О. Моргенштерн ), практическим вопросам ( Э. К. Беркли , Э. Штамм) и даже метафизике (Дж. [Ян] Саламуча, Х. Шольц, Я. М. Боченски ). Его приложения к истории логики оказались чрезвычайно плодотворными ( Й. Лукасевич , Х. Шольц, Б. Матес , А. Беккер, Э. Муди , Дж. Саламуча, К. . Duerr, Z. Jordan, P. Boehner , JM Bochenski, S. [Stanislaw] T. Schayer, D. Ingalls ) ". «Также были сделаны приложения к богословию (Ф. Древновски, Дж. Саламуча, И. Томас)».

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

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

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

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

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

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

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

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

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

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

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

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

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

Примечания

использованная литература

Тексты для бакалавриата

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

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

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

Боченски, Юзеф Мария, изд. (1959). Точность математической логики . Synthese Library, Vol. 1. Перевод Отто Берда. Дордрехт : Спрингер . DOI : 10.1007 / 978-94-017-0592-9 . ISBN 9789048183296.

  • Бурали-Форти, Чезаре (1897). Вопрос о трансфинитных числах .Перепечатано в van Heijenoort 1976 , pp. 104–111.

Кантор, Георг (1874). "Ueber eine Eigenschaft des Inbegriffes Aller reellen algebraischen Zahlen" (PDF) . Journal für die Reine und Angewandte Mathematik . 1874 (77): 258–262. DOI : 10,1515 / crll.1874.77.258 . S2CID  199545885 . Кэрролл, Льюис (1896). Символическая логика . Kessinger Legacy Reprints. ISBN 9781163444955.

Соаре, Роберт Ирвинг (22 декабря 2011 г.). "Теория вычислимости и приложения: искусство классической вычислимости" (PDF) . Кафедра математики . Чикагский университет . Проверено 23 августа 2017 года . Свинсхед, Ричард (1498). Calculationes Suiseth Anglici (на литовском языке). Папи: Per Franciscum Gyrardengum.

внешние ссылки