분해 증명

논리학에서 분해 증명(Resolution) 혹은 분해법이란 증명의 방법론 중의 하나이다. 1965년에 미국의 존 앨런 로빈슨(John Alan Robinson)이 공식적으로 제안하였다. 이것은 어떤 두 명제가 논리합으로 이어져 있을 때 다른 명제를 도입하여 증명하는 방법이다. 형식적으로 볼 때, 이는 추이 법칙 혹은 삼단논법의 일반화로 볼 수 있다.

공식화

논리적 기호와 연결사들을 이용하면, 분해 증명은 다음과 같이 표현될 수 있다.

[(P OR R) AND (NOT R OR Q)] ⇒ (P OR Q)

이 진술이 타당함은 진리표 등을 이용해 보일 수 있다. 여기서는 귀류법과 양도 논법을 사용해서 증명해 보자. 결론을 부정해서 P도 Q도 거짓이라고 가정한다. 이때 만약 R이 참이라면 NOT R이 거짓이므로 (NOT R OR Q)이 거짓이고, R이 거짓이라면 (P OR R)이 거짓이 된다. 어느 쪽도 좌변은 거짓이 되므로, 이는 모순이다. 따라서 원 명제는 참이다.

이 증명 방법을 이용하는 방법은 다음과 같다. 먼저 증명하고자 하는 명제 (P OR Q)를 고른다. 그러고 나서, 적절한 명제 R을 찾아내어서 좌변의 명제 조건이 만족됨을 보인다. 그러면 원론적으로 증명이 종료된다.

증명의 기법

그러나 이 논법을 증명에 막상 응용하려 할 때는 막연하여 쓸모가 없는 것처럼 보일 수 있는데, 좌변의 형식에서 P와 NOT R 혹은 R과 Q의 두 쌍 중 하나의 쌍에 속하는 명제들이 동시에 참임을 보여야 하기 때문이다. 그러므로, 이 조건을 실제적으로 응용하기 위하여 많은 경우 양도 논법과 결합하여 사용하는 것이 현실적이다. 새로운 명제 S를 도입하여,

(S → (P AND NOT R)) AND (NOT S → (R AND Q))

의 논리식을 도출할 수 있는데, 이 식은 위 식의 좌변을 함의한다. 이 역시 귀류법으로 증명할 수 있다. 만약 위 식의 좌변이 참이 아니라면, P와 NOT R 혹은 R과 Q의 두 쌍의 명제들은 결코 동시에 참이 될 수 없다. 따라서, 새로운 식의 AND 양쪽 가언문의 후건들은 모두 거짓이 된다. 그런데 S와 NOT S 중 하나는 항상 참이므로 전체 문장은 결코 참일 수 없다.

이로부터, 삼단논법에 의하여

[(S → (P AND NOT R)) AND (NOT S → (R AND Q))] ⇒ (P OR Q)

의 결론을 얻는다.

응용

이 방법을 이용하여 실제로 명제를 하나 증명해 보자. 우선 다음과 같은 상황을 가정한다.

철수는 먹으면 반드시 10시간 후에 죽는 농약을 치사량만큼 먹었다.

이제 증명할 명제는,

철수가 오늘 죽거나(P) 내일 죽는다.(Q)

라는 것이다. 먼저 상황 조건으로부터 다음과 같은 명제를 얻는다.

철수는 농약을 먹은 지 10시간 후에 반드시 죽는다.

그리고, 다음과 같은 명제를 양도 논법의 전건으로 가정하자.

철수가 농약을 먹은 시간이 14시 이전이다.(S)

이 때 소거할 명제 R을 NOT S로 놓고 위의 양도 논법과 결합한 형식을 사용하면, 증명이 끝난다.

삼단 논법의 유도

P의 자리에 NOT P라는 명제를 대입하고 나서, 다음의 논리식을 이용하면,

NOT P OR Q = P → Q

분해 증명을 삼단 논법 형식으로 전환시킬 수 있다.

같이 보기

참고 문헌

Richard Johnsonbaugh, 『이산수학』, 한티미디어, 2008

외부 링크

Alex Sakharov. “Resolution Principle”. 《Wolfram MathWorld》 (영어). Wolfram Research.
Alex Sakharov. “Resolution”. 《Wolfram MathWorld》 (영어). Wolfram Research.