В классической дедуктивной логике , последовательная теория является тот , который не приводит к логическому противоречию . [1] Отсутствие противоречия можно определить семантическим или синтаксическим языком. Семантическое определение гласит, что теория непротиворечива, если у нее есть модель , т. Е. Существует интерпретация, при которой все формулы в теории истинны. В этом смысле используется традиционная аристотелевская логика , хотя в современной математической логике вместо этого используется термин « выполнимый» . Синтаксическое определение утверждает теориюнепротиворечиво, если нет формулы так что оба и его отрицание являются элементами совокупности последствий . Позволятьбыть набором закрытых предложений (неформально «аксиом») и множество закрытых предложений доказуемо из при некоторой (указанной, возможно, неявно) формальной дедуктивной системе. Набор аксиомявляется последовательным , если без формулы . [2]
Если существует дедуктивная система, для которой эти семантические и синтаксические определения эквивалентны любой теории, сформулированной в определенной дедуктивной логике , такая логика называется полной . [ Править ] Полнота сентенционного исчисления была доказана Павла Бернайсом в 1918 году [ править ] [3] и Эмилю сообщение в 1921 году [4] , а полнота исчисления предикатов была доказана Курта Геделя в 1930 году [5] и доказательства непротиворечивости арифметики, ограниченной по схеме аксиом индукции, были доказаны Аккерманом (1924), фон Нейманом (1927) и Хербрандом (1931). [6] Более строгие логики, такие как логика второго порядка , неполны.
Доказательство непротиворечивости является математическим доказательством , что конкретная теория непротиворечива. [7] Раннее развитие математической теории доказательств было вызвано желанием предоставить доказательства конечной непротиворечивости для всей математики как часть программы Гильберта . На программу Гильберта сильно повлияли теоремы о неполноте , которые показали, что достаточно сильные теории доказательства не могут доказать свою собственную непротиворечивость (при условии, что они на самом деле непротиворечивы).
Хотя согласованность может быть доказана с помощью теории моделей, это часто делается чисто синтаксическим путем, без необходимости ссылаться на какую-либо модель логики. Вырез устранение (или , что эквивалентна нормализация из базового исчисления , если есть один) означает последовательность исчисления: так как нет разреза свободного доказательства ложности, нет никакого противоречия в целом.
Последовательность и полнота в арифметике и теории множеств
В теориях арифметики, таких как арифметика Пеано , существует сложная взаимосвязь между последовательностью теории и ее полнотой . Теория считается полной, если для каждой формулы φ на ее языке хотя бы одно из φ или ¬φ является логическим следствием теории.
Арифметика Пресбургера - это система аксиом для сложения натуральных чисел. Оно одновременно последовательное и полное.
Теоремы Гёделя о неполноте показывают, что любая достаточно сильная рекурсивно перечислимая теория арифметики не может быть одновременно полной и непротиворечивой. Теорема Гёделя применима к теориям арифметики Пеано (PA) и примитивно-рекурсивной арифметике (PRA), но не к арифметике Пресбургера .
Более того, вторая теорема Гёделя о неполноте показывает, что непротиворечивость достаточно сильных рекурсивно перечислимых теорий арифметики может быть проверена определенным образом. Такая теория непротиворечива тогда и только тогда, когда она не доказывает конкретное предложение, называемое гёделевским предложением теории, которое является формализованным заявлением о том, что теория действительно непротиворечива. Таким образом, непротиворечивость достаточно сильной, рекурсивно перечислимой и непротиворечивой теории арифметики никогда не может быть доказана в самой этой системе. Тот же результат верен для рекурсивно перечислимых теорий, которые могут описывать достаточно сильный фрагмент арифметики, включая теории множеств, такие как теория множеств Цермело – Френкеля (ZF). Эти теории множеств не могут доказать свое собственное предложение Гёделя - при условии, что они непротиворечивы, как принято считать.
Поскольку непротиворечивость ZF недоказуема в ZF, более слабое понятие относительная согласованность интересна в теории множеств (и в других достаточно выразительных аксиоматических системах). ЕслиT-теория,аA- дополнительнаяаксиома,T+Aназывается согласованным относительноT(или просто, чтоAсогласовано сT), если можно доказать, что еслиTсогласован, тоT+Aсогласован. Если обаи ¬согласуются сТ, тоназываетсянезависимымотТ.
Логика первого порядка
Обозначение
(Символ турникета) в следующем контексте математической логики означает «доказуемо из». Это,гласит: b можно доказать из a (в некоторой указанной формальной системе). См. Список логических символов . В остальных случаях символ турникета может означать подразумевает; позволяет получить. См .: Список математических символов .
Определение
- Набор формул в логике первого порядка согласован (написано) если нет формулы такой, что а также . Иначеявляется несовместимым (написано).
- называется просто непротиворечивым, если для какой-либо формулы из , оба и отрицание из теоремы . [ требуется разъяснение ]
- считается абсолютно непротиворечивым или непротиворечивым, если хотя бы одна формула на языке это не теорема .
- называется максимально согласованным, если для каждой формулы, если подразумевает .
- как говорят, содержит свидетелей, если для каждой формулы видасуществует термин такой, что , где обозначает замену каждого в автор ; см. также Логику первого порядка . [ необходима цитата ]
Основные результаты
- Следующие варианты эквивалентны:
- Для всех
- Каждый выполнимый набор формул согласован, где набор формул выполнимо тогда и только тогда, когда существует модель такой, что .
- Для всех а также :
- если не , тогда ;
- если а также , тогда ;
- если , тогда или же .
- Позволять - максимально непротиворечивый набор формул, и пусть он содержит свидетелей . Для всех а также :
- если , тогда ,
- либо или же ,
- если и только если или же ,
- если а также , тогда ,
- если и только если есть срок такой, что . [ необходима цитата ]
Теорема Хенкина
Позволять быть набором символов . Позволять быть максимально согласованным набором -формулы, содержащие свидетелей .
Определите отношение эквивалентности на съемках - термины если , где обозначает равенство . Позволятьобозначим класс эквивалентности терминов, содержащих; и разреши где набор терминов, основанный на наборе символов .
Определите - структура над , также называемый термоструктурой, соответствующей, от:
- для каждого символ -арное отношение , определять если [8]
- для каждого символ функции , определять
- для каждого постоянного символа , определять
Определить присвоение переменной от для каждой переменной . Позволятьбыть термином интерпретация, связанная с.
Тогда для каждого -формула :
если и только если [ необходима цитата ]
Эскиз доказательства
Есть несколько вещей, которые нужно проверить. Во-первых, этофактически является отношением эквивалентности. Затем необходимо проверить, что (1), (2) и (3) правильно определены. Это выпадает из того факта, что является отношением эквивалентности и также требует доказательства того, что (1) и (2) не зависят от выбора представители класса. Ну наконец то, проверяется индукцией по формулам.
Теория моделей
В теории множеств ZFC с классической логикой первого порядка , [9] несовместимая теория один такой, что существует закрытое предложение такой, что содержит оба и его отрицание . Последовательная теория является одним из такой , что следующие логически эквивалентных условий
- [10]
Смотрите также
- Когнитивный диссонанс
- Равносогласованность
- Проблемы Гильберта
- Вторая проблема Гильберта
- Ян Лукасевич
- Паранепротиворечивая логика
- ω-согласованность
- Доказательство непротиворечивости Гентцена
- Доказательство от противного
Сноски
- ^ Тарский 1946 утверждает это так: «Дедуктивная теория называется непротиворечивой или непротиворечивой, если никакие два утвержденных утверждения этой теории не противоречат друг другу, или, другими словами, если из любых двух противоречащих предложений… по крайней мере одно не может быть доказано, (стр. 135), где Тарский определяет противоречивое следующим образом: «С помощью слова ни одно из них не отрицает ни одно предложение; два предложения, из которых первое является отрицанием второго, называются противоречивыми предложениями » (стр. . 20). Это определение требует понятия «доказательство». Гёдель 1931 определяет это понятие следующим образом: «Класс доказуемых формул определяется как наименьший класс формул, содержащий аксиомы и замкнутый по отношению« немедленное следствие », т. е. формула c для a и b определяется как непосредственное следствие в терминах modus ponens или замещения; ср. Gödel 1931 , ван Хейеноорт 1967 , стр. 601. Тарский неформально определяет «доказательство» как «утверждения следуют одно за другим в определенном порядке в соответствии с определенными принципами… и сопровождаются соображениями, призванными установить их достоверность [истинный вывод для всех истинных посылок - Reichenbach 1947 , стр. 68]» см. Тарский 1946 , стр. 3. Kleene 1952 определяет понятие относительно индукции или перефразирования) конечной последовательности формул, так что каждая формула в последовательности является либо аксиомой, либо «непосредственным следствием» предыдущих формул; «А Доказательство называется доказательством из его последней формулы, и эта формула называется (формально) доказуемо или быть (формальная) теорема» сравни Клини 1952 , стр. 83.
- ^ Ходжес, Уилфрид (1997). Более короткая модельная теория . Нью-Йорк: Издательство Кембриджского университета. п. 37.
Пусть быть подписью, теория в а также предложение в . Мы говорим чтоявляется следствием из, или это влечет за собой , в символах , если каждая модель модель . (В частности, если нет моделей тогда влечет за собой .)
(Обратите внимание на определение Mod (T) на стр.30 ...)
Предупреждение : мы не требуем этого, если тогда есть доказательство из . В любом случае, с бесконечными языками не всегда ясно, что будет доказательством. Некоторые писатели используют иметь в виду, что выводится из в некотором конкретном формальном исчислении доказательств, и они пишут для нашего понятия следствия (обозначение, которое противоречит нашему ). Для логики первого порядка два вида вывода совпадают по теореме о полноте рассматриваемого исчисления доказательств.
Мы говорим чтоявляется действительным , или это логическая теорема , в символах, если верно в каждом -состав. Мы говорим чтоявляется последовательным , если верно в некоторых -состав. Точно так же мы говорим, что теорияявляется последовательным , если она имеет модель.
Мы говорим, что две теории S и T в L infinity omega эквивалентны, если они имеют одинаковые модели, т.е. если Mod (S) = Mod (T). - ^ Хейенорт 1967 , стр. 265 заявляет, что Бернейс определил независимость аксиом Principia Mathematica , результат не публиковался до 1926 года, но он ничего не говорит о том, что Бернейс доказал их непротиворечивость .
- ^ Пост доказывает как непротиворечивость, так и полноту исчисления высказываний PM, см. Комментарий ван Хейеноорта и Введение Поста 1931 года в общую теорию элементарных предложений в van Heijenoort 1967 , стр. 264ff. Также Тарский 1946 , стр. 134 и далее.
- ^ см. комментарий ван Хейенорта и Гёделя 1930 г. Полнота аксиом функционального исчисления логики у ван Хейенорта 1967 г. , стр. 582ff.
- ^ см. комментарий ван Хейеноорта и работу Хербрана 1930 г. « О непротиворечивости арифметики» у ван Хейенурта 1967 г. , стр. 618 и далее.
- ^ Неформально обычно предполагается теория множеств Цермело – Френкеля; некоторые диалекты неформальной математики обычно дополнительно предполагают аксиому выбора .
- ^ Это определение не зависит от выбора из-за свойств заместительности и максимальная согласованность .
- ^ общий случай во многих приложениях к другим областям математики, а также обычный способ рассуждений неформальной математики в исчислении и приложениях к физике, химии, технике
- ^ согласно законам Де Моргана
Рекомендации
- Клини, Стивен (1952). Введение в метаматематику . Нью-Йорк: Северная Голландия. ISBN 0-7204-2103-9. 10-е впечатление 1991 г.
- Райхенбах, Ганс (1947). Элементы символической логики . Нью-Йорк: Дувр. ISBN 0-486-24004-5.
- Тарский, Альфред (1946). Введение в логику и методологию дедуктивных наук (второе изд.). Нью-Йорк: Дувр. ISBN 0-486-28462-X.
- ван Хейеноорт, Жан (1967). От Фреге до Гёделя: Справочник по математической логике . Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 0-674-32449-8. (pbk.)
- "Последовательность". Кембриджский философский словарь .
- Эббингаус, HD; Flum, J .; Томас, В. Математическая логика .
- Джевонс, WS (1870). Элементарные уроки логики .
Внешние ссылки
- Мортенсен, Крис. «Непоследовательная математика» . Стэнфордская энциклопедия философии .