나무모에 미러 (일반/밝은 화면)
최근 수정 시각 : 2025-02-01 05:52:25

선형논리


논리학
Logics
{{{#!wiki style="margin: -0px -10px -5px; min-height: 28px"
{{{#!folding [ 펼치기 · 접기 ]
{{{#!wiki style="margin: -6px -1px -11px;"
<colbgcolor=#2ab5b5> 형식 논리 명제 논리(논리 연산 · 삼단논법(정언삼단논법) · 순환 논법) · 공리 · 진리치 · 술어 논리 · 논증(논증의 재구성) · 모순 · 역설 · 논리적 오류(논리적 오류/형식적 오류) · 변증법
<colcolor=#000,#fff> 비표준 논리 직관 논리 · 양상논리 · 초일관 논리 · 다치논리(퍼지논리) · 선형논리 · 비단조 논리
메타 논리 집합론 · 완전성 정리 · 불완전성 정리
비형식 논리 딜레마(흑백논리)
비형식적 오류 귀납적 오류 · 심리적 오류 · 언어적 오류 · 자료적 오류 · 양비론 · 진영논리 · 편견 및 고정관념 · 궤변 · 거짓 등가성
분야 수학철학 · 수리논리학
철학 관련 정보 · 논리학 관련 정보 · 수학 관련 정보 · 수리논리학 둘러보기
}}}}}}}}} ||

1. 개요2. 선형논리의 연산자들
2.1. 선형 함축 (linear implication)2.2. 결합적 논리곱 (multiplicative conjunction)2.3. 결합적 논리합 (additive conjunction)2.4. 분리적 논리합 (additive disjunction)2.5. 분리적 논리곱 (multiplicative disjunction)2.6. 선형 부정 (linear negation)2.7. 선형 동치 (linear equivalence)2.8. Of-course 연산자2.9. Why-not 연산자
3. 고전논리와의 관계4. 직관주의 논리와의 관계

1. 개요

선형논리()는 부분구조논리의 일부로 모든 가설은 한 번만 소비된다는 입장을 취한다. 고전논리와 직관논리에선 가설은 필요에 따라 여러 번 쓸 수 있다.

다만 일반적인 평서문으로는 쉽게 다룰 수 없는 면이 있다. 그래서 논리식을 평서문으로 옮겨적을 때 주의가 요구된다.

2. 선형논리의 연산자들

이 문단에서는 선형 논리의 해석들 중 자원 해석(resource interpretation)을 비유적으로 소개한다.

손님이 원하는 것이라면 뭐든지 준비하고자 하는 만물상이 있다고 하자. 이 세상에는 [math(P)]와 [math(Q)]등 다양한 "물건"들이 있다. 안타깝게도 정말 "뭐든지" 준비할 수는 없지만, 이 만물상은 더 나은 서비스를 위해 선형 논리의 연산자들로써 다양한 종류의 "교환권"을 제공하고자 한다.

2.1. 선형 함축 (linear implication)

손님이 [math(P ⊸ Q)]가 쓰여 있는 교환권을 가지고 있다고 하자. 그렇다면 이 손님은 이 교환권과 물건 [math(P)]를 함께 내고 물건 [math(Q)]를 받을 수 있다.

선형 함축이 고전적인 논리적 함의(material conditional)과 다른 점은 선형 논리가 다루는 "자원"이 마음대로 복제되거나 파괴될 수 없다는 점에서 기인한다. 고전 논리에서는 [math(P)]와 [math(P \to Q)]의 결합(conjunction)은 [math(P \land Q)]를 함의하는데, 이를 자원 해석에 곧이그대로 적용하면 위 손님은 물건 [math(Q)]를 받았음에도 불구하고 여전히 [math(P)]를 소유하는 것이 가능하기 때문이다.

2.2. 결합적 논리곱 (multiplicative conjunction)

