LTCT KOREA세계 논리학의 지도
프랑스편 · 연재 01

THE WORLD OF LOGIC · FRANCE / 01

한 번 쓴 전제를,
다시 써도 될까요?

장이브 지라르의 Linear Logic을 따라 읽는 가상 인터뷰.
사회자가 기호 앞에서 멈춰 묻고, 답변은 글과 그림으로 이어집니다.

원문 기반 가상 대담14개의 질문그림과 함께 읽기2026.10.04
이 대담의 성격

실제 인터뷰가 아닙니다. 원논문과 공개된 후속 해설을 바탕으로 재구성한 학습용 가상 대담입니다. 답변은 저자의 실제 발언이나 승인을 뜻하지 않습니다. 교환권·음료 사례와 도식은 이 연재를 위해 새로 만들었으며, 원문의 그림을 복제한 것이 아닙니다.

사회자 · 독자의 질문

“잠깐만요. 그 기호부터 읽어 주세요.”
뜻을 짐작하고 넘어가지 않고, 논증의 다음 걸음을 묻습니다.

2000년 강연에서 설명 중인 장이브 지라르

장이브 지라르 · 가상 답변

1987년 논문의 논리를 따라 구성한 답변.
후속 자료의 설명은 별도로 출처를 표시합니다.

사진: 2000년 강연 · UTLS / Wikimedia Commons

이 인터뷰가 따라갈 논문의 길

서론의 반복 설명을 여섯 질문으로 묶고, 기술 본문은 절 순서를 따라갑니다. 쪽수는 원문에 인쇄된 번호를 기준으로 표시했습니다. 원문 링크를 연 뒤 해당 쪽을 찾아보실 수 있습니다.

PART I · INTRODUCTION

낯선 기호 앞에서, 멈춰 묻다

먼저 논문이 무엇을 구별하려는지 알아봅니다.

01
사회자

이미 논리학이 있는데, 왜 새로운 논리가 필요했나요?

서론 · 문제 제기와 함의의 분석
JG지라르 · 원문 기반 가상 답변

한 가지 질문을 더 세밀하게 해보자는 것입니다. “결론이 나오느냐”와 함께 “그 과정에서 전제를 어떻게 사용했느냐”를 묻는 것이지요. 같은 전제를 두 번 참조했는지, 한 번도 쓰지 않았는지를 구별하면, 이전에는 비슷해 보이던 추론들이 다른 모습을 드러냅니다.

그림 01 · 정보와 사용권을 구별해 봅시다설명용 비유
반복 참조하는 정보
“오늘은 휴일”
여러 번 읽어도
그 정보는 남습니다.
한 번 행사하는 권리
교환권 A
한 잔과 바꿨다면
그 권리는 사용됐습니다.
둘의 차이를 논리의 표현에 담아보자는 비유입니다. 사실 자체가 읽을 때마다 사라진다는 뜻은 아닙니다.

여기서 교환권은 이해를 돕기 위해 만든 예시입니다. 실제 논문의 수학적 배경은 증명과 함수의 의미를 분석하는 연구입니다. 이제부터는 한 장의 교환권으로 시작해, 전제를 사용하는 방식이 기호에 어떻게 나타나는지 살펴보겠습니다.

원문 위치: 서론, 인쇄 pp. 2–3 · 보조 해설: Girard, 1995, PDF pp. 1–2
02
사회자

그러면 Γ ⊢ B와 A ⊸ B부터 읽어 주세요. 둘 다 화살표처럼 보입니다.

서론 · 시퀀트와 선형함의
JG지라르 · 원문 기반 가상 답변

Γ는 전제들의 모음을 줄여 쓴 글자입니다. Γ ⊢ B는 “그 전제들로 B를 도출할 수 있다”는 판단입니다. 반면 A ⊸ B는 논리식 안에서 쓰는 선형함의입니다. 자원 예시에서는 “A를 받아 B를 내놓는 변환”으로 읽을 수 있습니다.

그림 02 · 한 문장 안에서도 기호의 역할은 다릅니다기호 읽기
A, A ⊸ B
갖고 있는 전제들
교환권 + 변환 규칙
⊢
도출할 수 있다
B
얻는 결론
음료 한 잔
A+A ⊸ B→B
⊢는 판단을 표시하고, ⊸는 논리식의 일부입니다. 아래의 →는 상황 변화를 보여주는 설명용 화살표입니다.
사회자 · 한 번 더

두 장이 있는데 한 장만 쓰면, 나머지는 어디에 표시하나요?

결과에 남겨야 합니다. 두 장에서 한 장만 교환했다면 B ⊗ A, 즉 음료 한 잔과 아직 쓰지 않은 교환권 한 장입니다. 아래 실험에서는 가게의 교환 규칙을 여러 번 적용할 수 있다고 정하되, 교환권은 한 장씩 사용합니다.

직접 해보기 · 남은 전제까지 세어 보기INTERACTIVE 01
처음 가진 교환권

아직 쓸 수 있는 교환권

A₁

교환해서 받은 음료

