Вывод законов де моргана в исчислении высказываний

Обновлено: 22.12.2024

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

Конструктивное доказательство закона Де Моргана 10.09.2017, 14:24

Последний раз редактировалось epros 10.09.2017, 14:38, всего редактировалось 4 раз(а).

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

В книжке Гейтинга "Интуиционизм" доказывается так: Из аксиомы disjunction introduction с применением контрапозиции получаем . Аналогично - . Используя теорему дедукции и объединяя консеквенты двух последних формул с помощью conjunction introduction , получаем .

Про обратную формулу сказано просто: "Легко видеть, что имеет место и обратная формула". Некоторое время назад, как я припоминаю, мне тоже показалось, что это "легко видеть", но сейчас у меня что-то не получается это увидеть. Может я где-то туплю.

Очевидно, что это можно доказать сведением к противоречию , и . Здесь очень бы помогла дистрибутивность конъюнкции по дизъюнкции: , но я что-то тоже никак не соображу, как она выводится из аксиоматики. Для этого, в свою очередь, очень помогла бы формула . Но я, опять же, не вижу способа вывести её из стандартной Гильбертовской аксиоматики, из которой выкинули закон исключённого третьего. Аксиома disjunction elimination что-то не помогает.

10.09.2017, 15:18

Последний раз редактировалось gefest_md 10.09.2017, 15:41, всего редактировалось 1 раз.

Аксиома disjunction elimination что-то не помогает.

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

1. - гипотеза
2. - схема аксиома
3. - MP, 1, 2.
4. - схема аксиом.
5. - MP, 1, 4.
6. - схема аксиом.
7. - схема аксиом.
8. - схема аксиом.
9. - MP, 5, 8.
10. - теорема
11. - MP, 10, 9, 7.
12. - схема аксиом
13. - MP, 3, 12.
14. - MP, 11, 13, 6.

10.09.2017, 17:41

Очень рекомендую следующее определение отрицания: . С ним всё становится проще. Раскрываем это определение в , получаем . Это эквивалентно разбору случаев.

Эту теорему легко запомнить с помощью следующего инсайта. На языке теории категорий, означает биекцию между парами морфизмов типа и и морфизмами типа . Если надо без теории категорий, то морфизмы — это функции, — это дизъюнктное объединение множеств и . Я называю эту биекцию «веерная сумма морфизмов».

10.09.2017, 18:27

Последний раз редактировалось arseniiv 10.09.2017, 18:28, всего редактировалось 1 раз.

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

код: [ скачать ] [ спрятать ] код: [ скачать ] [ показать ] Используется синтаксис Haskell

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


Вообще типы этих функций можно, конечно, взять и более общие, заменив везде Void на какое-то c (если не указывать аннотацию типа, хаскель такие и выведет). 10.09.2017, 21:04 Натуральный вывод таков. Предположим Далее предположим и придём к противоречию. Разбор случаев: ведёт к противоречию, ведёт к противоречию, поэтому ведёт к противоречию. Бросайте мучаться с гильбертовыми системами и переходите на натуральный вывод. 10.09.2017, 21:10

Последний раз редактировалось arseniiv 10.09.2017, 21:11, всего редактировалось 1 раз.

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

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

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

10.09.2017, 21:29

Последний раз редактировалось arseniiv 10.09.2017, 21:47, всего редактировалось 2 раз(а).

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

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

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

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

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

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

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

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

Читайте также: