Контрольный вопрос по языковой логике: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]

Вот доказательство с использованием средства проверки доказательства естественной дедукции в стиле Fitch.

Чтобы составить правильно построенные предложения, мне пришлось переписать некоторые имена, используемые в примере ОП. Вместо «E» я использовал «P», так как «E» — это символ квантора существования в этой программе проверки доказательств. Кроме того, обозначения в этом средстве проверки доказательств более компактны. Например, «E(x,y)» стало «Pxy».

Вместо того, чтобы начинать с отрицания заключения, я удалил знак отрицания из заключения, чтобы ввести отрицание в конце, что я и сделал в строке 12.

От строки 2 до строки 10 я использовал вспомогательное доказательство, чтобы начать попытку исключить квантор существования (∃E в строке 11), взяв имя «a» для переменной «x». Я использовал то же имя, чтобы исключить квантор универсальности (∀E) в строке 3. Это позволило мне использовать закон исключенного третьего (LEM), чтобы прийти к противоречию в строке 10, отбросив предположения, сделанные в строках 4 и 7, закрыв поддоказательства.

Строка 10 позволила мне исключить квантор существования в строке 11, отменив предположение в строке 2. Противоречие в строке 10 позволило мне ввести отрицание в строке 12 и завершить доказательство.

---

использованная литература

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

PD Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикшированный и отредактированный Аароном Томасом-Болдуком, Ричардом Заком, forallx Calgary Remix: An Introduction to Formal Logic, зима 2018 г. http://forallx.openlogicproject.org

Я сам не использовал/не преподавал LPL, поэтому я не знаю формата или стандартов для завершения проверки RAA. Строки с отступом 1-4 верны; для строки без отступа 2 либо она искажена (Eaa, если и только если E?), либо я не понимаю, как ее анализировать.

На моих курсах логики я, вероятно, принял бы 4 как достаточное, чтобы показать, что 1 приводит к противоречию, КЭД.

Чтобы доказать ~P, начните с предположения P с целью демонстрации противоречия. Таким образом, используйте «введение отрицания». (Примечание: не допускайте двойного отрицания, если вы можете его избежать, особенно если ваш первый шаг состоит в его устранении.)

Чтобы получить противоречие от ƎxⱯy Qxy, используйте правила конкретизации квантора и покажите, что Qba является противоречием для свидетеля b и произвольного a (которым, возможно, может быть и b).

Чтобы получить противоречие от Eba <-> ~Eaa, для свидетеля b и произвольного a, заметьте, что когда a есть b, у вас есть противоречие. Итак, ваше универсальное устранение является свидетелем экзистенциального.

Подводя итог: мы должны принять ƎxⱯy (Exy <-> ~Eyy), затем предположить свидетеля [b] для экзистенциального, то есть Ɐy (Eby <-> ~Eyy), чтобы мы могли устранить это универсальное для свидетеля, поэтому Ebb <-> ~Ebb, и показать, что это противоречие, что позволяет нам, таким образом, снять допущения и закончить введением отрицания.

Демонстрация того, что Ebb <-> ~Ebb является противоречием, — это просто вопрос использования устранения отрицания и устранения биусловий. Предполагая, что Ebb выводит противоречие из бикондиционала, тем самым вводя отрицание. ~Ebb также выводит необходимое противоречие из бикондиционала.

 |_
 |  |_ Ǝx Ɐy (Exy <-> ~Eyy)
 |  |  |_ [b] Ɐy (Eby <-> ~Eyy)
 |  |  |  Ebb <-> ~Ebb
 |  |  |  |_ Ebb
 |  |  |  |  ~Ebb
 |  |  |  |  ┴
 |  |  |  ~Ebb
 |  |  |  Ebb
 |  |  |  ┴
 |  |  ┴
 |  ~Ǝx Ɐy (Exy <-> ~Eyy)

Утверждение ¬∃x∀y[E(x,y)⟷¬E(y,y)] эквивалентно, используя свойства отрицания, для

∀x∃y{[E(x,y)∧¬E(y,y)]∨[¬E(y,y)∧¬E(x,y)]} .

Предложение в фигурных скобках всегда верно при y=x при использовании ¬¬E→E, и это доказывает утверждение. Это доказательство имеет то преимущество, что позволяет избежать использования reductio ad absurdum и, следовательно, закона исключенного третьего; однако он использует тот факт, что ¬¬E→E. Следовательно, это доказательство неприемлемо в интуиционистской логике . Утверждение ОП является теоремой классической логики, но не более слабой интуиционистской логики.