아직 없습니다
현재 남아 있는 전체 결과A

A 한 장으로 음료 B 한 잔을 받을 수 있습니다.

모형의 조건: 교환 규칙 !(A ⊸ B)는 반복 사용 가능합니다. 이 배경 규칙은 결과식에서 생략하고, 교환권과 음료만 셉니다. 느낌표는 06번에서 설명합니다.

한 장을 이미 썼다면, 그 한 장을 다시 제출할 수 없습니다. 초기 수량을 바꾸거나 “처음 상태로”를 누르면 새로운 예시를 시작합니다.
기호 해설: Wadler, A Taste of Linear Logic, PDF pp. 3–5 · 교환 실험은 새로 구성한 예시입니다.
03
사회자

논문은 ‘수축’과 ‘약화’를 제한한다고 합니다. 이름만으로는 무슨 뜻인지 모르겠습니다.

서론 II.1 · 구조규칙
JG지라르 · 원문 기반 가상 답변

수축은 두 번 필요했던 같은 전제를 한 번 주어진 것으로 충당하도록 허용하는 규칙입니다. 약화는 결론을 만드는 데 쓰지 않는 전제를 추가해도 된다는 규칙이지요. 일반적인 전제에 이 두 가지를 자유롭게 허용하면, 반복 사용과 미사용의 차이가 흐려집니다.

그림 03 · 분수처럼 보이는 것은 추론규칙입니다규칙 읽기

수축 · contraction

Γ, A, A ⊢ B
Γ, A ⊢ B

아래 판단을 증명하려고 위로 올라가 보면, A 하나가 두 사용 자리를 감당합니다.

약화 · weakening

Γ ⊢ B
Γ, A ⊢ B

아래에 더해진 A를 쓰지 않아도 기존의 증명으로 B를 얻습니다.

가로선 위의 판단에서 아래의 판단으로 가는 규칙입니다. 선형논리는 이 두 규칙을 모든 전제에 일괄 적용하지 않습니다.

그래서 보통의 원자명제 A 하나에서 A ⊗ A를 얻는 것은 일반적으로 허용되지 않습니다. 여기서 두 A는 같은 종류의 자원 두 개를 뜻합니다. 종이에 글자가 몇 번 나타났는지만 세는 규칙은 아닙니다. 서로 다른 선택의 경우를 따로 검토하는 일은 다음 질문에서 구별하겠습니다.

원문 위치: 인쇄 pp. 4–5 · 규칙 확인: Beffara, 2013, §1.3
04
사회자

‘그리고’도 두 종류인가요? ⊗, &, ⊕를 그림으로 나눠 주세요.

서론 II.2 · 연결사의 분화
JG지라르 · 원문 기반 가상 답변

당신이 음료를 받는 사람이라고 고정해 봅시다. C는 커피, T는 차입니다. C ⊗ T는 둘을 함께 받는 약속입니다. C & T는 당신이 어느 쪽을 골라도 제공할 준비가 되어 있는 약속입니다. C ⊕ T는 제공자가 고른 한쪽을 받되, 무엇을 받았는지 알 수 있는 약속입니다.

그림 04 · 같은 두 음료, 서로 다른 약속INTERACTIVE 02
C ⊗ T

커피와 차를 모두 확보하는 약속입니다. 꼭 같은 순간에 마셔야 한다는 뜻은 아닙니다.

C커피
T차
받을 수 있는 것: 커피와 차, 두 잔
&와 ⊕에서는 한 번 약속을 사용하면 한 잔만 받습니다. 여기서 “누가 고르나”는 제공되는 음료를 받는 사람의 관점에 맞춘 해석입니다.

&가 ‘그리고’인 이유도 보입니다. 커피를 요구받는 경우의 준비와, 차를 요구받는 경우의 준비를 모두 갖춰야 하기 때문입니다. 다만 실제 사용에서 두 결과를 한꺼번에 꺼내지는 않습니다. 이 차이가 A ⊸ (A & A)는 가능하지만 A ⊸ (A ⊗ A)는 일반적으로 가능하지 않은 이유를 이해하는 출발점입니다.

원문 위치: 인쇄 p. 5 · 해석: Girard, 1995, PDF pp. 2–3 · 규칙: Pfenning, Linear Natural Deduction, pp. 13–17
05
사회자

A⊥는 ‘A가 없다’는 뜻인가요? 뒤집힌 기호 ⅋도 나옵니다.

서론 II.2 · 선형부정과 쌍대성
JG지라르 · 원문 기반 가상 답변

여기서는 서로 맞물리는 반대 역할로 생각해 보세요. 한쪽에서 A를 제공한다면, 그에 대응하는 쪽은 A를 받아 사용합니다. 이 관점 전환을 선형부정 A⊥로 읽을 수 있습니다. 두 번 뒤집으면 원래로 돌아옵니다: (A⊥)⊥ = A.

그림 05 · 반대 역할을 연결해서 함의를 읽기쌍대성의 비유
A를 내놓는 쪽
A

제공하는 역할

A를 받아 쓰는 쪽
A⊥

