1 1 -(Pv-P) 전제도입
2 2 P 전제도입
2 3 Pv-P 선언도입 2
1,2 4 (Pv-P)&-(Pv-P) 연언도입 1,3
1 5 -P 귀류법 1,2,4
1 6 Pv-P 선언도입 5
1 7 (Pv-P)&-(Pv-P) 연언도입 1, 6
0 8 --(Pv-P) 귀류법 1,6,7
0 9 Pv-P 이중부정 8
ㅁ
Pv-P는 전제없이 도출 됨. 따라서 이체계(표준적인 명제논리 체계)의 정리임.(Df teorem 체계의 규칙들을 사용해 전제없이 도출 됨. ㅏP)
2. 의도된 체계에 따라 다르긴 하지만 예를들어 레먼 노테이션에서는 정리(theorem)들을 정리도입규칙(TI :: theorem introduce)으로 임의의 행에 도입할 수 있음. 그런 규칙이 없다면 그냥 증명열 도중에 넣어서 증명하면 끝.
댓글 0