논리학 기초

증명과 프로그램이 같은 구조라고 말할 수 있을까?

Wadler는 명제-유형 대응을 따라 논리의 증명 규칙과 함수형 프로그램의 형식 규칙이 어떻게 같은 구조를 이루는지 설명합니다.

그림에서 무엇을 볼까요?

A의 증거, 함수 A → B, B의 증거의 관계와 검토 지점을 설명하는 LTCT 교육용 도식.

전제 ‘x는 짝수’의 증거를 k라고 놓으면 x=2k입니다. 상자는 k를 입력받아 k+1을 출력하고, 이 값이 x+2가 짝수라는 증거가 됩니다.

그림의 화살표는 명제 A의 증거가 함수 A→B를 거쳐 명제 B의 증거로 바뀌는 구조를 보여 줍니다.

명제-유형 대응은 특정 형식 체계 사이의 정밀한 대응입니다. 자연어 논증 전체가 곧 프로그램이라는 뜻은 아닙니다.

본문의 LTCT 활동은 이론을 교육에 옮긴 제안이며 학습효과 자료가 아닙니다.

‘A이면 B’의 증명에서 A가 참이라고 선언하는 것만으로 충분할까요?