파이썬으로 귀류법 검증하기
귀류법(Reductio ad Absurdum)을 코드로 구현해 봅시다.
0. 들어가며
인공지능으로 생성한 귀류법을 의인화 한 이미지지난번 글에서 귀류법을 울프럼 언어로 구현해 보았습니다. 이글에서는 귀류법을 우리에게 친숙한 파이썬 언어로 구현해 보겠습니다. 귀류법 자체에 대한 자세한 내용은 저의 이 글에서 확인 하 실 수 있습니다.
귀류법(Reductio ad Absurdum, RAA)은 수학과 논리학에서 매우 중요한 증명 기법입니다. 어떤 명제를 증명할 때, 그 명제의 '부정'을 가정한 뒤 모순(contradiction)이 도출됨을 보임으로써, 원래 명제가 참임을 결론짓습니다. 이는 고전 논리(Classical Logic) 체계에서 광범위하게 활용되는 증명 방식이며, 직관적으로도 "가정이 모순을 일으키니, 그 가정은 틀린 것이고 반대쪽이 참"이라는 논리를 체계화한 것입니다.
이 글에서는 파이썬(Python)을 이용해 귀류법이 고전 논리에서 항상 참(항진명제, tautology) 임을 직접 전수 검사 방식으로 간단히 확인해 보겠습니다.
핵심 아이디어
"(가정 P와 ¬Q를 함께 두면 모순이 발생)"이라는 전건으로부터 "(P라면 Q)"를 도출하는 명제 논리가 모든 경우에 대해 언제나 참인지 확인합니다.
이와 더불어, "그 역방향 식 역시 언제나 참인지, 그리고 두 식이 서로 동치인지도" 함께 확인합니다.
1. 논리적 배경
1.1. 고전 명제 논리에서의 기호
P, Q: 불리언 변수. {False, True}만을 가정.
¬P: P가 거짓임을 뜻하는 부정(negation).
P∧Q: P와 Q가 모두 참임을 뜻하는 논리곱(AND).
P∨Q: P 혹은 Q 중 최소 하나가 참임을 뜻하는 논리합(OR).
P→Q: P가 참이면 Q도 참이라는 함의(implication). 보통 "¬P∨Q"와 동치.
⊥: 모순(contradiction) 또는 '거짓(False) 임이 명확한 상태'.
1.2 귀류법(정방향)과 그 역방향
정방향: ((P∧¬Q)→⊥)→(P→Q)
이는 "P와 ¬Q를 동시에 가정하면 모순이 생긴다"라는 가정이 참일 때, "P라면 Q"가 성립한다는 내용입니다.
역방향: (P→Q)→((P∧¬Q)→⊥)
이는 “P→Q가 참이라면, P와 ¬Q를 동시에 가정할 수 없어서 모순이 난다”는 식으로, 사실상 위 식의 역을 표현한 것입니다.
고전 논리에서는 ((P∧¬Q)→⊥)⟺(P→Q)
라는 동치가 항상 성립함이 알려져 있습니다.(정방향과 역방향 모두가 항진명제임을 진리표로도 쉽게 증명할 수 있습니다.) 이번 글에서는 "파이썬으로 이러한 사실을 간단히 확인해 보는 시도"를 해볼 것입니다.
2. 파이썬 코드
아래 코드는 네 부분으로 구성됩니다.
implies(a, b): 함의(implication) 연산을 파이썬의 부울(bool) 로직으로 직접 정의하는 함수
check_reductio_ad_absurdum(): 정방향 귀류법 식이 모든 P, Q 조합에 대해 참인지 확인
check_converse_reductio(): 역방향 귀류법 식이 모든 P, Q 조합에 대해 참인지 확인
check_equivalence_of_two(): 두 식이 모든 P, Q 조합에서 동일한 진리값을 갖는지(동치성) 검사
아래는 파이썬으로 귀류법을 구현한 전체 코드입니다. 주석을 아주 자세하게 첨부했기 때문에 코드를 쉽게 이해하실 수 있을 것입니다.
https://gist.github.com/otter275/2ab6f1036df06c4cb5d9124e41b69dfc#file-_-nb
2.1. 코드에 대한 해설
1. implies(a, b)
a→b를 (not a) or b로 구현한 것입니다.
고전 논리에서 "a→b"는 "¬a∨b"와 동등한 의미입니다.
2. check_reductio_ad_absurdum()
"((P∧¬Q)→⊥)→(P→Q)"라는 식을 4가지 경우 (P, Q)∈{(F, F), (F, T), (T, F), (T, T)}에 대해서 평가합니다.
하나라도 거짓이 나오면 귀류법이 항진명제가 아닌 것으로 결론짓고 False를 반환. 전부 참이면 True.
3. check_converse_reductio()
"(P→Q)→((P∧¬Q)→⊥)"의 항진명제 여부를 같은 방식으로 전수 검사합니다.
4. check_equivalence_of_two()
정방향 식과 역방향 식이 각각의 (P, Q)에 대해 같은 진리값을 내는지, 즉 두 식의 평가 결과가 '모든 경우에 동일'하면 True를, 아니면 False를 반환합니다.
사실 고전 논리에서는 이 두 식이 동등함(진리표 등을 이용)을 쉽게 증명할 수 있으나, 여기서는 실제 코드를 통해 확인하는 것입니다.
3. 실행 결과 확인
정방향: ( (P and not Q) -> False ) -> (P -> Q )가 4가지 경우 모두에서 참임이 확인됨.
역방향: (P -> Q) -> ( (P and not Q) -> False ) 역시 4가지 경우 모두 참.
동치성: 결과가 전부 동일하므로, 두 식은 모든 (P, Q)에 대해 정확히 동일한 값을 가집니다(즉, 동치).
이로써 귀류법과 그 역방향이 고전 명제 논리에서 항진명제임을, 실제 부울 연산자 수준에서 재확인했습니다. 즉, "(P∧¬Q)→⊥"가 "P→Q"와 동일함을 파이썬 코드로도 확인 해 본 것입니다.
4. 귀류법 검증의 의의 및 한계
1. 직관적 의의:
귀류법이 "(가정 + 부정)으로부터 모순이 나오면, 결국 그 가정은 옳고 그 부정이 틀렸다"라는 추론 규칙이 언제나 성립함을 재확인하는 것은, 우리가 일상적으로 활용하는 증명 방식의 논리적 근거가 강건하다는 의미입니다.
컴퓨터를 통한 전수 검사(모든 경우의 수 확인)로 확인함으로써, 간단한 스케일에서나마 "항상 참"임을 직접 볼 수 있습니다.
2. 한계:
본 검사는 (P, Q) 두 변수만을 사용하는 매우 제한적인 전수 검사에 불과합니다.
실제 수학 증명에서는 훨씬 복잡한 명제, 술어, 무한 영역의 변수를 다루므로 이런 식으로는 포괄적으로 검증하기 어렵습니다.
더 정교한 자동 증명 이론(Automated Theorem Proving)이나 증명 보조 시스템(Proof Assistant) 등에서는 귀류법을 다양한 방식으로 형식화하여, 좀 더 일반적으로 귀류법의 타당성을 활용하고 있습니다.
3. 고전 논리 vs. 직관주의 논리:
여기서는 고전 논리(Classical Logic) 체계에서 "¬¬P ⟹ P"가 받아들여지므로 귀류법이 성립합니다.
직관주의 논리(Intuitionistic Logic)나 구성주의 논리(Constructive Logic)에서는 귀류법의 일부 형태가 수용되지 않는 경우도 있으므로, "모든 논리 체계에서 언제나 성립한다"라고 말하기에는 주의가 필요합니다.
5. 맺음말
이번 글에서는 파이썬 코드를 이용해 귀류법의 논리적 정당성을 직접 시뮬레이션해 보았습니다.
(정방향) "(P∧¬Q)→⊥"를 전건으로 "P→Q"를 도출하는 구조,
(역방향) "P→Q"에서 "(P∧¬Q)→⊥"가 성립하는 구조,
이 모두 네 가지 간단한 부울 조합에서 전혀 모순 없이 참값을 반환함을 코드로 확인한 것입니다. 이로써, 귀류법이 고전 논리에서 항진명제임을 매우 기초적인 수준에서 전수 검증했다고 볼 수 있습니다.
물론 실제 수학에서는 훨씬 복잡한 명제들을 다루므로, 이런 식의 전수 검사는 그저 직관적 이해를 돕는 작은 예시일 뿐입니다. 그러나 한 번쯤 컴퓨터 언어(파이썬)를 통해 "논리를 직접 확인해 본다"는 경험은, 논리학과 컴퓨터 과학의 연계를 체감하기에 좋은 학습 방법이 될 것입니다.
