논리학 기초

‘증명할 수 있다’를 논리 기호로 만들면 무엇이 달라질까?

증명가능성 논리는 ‘이 문장은 어떤 형식 체계에서 증명된다’를 상자 기호로 다루며, 자기언급과 괴델의 불완전성 정리를 한 언어 안에서 분석합니다.

그림에서 무엇을 볼까요?

명제 A, A가 증명 가능하다는 상자 A, 상자 A이면 A라는 반성 원리, 그리고 이를 다시 상자로 감싼 뢰프 조건을 층별로 보여 주는 도식.

LTCT가 만든 비유입니다. 채점 규칙 T가 있고 □A를 ‘T의 규칙으로 A에 만점 증명이 있다’로 읽습니다. A 자체와 □A, 그리고 □A→A는 서로 다른 주장입니다.

채점표에 답이 있다는 사실과 그 답이 실제로 맞다는 사실을 합치려면 채점 규칙의 건전성에 대한 외부 점검이 필요합니다. 체계가 자기 규칙의 무오류를 스스로 선언했다고 해서 외부 검증이 끝나는 것은 아닙니다.

SEP는 분야의 동료검토 백과 해설이지 새 참가자를 모집한 실험 연구가 아닙니다.

□의 의미는 특정 형식 이론과 증명 부호화에 상대적이므로 자연어의 ‘알 수 있다’ 전체를 대신하지 않습니다.

□A와 A가 같은 뜻이라면 왜 증명가능성 논리가 필요할까요?