맞물리는 반대 역할

A ⊸ B≡A⊥ ⅋ B

A를 입력으로 요구하는 역할과 B를 출력으로 제공하는 역할을 한 관계로 묶습니다.

⅋는 par라 부르는 곱셈적 논리합이며 ⊗의 쌍대입니다. “두 물건 중 마음대로 하나 고르기”와는 다른 기호입니다.

정확한 관계를 하나 더 적으면 A ⅋ B = (A⊥ ⊗ B⊥)⊥입니다. 이 정의가 “쌍대”라는 말의 뼈대입니다. 제공과 요구는 그 뼈대를 읽기 위한 비유이지, A⊥를 단순한 재고 부족으로 바꿔 놓는 정의는 아닙니다.

원문 위치: 인쇄 p. 5 · 후속 해설: Girard, 1995, PDF p. 3
06
사회자

그렇다면 느낌표 !와 물음표 ?는 무엇을 바꾸나요?

서론 II.3 · 지수 연산자
JG지라르 · 원문 기반 가상 답변

!A는 A를 반복 사용하거나 사용하지 않는 것을 허용하는 방식으로 다룹니다. 앞서 교환 실험에서 가게 규칙에 !를 붙인 이유가 이것입니다. 각 교환권은 쓰이고, 교환 규칙은 다시 적용할 수 있도록 모형을 정한 것입니다.

그림 06 · 반복 가능한 규칙, 한 번 쓰는 권리모형의 조건
여러 번 적용할 수 있다고 정한 가게 규칙
!(A ⊸ B)
첫 번째 교환
A₁ → B₁

교환권 1번을 사용

두 번째 교환
A₂ → B₂

교환권 2번을 사용

같은 교환권을 되살린 것이 아닙니다. 반복 가능한 규칙 아래에서 서로 다른 두 교환권을 각각 썼습니다.

아무 A에나 느낌표를 붙일 수 있는 것은 아닙니다. 일반적으로 A ⊢ !A는 성립하지 않습니다. 느낌표를 도입하는 증명에는 의존하는 다른 전제도 재사용 가능한 형태여야 한다는 조건이 있습니다. ?는 불확실성이나 확률을 표시하지 않습니다. (!A)⊥ = ?(A⊥)라는 관계로 !와 짝을 이룹니다.

기호를 더 정확히 · 느낌표 도입의 조건

한 결론을 쓰는 표현에서 대표적인 도입규칙은 아래와 같습니다. !Γ는 전제들이 모두 재사용 가능한 형태라는 표시입니다.

!Γ ⊢ A
!Γ ⊢ !A

이 글의 한 결론 표기는 설명을 위한 것입니다. 원논문은 선형부정이 있는 고전적 선형논리도 다룹니다.

원문 위치: 인쇄 pp. 5–6 · 도입 조건: Beffara, 2013, §2.4 · 한 결론 표기: Wadler, PDF pp. 13–17
PART II · THROUGH THE PAPER

그 기호로, 무엇을 증명했을까

이제 기술 본문의 여섯 절을 순서대로 방문합니다.

07
사회자

첫 절은 ‘위상 의미론’입니다. 새 기호에 의미가 있다는 것을 어떻게 보여 주나요?

§1 · Phase semantics · 인쇄 pp. 17–28
JG지라르 · 원문 기반 가상 답변

대상들을 결합하는 방법과 검사 조건을 정합니다. 어떤 대상들과 결합했을 때 그 조건을 만족하는지 조사하면, 한 집합에 대응하는 짝의 집합을 만들 수 있습니다. 짝들을 다시 조사했을 때 처음 집합으로 돌아오는 집합을 명제의 해석에 사용합니다. 어려운 정의의 작은 일부를 숫자로 직접 계산해 보겠습니다.

그림 07 · ‘함께 검사 조건을 만족하는가’작은 수학 모형

이 예시의 세계는 0 이상의 정수, 결합은 덧셈입니다.
지정한 검사 조건은 합이 2가 되는 것입니다.

1S에 있는 수
+
1맞물리는 짝
=
2지정한 조건
S = {1}　 S⊥ = {1}
S⊥⊥ = {1} = S
한 번 더 짝을 구해도 같은 집합으로 돌아옵니다.
편집용 수학 예시입니다. 여기서 숫자 1은 수이고, 논리의 단위 기호 설명이 아닙니다. 검사 조건을 만족하는 짝을 찾는 것과 명제의 유효성을 증명하는 것은 구별해야 합니다.

이 장의 더 큰 질문은 “이런 해석에서 논리의 규칙이 제대로 작동하는가”입니다. 이 예시는 정의를 읽기 위한 입구이며, 논문의 건전성·완전성 정리를 대신하는 증명은 아닙니다.

원문의 정의에 한 걸음 더 · ‘모든’이 중요합니다

지정집합을 P={2}라고 하면, S⊥는 모든 s∈S에 대해 s+m∈P를 만족하는 m들의 집합입니다. S=S⊥⊥인 집합을 이 의미론에서 fact라고 부릅니다.

