증명과 프로그램은 어떻게 같은 구조를 가질까?

그림에서 무엇을 볼까요?

논리곱은 값의 쌍, 논리합은 표시가 붙은 선택, 함의는 입력을 출력으로 바꾸는 함수와 대응한다는 세 줄 도식.

LTCT 가상 활동에서 P는 ‘초록 카드가 있다’, Q는 ‘번호표가 있다’라고 하겠습니다. P∧Q를 구성하려면 두 증거를 한 쌍으로 묶습니다. P∨Q라면 어느 쪽 증거를 넣었는지 표시해야 합니다. P→Q라면 P의 증거를 받았을 때 Q의 증거를 만드는 절차가 필요합니다.

아래 선택 상자에서 논리식과 프로그램 구성을 바꾸어 보세요. ‘P∧Q’에 P만 넣으면 결론의 일부만 마련한 상태입니다. ‘P→Q’에 함수 구성을 연결하면 입력 증거가 출력 증거로 변환되는 경로가 드러납니다. 화면의 판정은 세 대응을 익히기 위한 작은 형식 모형입니다.