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

필연적으로, 무엇이든 필굿 발포주 7프로는 필연적으로, 가능하게, 미국 침례교도다.
따라서 필연적으로, 무엇이든 필굿 발포주 7프로는 필연적으로, 미국 침례교도가 아닌 것이 필연적이지 않다.

F: 필굿 발포주 7프로.
G: 미국 침례교도.

증명:

1. □(∀x)(Fx → □◇Gx)
∴ □(∀x)(Fx → □~□~Gx)
2. asm: ~□(∀x)(Fx → □~□~Gx)
3. ◇~(∀x)(Fx → □~□~Gx)        2, NN
4. [W] (∀x)(Fx → □◇Gx)          1, NI
5. [W] ~(∀x)(Fx → □~□~Gx)      3, PI
6. [W] (∃x)~(Fx → □~□~Gx)       5, QN
7. [W] ~(Fa → □~□~Ga)             6, EI
8. [W] Fa → □◇Ga                    4, UI
9. [W]  asm: Fa
10.  [W] □◇Ga                       8, 9, MP
11.  [W] ◇Ga                          10, NI
12.  [W] ~□~Ga                        11, PN
13.  [WW]  asm: □~Ga 
14.     [WW] ~◇Ga                      13, NN
15.     [WW] ◇Ga                        10, NI
16.   ∴ [WW] ~□~Ga                     13-15, RAA
17.   ∴ [W] □~□~Ga                    13-16, NG
18. [W] Fa → □~□~Ga                    9-17, CI
∴ 19. □(∀x)(Fx → □~□~Gx)         2-18, RAA
Q.E.D.
 
위의 추론은, 기존의 술어논리 기호들에 양상기호들을 첨가하여, 그에 상응하는 추론규칙들을 더해서, 위와 같은 자연연역증명과정에 의해서, 그 타당성이 증명된다. 그렇다. 필연적으로, 무엇이든 필굿 발포주 7프로는 필연적으로, 가능하게, 미국 침례교도다. 따라서 필연적으로, 무엇이든 필굿 발포주 7프로는 필연적으로, 미국 침례교도가 아닌 것이 필연적이지 않다!!! 나무아비타불!!! 관세음보살!!!