Языковое доказательство и логика Глава 13 Вопрос 49 Помощь

Конец не должен быть мутным. Конец — это то, с чего вы начинаете, а затем продвигаетесь вперед.

Посмотрите, с чего вы начинаете и куда хотите пойти.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|   :
|   :
|  Ex (P(x) ^ Ay (P(y) -> y=x)     ...

Ясно, что вы должны ввести эту экзистенциальную предпосылку, и лучший вариант — исключить экзистенциальную предпосылку.

|  Ex P(x)                         Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)    Premise
|  |_ [a] P(a)                     Assumption
|  |   :
|  |   :
|  |  P(a) ^ Ay (P(y) -> y=a)      ...
|  |  Ex (P(x) ^ Ay (P(y) -> y=x)) Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Elimination

Теперь у вас есть универсал, который нужно исключить (дважды) и один ввести; а также союз.

|  Ex P(x)                            Premise
|_ Ax Ay ((P(x) ^ P(y)) -> x=y)       Premise
|  |_ [a] P(a)                        Assumption
|  |  |_ [b]                          Assumption
|  |  |  |_ P(b)                      Assumption
|  |  |  |  Ay ((P(a) ^ P(y)) -> a=y) Universal Elimination
|  |  |  |  (P(a) ^ P(b)) -> a=b      Universal Elimination
|  |  |  |   :
|  |  |  |   :
|  |  |  |  b=a                       ...
|  |  |  P(b) -> b=a                  Conditional Introduction
|  |  Ay (P(y) -> y=a)                Universal Introduction
|  |  P(a) ^ Ay (P(y) -> y=a)         Conjunction Introduction
|  |  Ex (P(x) ^ Ay (P(y) -> y=x))    Existential Introduction
|  Ex (P(x) ^ Ay (P(y) -> y=x))       Existential Elimination

Я уверен, что вы можете завершить. Добавлю подсказку: Введение о равенстве говорит b=b.

Следующее доказательство аналогично предложенному Грэмом Кемпом. Отличие заключается в том, что я использую первые восемь строк доказательства OP, демонстрируя использование другого средства проверки доказательств и предлагая способ понять правила идентификации.

В этом доказательстве обратите внимание, что a = b в строке 8 становится b = a в строке 10. Чтобы получить этот результат, я должен ввести тождество в строке 9, a = a . Мне не нужно ссылаться на какую-либо строку, чтобы ввести эту личность. Наличие этой строки дает мне строку, в которой я могу сделать замену, когда я использую устранение личности.

Устранение личности настолько просто, что легко пропустить то, что происходит. Вот как это описывает Фредерик Фитч (14.3, стр. 81):

Предположим, что (...a...) — это любое предложение, в котором упоминается a , и что (...b...) является результатом замены b на a в одном или нескольких местах в (...a... ) . В соответствии с этим правилом [устранения идентичности] мы можем вывести (...b...) из (...a...) и [a = b] .

В приведенном выше доказательстве тождество, необходимое для этого правила, находится в строке 8, a = b , а предложение, упоминающее a, в котором мы будем заменять b на a , — это строка 9, a = a , та самая, которую мы ввели как личность. Строка 9 теперь рассматривается не как тождество, а как предложение, содержащее . Мы заменяем только первую a в строке 9, оставляя другую. Это позволяет нам вывести строку 10: b = a .

---

Ссылка

Fitch, FB, Символическая логика: введение, 1952.

Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/