Последовательность

В классической дедуктивной логике непротиворечивой , является теория которая не приводит к логическому противоречию . ^[1]Отсутствие противоречия можно определить как в семантическом , так и в синтаксическом плане. Семантическое определение гласит, что теория непротиворечива, если она имеет модель , т. е. существует интерпретация , при которой все формулы теории истинны. Этот смысл используется в традиционной аристотелевской логике термин «выполнимый» , хотя в современной математической логике вместо этого используется . Синтаксическое определение формулирует теорию $T$ является непротиворечивым, если нет формулы $\varphi$ такой, что оба $\varphi$ и его отрицание $\lnot \varphi$ являются элементами совокупности последствий $T$ . Позволять $A$ быть набором закрытых предложений (неформально «аксиом») и $\langle A\rangle$ множество закрытых предложений, доказуемых из $A$ в рамках некоторой (определенной, возможно неявной) формальной дедуктивной системы. Набор аксиом $A$ является непротиворечивым , когда нет формулы $\varphi$ такой, что $\varphi \in \langle A\rangle$ и $\lnot \varphi \in \langle A\rangle$ . ^[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 непротиворечив. Если и A , и ¬A согласуются с T , то не говорят, что зависит от T. A

Логика первого порядка [ править ]

Обозначения [ править ]

В следующем контексте математической логики турникета символ $\vdash$ означает «доказуемый из». То есть, $a\vdash b$ гласит: b доказуемо из a (в некоторой заданной формальной системе).

Определение [ править ]

Набор формул $\Phi$ в логике первого порядка непротиворечива (записывается $\operatorname {Con} \Phi$ ) если нет формулы $\varphi$ такой, что $\Phi \vdash \varphi$ и $\Phi \vdash \lnot \varphi$ . В противном случае $\Phi$ противоречиво написано ( $\operatorname {Inc} \Phi$ ).
$\Phi$ называется просто непротиворечивым, если ни для одной формулы $\varphi$ из $\Phi$ , оба $\varphi$ и отрицание $\varphi$ являются теоремами $\Phi$ . ^{[ нужны разъяснения ]}
$\Phi$ называется абсолютно непротиворечивым или непротиворечивым по Посту, если хотя бы одна формула на языке $\Phi$ это не теорема $\Phi$ .
$\Phi$ называется максимально совместным , если $\Phi$ является последовательным и для каждой формулы $\varphi$ , $\operatorname {Con} (\Phi \cup \{\varphi \})$ подразумевает $\varphi \in \Phi$ .
$\Phi$ Говорят, что он содержит свидетелей , если для каждой формулы вида $\exists x\,\varphi$ существует термин $t$ такой, что $(\exists x\,\varphi \to \varphi {t \over x})\in \Phi$ , где $\varphi {t \over x}$ обозначает замену каждого $x$ в $\varphi$ по $t$ ; см. также Логика первого порядка . ^{[ нужна цитата ]}

Основные результаты [ править ]

Следующие действия эквивалентны:
1. $\operatorname {Inc} \Phi$
2. Для всех $\varphi ,\;\Phi \vdash \varphi .$
Всякий выполнимый набор формул непротиворечив, если набор формул $\Phi$ выполнима тогда и только тогда, когда существует модель ${\mathfrak {I}}$ такой, что ${\mathfrak {I}}\vDash \Phi$ .
Для всех $\Phi$ $\Фи$ и $\varphi$ $\varphi$ :
1. если не $\Phi \vdash \varphi$ , затем $\operatorname {Con} \left(\Phi \cup \{\lnot \varphi \}\right)$ ;
2. если $\operatorname {Con} \Phi$ и $\Phi \vdash \varphi$ , затем $\operatorname {Con} \left(\Phi \cup \{\varphi \}\right)$ ;
3. если $\operatorname {Con} \Phi$ , затем $\operatorname {Con} \left(\Phi \cup \{\varphi \}\right)$ или $\operatorname {Con} \left(\Phi \cup \{\lnot \varphi \}\right)$ .
Позволять $\Phi$ $\Фи$ — максимально непротиворечивый набор формул и предположим, что он содержит свидетели . Для всех $\varphi$ $\varphi$ и $\psi$ $\psi$ :
1. если $\Phi \vdash \varphi$ , затем $\varphi \in \Phi$ ,
2. или $\varphi \in \Phi$ или $\lnot \varphi \in \Phi$ ,
3. $(\varphi \lor \psi )\in \Phi$ если и только если $\varphi \in \Phi$ или $\psi \in \Phi$ ,
4. если $(\varphi \to \psi )\in \Phi$ и $\varphi \in \Phi$ , затем $\psi \in \Phi$ ,
5. $\exists x\,\varphi \in \Phi$ тогда и только тогда, когда существует термин $t$ такой, что $\varphi {t \over x}\in \Phi$ . ^{[ нужна цитата ]}

Теорема Хенкина [ править ]

Позволять $S$ быть набором символов . Позволять $\Phi$ быть максимально непротиворечивым множеством $S$ -формулы, содержащие свидетелей .

Определить отношение эквивалентности $\sim$ на съемках $S$ - условия по $t_{0}\sim t_{1}$ если $\;t_{0}\equiv t_{1}\in \Phi$ , где $\equiv$ означает равенство . Позволять ${\overline {t}}$ обозначим класс эквивалентности термов, содержащих $t$ ; и разреши $T_{\Phi }:=\{\;{\overline {t}}\mid t\in T^{S}\}$ где $T^{S}$ это набор терминов, основанный на наборе символов $S$ .

Определите $S$ - состав ${\mathfrak {T}}_{\Phi }$ над $T_{\Phi }$ , также называемая терминальной структурой, соответствующей $\Phi$ , к:

для каждого $n$ -арный символ отношения $R\in S$ , определять $R^{{\mathfrak {T}}_{\Phi }}{\overline {t_{0}}}\ldots {\overline {t_{n-1}}}$ если $\;Rt_{0}\ldots t_{n-1}\in \Phi ;$ ^[8]
для каждого $n$ -арный функциональный символ $f\in S$ , определять $f^{{\mathfrak {T}}_{\Phi }}({\overline {t_{0}}}\ldots {\overline {t_{n-1}}}):={\overline {ft_{0}\ldots t_{n-1}}};$
для каждого постоянного символа $c\in S$ , определять $c^{{\mathfrak {T}}_{\Phi }}:={\overline {c}}.$

Определить назначение переменной $\beta _{\Phi }$ к $\beta _{\Phi }(x):={\bar {x}}$ для каждой переменной $x$ . Позволять ${\mathfrak {I}}_{\Phi }:=({\mathfrak {T}}_{\Phi },\beta _{\Phi })$ быть термина интерпретацией , связанной с $\Phi$ .

Тогда для каждого $S$ -формула $\varphi$ :

{\mathfrak {I}}_{\Phi }\vDash \varphi

если и только если

\;\varphi \in \Phi .

^{[ нужна цитата ]}

Эскиз доказательства [ править ]

Есть несколько вещей, которые нужно проверить. Во-первых, это $\sim$ фактически является отношением эквивалентности. Затем необходимо убедиться, что (1), (2) и (3) корректно определены. Это вытекает из того, что $\sim$ является отношением эквивалентности и требует также доказательства того, что (1) и (2) не зависят от выбора $t_{0},\ldots ,t_{n-1}$ представители класса. Окончательно, ${\mathfrak {I}}_{\Phi }\vDash \varphi$ можно проверить индукцией по формулам.

Теория моделей [ править ]

В теории множеств ZFC с классической первого порядка логикой ^[9] теория противоречивая $T$ такое, что существует закрытое предложение $\varphi$ такой, что $T$ содержит оба $\varphi$ и его отрицание $\varphi '$ . Непротиворечивой : теорией называется такая, в которой выполняются следующие логически эквивалентные условия

$\{\varphi ,\varphi '\}\not \subseteq T$ ^[10]
$\varphi '\not \in T\lor \varphi \not \in T$

См. также [ править ]

Сноски [ править ]

^ Тарский 1946 формулирует это так: «Дедуктивная теория называется последовательной или непротиворечивой, если никакие два утвержденных утверждения этой теории не противоречат друг другу, или, другими словами, если из любых двух противоречивых предложений… хотя бы одно не может быть доказано, (с. 135), где Тарский определяет противоречивое так: «С помощью слова ни одно не образует отрицания какого-либо предложения; два предложения, из которых первое есть отрицание второго, называются противоречивыми предложениями » (с. . 20). Это определение требует понятия «доказательство». Гёдель 1931 определяет это понятие следующим образом: «Класс доказуемых формул определяется как наименьший класс формул, который содержит аксиомы и замкнут по отношению «непосредственное следствие», т. е. формула c для a и b определяется как непосредственное следствие с точки зрения modus ponens или замены, ср. Gödel 1931 , van Heijenoort 1967 , p. 601. Тарский неформально определяет «доказательство» как «утверждения, следующие друг за другом в определенном порядке в соответствии с определенными принципами… и сопровождаемые соображениями, призванными установить». их обоснованность [истинное заключение] для всех истинных посылок – Райхенбах 1947 , с. 68]» см. Тарский 1946 , стр. 3. Клини 1952 определяет это понятие либо в отношении индукции, либо в качестве перефразирования) конечной последовательности формул, такой, что каждая формула в последовательности является либо аксиомой, либо «непосредственным следствием» предыдущие формулы; « Доказательство называется доказательством своей последней формулы, и эта формула называется (формально) доказуемой или (формальной) теоремой» (см. Kleene 1952 , стр. 83).
^ Ходжес, Уилфрид (1997). Теория более коротких моделей . Нью-Йорк: Издательство Кембриджского университета. п. 37. Пусть $L$ быть подписью, $T$ теория в $L_{\infty \omega }$ и $\varphi$ предложение в $L_{\infty \omega }$ . Мы говорим, что $\varphi$ является следствием $T$ , или это $T$ влечет за собой $\varphi$ , в символах $T\vdash \varphi$ , если каждая модель $T$ является моделью $\varphi$ . (В частности, если $T$ тогда у него нет моделей $T$ влечет за собой $\varphi$ .)
Предупреждение : мы не требуем этого, если $T\vdash \varphi$ тогда есть доказательство $\varphi$ от $T$ . В любом случае, в случае с бесконечными языками не всегда ясно, что будет являться доказательством. Некоторые писатели используют $T\vdash \varphi$ иметь в виду, что $\varphi$ выводится из $T$ в каком-то конкретном формальном исчислении доказательств, и они пишут $T\models \varphi$ для нашего понятия следования (обозначение, которое противоречит нашему $A\models \varphi$ ). Для логики первого порядка два вида следствий совпадают по теореме о полноте рассматриваемого исчисления доказательств.
Мы говорим, что $\varphi$ действительна логической или является теоремой в символах $\vdash \varphi$ , если $\varphi$ верно в каждом $L$ -состав. Мы говорим, что $\varphi$ является последовательным , если $\varphi$ это правда в некоторых $L$ -состав. Аналогично мы говорим, что теория $T$ является непротиворечивым , если у него есть модель.
Мы говорим, что две теории S и T в L бесконечной омеге эквивалентны, если они имеют одинаковые модели, т. е. если Mod(S) = Mod(T). (Обратите внимание на определение Mod(T) на стр. 30...)
^ ван Хейеноорт 1967 , с. 265 утверждает, что Бернейс определил независимость аксиом Principia Mathematica , результат не был опубликован до 1926 года, но он ничего не говорит о том, что Бернейс доказал их непротиворечивость .
^ Пост доказывает как непротиворечивость, так и полноту исчисления высказываний PM, см. комментарий ван Хейеноорта и Введение Поста в общую теорию элементарных предложений 1931 года в van Heijenoort 1967 , стр. 264 и далее. Также Тарский 1946 , стр. 101-1. 134 и след.
^ см. комментарий ван Хейеноорта и Гёделя 1930 г. « Полнота аксиом функционального исчисления логики» в ван Хейеноорте 1967 г. , стр. 582 и далее.
^ см. комментарий ван Хейеноорта и статью Эрбрана 1930 г. «О непротиворечивости арифметики» в ван Хейеноорте 1967 г. , стр. 618 и далее.
^ Неофициально обычно предполагается теория множеств Цермело – Френкеля; некоторые диалекты неформальной математики обычно предполагают аксиому выбора . дополнительно
^ Это определение не зависит от выбора $t_{i}$ благодаря свойствам замещения $\equiv$ и максимальная согласованность $\Phi$ .
^ общий случай во многих приложениях к другим областям математики, а также обычный способ рассуждения неформальной математики в исчислении и приложениях к физике, химии, технике
^ по законам Де Моргана