유효한 fact가 되려면 결합의 항등원도 포함해야 합니다. 이 예시의 항등원은 0이므로 {1}은 fact이지만 유효한 fact은 아닙니다. ‘짝이 있다’와 ‘유효하다’를 같은 말로 읽지 않는 것이 중요합니다.

원문 정의: 인쇄 p. 18, 정의 1.1–1.3 · 숫자 계산과 도식은 해당 정의로 새로 만든 예시입니다.
08
사회자

다음 절에는 선이 잔뜩 나옵니다. 어떻게 그림이 증명이 되나요?

§2 · Proof-nets · 인쇄 pp. 28–47
JG지라르 · 원문 기반 가상 답변

증명을 규칙을 쌓은 나무로 적는 대신, 어떤 공식이 어떤 공식에 연결되는지를 직접 나타낼 수 있습니다. 서로 독립적인 규칙을 적용한 순서만 다른 두 증명도 같은 연결 구조로 나타낼 수 있지요. 다만 선을 연결했다고 모두 증명이 되지는 않습니다. 먼저 후보인 ‘증명 구조’를 만들고, 그 연결이 맞는지 검사해야 합니다.

그림 08 · 아주 작은 증명망을 검사해 봅시다INTERACTIVE 03
⅋로 묶은 경우
⊢ A⊥ ⅋ A
A⊥A공리 연결⅋한쪽 연결만 남겨 검사
왼쪽을 남김 · 연결되어 있고 순환 없음
⅋의 연결 검사

⅋에서는 어느 쪽을 남겨도 전체가 연결된 나무가 됩니다. 점선은 이번 검사에서 뺀 선입니다.

같은 두 원자를 ⊗로 묶은 경우
⊢ A⊥ ⊗ A
A⊥A공리 연결⊗둘 다 남겨야 하므로 순환 발생
이 구조는 정확성 검사를 통과하지 못함
범위: 단위와 추가 mix 규칙이 없는 곱셈선형논리, 원자 A의 예입니다. 각 ⅋에서 한쪽 연결만 남기는 모든 경우를 검사해 연결성과 비순환성을 확인합니다. 후대 강의자료의 스위칭 설명으로 새로 그린 그림이며, 1987년 원문의 그림을 옮긴 것은 아닙니다.

⅋로 묶은 구조는 어느 연결을 남겨도 검사에 통과합니다. ⊗로 묶은 구조는 두 연결을 모두 유지해야 하므로 순환이 생깁니다. 같은 원자와 같은 공리선이라도, 어떻게 결합했는지가 중요한 것입니다. 이것이 논문 속 선들을 장식이 아니라 논증으로 읽는 첫걸음입니다.

원문의 주제: §2, 인쇄 p. 28부터 · 이 검사법의 설명: Laurent, 2013, §1.2–1.4, PDF pp. 2–6
09
사회자

그런데 ‘컷’은 자른다는 말 아닌가요? 왜 두 증명을 연결한다고 하나요?

§2 · 컷의 도입과 변형 · 인쇄 pp. 40–47
JG지라르 · 원문 기반 가상 답변

먼저 연결하는 규칙을 보세요. 한 증명이 A를 만들어 내고, 다른 증명이 그 A를 전제로 써서 B를 만든다면, 두 증명을 이어 B를 얻을 수 있습니다. 중간 공식 A를 접점으로 삼는 것이 컷입니다.

그림 09 · 중간 결론과 다음 전제를 맞물리기컷의 모식도
첫 번째 증명
Γ ⊢ A
A를 만들어 냄
A로
연결
두 번째 증명
Δ, A ⊢ B
A를 써서 B를 만듦
합친 증명의 결론
Γ, Δ ⊢ B
Γ와 Δ는 두 증명의 다른 전제들입니다. 중간의 A를 연결한다고 해서 나머지 전제들을 마음대로 복제하거나 버리는 것은 아닙니다.

이제 왜 제거가 중요한지 질문할 수 있습니다. 중간 결과를 이름으로만 불러 연결한 증명에서, 그 안의 작업을 실제로 맞물리게 전개해 같은 결론을 얻을 수 있을까요? 논문은 이런 변형을 다루고, 뒤의 정규화 절에서 그 과정의 성질을 더 깊게 연구합니다.

원문 위치: 인쇄 pp. 40–47 · 규칙과 계산의 관계: Beffara, 2013, §2.2
10
사회자

이번에는 ‘코히어런스 공간’입니다. 공간이라는 말이 왜 필요한가요?

§3 · Coherent semantics · 인쇄 pp. 48–60
JG지라르 · 원문 기반 가상 답변

가능한 부분정보들을 점으로 놓고, 어떤 정보들이 함께 성립할 수 있는지를 관계로 정한 수학적 구조입니다. 어려운 이름을 잠깐 내려놓고, 한 잔의 음료에 관한 정보 세 개를 보겠습니다. 이 모형에서는 커피와 차를 서로 배타적인 종류로 정합니다.

