양상논리 추론 자연연역 증명하기 행복한 논리학

필연적으로, 무엇이든 바르트주의자인 것은, 하이네켄 맥주 500밀리리터 캔이다.
필연적으로, 무엇이든 하이네켄 맥주 500밀리리터 캔인 것은, 어떤 주류와 동일하다.
따라서 필연적으로, 무엇이든 바르트주의자인 것은, 어떤 주류와 동일하다.

F: 바르트주의자
G: 하이네켄 맥주 500밀리리터 캔
H: 주류

증명:

1. □(∀x)(Fx → Gx)
2. □(∀x)(Gx → (∃y)(Hy & x = y))
∴ □(∀x)(Fx → (∃y)(Hy & x = y))
3. asm: ~□(∀x)(Fx → (∃y)(Hy & x = y))
4. ◇~(∀x)(Fx → (∃y)(Hy & x = y))      3, NN
5. [W] ~(∀x)(Fx → (∃y)(Hy & x = y))   4, PWI
6. [W] (∀x)(Fx → Gx)                      1, PWI
7. [W] (∀x)(Gx → (∃y)(Hy & x = y))     2, PWI
8. [W] (∃x)~(Fx → (∃y)(Hy & x = y))    5, QN
9. [W] ~(Fa → (∃y)(Hy & a = y))           8, EI
10. [W] Fa → Ga                             6, UI
11. [W] Ga → (∃y)(Hy & a = y)             7, UI
12. [W] Fa → (∃y)(Hy & a = y)             10, 11, CR
∴ 13. □(∀x)(Fx → (∃y)(Hy & x = y))    3-12, RAA
Q.E.D.

위의 추론은 양상논리 추론으로서, 필연성, 가능성 등의 양상적 개념들이 추론과정에 포함되고, 또한 추론의 타당성에 어떤 식으로든 기여하는 추론이다. 아울러 기존의 1차술어논리의 추론규칙들에 더해서, 양상기호가 포함되는 추론규칙들을 더하여, 위와 같이 귀류법으로 추론의 타당성을 검증해보아, 증명과정의 9와 12에서 모순이 발생하였다. 추론의 결론의 역을 가정하여 증명과정을 진행할 때, 증명과정에서 위와 같이 모순이 발생한다는 것은, 추론의 결론이 옳다는 것을 나타낸다. 요시- 스바라시- 오홈마니 반메홈-!!!