명제태도 문장들이 포함된 논리 증명 행복한 논리학

다음은 형식적으로 타당한 명제태도 포함 추론이다.

딕 아드보카트 감독은 어떤 포르투갈 축구선수들이 네덜란드 축구 선수들이라는 것을 믿는다.
딕 아드보카트 감독은 움베르토 코엘류 감독이다.
따라서 움베르토 코엘류 감독은 어떤 포르투갈 축구선수들이 네덜란드 축구 선수들이라는 것을 믿는다.

증명:

1. (∃x)(Fx & ~(∃y)(Fy & x ≠ y) & (∃z)(Gz & Kxz(Hz)))
2. (∀x)(Fx ↔ Jx)
∴ (∃x)(Jx & ~(∃y)(Jy & x ≠ y) & (∃z)(Gz & Kxz(Hz)))
3. asm: ~(∃x)(Jx & ~(∃y)(Jy & x ≠ y) & (∃z)(Gz & Kxz(Hz)))
4. (∀x)~(Jx & ~(∃y)(Jy & x ≠ y) & (∃z)(Gz & Kxz(Hz)))       3, QN
5. Fa & ~(∃y)(Fy & a ≠ y) & (∃z)(Gz & Kaz(Hz))               1, EI
6. Fa ↔ Ja                                                        2, UI
7. Fa → Ja                                                           6, BCR
8. Fa                                                               5, S
9. Ja                                                                7, 8, MP
10. ~(Ja & ~(∃y)(Jy & a ≠ y) & (∃z)(Gz & Kaz(Hz)))        4, UI
11. ~Ja ∨ (∃y)(Jy & a ≠ y) ∨ ~(∃z)(Gz & Kaz(Hz))          10, DM
12. (∃y)(Jy & a ≠ y) ∨ ~(∃z)(Gz & Kaz(Hz))                  9, 11, MTP
13. (∃z)(Gz & Kaz(Hz))                                            5, S
14. (∃y)(Jy & a ≠ y)                                              12, 13, MTP
15. ~(∃y)(Fy & a ≠ y)                                           5, S
16. (∀y)~(Fy & a ≠ y)                                           15, QN
17. Jb & a ≠ b                                                   14, EI
18. ~(Fb & a ≠ b)                                               16, UI
19. ~Fb ∨ a = b                                                   18, DM
20. a ≠ b                                                             17, S
21. ~Fb                                                           19, 20, MTP
22. Fb ↔ Jb                                                      2, UI
23. Jb → Fb                                                       22, BCR
24. ~Jb                                                             21, 23, MT
25. Jb                                                                17, S
∴ 26. (∃x)(Jx & ~(∃y)(Jy & x ≠ y) & (∃z)(Gz & Kxz(Hz)))    from 3; 24 contradicts 25.
Q.E.D.