논리의 기초와 역사

논리 기호의 뜻을 진리표 없이 규칙으로 정할 수 있을까?

증명론적 의미론은 논리 기호의 뜻을 그 기호를 도입하고 제거하는 추론 규칙에서 찾습니다. 규칙 쌍의 ‘조화’가 왜 필요한지 반례와 함께 살펴봅니다.

‘그리고’의 뜻을 알려면 언제 문장이 참인지 먼저 말해야 할까요? 증명론적 의미론은 다른 길을 제안합니다. 어떤 주장을 어떻게 세울 수 있고, 그 주장을 얻은 뒤 무엇을 꺼낼 수 있는지를 규칙으로 설명하는 것입니다. Stanford Encyclopedia of Philosophy의 Schroeder-Heister 항목은 Gentzen의 자연연역 전통에서 도입 규칙이 논리 상수의 뜻을 정하고 제거 규칙은 그 정의가 허용한 범위 안에서 정당화된다는 생각을 정리합니다.

학술 자료의 내용

연구를 읽는 두 가지 질문

진리 대신 증명을 중심에 놓으면 무엇이 달라지나?

이 항목은 증명론적 의미론을 진리조건 의미론의 대안으로 소개합니다. 자연연역에서 ∧를 도입하려면 A의 증명과 B의 증명이 모두 필요하고, A∧B를 얻으면 A 또는 B를 제거 규칙으로 꺼낼 수 있습니다. 함의 A→B의 증명은 A의 증명을 받으면 B의 증명을 내놓는 구성적 기능처럼 읽힙니다. 핵심은 결론이 따라온다는 사실만이 아니라 어떤 가정과 규칙을 거쳐 결론에 이르는지입니다. [1]

왜 도입과 제거가 조화를 이뤄야 하나?

도입 직후 제거하는 우회는 더 짧은 증명으로 줄일 수 있어야 하고, 제거 규칙은 도입 규칙이 보장한 정보보다 더 많은 것을 빼내면 안 됩니다. SEP는 이 관계를 역전 원리 또는 조화라고 설명하며, ‘tonk’처럼 논리합의 느슨한 도입과 논리곱의 강한 제거를 섞으면 아무 관련 없는 주장까지 건너뛸 수 있음을 지적합니다. 다만 조화의 정확한 형식화에는 여러 견해가 있고 고전논리·부정·하위구조 논리로 가면 논쟁이 이어집니다. [1]

그림으로 생각하기

새 기호 ★를 발명해도 될까?

LTCT의 가상 기호 ★에는 ‘A만 증명해도 A★B를 만든다’는 도입 규칙이 있습니다. 그런데 제거 규칙으로 A★B에서 B를 꺼낼 수 있게 하면, 비가 온다는 증명만으로 달이 치즈라는 결론을 얻을 수 있습니다. 도입이 넣지 않은 정보를 제거가 꺼낸 것입니다.

아래 활동에서 기호를 ‘그리고’와 ‘가상 ★’ 중 고르고, 허용할 제거를 바꿔 보세요. 조화 검사는 도입 규칙이 제공한 보증 집합과 제거 규칙이 요구하는 보증을 비교합니다. 이는 SEP의 여러 형식 이론을 완전히 구현한 증명기가 아니라 핵심 직관을 보여 주는 유한 교육 모형입니다.

조화가 맞는 규칙 쌍은 학생에게 ‘이 기호를 썼을 때 무엇을 약속했는가’를 되묻게 합니다. 진리표 계산과 자연연역 규칙의 역할을 경쟁시키기보다 서로 다른 설명 수준으로 대조할 수 있습니다. 또한 도입-제거 우회를 직접 줄여 보게 하면 규칙이 단지 기호 조작이 아니라 정보 보증이라는 점이 드러납니다.

A와 B를 함께 넣어 A 그리고 B를 만든 뒤 A와 B를 각각 꺼내는 조화된 규칙과, A만 넣고 B를 꺼내는 불조화 규칙을 대비한 도식.
LTCT가 SEP의 도입·제거 규칙과 조화 설명을 바탕으로 새로 그린 개념 도식입니다. 원문 수식이나 그림을 복제하지 않았습니다. 그림 크게 보기 ↗
직접 조작하며 생각하기

기호와 제거 규칙을 바꾸어 조화를 검사하세요

도입 규칙이 보증한 정보와 제거 규칙이 꺼내려는 정보를 비교하세요.

조화 확인 · 도입이 보증한 정보만 꺼냅니다.

어디까지 말할 수 있을까요?

  • SEP 항목은 단일 실험이나 새 정리를 보고하는 논문이 아니라 2012년 처음 출판되고 2023년 개정된 전문 철학 백과의 종합 해설입니다.
  • 증명론적 의미론 내부에도 도입 우선, 제거 우선, 고전논리 처리 등 다양한 입장이 있습니다. 간단한 ★ 예시는 모든 조화 개념을 판정하지 않습니다.

원문에 근거한 한계와 LTCT의 적용 범위 검토입니다. [1]

배운 내용을 수업에 적용하기

교육 현장과 연결해 보면

논리 기호를 가르칠 때 진리표와 함께 ‘만드는 법’과 ‘사용하는 법’을 한 쌍으로 제시하고, 도입 직후 제거하는 우회를 지워 보게 할 수 있습니다.

평가에서는 규칙 이름 암기보다 새 기호의 도입·제거가 같은 정보 약속을 지키는지 반례를 구성하게 하면 추론 규칙의 의미를 확인할 수 있습니다.

한 번 더 생각하기

규칙만 일관되면 어떤 논리 기호든 좋은 정의인가요?

생각을 비교할 해설 펼치기

형식적 일관성만으로 충분하다고 단정할 수 없습니다. 도입과 제거의 조화, 정규화, 구조 규칙, 사용 목적을 함께 봐야 합니다. 이 글의 검사는 가장 기본적인 ‘넣지 않은 정보를 꺼내는가’만 확인합니다.

원문과 출처 정보

한국어 제목은 이해를 돕기 위한 LTCT 번역입니다. 한글 제목 뒤 괄호에 원제를 함께 표기했습니다. 저자·학술지·원문 버전은 원문 서지정보를 기준으로 확인할 수 있습니다.

  1. 증명론적 의미론 (Proof-Theoretic Semantics)

    Peter Schroeder-Heister (2023). Stanford Encyclopedia of Philosophy.

    자료 성격
    해외 대학 전문 철학 백과 · 공개 전문
    읽은 버전
    2012-12-05 초판, 2023-08-18 내용 개정판
    확인 범위
    공개 항목 전체 구조와 배경, 자연연역, 도입·제거, 정규화, 역전 원리·조화, 확장과 결론 확인
    원문 확인일
    영구 식별
    DOI 미기재 · 아래 보존판 주소로 안내

이 글은 한국어 해설이며 원문 전문 번역이 아닙니다. 도식과 활동의 제작·재구성 범위는 각 그림과 본문에 표시했습니다. 자료 선정과 출처 기준

출처·개념 네트워크

같은 연구 흐름에서 이어 읽기

같은 원문, 저자·연구 흐름, 공통 개념 태그를 기준으로 연결한 관련 해설입니다.