Как можно доказать следующее утверждение в логике предикатов?

Вы можете доказать это, приняв отрицательный экземпляр и доказав противоречие:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Предположим.
{1} 2. ~(Fa → Ga) и ~(Ga → Fa) 1 DM
{1} 3. ~(Fa → Ga) 2 &E
{1} 4. ~(~Fa ∨ Ga) 3 МИ
{1} 5. Fa&~Ga 4 ДМ
{1} 6. Фа 5 и Е
{1} 7. ~(Ga → Fa) 2 &E
{1} 8. ~(~Ga ∨ Fa) 7 МИ                        
{1} 9. Ga & ~ Fa 8 DM
{1} 10. ~Fa 9 и E
{1} 11. Фа и ~ Фа 6,10 и I
- 12. ~~((Fa → Ga) ∨ (Ga → Fa)) 1,11 RAA
- 13. (Fa → Ga) ∨ (Ga → Fa) 12 ДНЭ
- 14. ∀x[(Fx → Gx) ∨ (Gx → Fx)] 13 УИ

Вот еще одна версия, которая не опирается на такие тождества, как закон ДеМоргана:

{1} 1. ~((Fa → Ga) ∨ (Ga → Fa)) Предположим.
{2} 2. Fa → Ga предполож.
{2} 3. (Fa → Ga) ∨ (Ga → Fa) 2 ∨I
{1,2} 4. ⊥ 1,3 &I
{1} 5. ~(Fa → Ga) 2,4 RAA
{6} 6. Ga → Fa Assum.
{6} 7. (Fa → Ga) ∨ (Ga → Fa) 6 ∨I
{1,6} 8. ⊥ 1,7 &I
{1} 9. ~(Ga → Fa) 6,8 RAA
{10} 10. Фа Ассум.
{11} 11. Га Усп.
{10,11} 12. Предположение Фа и Га.
{10,11} 13. Ga 12 и E
{11} 14. Fa → Ga 10,13 CP
{1,11} 15. ⊥ 5,14 РАА
{1} 16. ~Ga 10,15 РАА
{17} 17. ~Fa Assum.
{1,17} 18. ~Fa & ~Ga 16,17 &I
{1,17} 19. ~Ga 18 и E
{1} 20. ~Fa → ~Ga 17,19 СР
{11} 21. ~~Га 11 ДНР
{1,11} 22. ~~Fa 20,21 MT
{1,11} 23. Фа 22 ДНЭ
{1} 24. Ga → Fa 11,23 CP
{1} 25. ⊥ 9,24 &I
- 26. ~~((Fa → Ga) ∨ (Ga → Fa)) 1,25 RAA
- 27. (Fa → Ga) ∨ (Ga → Fa) 26 ДНЭ
- 28. ∀x[(Fx → Gx) ∨ (Gx → Fx)] 27 УИ

В следующем доказательстве используется закон исключенного третьего (LEM), а не доведение до абсурда (RAA) , используемый user3017 .

Поскольку заключение представляет собой дизъюнкт без посылок, а «Gx» есть в обоих дизъюнктах, я попытался построить доказательство из тавтологии «Ga ∨ ¬Ga».

В каждом случае я использовал условное введение (→I) в строках 4 и 10. Затем я использовал введение дизъюнкции (∨I), чтобы получить одинаковый результат для обоих случаев в строках 5 и 11.

В первом случае я использовал повторение (R), чтобы скопировать строку 1 в строку 3.

Во втором случае я использовал взрыв (X), чтобы получить желаемое следствие (Fa) в строке 9.

Получение одного и того же результата для обоих случаев позволило мне закрыть дополнительные доказательства для этих случаев, используя закон исключенного третьего (LEM) в строке 11.

В строке 12 я ввел квантор универсальности для завершения доказательства.

Более подробную информацию об этих правилах можно найти в forall x: Calgary Remix .

---

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

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

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