그림 10 · 이어져 있다는 것과 모두 양립한다는 것정보의 모형
p와 r은 함께 성립하지 않음pqr커피따뜻함차함께 가능함께 가능
{p, q}
{q, r}

따뜻한 커피 또는 따뜻한 차.
각 묶음 안의 모든 쌍이 양립합니다.

{p, r}
{p, q, r}

이 모형에서는 커피이면서 차일 수 없습니다.
경로로 이어져 있어도 충분하지 않습니다.

선은 부분정보의 양립 가능성을 뜻합니다. 앞의 위상 의미론에서 말한 직교 관계와 다른 관계입니다. 각 점은 자신과도 양립하지만 자기 연결선은 생략했습니다.

묶음 안의 모든 두 점이 서로 양립하면 그것을 클리크라고 부릅니다. 이렇게 “함께 가능한 정보 묶음”을 정하고, 그것을 입력과 출력으로 다루는 함수의 성질을 조사할 수 있습니다. 논문에서는 이런 의미론이 앞에서 보았던 논리식과 증명에 어떤 구조를 부여하는지 살펴봅니다.

원문 위치: §3, 인쇄 p. 48부터 · 공간과 클리크의 정의: Beffara, 2013, §1.2 및 §3.2 · 음료의 부분정보 모형은 새로 만든 예시입니다.
11
사회자

정규화는 증명을 더 짧게 만든다는 말인가요? 아까의 컷으로 다시 설명해 주세요.

§4 · Normalization · 인쇄 pp. 60–78
JG지라르 · 원문 기반 가상 답변

핵심은 길이보다 증명의 연결을 변형하면서 무엇을 보존하는지입니다. 컷을 사용한 증명에서 컷 없는 증명을 얻더라도 결론은 유지되어야 합니다. 계산의 관점에서는 “만든 결과를 다음 작업에 실제로 넘겨 실행하기”에 대응하는 모습을 볼 수 있습니다.

그림 11 · 바로 만든 묶음을 바로 풀면?국소 변형의 예
묶어서 전달한 뒤 곧바로 풀기
a, b → ⟨a, b⟩
→ x := a, y := b
→ F(x, y)

a와 b를 포장해 넘기고, 받자마자 풀어 각각 사용합니다.

두 작업을 맞물리게 전개하기
F(a, b)

같은 a와 b를 같은 사용 자리에 직접 연결합니다. 둘 다 한 번씩 사용한다고 가정합니다.

보존할 것: 얻는 결론과 자원이 연결되는 관계.
이 작은 예에서 중간 포장을 없앴다는 사실이 모든 증명의 길이 감소를 뜻하지는 않습니다.
묶음의 도입과 제거가 만나는 경우를 프로그램식으로 새로 그린 설명용 모식도입니다. 임의의 현실 프로그램 전체에 대한 최적화 보장은 아닙니다.

또 “끝까지 변형할 수 있다”와 “언제나 똑같은 유일한 결과에 도착한다”는 다른 주장입니다. 원논문의 해당 증명망 체계에서는 강정규화를 다루면서도 정규형이 달라질 수 있음을 함께 밝힙니다. 여기서 강정규화란 정해진 정규화 규칙을 어떤 순서로 계속 적용해도 그 과정이 유한 번 안에 끝난다는 뜻입니다. 정규형의 모양이 달라도 의미론적 해석은 보존됩니다. 따라서 정규화를 유일한 최단 증명을 찾는 일로 읽어서는 안 됩니다.

원문 위치와 범위: 인쇄 pp. 60–61, PN2 정규화 · 증명과 계산의 해설: Pfenning, Linear Natural Deduction
12
사회자

그럼 기존 논리는 어떻게 되나요? 논문에 ‘번역’이라는 절이 있습니다.

§5 · Translations · 인쇄 pp. 78–93
JG지라르 · 원문 기반 가상 답변

기존 체계에서 하나로 취급하던 일을 더 세밀한 구성으로 나타내 봅니다. 예를 들어 직관주의적 함의를 옮기는 대표적인 방식에서는, 입력을 재사용할 수 있도록 준비하는 일과 입력에서 출력으로 가는 일을 나눕니다. 그 구조를 아래처럼 볼 수 있습니다.

그림 12 · 함의 안에 들어 있던 두 가지 일번역의 핵심 모양
A ⇒ B↦!A ⊸ B
!A

입력을 반복 사용하거나 쓰지 않아도 되는 형태로 다룹니다.

⊸ B

그 입력에서 결론 B를 만드는 선형적인 연결을 나타냅니다.

번역의 핵심을 보여주는 축약입니다. 실제로는 A와 B 안의 연결사도 정해진 규칙으로 번역합니다. 모든 논리의 번역이 이 한 줄만으로 끝나는 것은 아닙니다.

이렇게 보면 “기존 논리에서 당연히 허용하던 반복”이 어디에 놓여 있는지 드러납니다. 논문의 번역 절은 직관주의논리와 고전논리, 계산 체계 등을 더 넓게 다룹니다. 기존 논리와 선형논리를 연결해 읽을 수 있다는 점이 이 절의 역할입니다.

