Минимальная логика

Минимальная логика , или минимальное исчисление , представляет собой систему символической логики, первоначально разработанную Ингебригт Йоханссон . Это интуиционистская и парапоследовательная логика , которая отвергает как закон исключенного третьего, так и принцип взрыва ( ex falso quodlibet ) и, следовательно, не считает ни один из следующих двух выводов действительным:

$\vdash (B\lor \neg B)$

$(A\land \neg A)\vdash$

где $A$ и $B$ есть какие-то предложения. Большинство конструктивных логик отвергают только первый закон — закон исключенного третьего. В классической логике ex false действуют законы .

$(A\land \neg A)\to B,$

$\neg (A\lor \neg A)\to B,$

$\neg A\to (A\to B),$

а также их варианты с $A$ и $\neg A$ переключены, эквивалентны друг другу и действительны. Минимальная логика также отвергает эти принципы.

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

Аксиоматизация

Минимальная логика аксиоматизируется над позитивным фрагментом интуиционистской логики. Обе эти логики могут быть сформулированы на языке, используя одни и те же аксиомы для импликация $\to$, соединение $\land$ и дизъюнкция $\lor$ в качестве основных связок , но традиционно добавляется минимальная логика ложь или абсурд $\bot$ как часть языка.

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

Теоремы

Введение в отрицание

Быстрый анализ действующих правил отрицания дает хорошее представление о том, что может и чего не может доказать эта логика, лишенная полного раскрытия.Естественным утверждением в языке с отрицанием , таком как минимальная логика, является, например, принцип введения отрицания , согласно которому отрицание утверждения доказывается путем принятия утверждения и вывода противоречия. В рамках минимальной логики этот принцип эквивалентен следующему:

$(B\to (A\land \neg A))\to \neg B$,

для любых двух предложений. Для $B$ воспринимается как противоречие $A\land \neg A$ само по себе это устанавливает закон непротиворечия

$\neg (A\land \neg A)$.

Предполагая любой $C$, правило введения материального кондиционала дает $B\to C$, а также когда $B$ и $C$ не имеют существенного отношения. С учетом этого и исключения импликаций из приведенного выше принципа введения следует

$(A\land \neg A)\to \neg B$,

т.е. допуская любое противоречие, каждое предложение можно отрицать. Введение отрицания возможно в минимальной логике, поэтому здесь любое противоречие, кроме того, доказывает любое двойное отрицание. $\neg \neg B$. Взрыв позволил бы устранить последнее двойное отрицание, но этот принцип не принят.

Аксиоматизация через абсурд

Одна из возможных схем распространения позитивного исчисления на минимальную логику состоит в рассмотрении $\neg B$ как импликация, и в этом случае теоремы конструктивного исчисления импликаций логики переносятся на утверждения отрицания. С этой целью, $\bot$ вводится как утверждение, недоказуемое, если только система не непротиворечива, а отрицание $\neg B$ тогда рассматривается как сокращение от $B\to \bot$.Конструктивно, $\bot$ представляет собой утверждение, для которого не может быть никаких оснований верить в него.

Последствия

Что касается принятых в исчислении импликаций принципов, не предполагающих отрицаний, то на странице, посвященной системе Гильберта, они представлены через пропозициональные формы аксиом закона тождества , введение импликации и вариант modus ponens . Обратите внимание на эквивалентность ${\big (}A\to (B\to C){\big )}\leftrightarrow {\big (}B\to (A\to C){\big )}$ там доказано. Для первого вывода положим $C=\bot$ тут сразу приводит схему

${\big (}A\to \neg B{\big )}\leftrightarrow {\big (}B\to \neg A{\big )}$.

В интуиционистской системе Гильберта, если не вводить $\bot$ как константу это можно принять как вторую аксиому, характеризующую отрицание. (Второй — взрыв.)

Теперь, во-первых, с $A$ взято как $\neg B$, это выше показывает, что

$B\to \neg \neg B$.

Но, во-вторых, эта короткая импликация может быть выведена и более непосредственно из modus ponens в пропозициональной форме. $B\to ((B\to C)\to C)$ рассматривая $C=\bot$.

В-третьих, это следует из действительной слабой формы консеквенции мирабилис : $(\neg B\to \neg \neg B)\leftrightarrow \neg \neg B$. Другими словами, утверждение не может быть отвергнуто именно тогда, когда отрицание утверждения подразумевает, что оно не может быть отвергнуто. В частности, можно доказать $\neg \neg B$ например, доказав $\neg B\to B$.

В-четвертых, изложенное выше следует также из

${\big (}\neg \neg (A\to B){\big )}\to {\big (}A\to \neg \neg B{\big )}$

