기술 요약: 2차원 시퀀트 계산법의 모든*연결사들에 대한 추론-행위 의미론

1. 문제 제기

본 논문은 증명론적 의미론(Proof-Theoretic Semantics, P-tS)의 핵심 과제, 즉 서로 다른 논리 체계(예: 고전 논리, 직관주의 논리, 선형 논리 및 이중 직관주의 논리) 전반에 걸쳐 논리적 연결사에 대해 어떻게 의미 불변적인(meaning-invariant) 의미 설명을 제공할 것인가를 다룬다. 모델 이론적 의미론(M-tS)이나 기저 확장 의미론(B-eS)과 같은 전통적인 접근 방식들은 종종 "전역성(globalism)" 문제에 직면한다. 즉, 논리를 변경할 때마다 연결사의 의미도 변경해야 한다는 점이다(예: 고전적 'and'와 직관주의적 'and'의 차이). 이는 논리적 이견을 공유된 개념에 대한 실질적인 이견이 아니라, 단지 정의가 서로 다르기 때문에 발생하는 의사소통의 결함으로 격하시키는 결과를 초래한다.

이 논문이 다루는 구체적인 문제는 Nagler [Nag26]가 제안한 최근의 접근법인 **추론-행위 의미론(Inference-Behaviour Semantics, I-bS)**의 체계적이고 형식적인 구현 방법이 결여되어 있다는 점이다. I-bS는 연결사의 "최소 추론 행위"를 격리하여 그 의미를 정의하는 유망한 프레임워크를 제공하지만, 이전에는 가능한 연결사 규칙의 공간 전체에 대한 포괄적인 기술적 평가가 부족했다. 본 논문은 I-bS를 검증하기 위해, 특정 구조 규칙(약화나 축약 등)에 독립적인 독특하고 최소한의 의미를 갖는 연결사가 존재하는지 여부를 판별하고자, 광범위하고 구조화되지 않은 후보 연결사 집합에 I-bS를 적용한다.

2. 방법론

본 연구는 최소한의 설정 내에서 연결사의 추론적 사용에 기반하여 그 "의미"를 측정하는 엄격하고 데이터 중심적인 접근 방식을 채택한다.

2.1 조사 대상: 모든연결사 (AllConnectives)

저자들은 조사 범위를 다음 제약 조건을 따르는 2차원 시퀀트 계산법에서 공식화 가능한 모든*연결사(operational rule pairs)로 정의한다:

• 연산 규칙: 별도로 존재하며, 명시적이고, 대칭적이어야 한다 (정의 3).
• 제약 조건: 최대 두 개의 전제 시퀀트와 규칙당 최대 두 개의 활성 공식(active formulae)을 가져야 한다.
• 전체 공간: 이는 정확히 10,816개의 구문론적으로 고유한 규칙 쌍(전제 형태와 활성 공식 위치의 조합)을 생성한다.

2.2 테스트 환경: 최소 유도 관계

특정 논리의 구조적 특징으로부터 연결사의 의미를 격리하기 위해, 저자들은 다음과 같은 최소 배경 계산법을 활용한다:

• 항등식 ($Id_{pr}$): 오직 원시 공식(primitive formulae)에 대해서만 제한된다.
• 컷 ($Cut_{cd}$): 문맥을 차별화하는 컷 규칙.
• 구조적 가정: 계산법은 교환 법칙(멀티셋)을 가정하지만, 약화(Weakening)와 축약(Contraction)은 제외한다. 이는 많은 논리들의 공통된 "부수적 핵(substructural kernel)"을 나타낸다.

2.3 측정 장치: 추론 행위

핵-측정치는 최소 설정 내에서 연결의 정의 가능성이 증명될 때 연결사가 보이는 구문론적 패턴인 추서 행위이다.

• 정의 가능성 기준: Belnap [Bel62]을 따라, 연결사가 계산법에 추가되었을 때 보존적 확장(새로운 정리가 연결사 없이 도출되지 않음)이 되고 고유성(연결사가 동형(isomorphism)까지 유일하게 결정됨)을 갖는다면 해당 연결사는 정의 가능하다.
• 의 의미 절 (Semantic Clause): 연결사의 "의미"는 최소한의 추론 행위 프로파일(정의 증명 과정 중 연결사와 그 활성 공식이 점유하는 구성 요소 위치의 가장 짧은 목록)을 산출하는 최소 연산 규칙 쌍으로 식별된다.

2.4 데이터 생성 및 분석

저자들은 10,816개의 후보를 체계적으로 필터링한다:

1. 필터 1 (공식화 가능성): 10,816개의 모든 규칙 쌍.
2. 필터 2 (보존성): 양의 사례(positive cases)에 대해 컷 제거(Cut-elimination)를 증명하고, 비보존적 사례에 대해 반례를 구성한다. 이를 통해 집합을 376개의 보존적 연결사로 줄인다.
3. 필터 3 (고유성): 수평적 및 수직적 상호 유도 가능성을 확립한다. 이를 통해 집합을 150개의 유일하게 정의 가능한 연결사로 더 줄인다.
4. 최소성 분석: 150개의 정의 가능한 연결사 중에서, 저자들은 "최소 의미 있는 연결사"와 "블로트넥티브(bloatnectives, 구문론적 중복이 있는 동등한 연결사)"를 구분한다. 전제 유형의 최소성(전제 시퀀트의 최소 카디널리티) 기준을 적용함으로써, 진정한 의미의 최소 의미 절들을 격리한다.

3. 주요 기여 및 결과

