Конструктивное доказательство закона Де Моргана

[epros]

Известно, что из классических эквивалентностей Де Моргана

$$\neg P \lor \neg Q \leftrightarrow \neg (P \land Q)$$

и

$$\neg P \land \neg Q \leftrightarrow \neg (P \lor Q)$$

в конструктивном (интуиционистском) исчислении высказываний полностью выполняется только втовая (первая выполняется только в прямом, но не в обратном направлении).

В книжке Гейтинга "Интуиционизм" $\neg (P \lor Q) \to \neg P \land \neg Q$ доказывается так: Из аксиомы disjunction introduction $P \to P \lor Q$ с применением контрапозиции получаем $\neg (P \lor Q) \to \neg P$. Аналогично - $\neg (P \lor Q) \to \neg Q$. Используя теорему дедукции и объединяя консеквенты двух последних формул с помощью conjunction introduction $A \to (B \to A \land B)$, получаем $\neg (P \lor Q) \to \neg P \land \neg Q$.

Про обратную формулу $\neg P \land \neg Q \to \neg (P \lor Q)$ сказано просто: "Легко видеть, что имеет место и обратная формула". Некоторое время назад, как я припоминаю, мне тоже показалось, что это "легко видеть", но сейчас у меня что-то не получается это увидеть. Может я где-то туплю.

Очевидно, что это можно доказать сведением к противоречию $\neg P$, $\neg Q$ и $P \lor Q$. Здесь очень бы помогла дистрибутивность конъюнкции по дизъюнкции: $A \land (P \lor Q) \to (A \land P) \lor (A \land Q)$, но я что-то тоже никак не соображу, как она выводится из аксиоматики. Для этого, в свою очередь, очень помогла бы формула $(A \lor B \to C) \to ((A \to C) \lor (B \to C))$. Но я, опять же, не вижу способа вывести её из стандартной Гильбертовской аксиоматики, из которой выкинули закон исключённого третьего. Аксиома disjunction elimination $(A \to C) \to ((B \to C) \to (A \lor B \to C))$ что-то не помогает.

[gefest_md]

epros в сообщении #1246674 писал(а):

Аксиома disjunction elimination $(A \to C) \to ((B \to C) \to (A \lor B \to C))$ что-то не помогает.

Это разбор случаев. Обязано помочь.

1. $\neg P\wedge\neg Q$ - гипотеза
2. $\neg P\wedge\neg Q\to\neg P$ - схема аксиома
3. $\neg P$ - MP, 1, 2.
4. $\neg P\wedge\neg Q\to\neg Q$ - схема аксиом.
5. $\neg Q$ - MP, 1, 4.
6. $(P\vee Q\to P)\to((P\vee Q\to\neg P)\to\neg(P\vee Q))$ - схема аксиом.
7. $(P\to P)\to((Q\to P)\to(P\vee Q\to P))$ - схема аксиом.
8. $\neg Q\to(Q\to P)$ - схема аксиом.
9. $Q\to P$ - MP, 5, 8.
10. $P\to P$ - теорема
11. $P\vee Q\to P$ - MP, 10, 9, 7.
12. $\neg P\to(P\vee Q\to\neg P)$ - схема аксиом
13. $P\vee Q\to\neg P$ - MP, 3, 12.
14. $\neg(P\vee Q)$ - MP, 11, 13, 6.

[beroal]

Очень рекомендую следующее определение отрицания: \(\lnot\varphi:=\varphi\to\bot \). С ним всё становится проще. Раскрываем это определение в \(\lnot P \land \lnot Q \to \lnot (P \lor Q)\), получаем \((P\to\bot)\land(Q\to\bot) \to (P \lor Q\to\bot)\). Это эквивалентно разбору случаев.

Эту теорему легко запомнить с помощью следующего инсайта. На языке теории категорий, \((P\to Q)\land(P'\to Q) \leftrightarrow (P \lor P'\to Q)\) означает биекцию между парами морфизмов типа \(P\to Q\) и \(P'\to Q\) и морфизмами типа \(P+P'\to Q\). Если надо без теории категорий, то морфизмы — это функции, \(P+P'\) — это дизъюнктное объединение множеств \(P\) и \(P'\). Я называю эту биекцию «веерная сумма морфизмов».