Ссылки [ править ]

Гёдель, Курт (1 декабря 1931 г.). «О формально неразрешимых теоремах Principia Mathematica и родственных систем I». Ежемесячные журналы по математике и физике . 38 (1): 173–198. дои : 10.1007/BF01700692 .
Клини, Стивен (1952). Введение в метаматематику . Нью-Йорк: Северная Голландия. ISBN 0-7204-2103-9 . 10-е впечатление 1991 года.
Райхенбах, Ганс (1947). Элементы символической логики . Нью-Йорк: Дувр. ISBN 0-486-24004-5 .
Тарский, Альфред (1946). Введение в логику и методологию дедуктивных наук (второе изд.). Нью-Йорк: Дувр. ISBN 0-486-28462-Х .
ван Хейеноорт, Жан (1967). От Фреге до Гёделя: Справочник по математической логике . Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 0-674-32449-8 . (пбк.)
"Последовательность". Кембриджский философский словарь .
Эббингауз, HD; Флум, Дж.; Томас, В. Математическая логика .
Джевонс, WS (1870). Элементарные уроки логики .

Внешние ссылки [ править ]

Мортенсен, Крис (2017). «Непоследовательная математика» . Стэнфордская энциклопедия философии .

[1] Тарский 1946 формулирует это так: «Дедуктивная теория называется последовательной или непротиворечивой, если никакие два утвержденных утверждения этой теории не противоречат друг другу, или, другими словами, если из любых двух противоречивых предложений… хотя бы одно не может быть доказано, (с. 135), где Тарский определяет противоречивое так: «С помощью слова ни одно не образует отрицания какого-либо предложения; два предложения, из которых первое есть отрицание второго, называются противоречивыми предложениями » (с. . 20). Это определение требует понятия «доказательство». Гёдель 1931 определяет это понятие следующим образом: «Класс доказуемых формул определяется как наименьший класс формул, который содержит аксиомы и замкнут по отношению «непосредственное следствие», т. е. формула c для a и b определяется как непосредственное следствие с точки зрения modus ponens или замены, ср. Gödel 1931 , van Heijenoort 1967 , p. 601. Тарский неформально определяет «доказательство» как «утверждения, следующие друг за другом в определенном порядке в соответствии с определенными принципами… и сопровождаемые соображениями, призванными установить». их обоснованность [истинное заключение] для всех истинных посылок – Райхенбах 1947 , с. 68]» см. Тарский 1946 , стр. 3. Клини 1952 определяет это понятие либо в отношении индукции, либо в качестве перефразирования) конечной последовательности формул, такой, что каждая формула в последовательности является либо аксиомой, либо «непосредственным следствием» предыдущие формулы; « Доказательство называется доказательством своей последней формулы, и эта формула называется (формально) доказуемой или (формальной) теоремой» (см. Kleene 1952 , стр. 83).