что связано с принципом двойного отрицания. Эта теорема может быть установлена ​​из $A\to {\big (}B\leftrightarrow (A\to B){\big )}$, снова рассуждая с другой переменной $C$ очень похоже на вышеизложенное, что доказывает $A\to {\big (}(\neg B)\leftrightarrow \neg (A\to B){\big )}$, и так далее.

Из первой теоремы далее получаем ${\big (}A\to \neg B{\big )}\leftrightarrow {\big (}\neg \neg A\to \neg B{\big )}$, и так

$\neg \neg \neg B\leftrightarrow \neg B$.

Обобщая некоторые из вышеизложенных по-другому, можно ${\big (}((B\to C)\to C)\to D{\big )}\to (B\to D)$. В соответствии с соответствием Карри-Говарда это, как один из примеров, оправдывается лямбда-выражением $\lambda f^{((B\to C)\to C)\to D}.\ \lambda b^{B}.\ f(\lambda g^{B\to C}.g(b))$.Modus ponens далее действительно подразумевает эквивалентность ${\big (}((B\to C)\to C)\to C{\big )}\leftrightarrow (B\to C)$, из чего теперь $\neg \neg \neg B\leftrightarrow \neg B$ следует и по-другому.

Наконец, путем введения импликации, $C\to (B\to C)$, а это тоже уже подразумевает $\bot \to (B\to \bot )$ прямо показывая, как предположить $\bot$ в минимальной логике доказывает все отрицания. Это может быть выражено как

$\bot \to \neg B.$

Если абсурд примитивен, принцип полного взрыва можно также сформулировать как $\bot \to B$.

Союзы

Выйдя за рамки утверждений исключительно с точки зрения следствий, принципы, обсуждавшиеся ранее, теперь также могут быть установлены в виде теорем: С определением отрицания через $\bot$, утверждение modus ponens в форме $(A\land (A\to C))\to C$ сам специализируется на принципе непротиворечия при рассмотрении $C=\bot$. Когда отрицание является импликацией, тогда снова используется каррированная форма непротиворечия. $A\to \neg \neg A$.Далее, введение отрицания в форме с союзом, изложенное в предыдущем разделе, подразумевается лишь как частный случай ${\big (}B\to (A\land (A\to C)){\big )}\to (B\to C)$

Таким образом, минимальную логику можно охарактеризовать как конструктивную логику только без устранения отрицания (так называемого взрыва).

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

Дизъюнкции

Стоит подчеркнуть важную эквивалентность

${\big (}(A\lor B)\to C{\big )}\leftrightarrow {\big (}(A\to C)\land (B\to C){\big )}$,

выражая, что это два эквивалентных способа сказать, что оба $A$ и $B$ подразумевать $C$. два известных закона Де Моргана Из него получаются :

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$.

Также можно вывести третий действительный закон Де Моргана.

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

$\neg \neg (B\lor \neg B)$

Этот результат также можно рассматривать как частный случай ${\big (}(B\lor (B\to C))\to C{\big )}\to C$, что следует из $((A\lor B)\to C)\to (B\to C)$ при рассмотрении $B\to C$ для $A$.

Наконец, анализ случаев показывает

${\big (}(B\lor \neg A)\land \neg \neg A{\big )}\to {\big (}(B\lor \neg B)\land \neg \neg B){\big )}$

Эту импликацию следует сравнить с полным дизъюнктивным силлогизмом , подробно обсуждаемым ниже.

через

Следует отметить еще одну теорему, касающуюся только импликаций: Относящуюся к принципу введения отрицания, из

$(B\to A)\to ((A\to C)\to (B\to C))$.

минимальная логика доказывает противоположность

$(B\to A)\to (\neg A\to \neg B)$,

что, как и введение отрицания, снова доказывает $(A\land \neg A)\to \neg B$.Все вышеперечисленные принципы можно получить, используя теоремы положительного исчисления в сочетании с константой $\bot$.

Вместо формулировки с этой константой можно принять в качестве аксиом только что сформулированный принцип противопоставления вместе с принципом двойного отрицания. $B\to \neg \neg B$. Это дает альтернативную аксиоматизацию минимальной логики над позитивным фрагментом интуиционистской логики.

Отношение к классической логике

Тактика обобщения $\neg A$ к $A\to C$ не помогает доказать все классически верные утверждения, включающие двойное отрицание. В частности, неудивительно, что наивное обобщение исключения двойного отрицания $\neg \neg B\to B$ не может быть доказано таким способом. Действительно, что угодно $A$ похоже, любая схема синтаксической формы $(A\to C)\to B$ было бы слишком сильным: рассматривая любое истинное предложение для $C$ делает это эквивалентным просто $B$.