[arseniiv]

А вот как к этому относится функциональное программирование. Доказательство строится весьма естественным образом: сопоставлению с шаблонами соответствует разбор случаев, применению функции — modus ponens, абстракции — вывод из гипотез. _ означает, что значение не используется.

Используется синтаксис Haskell

import Data.Void
type Not a = a -> Void

m1 :: Either (Not a) (Not b) -> Not (a, b)
m1 (Left na) (a, _) = na a
m1 (Right nb) (_, b) = nb b

m2 :: (Not a, Not b) -> Not (Either a b)
m2 (na, _) (Left a) = na a
m2 (_, nb) (Right b) = nb b

m3 :: Not (Either a b) -> (Not a, Not b)
m3 nx = (nx . Left, nx . Right)
-- m3 nx = (\a -> nx (Left a), \b -> nx (Right b))

Вообще типы этих функций можно, конечно, взять и более общие, заменив везде Void на какое-то c (если не указывать аннотацию типа, хаскель такие и выведет).

[george66]

Натуральный вывод таков. Предположим $\neg P,\neg Q$ Далее предположим $P\vee Q$ и придём к противоречию. Разбор случаев: $P$ ведёт к противоречию, $Q$ ведёт к противоречию, поэтому $P\vee Q$ ведёт к противоречию. Бросайте мучаться с гильбертовыми системами и переходите на натуральный вывод.

[arseniiv]

george66
Или в какую-нибудь подходящую теорию типов (разница только в ярлычках для выводов). Если нужна первопорядковость — пожалуйста, Мартин-Лёф.

[epros]

gefest_md, спасибо, понятно. Разочаровывают две вещи:
1) Это непохоже на "легко видеть".
2) Доказательство опирается на ex falso quodlibet, В данном случае - в форме аксиомы на шаге 8. Это наводит на подозрение, что в т.н. "минимальной логике" это всё недоказуемо (в ней можно вывести $\bot \to \neg A$, но не $\bot \to A$).

P.S. Попробую теперь вывести $(A \lor B \to C) \to ((A \to C) \lor (B \to C))$. Вроде бы в конструктивной логике (включающей ex falso quodlibet) она должна выводиться. Хотя это на первый взгляд противоречит "идеологии" конструктивизма: Согласно интерпретации BHK утверждать $(A \to C) \lor (B \to C)$ вроде бы можно только если известно из чего конкретно выводится $C$ - из $A$ или из $B$, а предположение $A \lor B \to C$ не даёт нам такой информации. Будет довольно любопытно, если это выводится тоже с помощью ex falso quodlibet.

[arseniiv]

epros в сообщении #1246835 писал(а):

2) Доказательство опирается на ex falso quodlibet, В данном случае - в форме аксиомы на шаге 8. Это наводит на подозрение, что в т.н. "минимальной логике" это всё недоказуемо (в ней можно вывести $\bot \to \neg A$, но не $\bot \to A$).

Должно быть доказуемо, гляньте на мои определения. Там можно обойтись совершенно без $\bot$ (это Void) одними свойствами импликации, дизъюнкции и конъюнкции.

-- Вс сен 10, 2017 23:34:34 --

epros в сообщении #1246835 писал(а):

Вроде бы в конструктивной логике (включающей ex falso quodlibet) она должна выводиться.

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

-- Вс сен 10, 2017 23:47:24 --

arseniiv в сообщении #1246843 писал(а):

гляньте на мои определения

Если там не всё так очевидно, допишу типы используемых, скажем, примитивов (хотя они определяются). Конструкторы значений, соответствующие аксиомам/правилам введения связок:

Используется синтаксис Haskell

Left :: a -> Either a b
Right :: b -> Either a b
(,) :: a -> b -> (a, b)

Определение разбором случаев

Используется синтаксис Haskell

f (Left a) = g a
f (Right b) = h b

можно выразить через функцию either :: (a -> c) -> (b -> c) -> Either a b -> c как f = either g h. Оно соответствует удалению дизъюнкции.