손님이 [math(P \otimes Q)]가 쓰여 있는 교환권을 가지고 있다고 하자. 그렇다면 이 손님은 이 교환권을 내고 물건 [math(P)]와 물건 [math(Q)]를 함께 받을 수 있다.

고전적인 논리적 결합([math(\land)])과 가장 가까운 의미를 가지고 있는 연산자이다.

[math(\otimes)]의 항등원인 [math(1)]는 임의의 물건 "0개"를 의미한다. 즉 [math(1 ⊸ P)]는 물건 [math(P)]를 받을 수 있는 교환권이다. 한편, 교환권 [math(P ⊸ 1)]를 낸다면 물건 [math(P)]를 처분할 수 있다.

2.3. 결합적 논리합 (additive conjunction)

손님이 [math(P \& Q)]가 쓰여 있는 교환권을 가지고 있다고 하자. 그렇다면 이 손님은 물건 [math(P)]와 물건 [math(Q)] 중 자신이 원하는 것을 하나 받을 수 있다. 둘 다 받을 수는 없다.

[math(\&)]의 항등원인 [math(\top)]은 이 물건이 어떠한 물건인지에 관한 정보가 없음을 의미한다. 그러한 정보가 없으므로 손님은 이러한 물건을 받길 원할 수 없다. 임의의 물건 [math(P)]에 대해 이 물건의 정보를 지울 수 있는데, 이는 곧 교환권 [math(P ⊸ \top)]과 같다. 이러한 점에서 [math(\top)]은 고전적인 항진(tautology)의 성격을 띤다.

2.4. 분리적 논리합 (additive disjunction)

손님이 [math(P \oplus Q)]가 쓰여 있는 교환권을 가지고 있다고 하자. 그렇다면 이 손님은 물건 [math(P)]를 하나 받거나 물건 [math(Q)]를 하나 받을 수 있는데, 어느 것을 받을지는 만물상 마음이다. 둘 중 어느 것을 받을지를 정하는 주체가 다르다는 점에서 [math(\oplus)]는 [math(\&)]와 구별된다.

고전적인 논리적 분리([math(\lor)])와 가장 가까운 의미를 가지고 있는 연산자지만, 고전적인 [math(\lor)]에서 양쪽 명제 모두가 참일 수도 있는 것과 달리, [math(\oplus)]에서는 둘 중 하나만을 받을 수 있다. 이 점에서 [math(\oplus)]는 [math(\lor)]보다 자연어의 "또는"(or)에 더 가까운 의미를 가지고 있다.

[math(\oplus)]의 항등원인 [math(0)]은 존재가 불가능한 물건을 가리킨다. 즉 만물상이 손님에게 [math(0)]을 주고 싶어도 줄 수가 없다. 존재 자체가 모순이란 점에서 폭발 원리의 대상이 된다. 즉 임의의 물건 [math(P)]에 대해 교환권 [math(0 ⊸ P)]은 반드시 존재한다. 다만 실제 사용은 불가능하다.

2.5. 분리적 논리곱 (multiplicative disjunction)

선형 논리의 연산자들 중 자연어로서의 설명이 가장 곤란하다.

손님이 [math(P ⅋ Q)]가 쓰여 있는 교환권을 가지고 있다고 하자. 그렇다 하더라도 물건 [math(P)]나 물건 [math(Q)]를 당장 받을 수는 없는데, 왜냐하면 이 교환권을 사용하려는 손님은 자신이 물건 [math(P)]를 받을 수 없다는 걸 증명하거나 (이 경우 물건 [math(Q)]를 받게 된다), 물건 [math(Q)]를 받을 수 없다는 걸 증명해야 (이 경우 물건 [math(P)]를 받게 된다) 하기 때문이다.