Предложение $\neg \neg (B\lor \neg B)$ является теоремой минимальной логики, как и $(A\land \neg A)\to \neg \neg B$. Поэтому, приняв полный принцип двойного отрицания $\neg \neg B\to B$ в минимальной логике фактически также доказывается взрыв и, таким образом, возвращается исчисление к классической логике , также пропуская все промежуточные логики .

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

$\nvdash \neg \neg \forall (n\in {\mathbb {N} }).Q(n)\lor \neg Q(n)$

В свою очередь, схема сдвига двойного отрицания (DNS) также недействительна, т.е.

$\nvdash {\big (}\forall (n\in {\mathbb {N} }).\neg \neg P(n){\big )}\to \neg \neg \forall (n\in {\mathbb {N} }).P(n)$

Помимо арифметики , эта недоказуемость позволяет аксиоматизировать неклассические теории.

Отношение к паранепротиворечивой логике

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

к

Любая формула, использующая только $\land ,\lor ,\to$ доказуемо в минимальной логике тогда и только тогда, когда оно доказуемо в интуиционистской логике.Но существуют также утверждения пропозициональной логики, которые недоказуемы в минимальной логике, но верны интуиционистски.

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

При взрыве отрицательных утверждений полный взрыв эквивалентен его особому случаю. $((\neg B)\land \neg (\neg B))\to B$. Последнее можно сформулировать как устранение двойного отрицания для отвергаемых предложений. $\neg B\to (\neg \neg B\to B)$. Короче говоря, взрыв в интуиционистской логике в точности предоставляет частные случаи принципа устранения двойного отрицания, которых нет в минимальной логике.Этот принцип также непосредственно доказывает полный дизъюнктивный силлогизм.

Дизъюнктивный силлогизм

Практически, в интуиционистском контексте, принцип взрыва делает возможным дизъюнктивный силлогизм:

$((A\lor B)\land \neg A)\to B.$

Это можно прочитать следующим образом: Учитывая конструктивное доказательство $A\lor B$ и конструктивный отказ от $A$, то безоговорочно допускается положительный случай выбора $B$. Таким образом, силлогизм является принципом распаковки дизъюнкции. Это можно рассматривать как формальное следствие взрыва, и оно также подразумевает его. Это потому, что если $A\lor B$ было доказано путем доказательства $B$ затем $B$ уже доказано, а если $A\lor B$ было доказано путем доказательства $A$, затем $B$ также следует, поскольку интуиционистская система допускает взрыв.

Например, при наличии конструктивного аргумента, что при подбрасывании монеты выпадает либо орел, либо решка ( $A$ или $B$), вместе с конструктивным аргументом о том, что результатом на самом деле не была решка, силлогизм выражает, что тогда это уже составляет аргумент о том, что выпала решка.

Если интуиционистская логическая система металогически предполагается непротиворечивой, силлогизм можно прочитать как утверждение, что конструктивная демонстрация $A\lor B$ и $\neg A$, в отсутствие других нелогических аксиом, демонстрирующих $B$, на самом деле содержит демонстрацию $B$.

В минимальной логике невозможно получить доказательство $B$ таким образом. Однако та же посылка подразумевает двойное отрицание $B$, то есть $\neg \neg B$. Если минимальная логическая система металогически предполагается непротиворечивой, то эту формулу импликации можно выразить, сказав, что $B$ просто не может быть отвергнуто.

Слабые формы взрыва доказывают дизъюнктивный силлогизм, а в другую сторону - пример силлогизма с $A=\neg B$ читает ${\big (}(B\lor \neg B)\land \neg \neg B{\big )}\to B$ и эквивалентно исключению двойного отрицания для предложений, для которых имеет место исключенное среднее.

$(B\lor \neg B)\to (\neg \neg B\to B)$.

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

использования в

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

Позволять $P$ быть любым предикатом без кванторов и, следовательно, разрешимым для всех чисел $n$, так что исключенное среднее сохраняется,

$P(n)\lor \neg P(n)$.

Тогда индукцией по $m$,

$\forall m.\ \neg {\big (}\forall (n<m).\neg P(n){\big )}\to \exists (b<m).P(b)$

Прописью: Для цифр $n$ в конечном диапазоне до $m$, если можно исключить, что ни один случай не является проверяемым, т. е. если можно исключить, что для каждого числа, скажем, $n=a$, соответствующее предложение $P(a)$ всегда будет опровергаемо, то это означает, что существует некоторая $n=b$ среди тех $n$для чего $P(b)$ доказуемо.