Сопоставление с элементами пары

Используется синтаксис Haskell

f (a, b) = g a b

можно выразить через функции fst :: (a, b) -> a и snd :: (a, b) -> b: f = \p -> g (fst p) (snd p). Они соответствуют удалению конъюнкции.

Остальное я уже описал.

[epros]

beroal в сообщении #1246724 писал(а):

$(P\to\bot)\land(Q\to\bot) \to (P \lor Q\to\bot)$. Это эквивалентно разбору случаев.

Хм. Попробую "разбор случаев" без ex falso quodlibet,

1. $(P \to \bot) \land (Q \to \bot)$ - гипотеза.
2. $P \to \bot$ - conjunction elimination из 1.
3. $Q \to \bot$ - conjunction elimination из 1.
4. $(Q \to \bot) \to (P \lor Q \to \bot)$ - modus ponens из 2 и disjunction elimination.
5. $P \lor Q \to \bot$ modus ponens из 3 и 4.

-- Вс сен 10, 2017 23:04:12 --

Да, это больше похоже на "легко видеть". Видно, я всё же слегка ступил.

arseniiv в сообщении #1246843 писал(а):

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

Вот, нашёл страничку, на которой это указано как тавтология интуиционистской логики.

[arseniiv]

Не вижу там именно

epros в сообщении #1246835 писал(а):

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

Самое близкое — это

Цитата:

stmt (DisjunctionComposition () () (((p → r) ∧ (q → r)) ↔ ((p ∨ q) → r)))

но это не в точности то же.

[epros]

Да, точно, проглядел.

-- Вс сен 10, 2017 23:36:16 --

И вообще я что-то не то написал. Надо было:
$(C \to A \lor B) \to ((C \to A) \lor (C \to B))$.
В обратную-то сторону выводится, а вот так - вопрос.

[Xaositect]

epros в сообщении #1246835 писал(а):

P.S. Попробую теперь вывести $(A \lor B \to C) \to ((A \to C) \lor (B \to C))$. Вроде бы в конструктивной логике (включающей ex falso quodlibet) она должна выводиться. Хотя это на первый взгляд противоречит "идеологии" конструктивизма: Согласно интерпретации BHK утверждать $(A \to C) \lor (B \to C)$ вроде бы можно только если известно из чего конкретно выводится $C$ - из $A$ или из $B$, а предположение $A \lor B \to C$ не даёт нам такой информации. Будет довольно любопытно, если это выводится тоже с помощью ex falso quodlibet.

Так ведь тут действительно известно: из обоих выводится. $A \Rightarrow A \vee B \Rightarrow C$, $B \Rightarrow A \vee B \Rightarrow C$

-- Вс сен 10, 2017 20:50:49 --

epros в сообщении #1246856 писал(а):

И вообще я что-то не то написал. Надо было:
$(C \to A \lor B) \to ((C \to A) \lor (C \to B))$.
В обратную-то сторону выводится, а вот так - вопрос.

А это выводиться не должно.

[gefest_md]

epros в сообщении #1246835 писал(а):

Доказательство опирается на ex falso quodlibet, В данном случае - в форме аксиомы на шаге 8. Это наводит на подозрение, что в т.н. "минимальной логике" это всё недоказуемо

Теоремы:

$\vdash A\to\neg(\neg A\wedge\neg B)$

$\vdash B\to\neg(\neg A\wedge\neg B)$

$\vdash A\vee B\to\neg(\neg A\wedge\neg B)$

$\vdash (X\to\neg Y)\to(Y\to\neg X)$ (вариант контрапозиции)

доказуемы в минимальном исчислении. "Де Морган" получается из 3-й и 4-й.

[Sinoid]

(Оффтоп)

epros в сообщении #1246674 писал(а):

втовая

[arseniiv]

Xaositect в сообщении #1246869 писал(а):

Так ведь тут действительно известно: из обоих выводится. $A \Rightarrow A \vee B \Rightarrow C$, $B \Rightarrow A \vee B \Rightarrow C$

А не напишете функцию с типом (Either a b -> c) -> Either (a -> c) (b -> c)? По-моему, её всё-таки нет.