a
(Я не понимаю преимуществ этого перед таблицей истинности.)
Size: a a a
2021 November 16
s
Преимущество — уметь работать с формальными доказательствами. Так-то даже самая дохлая автоматизация может решить это без участия человека.
s
Да, кстати, все эти show писать не обязательно. Но полезно, чтобы доказательства не выглядели так, как типичные доказательства на Coq.
i
Можно через индикатор или через формальные доказательства
NC
Спасибо
a
Я б посмотрел на доказательство через индикатор.
s
Я даже нагуглить такое не могу.
s
Одна лишь индикаторная функция находится.
i
Да через нее
i
A and b =Ind A * Ind b
a
Ну да, а or?
i
Через деморгана
i
Not a = 1- Ind a
a
Угу, как раз через то, что надо доказать.
i
Для индикатора деморган просто доказывается
i
A or b = мах а,б
a
И что дальше?
a
Хотите сказать, доказательство не сведется к перебору вариантов?
X
тратить столько времени на банальные утверждения самим не жалко?
a
М.б. есть концептуальное доказателство, это было бы хорошо.
Рассмотрим категорию, где объекты утверждения, а стрелки это импликации (это примерно как топос, но все же куда слабее). not по идее должен быть эквивалентностью (?) этой категории и двойственной ей. Наши утверждения могли бы оказаться утверждениями о двойственности суммы и произведения.
Рассмотрим категорию, где объекты утверждения, а стрелки это импликации (это примерно как топос, но все же куда слабее). not по идее должен быть эквивалентностью (?) этой категории и двойственной ей. Наши утверждения могли бы оказаться утверждениями о двойственности суммы и произведения.