|
С помощью правил естественного вывода доказать выводимость формулы в теории L. Правилом замены эквивалентным не пользоваться. (¬(¬X ∪ Z) ⊃ ¬(Y ⋂ ¬Z)) ≡ (¬ X ∪ ¬Y ∪ Z) задан 11 Окт '17 20:48 
flamingo
показано 5 из 9
показать еще 4
|
Здравствуйте
Математика - это совместно редактируемый форум вопросов и ответов для начинающих и опытных математиков, с особенным акцентом на компьютерные науки.
Присоединяйтесь!
отмечен:
задан
11 Окт '17 20:48
показан
741 раз
обновлен
23 Окт '17 1:40
Связанные вопросы
Дизайн сайта/логотип © «Сеть Знаний». Контент распространяется под лицензией cc by-sa 3.0 с обязательным указанием авторства.
@flamingo: логические исчисления -- это примерно как языки программирования. Под L можно понимать, вообще говоря, что угодно. Такое обозначение есть в учебнике Мендельсона, то там логическими связками являются только отрицание и импликация. Нужно точное описание правил. Естественный вывод -- это очень хорошая современная идея, и её я бы применял как можно чаще. Но без дополнительной информации тут в принципе ничего сделать нельзя.
Наверное, вместо объединения и пересечения там всё-таки дизъюнкция и конъюнкция?
@falcao Да, дизъюнкция и конъюнкция, конечно
@flamingo: а где ссылка на описание исчисления? Я вроде бы привёл доводы в пользу того, что она обязательна. Почему-то примерно в 90% случаев приходится вещи этого рода дополнительно уточнять.
Вот представьте себе, что кто-то просит написать программу для нахождения, скажем, суммы двух чисел. Вроде бы просто, но на каком языке программирования? Их же целая куча, и везде свои правила синтаксиса. Так же и с исчислениями.
@falcao https://studopedia.su/4_24911_aksiomaticheskaya-teoriya-L-ischisleniya-viskazivaniy.html что-то в этом роде
@flamingo: эта ссылка не соответствует Вашему условию. По ней L означает то же, что в Мендельсоне, и это хорошо известная вещь. Но там нет в сигнатуре конъюнкций или дизъюнкций. Кроме того, правила естественного вывода -- вещь более современная. Мендельсон был издан очень давно. Это хорошая книга, но о естественном выводе там нет ничего. Хотя я всегда эти вещи трактовал именно в таком духе, и у меня даже некоторые заметки на эту тему были написаны.
@falcao Ну я так думаю, что (¬(¬X ∪ Z) ⊃ ¬(Y ⋂ ¬Z)) можно представить как (¬X ∪ Z) ∪ ¬(Y ⋂ ¬Z)). И тогда правомерно ¬X -> ¬X ∪ Z -> ¬X ∪ Z ∪ ¬(Y ⋂ ¬Z)). Аналогично из Z -> ¬X ∪ Z ∪ ¬(Y ⋂ ¬Z)). Но вот как без закона де Моргана вывести, что ¬Y -> ¬X ∪ Z ∪ ¬(Y ⋂ ¬Z)), я не знаю. Но вообще, насколько я поняла задание, можно использовать помимо импликации и отрицания конъюнкцию и дизъюнкцию, вместе с их выводами
@flamingo: мы не можем по своему усмотрению заменять формулы на логически эквивалентные. Должна быть задана чёткая система аксиом и правил вывода. Скорее всего, имелось в виду то, что здесь было выписано в одном из комментариев. При наличии чётких правил, я там изложил решение.
@falcao Да, наверно, те же правила, как и там. Исходя из этого в правую сторону получилось ¬X ∪ Z -> ¬X ∪ Z ∪ ¬Y, ¬Y ∪ Z -> ¬X ∪ Z ∪ ¬Y, и так как (¬(¬X ∪ Z) ⊃ ¬(Y ⋂ ¬Z)) можно представить как (¬X ∪ Z) ∪ ¬(Y ⋂ ¬Z)), то в правую сторону этого достаточно. Все же не могли бы вы, пояснить, как в левую сторону можно доказать?
@flamingo: я сейчас ещё раз окинул взором список правил, и понял, что эта система не полна, то есть в ней можно вывести не все тавтологии. Там нет правил, позволяющих что-либо извлечь из дизъюнкции. Не удивительно, что импликация справа налево не получается. Ведь если дизъюнкцию переинтерпретировать, и считать, что она всегда истинна, то все правила останутся корректными, но система явно будет неполна. Поэтому нужно уточнить постановку задачи у того, кто её предложил.