|
В ходе доказательства одной секвенции, столкнулся с необходимостью доказать следующую: задан 4 Июн '15 16:23 
gibsonman01 |
|
Здесь вообще-то желательно знать точный список используемых аксиом и правил вывода -- они могут быть разными, как и языки программирования. Но общая суть вот какая. Доказываем от противного, предполагая $%\bar{Z}$%. Тогда у нас есть как $%Y$%, так и $%\bar{Z}$%, поэтому конъюнкцию $%Y\land\bar{Z}$% можно считать доказанной. Используя первую импликацию, по правилу modus ponens выводим $%\bar{X}\lor Z$%. Учитывая, что $%X$% нам дано, отсюда по одному из правил или по одной из аксиом должно вытекать $%Z$%. Это приводит к противоречию. отвечен 4 Июн '15 16:50 
falcao Аксиомы всего три: $$A \to (B \to A)$$ $$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$$ $$(\bar{B} \to \bar{A}) \to ((\bar{B} \to A) \to B)$$ Правило одно - modus ponens.
(4 Июн '15 17:05)
gibsonman01
@gibsonman01: это известная система правил, но в неё используется минимальное число связок -- только отрицание и импликация. У Вас же в формулах присутствуют конъюнкция и дизъюнкция. Понятно, что обе они выражаются (хотя это по-разному можно делать), но вообще-то при использовании такой версии исчисления высказываний надо все формулы давать с нужным набором связок.
(4 Июн '15 17:14)
falcao
@falcao: тогда задача переформулируется $$\overline {Y \to \overline{\overline{Z}}} \to (\overline{\overline{X}} \to Z), X, Y \vdash Z$$
(4 Июн '15 17:27)
gibsonman01
@gibsonman01: с большим числом двойных отрицаний вывод будет слишком длинным. Я могу предложить более простую "адаптацию". Вместо $%\bar{X}\lor Z$% пишем $%X\to Z$%. Далее, конъюнкцию в посылке импликации вида $%A\land B\to C$% удобно переработать в $%A\to(B\to C)$%. Если это годится, могу написать соответствующий вывод. То есть первая формула там будет $%Y\to(\bar Z\to(X\to Z))$%.
(4 Июн '15 17:35)
falcao
@falcao: а как доказать следующую секвенцию? $$ (\overline{(\overline{\overline{X}} \to Z}) \to \overline{\overline{(Y \to \overline{\overline{Z}})}}) \vdash ((\overline{\overline{\overline{X}} \to \overline{Y}}) \to Z) $$ Я пробовал использовать 2, 6, 7, 9 секвенции и схему 3, но ничего не вышло.
(5 Июн '15 23:24)
gibsonman01
Секвенции: $$ 1. \space\space A \to B, B\to C \vdash A \to C $$ $$ 2. \space\space A \to (B \to C), B \vdash A \to C $$ $$ 3. \space\space \vdash(\bar{\bar{A}} \to A) $$ $$ 4. \space\space \vdash(A \to \bar{\bar{A}}) $$ $$ 5. \space\space \vdash (A \to (\bar{A} \to B)) $$ $$ 6. \space\space \vdash (\bar{B} \to \bar{A}) \to (A \to B) $$ $$ 7. \space\space \vdash (A \to B) \to (\bar{B} \to \bar{A}) $$ $$ 8. \space\space \vdash (A \to (\bar{B} \to \overline{A \to B})) $$ $$ 9. \space\space \vdash ((A \to B) \to ((\bar{A} \to B) \to B)) $$
(5 Июн '15 23:24)
gibsonman01
Можно в правой части выделить конъюнкцию и использовать её свойства, получим, что $$ \bar{\bar{X}} и Y $$, далее их использовать для вывода из левой части Z, а после один раз использовать теорему дедукции.
(5 Июн '15 23:27)
gibsonman01
@gibsonman01: Вы не могли бы сделать это отдельным вопросом? Я боюсь, что в комментарии ответ может не уместиться. Правильно ли я понимаю, что обилие двойных отрицаний в условии -- это так и должно быть? Без двойных отрицаний всё получается очень просто.
(5 Июн '15 23:37)
falcao
показано 5 из 8
показать еще 3
|