3.1 21개의 최소 의미 있는 연결사 식별

주요 결과는 정확히 21개의 최소 의미 있는 연결사를 식별한 것이다. 이들은 익숙한 논리 상수들과 그 역(converse) 또는 역원(inverse)에 대응하지만, 가법적(additive, lattice) 버전과 승법적(multiplicative, group) 버전 사이의 정밀한 구분이 존재한다:

• 영항(Nullary): 하한($\bot$) 및 상한($\top$).
• 단항(Unary): 두 가지 형태의 부정(직관주의적 $\neg$ 및 이중 직관주의적 $\sim$), 그리고 "사소한" 역 부정.
• 이항(Binary):
  • 논리곱(Conjunction): 가법적($\sqcap$) 및 승법적($\otimes$).
  • 논리합(Disjunction): 가법적($\sqcup$) 및 승법적($\oplus$).
  • 함축(Implication): 가법적 우측($\rightsquigarrow$), 승법적 우측($\to$), 가법적 좌측, 및 승법적 좌측.
  • 역(Converses) 및 역원(Inverses): 위 각각의 연결사는 그 역(구성 요소를 교체함)과 역원에 대해 별도의 의미 절을 가진다.

3.2 의미 절 및 프레임워크

본 논문은 21개의 연결사 각각에 대한 명시적인 의미 절(최소 규칙 쌍)을 제공한다. 결정적으로, 이러한 의미들이 논리 독립적임을 입증한다. 예를 들어, 승법적 논리곱($\otimes$)의 의미 절은 그것이 선형 논리, 고전 논리, 또는 직관주의 논리에 나타나더라도 동일하다. 이러한 연결사들이 완전한 논리(예: $\otimes$와 $\sqcap$가 동등한 고전 논리)에서 어떻게 행동하는지에 대한 차이는 연결사의 핵심 의미가 아니라 구조적 자원(축약 및 약화)에 기인한다.

3.3 다양한 논리 간의 의미론적 상호관계

본 연구는 이 21개의 연결사가 다양한 논리에서 갖는 의미론적 호환성을 매핑한다:

• 고전 논리 (LK): 논리곱, 논리합, 함축의 가법적 버전과 승법적 버전을 하나로 통합(conflate)한다. 또한 두 가지 형태의 부정을 통합한다.
• 직관주의 논리 (LJ): 논리곱과 논리합의 가법적 버전, 그리고 "우측" 함축과는 호환되지만, 고전적 부정의 절반만을 포착한다(구체적으로 $\sim_{min}$을 제외한 $\neg_{min}$만 포착).
• 이중 직관주의 논리 (LDJ): 고전적 부정의 나머지 절반($\sim_{min}$)과 다른 연결사들의 듀얼(duals)을 포착한다.
• 선형 논리 (LL): 21개의 모든 연결사를 구별하며, 이를 모두 의미론적으로 별개의 것으로 취급한다.

3.4 I-bS의 검증

본 논문은 특정 논리에 대한 편향 없이 가능한 규칙들에 대한 맹목적이고 철저한 탐색을 적용했을 때, 이론이 자연스럽게 기존의 확립된 논리 체계에서 발견되는 표준 연결사들로 수렴한다는 점을 보여줌으로써 I-bS의 타당성을 입증한다고 주장한다. 나머지 10,795개의 규칙 쌍이 정의 불가능하거나 최소가 아니라는 이유로 "노이즈"로서 걸러진다는 사실은 이 이론에 대한 "정당성 검사(sanity check)" 역할을 한다.

4. 의의 및 주장

본 논문은 자신의 연구 결과가 추론-행위 의미론 프레임워크의 검증임을 위치시킨다. 본 연구의 의의는 다음과 같다:

1. 논리 독립성: 연결사의 의미를 다양한 논리 전반에 걸쳐 불변하도록 정의하는 방법을 제공한다. 논리를 변경하는 것(예: 약화 추가)은 연결사의 의미를 바꾸는 것이 아니라, 그 연결사가 작동하는 구조적 문맥을 바꿀 뿐이다.
2. 의미 변화의 해결: 고전 논리와 직관주의 논리가 왜 서로 다르게 보이는지에 대한 의미론적 설명을 제공한다. 그들은 "and"나 "or"의 의미에 대해 이견을 갖는 것이 아니라, 어떤 최소 연결사를 허용하고 어떤 구조적 규칙을 허용하는지에 대해 서로 다를 뿐이다. 예를 들어, 고전적 "and"는 두 개의 구별된 최소 의미($\otimes$와 $\sq합$)의 혼합인 반면, 직관주의적 "and"는 엄격히 $\sqcap$이다.
3. 존재론적 검소함: 외부 모델이나 기저를 필요로 하지 않고, 오직 증명 체계의 부수적 핵에만 의존한다.
4. 포괄성: 주어진 제약 조건 하에서 공식화 가능한 모든 규칙의 공간을 다룸으로써, 본 논문은 2차원 시퀀트 계산법에서의 최소 연결사 의미에 대한 완전한 분류를 제공했다고 주장한다.

저자들은 결과가 특정 제약 조건(두 개의 전제, 두 개의 활성 공식, 특정 최소 계산법)에 상대적이라는 점을 언급하며 신중한 태도를 유지한다. 향후 연구에서는 다차원 계산법, 양화, 또는 대안적인 최소 유도 관계를 탐구할 수 있을 것이다. 그러나 정의된 범위 내에서, 본 논문은 I-bS가 논리적 연결사의 원시적 의미를 성공적으로 격리해 냈다고 단언한다.