원문 위치: §5, 인쇄 p. 78부터 · 의미론적 분해: 인쇄 p. 16 · 입문 번역: Wadler, PDF pp. 15–17
13
사회자

마지막 기술 절의 ‘슬라이스’는 무엇을 잘라 보는 건가요?

§6 · Slices · 인쇄 pp. 93–97
JG지라르 · 원문 기반 가상 답변

선택으로 묶여 있는 증명의 구조를 조각들로 펼쳐 살펴보려는 시도입니다. 앞서 C & T에서 선택에 따라 사용되는 갈래가 달라졌지요. 아래는 그 아이디어만 꺼내 그린 모식도입니다. 같은 전체에서 나온 선택의 정보를 추적한다는 점을 보세요.

그림 13 · 한 전체의 선택 갈래를 펼쳐 보기아이디어 모식도
선택 구조를 가진 전체
C & T
왼쪽 선택을 따라 본 조각
C

↓ 커피 쪽의 연결을 추적

C & T

전체의 결론 표지는 유지

오른쪽 선택을 따라 본 조각
T

↓ 차 쪽의 연결을 추적

C & T

전체의 결론 표지는 유지

조각 하나만으로 충분하지 않습니다. 같은 전체에 속한 조각들의 관계를 함께 살펴봅니다.
정식 슬라이스의 모든 구조를 그린 그림은 아닙니다. 원논문은 개별 슬라이스 자체를 완성된 증명으로 볼 수 없다고 설명하며, 이 절을 당시 진행 중인 연구로 제시합니다.

연구 논문의 끝에는 완결된 정리만 있는 것이 아닙니다. 어떤 표현이 필요해 보이지만 아직 충분한 특징짓기가 남아 있는지도 기록됩니다. 이 지점에서는 성과와 남은 질문을 구분해서 읽는 것이 좋습니다.

원문 위치: 인쇄 pp. 94–95, 정의 6.1–6.2 및 논평 6.3 · 이 문답은 아이디어의 입구만 다루며 해당 절의 기술적 정의를 모두 해설하지 않습니다.
14
사회자

이것을 ‘프랑스편’으로 읽을 때, 마지막으로 무엇을 기억하면 좋을까요?

논문 끝의 형성과정 회고 · 인쇄 pp. 97–101
JG지라르 · 원문 기반 가상 답변

논문이 나온 장소와, 그 질문이 자라난 연구의 연결을 함께 보는 것이 좋겠습니다. 이 논문의 당시 소속은 파리 7대학과 CNRS이고, 원문은 영어입니다. 끝의 회고에는 베리와 퀴리앵이 제기한 의미론의 문제가 실마리로 등장합니다. 자원 비유보다 먼저 수학적 문제와 연구자 사이의 대화가 있었던 것입니다.

그림 14 · 국가의 이름 뒤에 있는 연구의 연결논문을 놓는 자리
논문이 만들어진 맥락
1987

파리 7대학 · CNRS
증명과 함수의 의미를 분석하는 질문
영어로 발표된 Linear Logic

독자가 따라갈 연구의 계보

질문 → 논문 → 후속 연구

어떤 문제를 이어받았는가
어떤 구별을 새로 만들었는가
다음 연구는 무엇을 더 묻는가

국가는 출발점을 찾는 표지입니다. 이 한 논문을 프랑스 전체의 사고방식으로 일반화하지 않고, 구체적인 문제와 연구의 이동을 따라 읽습니다.

이 대담에서 따라온 가장 작은 질문을 기억해 보세요. 같은 전제를 두 번 썼는가, 선택한 갈래에서 한 번 썼는가, 애초에 반복 가능한 전제였는가. 그 차이를 기호와 증명의 구조로 드러내면, “무엇이 참인가”를 넘어 추론과 계산의 작동 방식도 더 정밀하게 살펴볼 수 있습니다.

소속과 언어: 원문 첫 장 · 형성과정: 인쇄 p. 97부터 · 저자의 후속 회고: Girard, 1995, PDF p. 26
이 논문을 다시 펼칠 때 가져갈 질문

“이 전제는 몇 번 쓰였을까?”
그 질문 하나로, 같은 기호도 다르게 보이기 시작합니다.

옆에 놓고 보는 작은 기호 사전

이 글의 예시와 관점에서 기억할 수 있는 뜻입니다. 정식 의미는 본문의 규칙과 조건을 함께 읽어 주세요.

Γ ⊢ B
시퀀트 · 판단전제들 Γ에서 B를 도출할 수 있다.
A ⊸ B
선형함의A를 받아 B를 만드는 연결.
A ⊗ B
텐서 · 곱셈적 논리곱A와 B를 함께 확보한다.
A & B
위드 · 덧셈적 논리곱받는 쪽이 어느 쪽을 골라도 제공할 준비.
A ⊕ B
플러스 · 덧셈적 논리합제공하는 쪽이 고른 한쪽을 받는다.
A ⅋ B
파 · 곱셈적 논리합⊗의 쌍대. A⊥ ⊸ B로도 읽는다.
A⊥
선형부정맞물리는 반대 역할. 두 번 뒤집으면 A.
!A · ?A
지수 연산자재사용의 허용과 그 쌍대적 표현.

