Formal   Proof

 

증명과정에서 나타나는 모든 명제는 어느것이나 그 정당한 도출근거 가 명시되어야 한다. 즉 그 앞에 나온 어떤 명제로부터 어떤 규칙에 의거하여 도출된 것인지를 표시하여야 한다. 그 표시는 각 명제 오른쪽 끝에 명시한다. 이런 형식의 증명법을 형식적 증명 (formal proof) 라 한다.

다음과 같은 추론을 증명해 보자.

결론 'I ∨∼R'를 얻으려면 세 가지 방법을 생각해 볼 수 있다.

첫째 교환규칙에 의하여 '∼R⊃I' 에서 도출하는 법, 둘째 부가규칙(add) 에 의한 방법, 셋째 CD에 의한 방법이다. 교환규칙에 의하려 하더라도 선언명제 '∼R∨I' 를 얻어야 하며, 부가규칙에 의하려면 'I'와 '∼R'를 분리시켜 얻어야 하는데 3개의 전제에서는 어려울 것 같다.

CD 에 의한 방법을 모색해 보자. 'I ∨∼R'을 CD에 의해서 도출하려면 'I'와 '∼R'을 각각 후건으로 하는 두 개의 가언명제와 그 전건들을 선언적으로 긍정할 하나의 선언명제가 요구된다. 우선 1)에서 'W⊃I' 와 'L⊃∼R' 을 분리해 내고 'W∨L' 을 도출하면 CD가 가능할 것이다. 'W⊃I'와 'L⊃∼R'은 'G'와 '∼C'가 도출되면 각각 Modus Ponens 에 의하여 도출된다. 그런데 2)와 3)에서 MP에 의하여 'Gㆍ∼C'가 도출될 수 있으므로 이것을 Simp 하면 'G'와 '∼C'를 얻는다. 또 'W∨L' 은 3)에 'W'를 Add 하여 'L∨W' 를 얻고 이것을 Com 하면 얻을 수 있다. 이상의 추론절차를 역순으로 기호화하면 위의 추론은 다음과 같이 증명된다.

명제 앞의 숫자는 각 명제를 구별하기 위한 것이고 오른쪽 끝에 있는 숫자는 그 명제가 도출된 원명제를 가리키며 그 뒤의 약자는 도출할 때 사용된 추론규칙이다.