자연연역에 의한 타당성 증명 질문요!!!

[노랑이(112.163)]

이거 10번 11번 12번 왜 답지처럼 증명되는 거죠??? 독학의 한계를 뼈저리 느끼내요ㅠㅠ

[익명(223.62)]

정확히 뭐가 이해가 안가시나요?

[노랑이(118.39)]

가정부분이 잘 이해가 안되내요ㅠㅠ...

[익명(222.104)]

예를 들면, 10에서 ~도입 규칙을 쓰기 위해서, 결론과 반대인 ~C를 가정한 겁니다. 그걸 가정하면 모순이 나오면 ~도입 규칙에 의해 ~~C라 할 수 있고, 그건 다시 C와 같으니 증명이 끝나죠!

[노랑이(118.39)]

음 10번에서 4,7은 서로 왜 모순이 되는 걸까요??? 7번에서 3반복을 쓴 이유도 궁금해요ㅠ

[럿셀수리(114.200)]

즉 다음과 같이 말하는걸로 이해하셔도 됩니다.(간단한 연역절차 한정) 귀류법을 위해 결론인 C를 부정해 보자. 그럼 2에서 or가 제거되어 A가 유도된다. A가 나왔으니 1번에서 전건긍정을 쓸 수 있다. 그럼 B의 부정이 유도되는데 이는 전제 3과 모순이다. C의 부정과 1,2,3을가정하니 이런 모순이 나온다. C는 1,2,3으로부터 논리적으로 연역된다.

[PaulSohn(paulsohn)]

아마 저 책에선 ~도입이 (문장 X를 가정) - (가정 안에서 문장 Y와 그 부정 ~Y를 동시에 유도) - (가정 X를 해제하고 ~X로 결론지음) 순으로 구성되어 있을 겁니다. 핵심은 '가정 안에서' Y(여기선 B)와 ~Y(여기선 ~B)가 다 있어야 된다는 거고, 그래서 7행에서 B를 반복한 겁니다.

[노랑이(112.163)]

오오 그럼 11번문제 7번도 3과 모순 되니까 귀류법이 맞게 되는군요??? 감사합니다ㅠㅠ

[익명(222.104)]

좀 지엽적인거지만 저건 귀류법이 아닙니다 ~도입이죠

[익명(222.104)]

오히려 ~~p에서 p를 얻는 과정이 귀류법에 가깝습니다

[PaulSohn(paulsohn)]

사견이지만 불필요한 구분이라고 봅니다. 귀류법은 알고리즘이 아니라 사고방식이기 때문에 "뭔가를 가정했더니 모순이라 가정의 부정이라 결론지었다" 면 족하며 그 가정이 꼭 부정문이어서 ~~제거를 써야만 귀류법이라 부른다는 법은 없습니다.

[익명(222.104)]

글쎄요. ~도입은 일반적으로 직관주의 논리에서도 받아들여지는 규칙이라 ~의 정의라고 생각하는게 더 낫지않을까 합니다. 직관주의자도 귀류법을 받아들인다고 말하는 것이 아니라면요.

[PaulSohn(paulsohn)]

저는 귀류법(=proof by contradiction)의 본질이 ~도입이라고 봅니다. 이 관점에서는 물론 "직관주의자들도 귀류법을 받아들입니다". 고전논리와 직관주의논리가 갈리는 부분은 귀류법 자체가 아니라 "긍정문을" 귀류법으로 증명할 수 있느냐입니다.

[PaulSohn(paulsohn)]

즉, 일반적으로 proof of negation(혹은 nLab 표현으로 refutation by contradiction)이라고 표현하는 것과 귀류법을 용어상 딱히 구별할 필요가 없고 광의로 귀류법이라고 부르자는 게 제 입장입니다.

[익명(222.104)]

그렇군요. 설득력이 있는 말씀 같습니다. 귀류법은 특정 알고리듬이 아니라 사고방식이라는 말씀은 저도 동의합니다.

[익명(222.104)]

그런데 ~의 도입의 사고방식과 긍정문을 귀류법으로 증명할 때의 사고방식은 좀 다른 것 같습니다. 실제로 부정문은 딱히 다른 사고방식으로 증명할 방법이 없는 반면, 긍정문은 다른 방식으로도 충분히 증명할 수 있다는 점도 그렇고요. 이 둘은 공통점은 있으나 같은 사고방식이라고 묶는 것은 아주 와닫지는 않는군요. 어쨋든 이건 좀 철학적?인 문제 같네요.