[2] Ходжес, Уилфрид (1997). Теория более коротких моделей . Нью-Йорк: Издательство Кембриджского университета. п. 37. Пусть $L$ быть подписью, $T$ теория в $L_{\infty \omega }$ и $\varphi$ предложение в $L_{\infty \omega }$ . Мы говорим, что $\varphi$ является следствием $T$ , или это $T$ влечет за собой $\varphi$ , в символах $T\vdash \varphi$ , если каждая модель $T$ является моделью $\varphi$ . (В частности, если $T$ тогда у него нет моделей $T$ влечет за собой $\varphi$ .)
Предупреждение : мы не требуем этого, если $T\vdash \varphi$ тогда есть доказательство $\varphi$ от $T$ . В любом случае, в случае с бесконечными языками не всегда ясно, что будет являться доказательством. Некоторые писатели используют $T\vdash \varphi$ иметь в виду, что $\varphi$ выводится из $T$ в каком-то конкретном формальном исчислении доказательств, и они пишут $T\models \varphi$ для нашего понятия следования (обозначение, которое противоречит нашему $A\models \varphi$ ). Для логики первого порядка два вида следствий совпадают по теореме о полноте рассматриваемого исчисления доказательств.
Мы говорим, что $\varphi$ действительна логической или является теоремой в символах $\vdash \varphi$ , если $\varphi$ верно в каждом $L$ -состав. Мы говорим, что $\varphi$ является последовательным , если $\varphi$ это правда в некоторых $L$ -состав. Аналогично мы говорим, что теория $T$ является непротиворечивым , если у него есть модель.
Мы говорим, что две теории S и T в L бесконечной омеге эквивалентны, если они имеют одинаковые модели, т. е. если Mod(S) = Mod(T). (Обратите внимание на определение Mod(T) на стр. 30...)

