Лекция
Привет, Вы узнаете о том , что такое математическая логика, Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое математическая логика, теоретическая логика, символическая логика, теория рекурсий, теория моделей , настоятельно рекомендую прочитать все из категории введение в математику. основы.
математическая логика ( теоретическая логика , символическая логика , устар. логистика ) — раздел математики, изучающий математические обозначения, формальные системы, доказуемость математических суждений, природу математического доказательства в целом, вычислимость и прочие аспекты оснований математики .
В более широком смысле рассматривается как математизированная ветвь формальной логики — «логика по предмету, математика по методу» , «логика, развиваемая с помощью математических методов»[.
Теории логики развивались во многих культурах истории, в том числе в Древнем Китае , Индии , Греции , Римской империи и исламском мире . Греческие методы, в частности аристотелевская логика (или терминологическая логика) , изложенная в « Органоне» , нашли широкое применение и признание в западной науке и математике на протяжении тысячелетий Стоики , особенно Хрисипп , начали разработку пропозициональной логики . В Европе XVIII века попытки трактовать операции формальной логики символическим или алгебраическим способом предпринимались философами-математиками, включая Лейбница и Ламберта , но их труды оставались изолированными и малоизвестными.
Первые попытки математизации логических операций были предприняты на рубеже XIII—XIV вв., Раймундом Луллием, сконструировавшим специальную «логическую машину» для механизации процесса логического вывода, которую он описал в своем трактате «Ars Magna» («Великое искусство»). Его машина состояла из семи концентрических кругов, на которых были обозначены термины и буквы. Для получения комбинаций Луллий использовал два концентрических круга, разделенных радиальными линиями на секторы. Вращая внутренний круг он получал таблицу различных комбинаций. Конечно эта попытка была несовершенной, но сыграла свою роль в дальнейшем развитии идеи математизации логических выводов.
Первое дошедшее до нас сочинение по формальной логике — «Первая Аналитика» Аристотеля (384—322 гг. до нашей эры). В нем рассматриваются основы силлогистики — правила вывода одних высказываний из других. Так из высказываний «Все люди смертны» и «Сократ — человек» можно сделать вывод, что «Сократ смертен». Однако на практике такие рассуждения встречаются крайне редко.
В середине XIX века Джордж Буль , а затем и Август де Морган представили систематическую математическую трактовку логики. Их работа, основанная на трудах таких алгебраистов, как Джордж Пикок , расширила традиционную аристотелевскую доктрину логики до достаточной основы для изучения оснований математики В 1847 году Ватрослав Бертич независимо от Буля проделал значительную работу по алгебраизации логики. Позже Чарльз Сандерс Пирс , опираясь на работу Буля, разработал логическую систему для отношений и кванторов, которую он опубликовал в нескольких статьях с 1870 по 1885 год.
Готлоб Фреге представил независимое развитие кванторной логики в своем труде «Begriffsschrift» , опубликованном в 1879 году, который обычно считается поворотным моментом в истории логики. Однако работа Фреге оставалась малоизвестной до тех пор, пока Бертран Рассел не начал ее пропагандировать на рубеже веков. Двумерная нотация, разработанная Фреге, так и не получила широкого распространения и не используется в современных ему текстах.
С 1890 по 1905 год Эрнст Шредер опубликовал трехтомный труд « Vorlesungen über die Algebra der Logik» . Этот труд обобщил и расширил работы Буля, де Моргана и Пирса и представлял собой исчерпывающее руководство по символической логике, как ее понимали в конце XIX века.
Вопрос о создании символической логики как универсального научного языка рассматривал Лейбниц в 1666 году в работе «Искусство комбинаторики» (De arte combinatoria). Он думал о записи высказываний на специальном языке, чтобы затем по логическим законам вычислять истинность других. В середине XIX века появились первые работы по алгебраизации аристотелевой логики, сформировавшие первооснову исчисления высказываний (Буль, де Морган, Шредер). В 1847 г. Дж. Буль опубликовал работу «The Mathematical Analysis of Logic» («Математический анализ логики»), а в 1854 г.— «An Investigation of the Laws of Thought» «Исследование законов мышления»). В них Буль изложил основы своей алгебры логики, где применил алгебраическую символику для записи логических операций и логических выводов. Булева алгебра логики в виде исчисления классов явилась первой системой математической логики. Основным результатом Булевой алгебры отмечается то, что теперь не ограничиваются применением символики к логике, а строят специальные логические исчисления; логические законы выступают в алгебре логики как необходимый момент формализованных систем; всякое суждение рассматривается как утверждение о равенстве классов; процесс умозаключения сводится к решению логических равенств. Однако, как отмечал Джевонс, операция вычитания в этой алгебре логики была не совсем удобной и иногда приводила к недоразумениям. Алгебру логики Буля усовершенствовали У. С. Джевонс и Э. Шредер. Сам Джевонс в книге «Чистая логика» критиковал излишнюю математизацию, алгебры логики Буля и предложил свою теорию, основанную на принципе замещения, то есть замене равного равным.
В 1877 году Шредер опубликовал книгу по математической логике «Der Operationskreis des Logikkalkuls», в которой систематически изложил основы математической логики. Большой вклад в развитие математической логики внес русский астроном, логик и математик, профессор Казанского университета П. С. Порецкий. Обобщив достижения Буля, Джевонса и Шредера, он на основе многолетних самостоятельных исследований создал содержательный труд «О способах решения логических равенств и об обратном способе математической логики», в котором значительно продвинул вперед разработку аппарата алгебры логики. Работы П. С. Порецкого превосходят не только труды его коллег — современников, но и в части, касающиеся алгебры логики превосходят соответствующие разделы Уайтхеда и Рассела. П. С. Порецкий первым в России начал читать лекции по математической логике. Математическая логика, говорил он, «по предмету своему есть логика, а по методу математика». Задачу математической логики он видел в «построении теории умозаключений», но при этом, точно определял связь и границу между математикой и математической логикой. "Если формы, изучаемые алгеброй, суть количественные, — писал он, — то, наоборот, те формы, с которыми имеет дело логика, суть качественные, то есть существенно отличные от первых. Это различие ближайших предметов изучения алгебры и логики делает невозможным прямое перенесение, то есть непосредственное применение, принципов и приемов алгебры к предмету логики. Однако приспособление этих приемов (с полным сохранением их точности) к изучению качественных форм вполне возможно. Большим вкладом П. С. Порецкого в математическую логику явилась предложенная им полная законченная теория качественных форм. Он разработал теорию логических равенств, предложил наиболее общий, исчерпывающий метод нахождения всех эквивалентных форм посылок, всех следствий из них, всех простейших неразложимых посылок, на которые может быть разложена система посылок.
В работах Фреге и Пирса (конец 1870-х — начало 1880-х) в логику введены предметные переменные, кванторы и, тем самым, основано исчисление предикатов. В 1879 году, в своей книге «Исчисление понятий», Фреге представил свою теорию исчисления высказываний, которая стала первым разделом современной математической логики. В ней Фреге представил первое аксиоматическое построение логики высказываний, ввел в математическую логику понятие квантора, которое затем уже Пирс вводит в обиход логической науки. Фреге также ввел понятие истинностного значения, предложил различать свойства и отношения как значения, соответственно, одноместных и многоместных пропозициональных функций. Но идеи Фреге не сразу нашли сторонников, а исчисления высказываний развивалось, как отмечает А.Черч, на основе более старой точки зрения, как это можно видеть в работах Пирса, Шредера и других.
В конце 1880-х годов Дедекинд и Пеано применили эти инструменты в попытках аксиоматизации арифметики, при этом Пеано создал удобную систему обозначений, закрепившуюся и в современной математической логике. Он ввел в математическую логику символы: ∈ — знак принадлежности множеству, ⊂ — знак включения, ⋃ — знак объединения, ∩ — знак пересечения множеств; разработал систему аксиом для арифметики натуральных чисел. Но главное, Пеано с помощью изобретенного им символического исчисления попытался исследовать основные математические понятия, что стало первым шагом практического применения математической логики к изучению основ математики. В своем пятитомном труде «Formulaire de Mathematiques» (1895—1905) Пеано показал, как с помощью символического исчисления можно аксиоматически построить математические дисциплины.
Опасения относительно того, что математика не имеет под собой прочной основы, привели к разработке аксиоматических систем для фундаментальных областей математики, таких как арифметика, анализ и геометрия.
В логике термин арифметика относится к теории натуральных чисел . Джузеппе Пеано опубликовал набор аксиом для арифметики, который стал носить его имя ( аксиомы Пеано ), используя вариацию логической системы Буля и Шредера, но добавив кванторы. Пеано в то время не знал о работе Фреге. Примерно в то же время Ричард Дедекинд показал, что натуральные числа однозначно характеризуются своими индукционными свойствами. Дедекинд предложил другую характеризацию, в которой отсутствовал формальный логический характер аксиом Пеано. Однако работа Дедекинда доказала теоремы, недоступные в системе Пеано, включая единственность множества натуральных чисел (с точностью до изоморфизма) и рекурсивные определения сложения и умножения из функции следования и математической индукции.
В середине 19-го века стали известны недостатки аксиом Евклида для геометрии. В дополнение к независимости постулата о параллельных , установленного Николаем Лобачевским в 1826 году, математики обнаружили, что некоторые теоремы, считавшиеся само собой разумеющимися Евклидом, на самом деле не доказуемы из его аксиом. Среди них — теорема о том, что прямая содержит по крайней мере две точки, или что окружности одинакового радиуса, центры которых разделены этим радиусом, должны пересекаться. Гильберт разработал полный набор аксиом для геометрии , основываясь на предыдущей работе Паша. Успех в аксиоматизации геометрии побудил Гильберта искать полную аксиоматизацию других областей математики, таких как натуральные числа и вещественная прямая . Это оказалось основной областью исследований в первой половине 20-го века.
XIX век стал свидетелем больших успехов в теории действительного анализа , включая теории сходимости функций и рядов Фурье . Математики, такие как Карл Вейерштрасс, начали строить функции, которые расширяли интуицию, такие как нигде не дифференцируемые непрерывные функции . Предыдущие концепции функции как правила для вычисления или гладкого графика больше не были адекватными. Вейерштрасс начал отстаивать арифметизацию анализа , которая стремилась аксиоматизировать анализ, используя свойства натуральных чисел. Современное (ε, δ)-определение предела и непрерывных функций было уже развито Больцано в 1817 году, но оставалось относительно неизвестным. Коши в 1821 году определил непрерывность в терминах бесконечно малых (см. Cours d'Analyse, стр. 34). В 1858 году Дедекинд предложил определение действительных чисел в терминах дедекиндовских сечений рациональных чисел, определение, которое все еще используется в современных текстах.
Георг Кантор разработал фундаментальные концепции теории бесконечных множеств. Его ранние результаты развили теорию мощности и доказали , что действительные и натуральные числа имеют разные мощности. В течение следующих двадцати лет Кантор разработал теорию трансфинитных чисел в серии публикаций. В 1891 году он опубликовал новое доказательство несчетности действительных чисел, которое ввело диагональный аргумент , и использовал этот метод для доказательства теоремы Кантора о том, что никакое множество не может иметь ту же мощность, что и его супермножество . Кантор считал, что любое множество может быть вполне упорядочено , но не смог предоставить доказательство этого результата, оставив его открытой проблемой в 1895 году.
В первые десятилетия XX века основными направлениями исследований были теория множеств и формальная логика. Обнаружение парадоксов в неформальной теории множеств заставило некоторых задуматься о противоречивости самой математики и искать доказательства ее непротиворечивости.
В 1900 году Гильберт сформулировал знаменитый список из 23 проблем, которые должны были решить в следующем столетии. Первые две из них касались, соответственно, подтверждения континуум-гипотезы и доказательства непротиворечивости элементарной арифметики; десятая заключалась в разработке метода, позволяющего определить, имеет ли решение многомерное полиномиальное уравнение над целыми числами . Об этом говорит сайт https://intellect.icu . Последующие работы по решению этих проблем определили направление развития математической логики, как и попытки решения Entscheidungsproblem Гильберта , поставленной в 1928 году. Эта проблема требовала процедуры, которая по заданному формализованному математическому утверждению определяла бы, является ли это утверждение истинным или ложным.
Уайтхед и Рассел создают в 1910—1913 годах трактат Principia Mathematica. Этот труд значительно способствовал развитию математической логики по пути дальнейшей аксиоматизации и формализации исчисления высказываний, классов и предикатов. Б. Рассел и А. Уайтхед выход из кризиса, в котором оказалась математика в связи с обнаружением парадоксов в теории множеств, видели в том, чтобы свести всю чистую математику к логике. Это была концепция логицизма. С этой целью они построили формализованную логико-математическую систему, в которой, по их утверждению, могут быть доказаны все содержательно истинные предложения. Но вскоре стало понятно, что попытка Б. Рассела и А. Уайтхеда свести всю чистую математику к логике не увенчалась успехом. В 1930—1931 годах К. Гедель установил, что не только разработанная Б. Расселом и А. Уайтхедом система, но и любая система формализованной математики является неполной, то есть не все содержательно истинные предложения могут быть в ней доказаны.
Свой выход из кризиса математики и дальнейшее развитии логики внесла концепция интуиционизма и интуиционистская логика (Брауэр, 1908). Математика, говорили они, это — математические конструкции. Математический объект существует, если известно, как его строить. Математик имеет дело с миром мысленных объектов, некоторые из них можно создать только в пределе за неограниченную последовательность шагов, никогда не завершающуюся и находящуюся в процессе постоянного становления. С точки зрения интуиционизма понятие актуальной, существующей бесконечности, которого придерживались представители теоретико-множественной концепции математики, является ошибочным. Поэтому интуиционистская логика исследует только конструктивные объекты, существование таких объектов считается доказанным в том и только в том случае, когда указывается конечный способ их построения. В этой логике отрицается применимость закона исключенного третьего в операциях с бесконечными множествами. Возникшая позднее конструктивная логика критически восприняла объективное содержание интуиционистской логики, и не приняла ее философско-методических основ.
Большую роль в развитии математической логики сыграла работа Гильберта и В. Аккермана «Основные черты теоретической логики» (1928 г.), изданная в России на русском языке под названием «Основы теоретической логики» в 1947 году, в которой была создана программа обоснования математики посредством аксиоматической формализации с использованием строго ограниченных средств, не приводящих к противоречиям. В своей работе они высказались о новом в математической логике: «Логические связи, которые существуют между суждениями, понятиями и т. д. — писали они, — находят свое выражение в формулах, толкование которых свободно от неясностей, какие легко могли бы возникнуть при словесном выражении. Переход к логическим следствиям, совершающийся посредством умозаключения, разлагается на свои последние элементы и представляется как формальное преобразование исходных формул по известным правилам, которые аналогичны правилам счета в алгебре; логическое мышление отображается в логическом исчислении. Это исчисление делает возможным успешный охват проблем, перед которыми принципиально бессильно чисто содержательное логическое мышление». Гильберт выступал против интуиционизма. Он возражал против того, что интуиционисты отрицали закон исключенного третьего в операциях с множествами. «Запрещение теорем существования и закона исключенного третьего — писал он, — равносильно полному отказу от математической науки». В своем методе формализации Гильберт предложил превратить всю математику в совокупность формул, в которых элементы связаны с помощью логических знаков. В фундаменте построения математики заложены некоторые определенные формулы, которые называются аксиомами. В качестве таких аксиом Гильберт взял аксиомы исчисления высказываний математической логики, математические аксиомы равенства и аксиомы числа, из которых он с помощью правил вывода получил новые, выводимые аксиомы. Вывод получался только на основании формы символов и знаков, за которыми не стояло никакого содержания. Формализованная теория по своей структуре представляла уже не систему осмысленных предложений, а систему символов, рассматриваемых как последовательность терминов. Основное требование, которое Гильберт предъявлял при определении понятия «существование» математического объекта сводилось к доказательству его непротиворечивости. Если в той или иной системе окажется, что в ней выводимо А и не-А, то такая система должна быть отвергнута. Гильберт и его школа пытались обосновать математику только аксиоматически, не выходя за пределы логики и математики.
В тридцатых и сороковых годах XX века начинается разработка металогики, предметом которой является исследование системы положений и понятий самой математической логики, которая определяет границы этой логики, изучает теорию доказательства. Основными разделами металогики являются логический синтез и логическая семантика, изучение значений выражения языка, интерпретаций логических исчислений. В металогических исследованиях уделяется анализу различных свойств формализованных языков, которые в дальнейшем легли в основу электронных машин для автоматизации научных умозаключений. В области логической семантики самыми значительными признаны работы А. Тарского «О понятии истины и формализованных языках» 1933 года, а также работы Р. Карнапа «Исследования по семантике» 1942—1947 года. Также важное значение в развитии математической логики имели работы в области многозначных логик, в которых высказываниям приписывается любое конечное или бесконечное множество значений истинности. Первую такую систему трехзначной логики высказываний разработал и предложил Я. Лукасевич. В 1954 году Я. Лукасевич предложил четырехзначную систему логики, и далее бесконечнозначную логику. Проблемами многозначной логики занимались также такие известные математики и логики как Э. Пост, С. Яськовский, Д. Вебб, А. Гейтинг, А. Н. Колмогоров, Д. А. Бочвар, В. И. Шестаков, Х. Рейхенбах, С. К. Клини и другие. Одним из крупнейших направлений в математической логике стала теория математических доказательств, которая возникла из применения логических исчислений к вопросам оснований математики. Она вышла из алгебры логики девятнадцатого века, предметом изучения которой были конечные объекты. Теория математических доказательств же занимается в основном проблемой бесконечности. Одной из главных задач математической логики, применяемых в математике исчислений, считается задача установления непротиворечивости, то есть считается, что исчисление непротиворечиво, если в нем нельзя вывести формулу А вместе с формулой Ā (не-А). С помощью метода формализации доказательств математическая логика помогла математике решить проблемы доказуемости и непротиворечивости в аксиоматических теориях. Преимущество математической логики состоит в том, что применяемый ею символический аппарат позволяет строго выразить самые сложные рассуждения, понятия для алгоритмической обработки вычислительными системами.
Эрнст Цермело доказал, что любое множество может быть вполне упорядочено , чего не смог получить Георг Кантор . Для доказательства Цермело ввел аксиому выбора , которая вызвала бурные споры и исследования среди математиков и пионеров теории множеств. Немедленная критика метода побудила Цермело опубликовать второе изложение своего результата, непосредственно отвечая на критику его доказательства. Эта статья привела к общему принятию аксиомы выбора в математическом сообществе.
Скептицизм относительно аксиомы выбора был усилен недавно обнаруженными парадоксами в наивной теории множеств . Чезаре Бурали-Форти был первым, кто сформулировал парадокс: парадокс Бурали-Форти показывает, что совокупность всех порядковых чисел не может образовать множество. Вскоре после этого, в 1901 году, Бертран Рассел открыл парадокс Рассела , а Жюль Ришар — парадокс Ришара .
Цермело предложил первый набор аксиом для теории множеств. Эти аксиомы, вместе с дополнительной аксиомой замены, предложенной Абрахамом Френкелем , теперь называются теорией множеств Цермело–Френкеля (ZF). Аксиомы Цермело включали принцип ограничения размера , чтобы избежать парадокса Рассела.
В 1910 году был опубликован первый том «Principia Mathematica» Рассела и Альфреда Норта Уайтхеда . В этой основополагающей работе теория функций и мощности была развита в полностью формальном контексте теории типов , разработанном Расселом и Уайтхедом в попытке избежать парадоксов. «Principia Mathematica» считается одним из самых влиятельных трудов XX века, хотя концепция теории типов не стала популярной в качестве основополагающей теории для математики.
Френкель доказал, что аксиома выбора не может быть доказана из аксиом теории множеств Цермело с праэлементами . Более поздние работы Пола Коэна показали, что добавление праэлементов не требуется, и аксиома выбора недоказуема в теории множеств Цермело. Доказательство Коэна развило метод принудительного принуждения , который в настоящее время является важным инструментом для установления независимости результатов в теории множеств.
Леопольд Левенгейм и Торальф Скулем получили теорему Левенгейма–Скулема , утверждающую, что логика первого порядка не может контролировать мощности бесконечных структур. Скулем понял, что эта теорема применима к формализаций теории множеств первого порядка и что из нее следует, что любая такая формализация имеет счетную модель . Этот контринтуитивный факт стал известен как парадокс Скулема .
Портрет молодого Курта Геделя , студента в Вене , 1925 г.
В своей докторской диссертации Курт Гедель доказал теорему о полноте , которая устанавливает соответствие между синтаксисом и семантикой в логике первого порядка Гедель использовал теорему о полноте для доказательства теоремы о компактности , демонстрируя финитную природу логического следования первого порядка . Эти результаты помогли утвердить логику первого порядка как доминирующую логику, используемую математиками.
В 1931 году Гедель опубликовал работу «О формально неразрешимых предложениях Principia Mathematica и родственных систем» , в которой была доказана неполнота (в ином смысле этого слова) всех достаточно сильных и эффективных теорий первого порядка. Этот результат, известный как теорема Геделя о неполноте , устанавливает серьезные ограничения на аксиоматические основания математики, нанося серьезный удар по программе Гильберта. Он показал невозможность предоставить доказательство непротиворечивости арифметики в рамках какой-либо формальной теории арифметики. Гильберт, однако, некоторое время не признавал важности теоремы о неполноте.
Теорема Геделя показывает, что доказательство непротиворечивости любой достаточно сильной и эффективной системы аксиом не может быть получено ни в самой системе, если она непротиворечива, ни в какой-либо более слабой системе. Это оставляет открытой возможность доказательств непротиворечивости, которые не могут быть формализованы в рамках рассматриваемой ими системы. Генцен доказал непротиворечивость арифметики, используя финитную систему вместе с принципом трансфинитной индукции . Результат Генцена ввел идеи устранения сечения и ординалов теории доказательств , которые стали ключевыми инструментами в теории доказательств. Гедель дал другое доказательство непротиворечивости, которое сводит непротиворечивость классической арифметики к непротиворечивости интуиционистской арифметики в высших типах.
Первый учебник по символической логике для неспециалистов был написан Льюисом Кэрроллом , автором « Приключений Алисы в Стране чудес» , в 1896 году.
Альфред Тарский разработал основы теории моделей .
Начиная с 1935 года группа выдающихся математиков под псевдонимом Николя Бурбаки совместно опубликовала «Элементы математики» – серию энциклопедических математических текстов. Эти тексты, написанные в строгом аксиоматическом стиле, делали акцент на строгом изложении и теоретико-множественных основах. Терминология, созданная в этих текстах, такая как «биекция» , «инъекция» и «сюръекция» , а также используемые в них теоретико-множественные основы, получили широкое распространение в математике.
Изучение вычислимости стало известно как теория рекурсии или теория вычислимости , поскольку ранние формализации Геделя и Клини опирались на рекурсивные определения функций. Когда было показано, что эти определения эквивалентны формализации Тьюринга, включающей машины Тьюринга , стало ясно, что было открыто новое понятие — вычислимая функция — и что это определение достаточно надежно, чтобы допускать многочисленные независимые характеризации. В своей работе над теоремами о неполноте в 1931 году Геделю не хватало строгой концепции эффективной формальной системы; он сразу понял, что новые определения вычислимости могут быть использованы для этой цели, позволяя ему сформулировать теоремы о неполноте в общности, которая могла подразумеваться только в исходной статье.
Многочисленные результаты в теории рекурсии были получены в 1940-х годах Стивеном Коулом Клини и Эмилем Леоном Постом . Клини ввел понятия относительной вычислимости, предвосхищенные Тьюрингом, и арифметической иерархии . Позже Клини обобщил теорию рекурсии на функционалы более высокого порядка. Клини и Георг Крайзель изучали формальные версии интуиционистской математики, особенно в контексте теории доказательств.
Математическая логика, так же как и традиционная логика, формальная в том смысле, что она абстрагируется от значения и судит о взаимосвязи, отношениях и переходах от одного предложения (высказывания) к другому и получающемся в итоге выводе из этих предложений не на основании содержания их, а только на основании формы последовательности предложений.
Применение в логике математических методов становится возможным тогда, когда суждения формулируются на некотором точном языке. Такие точные языки имеют две стороны: синтаксис и семантику. Синтаксисом называется совокупность правил построения объектов языка (обычно называемых формулами). Семантикой называется совокупность соглашений, описывающих наше понимание формул (или некоторых из них) и позволяющих считать одни формулы верными, а другие — нет.
Важную роль в математической логике играют понятия дедуктивной теории и исчисления. Исчислением называется совокупность правил вывода, позволяющих считать некоторые формулы выводимыми. Правила вывода подразделяются на два класса. Одни из них непосредственно квалифицируют некоторые формулы как выводимые. Такие правила вывода принято называть аксиомами. Другие же позволяют считать выводимыми формулы A , синтаксически связанные некоторым заранее определенным способом с конечными наборами A1,…An выводимых формул. Широко применяемым правилом второго типа является правило modus ponens: если выводимы формулы A и (A→B) , то выводима и формула B .
Отношение исчислений к семантике выражается понятиями семантической пригодности и семантической полноты исчисления. Исчисление И называется семантически пригодным для языка Я , если любая выводимая в И формула языка Я является верной. Аналогично, исчисление И называется семантически полным в языке Я , если любая верная формула языка Я выводима в И .
Многие из рассматриваемых в математической логике языков обладают семантически полными и семантически пригодными исчислениями. В частности, известен результат Курта Геделя о том, что классическое исчисление предикатов является семантически полным и семантически пригодным для языка классической логики предикатов первого порядка (теорема Геделя о полноте). С другой стороны, имеется немало языков, для которых построение семантически полного и семантически пригодного исчисления невозможно. В этой области классическим результатом является теорема Геделя о неполноте, утверждающая невозможность семантически полного и семантически пригодного исчисления для языка формальной арифметики. С другой стороны в 1936 году Герхард Генцен доказал полноту и непротиворечивость арифметики, используя примитивно рекурсивную арифметику с дополнительной аксиомой для трансфинитной индукции до ординала ε0.
На практике множество элементарных логических операций является обязательной частью набора инструкций всех современных микропроцессоров и, соответственно, входит в языки программирования. Это является одним из важнейших практических приложений методов математической логики, изучаемых в современных учебниках информатики.
В Математической предметной классификации математическая логика объединена в одну секцию верхнего уровня с основаниями математики, в которой выделены следующие разделы:
Теория множеств — это изучение множеств , которые являются абстрактными коллекциями объектов. Многие из основных понятий, таких как порядковые и кардинальные числа, были неформально разработаны Кантором до того, как были разработаны формальные аксиоматизации теории множеств. Первая такая аксиоматизация , предложенная Цермело, [ 23 ] была немного расширена и стала теорией множеств Цермело–Френкеля (ZF), которая в настоящее время является наиболее широко используемой фундаментальной теорией для математики.
Были предложены и другие формализации теории множеств, включая теорию множеств фон Неймана–Бернейса–Геделя (NBG), теорию множеств Морса–Келли (MK) и Новые основания (NF). Из них ZF, NBG и MK схожи в описании кумулятивной иерархии множеств. Новые основания используют другой подход; они допускают такие объекты, как множество всех множеств, за счет ограничений на аксиомы существования множества. Система теории множеств Крипке–Платека тесно связана с обобщенной теорией рекурсии.
Два известных утверждения в теории множеств — аксиома выбора и гипотеза континуума . Аксиома выбора, впервые сформулированная Цермело [ 19 ], была доказана независимо от ZF Френкелем [ 25 ] , но стала широко принятой математиками. Она гласит, что для данного набора непустых множеств существует единственное множество C , которое содержит ровно один элемент из каждого набора в наборе. Говорят, что множество C «выбирает» один элемент из каждого набора в наборе. Хотя возможность сделать такой выбор некоторые считают очевидной, поскольку каждое множество в наборе непусто, отсутствие общего, конкретного правила, по которому можно сделать выбор, делает аксиому неконструктивной. Стефан Банах и Альфред Тарский показали, что аксиому выбора можно использовать для разложения сплошного шара на конечное число частей, которые затем можно переставить без масштабирования, чтобы сделать два сплошных шара исходного размера. [ 40 ] Эта теорема, известная как парадокс Банаха-Тарского , является одним из многих контринтуитивных результатов аксиомы выбора.
Гипотеза континуума, впервые предложенная как гипотеза Кантором, была указана Дэвидом Гильбертом как одна из его 23 проблем в 1900 году. Гедель показал, что гипотеза континуума не может быть опровергнута из аксиом теории множеств Цермело–Френкеля (с аксиомой выбора или без нее), путем разработки конструируемой вселенной теории множеств, в которой гипотеза континуума должна быть верна. В 1963 году Пол Коэн показал, что гипотеза континуума не может быть доказана из аксиом теории множеств Цермело–Френкеля. [ 26 ] Однако этот результат о независимости не полностью разрешил вопрос Гильберта, поскольку возможно, что новые аксиомы для теории множеств могли бы разрешить гипотезу. Недавняя работа в этом направлении была проведена У. Хью Вудином , хотя ее важность пока не ясна. [ 41 ]
Современные исследования в теории множеств включают изучение больших кардиналов и определенности . Большие кардиналы — это кардинальные числа с особыми свойствами, настолько сильными, что существование таких кардиналов не может быть доказано в ZFC. Существование наименьшего большого кардинала, обычно изучаемого, недостижимого кардинала , уже подразумевает согласованность ZFC. Несмотря на то, что большие кардиналы имеют чрезвычайно высокую мощность , их существование имеет много последствий для структуры действительной линии. Определенность относится к возможному существованию выигрышных стратегий для определенных игр двух игроков (игры считаются определенными ). Существование этих стратегий подразумевает структурные свойства действительной линии и других польских пространств .
Теория моделей изучает модели различных формальных теорий. Здесь теория — это набор формул в определенной формальной логике и сигнатуре , тогда как модель — это структура, которая дает конкретную интерпретацию теории. Теория моделей тесно связана с универсальной алгеброй и алгебраической геометрией , хотя методы теории моделей больше сосредоточены на логических соображениях, чем на этих областях.
Совокупность всех моделей конкретной теории называется элементарным классом ; классическая теория моделей стремится определить свойства моделей в конкретном элементарном классе или определить, образуют ли определенные классы структур элементарные классы.
Метод исключения кванторов может быть использован для того, чтобы показать, что определимые множества в конкретных теориях не могут быть слишком сложными. Тарский установил исключение кванторов для вещественно-замкнутых полей , результат, который также показывает, что теория поля вещественных чисел разрешима Он также отметил, что его методы в равной степени применимы к алгебраически замкнутым полям произвольной характеристики. Современная подобласть, развивающаяся из этого, занимается o-минимальными структурами .
Теорема Морли о категоричности , доказанная Майклом Д. Морли , утверждает, что если теория первого порядка в счетном языке категорична в некоторой несчетной мощности, т. е. все модели этой мощности изоморфны, то она категорична во всех несчетных мощностях.
Тривиальным следствием гипотезы континуума является то, что полная теория с меньшим, чем континуум, числом неизоморфных счетных моделей может иметь только счетное число. Гипотеза Воота , названная в честь Роберта Лоусона Воота , утверждает, что это верно даже независимо от гипотезы континуума. Было установлено много частных случаев этой гипотезы.
Теория рекурсии , также называемая теорией вычислимости , изучает свойства вычислимых функций и степеней Тьюринга , которые делят невычислимые функции на множества, имеющие одинаковый уровень невычислимости. Теория рекурсии также включает изучение обобщенной вычислимости и определимости. Теория рекурсии выросла из работы Рожи Петера , Алонзо Черча и Алана Тьюринга в 1930-х годах, которая была значительно расширена Клини и Постом в 1940-х годах.
Классическая теория рекурсии фокусируется на вычислимости функций от натуральных чисел до натуральных чисел. Фундаментальные результаты устанавливают надежный канонический класс вычислимых функций с многочисленными независимыми эквивалентными характеризациями с использованием машин Тьюринга , λ-исчисления и других систем. Более продвинутые результаты касаются структуры степеней Тьюринга и решетки рекурсивно перечислимых множеств .
Обобщенная теория рекурсии расширяет идеи теории рекурсии на вычисления, которые больше не обязательно являются конечными. Она включает в себя изучение вычислимости в высших типах, а также такие области, как гиперарифметическая теория и теория α-рекурсии .
Современные исследования в области теории рекурсии включают изучение таких приложений, как алгоритмическая случайность , теория вычислимых моделей и обратная математика , а также новых результатов в чистой теории рекурсии.
Важная подобласть теории рекурсии изучает алгоритмическую неразрешимость; проблема принятия решений или проблема функций алгоритмически неразрешима , если не существует возможного вычислимого алгоритма, который возвращает правильный ответ для всех допустимых входных данных задачи. Первые результаты о неразрешимости, полученные независимо Черчем и Тьюрингом в 1936 году, показали, что Entscheidungsproblem алгоритмически неразрешима. Тьюринг доказал это, установив неразрешимость проблемы остановки , что имело далеко идущие последствия как для теории рекурсии, так и для компьютерной науки.
Существует множество известных примеров неразрешимых проблем из обычной математики. Алгоритмическая неразрешимость проблемы поиска слов для групп была доказана Петром Новиковым в 1955 году и независимо У. Буном в 1959 году. Задача о занятом бобре , разработанная Тибором Радо в 1962 году, является еще одним известным примером.
Десятая проблема Гильберта требовала алгоритма для определения того, имеет ли многомерное полиномиальное уравнение с целыми коэффициентами решение в целых числах. Частичный прогресс был достигнут Джулией Робинсон , Мартином Дэвисом и Хилари Патнэмом . Алгоритмическая неразрешимость проблемы была доказана Юрием Матиясевичем в 1970 году
Теория доказательств — это изучение формальных доказательств в различных системах логического вывода. Эти доказательства представляются как формальные математические объекты, что облегчает их анализ математическими методами. Обычно рассматриваются несколько систем вывода, включая системы вывода в стиле Гильберта , системы естественного вывода и секвенциальное исчисление , разработанное Генценом.
Изучение конструктивной математики в контексте математической логики включает изучение систем неклассической логики, таких как интуиционистская логика, а также изучение предикативных систем. Одним из первых сторонников предикативизма был Герман Вейль , который показал, что можно развить большую часть реального анализа, используя только предикативные методы.
Поскольку доказательства полностью конечны, тогда как истина в структуре не является таковой, в конструктивной математике принято подчеркивать доказуемость. Связь между доказуемостью в классических (или неконструктивных) системах и доказуемостью в интуиционистских (или конструктивных, соответственно) системах представляет особый интерес. Такие результаты, как отрицательный перевод Геделя–Гентцена, показывают, что можно встроить (или перевести ) классическую логику в интуиционистскую логику, что позволяет перенести некоторые свойства интуиционистских доказательств обратно в классические доказательства.
Последние разработки в теории доказательств включают исследование добычи доказательств Ульрихом Коленбахом и исследование ординалов теории доказательств Михаэлем Ратьеном .
Модальные логики включают в себя дополнительные модальные операторы, например, оператор, утверждающий, что определенная формула не просто истинна, но и обязательно истинна. Хотя модальная логика нечасто используется для аксиоматизации математики, она применялась для изучения свойств доказуемости первого порядка и теоретико-множественного форсинга.
Интуиционистская логика была разработана Гейтингом для изучения программы интуиционизма Брауэра, в которой сам Брауэр избегал формализации. Интуиционистская логика, в частности, не включает закон исключенного третьего , который гласит, что каждое предложение либо истинно, либо его отрицание истинно. Работа Клини с теорией доказательств интуиционистской логики показала, что конструктивная информация может быть извлечена из интуиционистских доказательств. Например, любая доказуемо полная функция в интуиционистской арифметике вычислима ; это неверно в классических теориях арифметики, таких как арифметика Пеано .
Алгебраическая логика использует методы абстрактной алгебры для изучения семантики формальных логик. Фундаментальным примером служит использование булевых алгебр для представления истинностных значений в классической пропозициональной логике и использование гейтинговых алгебр для представления истинностных значений в интуиционистской пропозициональной логике. Более сильные логики, такие как логика первого порядка и логика высшего порядка, изучаются с использованием более сложных алгебраических структур, таких как цилиндрические алгебры .
Логика первого порядка — это особая формальная система логики . Ее синтаксис включает только конечные выражения в виде правильно построенных формул , тогда как ее семантика характеризуется ограничением всех кванторов фиксированной областью дискурса .
Ранние результаты формальной логики выявили ограничения логики первого порядка. Теорема Левенгейма–Сколема (1919) показала, что если множество предложений счетного языка первого порядка имеет бесконечную модель, то у него существует по крайней мере одна модель каждой бесконечной мощности. Это показывает, что множество аксиом первого порядка не может описывать натуральные числа, действительные числа или любую другую бесконечную структуру с точностью до изоморфизма . Поскольку целью ранних фундаментальных исследований было создание аксиоматических теорий для всех разделов математики, это ограничение было особенно существенным.
Теорема Геделя о полноте установила эквивалентность между семантическими и синтаксическими определениями логического следствия в логике первого порядка. Она показывает, что если конкретное предложение истинно в каждой модели, которая удовлетворяет конкретному набору аксиом, то должен быть конечный вывод предложения из аксиом. Теорема о компактности впервые появилась как лемма в доказательстве Геделя теоремы о полноте, и прошло много лет, прежде чем логики поняли ее значение и начали применять ее повседневно. Она гласит, что набор предложений имеет модель тогда и только тогда, когда каждое конечное подмножество имеет модель, или, другими словами, что противоречивый набор формул должен иметь конечное противоречивое подмножество. Теоремы о полноте и компактности позволяют проводить сложный анализ логического следствия в логике первого порядка и развивать теорию моделей , и они являются ключевой причиной известности логики первого порядка в математике.
Теоремы Геделя о неполноте устанавливают дополнительные ограничения на аксиоматизации первого порядка. Первая теорема о неполноте утверждает, что для любой непротиворечивой, эффективно заданной (определенной ниже) логической системы, способной интерпретировать арифметику, существует утверждение, которое является истинным (в том смысле, что оно верно для натуральных чисел), но недоказуемым в рамках этой логической системы (и которое действительно может быть неверным в некоторых нестандартных моделях арифметики , которые могут быть совместимы с этой логической системой). Например, в каждой логической системе, способной выразить аксиомы Пеано , утверждение Геделя верно для натуральных чисел, но не может быть доказано.
Здесь говорят, что логическая система эффективно задана, если по любой формуле на языке этой системы можно определить, является ли она аксиомой, а формула, выражающая аксиомы Пеано, называется «достаточно сильной». Применительно к логике первого порядка первая теорема о неполноте подразумевает, что любая достаточно сильная, непротиворечивая и эффективная теория первого порядка имеет модели, которые элементарно не эквивалентны , что является более сильным ограничением, чем установленное теоремой Левенгейма–Скулема. Вторая теорема о неполноте утверждает, что никакая достаточно сильная, непротиворечивая и эффективная система арифметических аксиом не может доказать свою собственную непротиворечивость, что было интерпретировано как доказательство недостижимости программы Гильберта .
Изучение теории вычислимости в информатике тесно связано с изучением вычислимости в математической логике. Однако есть разница в акцентах. Специалисты по информатике часто фокусируются на конкретных языках программирования и возможной вычислимости , в то время как исследователи в математической логике часто фокусируются на вычислимости как теоретической концепции и на невычислимости.
Теория семантики языков программирования связана с теорией моделей , как и верификация программ (в частности, проверка моделей ). Соответствие Карри–Ховарда между доказательствами и программами связано с теорией доказательств , особенно с интуиционистской логикой . Формальные исчисления, такие как лямбда-исчисление и комбинаторная логика, в настоящее время изучаются как идеализированные языки программирования .
Информатика также вносит вклад в математику, разрабатывая методы автоматической проверки или даже поиска доказательств, такие как автоматизированное доказательство теорем и логическое программирование .
Теория описательной сложности связывает логику с вычислительной сложностью . Первый значительный результат в этой области, теорема Фейгина (1974), установила, что NP — это в точности множество языков, выражаемых предложениями экзистенциальной логики второго порядка .
Исследование, описанное в статье про математическая логика, подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое математическая логика, теоретическая логика, символическая логика, теория рекурсий, теория моделей и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории введение в математику. основы
Ответы на вопросы для самопроверки пишите в комментариях, мы проверим, или же задавайте свой вопрос по данной теме.
Комментарии
Оставить комментарий
введение в математику. основы
Термины: введение в математику. основы