읽은 내용을 적용하기

한 장의 표로 두 번 입장할 수 있을까요?

전제 A를 입장권 한 장으로 읽어 봅니다. A를 사용해 B를 얻었다면 그 A는 사용 기록에 남습니다. 같은 표를 다시 쓰려면 복제를 허용하는 별도의 규칙을 확인해야 합니다.

직접 확인하기

종이에 A 한 개를 적고, 사용할 때마다 지워 보세요. A 두 개로 시작했을 때와 결론이 어떻게 달라지는지 비교하면 전제의 개수가 왜 중요한지 드러납니다.

학습 안내 · 위 사례는 본문 개념을 연습하도록 편집부가 구성했습니다. 원문의 정의와 정리의 적용 범위는 각 문답의 출처에서 확인할 수 있습니다.

원문으로 돌아가는 길

논문의 흐름은 1987년 원문을 따릅니다. 기호를 풀어 읽는 설명에는 저자의 후속 해설과 학술 강의자료를 함께 참고했습니다. 이 글은 원문 전체의 번역이 아니며, 원문의 모든 정의와 정리의 증명을 재현하지 않습니다.

  1. Jean-Yves Girard · Linear Logic · 1987

    Theoretical Computer Science, 50. 이 인터뷰가 따라가는 원논문. 본문의 쪽수는 원문에 인쇄된 번호를 기준으로 표시했습니다.

    저자 공개 PDFDOI / 출판 정보
  2. Jean-Yves Girard · Linear Logic: Its Syntax and Semantics · 1995

    저자가 뒤에 쓴 해설. 자원·행동의 해석, 연결사, 쌍대성, 연구 배경을 읽는 데 참고했습니다.

    저자 공개 PDF저자 논문 목록
  3. Philip Wadler · A Taste of Linear Logic · 1993 / 공개 수정본 2014

    기호의 층위, 구조규칙, 직관주의 선형논리와 번역에 관한 입문 해설.

    저자 공개 PDF
  4. Emmanuel Beffara · Introduction to Linear Logic · 2013

    구조규칙, 지수 연산자, 코히어런스 공간과 증명망의 정의를 확인한 강의자료.

    대학 공개 PDF
  5. Frank Pfenning · Linear Natural Deduction · 2001

    한 결론을 쓰는 자연연역의 표기와 연결사 규칙을 확인한 강의자료.

    CMU 공개 PDF
  6. Olivier Laurent · An Introduction to Proof Nets · 2013

    증명 구조와 증명망의 구별, 스위칭과 정확성 검사의 참고자료.

    ENS de Lyon 공개 PDF
  7. Philip Wadler · Propositions as Sessions · 2014

    후속 연구: 명제와 세션 타입의 대응. Journal of Functional Programming, 24(2–3), 384–418.

    저자 공개 PDFDOI
  8. Congard · Munch-Maccagnoni · Douence · Linear Effects, Exceptions, and Resource Safety · 2026

    후속 연구: 자원 안전성과 예외를 결합한 계산 체계. ESOP 2026. 전체 부제: A Curry-Howard Correspondence for Destructors.

    저자 공개본 v2출판 DOI

제작 안내 · LTCT KOREA의 《세계 논리학의 지도》 제1회 · 프랑스편입니다. 대화는 AI를 활용해 구성한 가상 대담이며, 문답과 도식은 새로 작성했습니다. 원문의 직접 인용문이나 실제 인터뷰 기록이 아닙니다.

사진 · 장이브 지라르의 2000.06.17 강연 장면. UTLS / Wikimedia Commons · CC BY-SA 4.0. 사진은 원본 비율로 크기만 조정해 사용했습니다.

서체 · Noto Sans KR과 DejaVu Sans의 필요한 글자를 파일에 포함했습니다. 본문과 그림은 인터넷 연결 없이 읽을 수 있으며, 원문 링크는 인터넷 연결이 필요합니다.

포함된 서체의 라이선스 보기
Copyright 2014-2021 Adobe (http://www.adobe.com/), with Reserved Font Name 'Source'

This Font Software is licensed under the SIL Open Font License, Version 1.1.
This license is copied below, and is also available with a FAQ at:
https://scripts.sil.org/OFL


-----------------------------------------------------------
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
-----------------------------------------------------------

PREAMBLE
The goals of the Open Font License (OFL) are to stimulate worldwide
development of collaborative font projects, to support the font creation
efforts of academic and linguistic communities, and to provide a free and
open framework in which fonts may be shared and improved in partnership
with others.

The OFL allows the licensed fonts to be used, studied, modified and
redistributed freely as long as they are not sold by themselves. The
fonts, including any derivative works, can be bundled, embedded, 
redistributed and/or sold with any software provided that any reserved
names are not used by derivative works. The fonts and derivatives,
however, cannot be released under any other type of license. The
requirement for fonts to remain under this license does not apply
to any document created using the fonts or their derivatives.

DEFINITIONS
"Font Software" refers to the set of files released by the Copyright
Holder(s) under this license and clearly marked as such. This may
include source files, build scripts and documentation.

"Reserved Font Name" refers to any names specified as such after the
copyright statement(s).

"Original Version" refers to the collection of Font Software components as
distributed by the Copyright Holder(s).

"Modified Version" refers to any derivative made by adding to, deleting,
or substituting -- in part or in whole -- any of the components of the
Original Version, by changing formats or by porting the Font Software to a
new environment.

"Author" refers to any designer, engineer, programmer, technical
writer or other person who contributed to the Font Software.

PERMISSION & CONDITIONS
Permission is hereby granted, free of charge, to any person obtaining
a copy of the Font Software, to use, study, copy, merge, embed, modify,
redistribute, and sell modified and unmodified copies of the Font
Software, subject to the following conditions:

1) Neither the Font Software nor any of its individual components,
in Original or Modified Versions, may be sold by itself.