Как и в примерах, обсуждавшихся ранее, доказательство этого требует взрыва антецедентной стороны, чтобы получить предложения без отрицаний. Если предложение сформулировано так, начиная с $m=0$, то этот начальный случай уже дает форму взрыва из пустого предложения

$\bot \to \exists (b<0).P(b)$.

Следующий случай $m=1$ утверждает исключение двойного отрицания для разрешимого предиката,

$\neg \neg P(0)\to P(0)$.

The $m=2$ дело гласит

$\neg {\big (}\neg P(0)\land \neg P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$,

что, как уже отмечалось, эквивалентно

$\neg \neg {\big (}P(0)\lor P(1){\big )}\to {\big (}P(0)\lor P(1){\big )}$.

Оба $m=0$ и $m=1$ снова являются случаями исключения двойного отрицания для разрешимого предиката.Конечно, заявление $\exists (b<m).P(b)$ для фиксированного $m$ и $P$ может быть доказуемо другими средствами, используя принципы минимальной логики.

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

с

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

Абсурд $\bot$ используется не только в естественной дедукции , но и в теоретических формулировках типов в соответствии с соответствием Карри–Ховарда . В системах типов $\bot$ часто также обозначается как пустой тип.

Во многих контекстах $\bot$ не обязательно должна быть отдельной константой в логике, но ее роль может быть заменена любым отвергнутым предложением. Например, его можно определить как $a=b$ где $a,b$ должно быть различимо. Утверждение об отсутствии доказательства для этого предложения является тогда заявлением о непротиворечивости.

Пример характеристики для $\bot$ является $0=1$ в теории натуральных чисел. Это также можно принять за простую конструктивную логику.При этом доказывая $3^{4}=8$ быть ложным, т.е. $\neg (3^{4}=8)$, просто значит доказать $(3^{4}=8)\to (0=1)$. Мы можем ввести обозначение $3^{4}\neq 8$ также зафиксировать иск.И действительно, используя арифметику, ${\tfrac {3^{4}-8}{73}}=1$ держится, но $(3^{4}=8)$ также подразумевает ${\tfrac {3^{4}-8}{73}}=0$. Таким образом, это будет означать $1=0$ и, следовательно, мы получаем $\neg (3^{4}=8)$. ЯВЛЯЕТСЯ

Простые типы

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

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

${\dfrac {}{\Gamma \cup \{A\}\vdash A}}{\mbox{ axiom}}$         ${\dfrac {\Gamma \cup \{A\}\vdash B}{\Gamma \vdash A\to B}}{\mbox{ intro}}$         ${\dfrac {\Gamma \vdash A\to B~~~~~~~~~~\Delta \vdash A}{\Gamma \cup \Delta \vdash B}}{\mbox{ elim.}}$

Каждая формула этой ограниченной минимальной логики соответствует типу в просто типизированном лямбда-исчислении , см. соответствие Карри-Ховарда . В этом контексте фраза «минимальная логика» иногда используется для обозначения ограничения минимальной логики. Этот импликативный фрагмент минимальной логики то же самое, что позитивный импликативный фрагмент интуиционистской логики, поскольку минимальная Логика уже является просто позитивным фрагментом интуиционистской логики.

Семантика

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

См. также

• Интуиционистская логика
• Паранепротиворечивая логика
• Импликативное исчисление высказываний
• Список логических систем

Ссылки

• Колачито, Альмудена (2016). Минимальная и субминимальная логика отрицания (PDF) . Магистерская диссертация (Afstudeerscriptie). Институт логики, языка и вычислений .
• Юэ, Жерар (май 1986 г.). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и расчетам дискретного проектирования. Архивировано из оригинала 14 июля 2014 г.
• Йоханссон, Ингебригт (1937). «Минимальное исчисление, уменьшенный интуиционистский формализм» . Compositio Mathematica (на немецком языке). 4 : 119–136.
• Соренсен, Мортен Хейне Б.; Уржичин, Павел [на польском языке] (май 1998 г.). «Лекции по изоморфизму Карри-Говарда» (PDF) .
• Троэльстра, Энн Шерп ; Швихтенберг, Хельмут (2003) [1996]. Основная теория доказательств (2-е изд.). Издательство Кембриджского университета . стр. XII, 417. ISBN.  9780521779111 .
• Вебер, Матиас; Саймонс, Мартин; Лафонтен, Кристина (1993). Общий язык разработки Deva: презентация и практические примеры . Конспекты лекций по информатике (LNCS). Том. 738. Спрингер. п. 246. ИСБН  3-540-57335-6 .