즉 분리적 논리곱은 손님과 만물상 사이의 일종의 "약속"으로, [math(⅋)]의 항등원인 [math(\bot)]는 존재성을 증명할 수 없는 물건을 의미한다. [math(0)]과의 차이점은, 상품 [math(\bot)]는 실제로는 존재할지도 모른다는 것이다. 이러한 점에서 선형 논리가 초일관 논리의 일종임을 알 수 있다.

2.6. 선형 부정 (linear negation)

물건 [math(P)]의 부정인 [math(P^\bot)]은 [math(P ⊸ \bot)]이라고 정의된다. 즉 교환권 [math(P^\bot)]와 물건 [math(P)]를 함께 내면 존재성을 증명할 수 없는 상품을 받게 되는데, 이러한 상품을 받게 되면 그 존재성이 증명되므로 이는 모순이다. 다시 말해 교환권 [math(P^\bot)]는 이를 가지고 있는 사람이 물건 [math(P)]를 가지고 있어서는 안 된다는 증빙이다.

선형 부정은 고전 논리의 부정처럼 대합(involution)인데, 즉 [math(P)]와 [math(\left(P^\bot\right)^\bot)]은 동치이다. 이 점에서 직관주의 논리의 부정과는 다르다.

한편, 위 이항 연산자들 사이에는 선형 부정을 통한 항진명제들이 존재하는데, [math(P ⊸ Q)]는 [math(P^\bot ⅋ Q)]와 동치이고, [math(\left(P \otimes Q\right)^\bot)]는 [math(P^\bot ⅋ Q^\bot)]과 동치이며, [math(\left(P \oplus Q\right)^\bot)]는 [math(P^\bot \& Q^\bot)]과 동치이다.

또 한편으로는, [math(P ⅋ Q)]가 [math(P^\bot ⊸ Q)]와 동치이고 [math(Q^\bot ⊸ P)]와도 동치임을 알 수 있다. 즉 [math(P ⅋ P)]는 [math(P^\bot ⊸ P)]와 동치인데, 다시 말해 교환권 [math(P ⅋ P)]를 내면 자신이 물건 [math(P)]를 가지고 있어선 안 된다는 증빙을 포기하는 대가로 물건 [math(P)]를 받을 수 있다.

2.7. 선형 동치 (linear equivalence)

선형 동치 [math(P \equiv Q)]는 [math(\left(P ⊸ Q\right) \& \left(Q ⊸ P\right))]라고 정의된다.

2.8. Of-course 연산자

[math(!P)]는 [math(1 \& P \& \left(P \otimes P\right) \& \left(P \otimes P \otimes P\right) \& \cdots)]라고 정의된다. 즉 [math(!P)]가 쓰여 있는 교환권을 가지고 있는 손님은 이 교환권을 내서 물건 [math(P)]를 원하는 개수만큼(0개 포함) 받을 수 있다.

2.9. Why-not 연산자

[math(?P)]는 [math(\bot \oplus P \oplus \left(P ⅋ P\right) \oplus \left(P ⅋ P ⅋ P\right) \oplus \cdots)]라고 정의된다.

3. 고전논리와의 관계

고전논리의 동일률([math(P \to P)])은 선형논리에서도 그대로 수용된다([math(P ⊸ P)]).

고전논리의 모순율([math(\neg\left(P \land \neg P\right))])은 선형논리에서 [math(\left(P \otimes P^\bot\right)^\bot)]라고 수용된다.

고전논리의 배중률([math(P \lor \neg P)])은 선형논리에서 [math(P ⅋ P^\bot)]라고 수용된다. [math(P \oplus P^\bot)]가 아닌 이유는 직관주의 논리와도 일맥상통하는데, [math(P)]와 [math(P^\bot)] 모두가 증명불가할 수 있기 때문이다.

4. 직관주의 논리와의 관계

직관주의 논리에서는 한 명제를 몇 번이라도 사용할 수 있으므로, 직관주의 논리의 함축 [math(P \to Q)]는 선형 논리의 [math(!P ⊸ Q)]와 같다.

분류