[3] ван Хейеноорт 1967 , с. 265 утверждает, что Бернейс определил независимость аксиом Principia Mathematica , результат не был опубликован до 1926 года, но он ничего не говорит о том, что Бернейс доказал их непротиворечивость .

[4] Пост доказывает как непротиворечивость, так и полноту исчисления высказываний PM, см. комментарий ван Хейеноорта и Введение Поста в общую теорию элементарных предложений 1931 года в van Heijenoort 1967 , стр. 264 и далее. Также Тарский 1946 , стр. 101-1. 134 и след.

[5] см. комментарий ван Хейеноорта и Гёделя 1930 г. « Полнота аксиом функционального исчисления логики» в ван Хейеноорте 1967 г. , стр. 582 и далее.

[6] см. комментарий ван Хейеноорта и статью Эрбрана 1930 г. «О непротиворечивости арифметики» в ван Хейеноорте 1967 г. , стр. 618 и далее.

[7] Неофициально обычно предполагается теория множеств Цермело – Френкеля; некоторые диалекты неформальной математики обычно предполагают аксиому выбора . дополнительно

[8] Это определение не зависит от выбора $t_{i}$ благодаря свойствам замещения $\equiv$ и максимальная согласованность $\Phi$ .

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

[10] по законам Де Моргана

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

v т Это ‌ Логическая Logical truth истина ⊤
Functional:	truth value truth function ⊨ tautology
Formal:	theory formal proof theorem
Negation	⊥ false contradiction inconsistency