양상논리학에서는 다음과 같은 추론 규칙이 있다.
~◇~ = □
~□~ = ◇
즉, '□'를 '필연적으로'라고 해석하고, '◇'를 '가능하게'라고 해석할 때, 전자는 '~◇~'와 동치이고, 후자는 '~□~'와 동치이다. 이를 다음과 같이 자연연역으로 증명할 수 있다.
증명:
1. □(∃x)Fx
∴ ~◇~(∃x)Fx
2. asm: ◇~(∃x)Fx
3. [W] ~(∃x)Fx 2, WI
4. [W] (∃x)Fx 1, WI
∴ 5. ~◇~(∃x)Fx 2-4, RAA
Q.E.D.
증명:
1. ◇(∃x)Fx
∴ ~□~(∃x)Fx
2. asm: □~(∃x)Fx
3. [W] (∃x)Fx 1, WI
4. [W] ~(∃x)Fx 2, WI
∴ 5. ~□~(∃x)Fx 2-4, RAA
Q.E.D.
말하자면, 임의의 술어 'F'와 그에 대한 존재양화에 대해서 위의 양상 기호들이 서로 동치라는 것을, 위와 같이 자연연역으로 증명할 수 있다. 귀류법을 위해서 결론의 역을 증명과정 2번에서 가정하고, 증명과정 3번과 4번에서 가능세계 예화를 '가능하게'와 '필연적으로'에 해당하는 구조 순으로 각각 한 다음에, 증명과정 3번과 4번에서 모순이 발생함을 본다. 그래서 증명과정 5번에서, 증명과정 2번의 역, 즉 결론의 역의 역이 옳다는 것이 뒤따른다. 요시!!! 스바라시!!!