2) Original or Modified Versions of the Font Software may be bundled,
redistributed and/or sold with any software, provided that each copy
contains the above copyright notice and this license. These can be
included either as stand-alone text files, human-readable headers or
in the appropriate machine-readable metadata fields within text or
binary files as long as those fields can be easily viewed by the user.

3) No Modified Version of the Font Software may use the Reserved Font
Name(s) unless explicit written permission is granted by the corresponding
Copyright Holder. This restriction only applies to the primary font name as
presented to the users.

4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
Software shall not be used to promote, endorse or advertise any
Modified Version, except to acknowledge the contribution(s) of the
Copyright Holder(s) and the Author(s) or with their explicit written
permission.

5) The Font Software, modified or unmodified, in part or in whole,
must be distributed entirely under this license, and must not be
distributed under any other license. The requirement for fonts to
remain under this license does not apply to any document created
using the Font Software.

TERMINATION
This license becomes null and void if any of the above conditions are
not met.

DISCLAIMER
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
OTHER DEALINGS IN THE FONT SOFTWARE.


DejaVu Sans license and copyright:

Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: DejaVu fonts
Upstream-Author: Stepan Roh <src@users.sourceforge.net> (original author),
                  see /usr/share/doc/fonts-dejavu-core/AUTHORS for full list
Source: https://dejavu-fonts.github.io/

Files: *
Copyright: Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. 
 Bitstream Vera is a trademark of Bitstream, Inc.
 DejaVu changes are in public domain.
License: bitstream-vera
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of the fonts accompanying this license ("Fonts") and associated
 documentation files (the "Font Software"), to reproduce and distribute the
 Font Software, including without limitation the rights to use, copy, merge,
 publish, distribute, and/or sell copies of the Font Software, and to permit
 persons to whom the Font Software is furnished to do so, subject to the
 following conditions:
 .
 The above copyright and trademark notices and this permission notice shall
 be included in all copies of one or more of the Font Software typefaces.
 .
 The Font Software may be modified, altered, or added to, and in particular
 the designs of glyphs or characters in the Fonts may be modified and
 additional glyphs or characters may be added to the Fonts, only if the fonts
 are renamed to names not containing either the words "Bitstream" or the word
 "Vera".
 .
 This License becomes null and void to the extent applicable to Fonts or Font
 Software that has been modified and is distributed under the "Bitstream
 Vera" names.
 .
 The Font Software may be sold as part of a larger software package but no
 copy of one or more of the Font Software typefaces may be sold by itself.
 .
 THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
 OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY,
 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT,
 TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME
 FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING
 ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES,
 WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
 THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE
 FONT SOFTWARE.
 .
 Except as contained in this notice, the names of Gnome, the Gnome
 Foundation, and Bitstream Inc., shall not be used in advertising or
 otherwise to promote the sale, use or other dealings in this Font Software
 without prior written authorization from the Gnome Foundation or Bitstream
 Inc., respectively. For further information, contact: fonts at gnome dot
 org.

Files: debian/*
Copyright: (C) 2005-2006 Peter Cernak <pce@users.sourceforge.net> 
           (C) 2006-2011 Davide Viti <zinosat@tiscali.it>
           (C) 2011-2013 Christian Perrier <bubulle@debian.org>
           (C) 2013 Fabian Greffrath <fabian+debian@greffrath.com>
License: GPL-2+
 This program is free software; you can redistribute it
 and/or modify it under the terms of the GNU General Public
 License as published by the Free Software Foundation; either
 version 2 of the License, or (at your option) any later
 version.
 .
 This program is distributed in the hope that it will be
 useful, but WITHOUT ANY WARRANTY; without even the implied
 warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
 PURPOSE.  See the GNU General Public License for more
 details.
 .
 You should have received a copy of the GNU General Public
 License along with this package; if not, write to the Free
 Software Foundation, Inc., 51 Franklin St, Fifth Floor,
 Boston, MA  02110-1301 USA
 .
 On Debian systems, the full text of the GNU General Public
 License version 2 can be found in the file
 /usr/share/common-licenses/GPL-2'.