Вывод законов де моргана в исчислении высказываний
Обновлено: 22.11.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, 18:27Последний раз редактировалось arseniiv 10.09.2017, 18:28, всего редактировалось 1 раз.
А вот как к этому относится функциональное программирование. Доказательство строится весьма естественным образом: сопоставлению с шаблонами соответствует разбор случаев, применению функции — modus ponens, абстракции — вывод из гипотез. _ означает, что значение не используется.
код: [ скачать ] [ спрятать ] код: [ скачать ] [ показать ] Используется синтаксис Haskellimport 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 --
гляньте на мои определенияЕсли там не всё так очевидно, допишу типы используемых, скажем, примитивов (хотя они определяются). Конструкторы значений, соответствующие аксиомам/правилам введения связок:
Читайте также: