The Varieties of Ought-Implies-Can and Deontic STIT Logic

1. 연구 문제 (Problem)

• 배경: 의무 논리 (Deontic Logic) 는 에이전트의 행위와 선택 이론 (Praxeology) 과 밀접하게 연결되어 있습니다. STIT 논리는 다중 에이전트 상호작용을 분석하는 강력한 프레임워크이며, 여기에 의무를 도입한 'Deontic STIT'가 개발되었습니다.
• 문제점: 전통적인 Deontic STIT 는 효용주의 (Utilitarian) 접근에 기반하여 특정 형태의 OiC 원리 (에이전트가 해야 할 일은 에이전트가 할 수 있어야 한다) 를 내포합니다. 그러나 철학 문헌에서는 '가능성 (Can)'의 의미 (논리적 가능성, 실제 가능성, 능력, 위반 가능성, 통제력 등) 에 따라 다양한 OiC 해석이 제안되어 왔습니다.
• 한계: 기존 프레임워크는 이러한 다양한 OiC 해석들을 포괄적으로 수용하거나, 서로 간의 논리적 의존성 (어떤 원리가 다른 원리를 함의하는지) 을 체계적으로 분석하기에 부적합했습니다. 또한, 기존 연구는 주로 공리 체계 (Axiomatic systems) 에 의존하여 증명 탐색이나 반례 추출이 어려웠습니다.

2. 방법론 (Methodology)

저자들은 다음과 같은 방법론적 혁신을 통해 문제를 해결했습니다.

• 모듈식 의미론 (Modular Semantics) 도입:
  • 기존 STIT 의 복잡한 시간적 분기 (Branching time) 와 효용 함수를 배제하고, **관계적 의미론 (Relational Semantics)**을 기반으로 한 모듈식 프레임워크를 제안했습니다.
  • 이를 통해 다양한 OiC 원리를 프레임 속성 (Frame properties) 으로 추가하거나 제거함으로써 유연하게 논리를 확장할 수 있게 되었습니다.
• 라벨된 시퀀트 계산 (Labelled Sequent Calculi) 개발:
  • 각 OiC 원리에 대응하는 논리 체계에 대해 **건전하고 완전한 (Sound and Complete) 라벨led 시퀀트 계산 (G3DSnX)**을 구성했습니다.
  • 시퀀트 규칙에 의미론적 정보 (예: 관계적 원자 $R_{\alpha}xy$) 를 명시적으로 포함시켜, 증명 탐색 (Proof-search) 과 반례 모델 (Counter-model) 추출을 가능하게 했습니다.
• 10 가지 OiC 원리의 형식화 및 분류:
  • 철학 문헌에서 논의된 10 가지 주요 OiC 해석 (OiLP, OiAP, OiA, OiV, OiR, OiO, OiA+O, OiCtrl, OiNC, OiNA) 을 STIT 언어로 정밀하게 형식화했습니다.
  • 특히 '의사결정적 (Deliberative)' 의무를 다루기 위해 새로운 연산자 ($\otimes^d_i$, $\otimes^c_i$) 를 정의했습니다.

3. 주요 기여 (Key Contributions)

1. OiC 원리의 체계적 분류 (Taxonomy):
   • 10 가지 OiC 원리를 논리적 강도에 따라 분류했습니다. 이는 기존에 체계적으로 정리된 바가 없었던 작업입니다.
2. 증명 이론적 분석 도구 제공:
   • 모든 Deontic STIT 논리에 대해 적용 가능한 시퀀트 계산 시스템을 제공했습니다. 이 시스템은 공리 체계보다 증명 탐색과 반례 생성에 유리합니다.
3. 논리적 의존성 규명 (Endorsement Principle):
   • 계산기 (Calculus) 간의 포함 관계를 분석하여, 어떤 OiC 원리를 수용하면 다른 어떤 원리들이 논리적으로 필연적으로 수용되어야 하는지를 규명하는 **'승인 원칙 (Endorsement Principle)'**을 제시했습니다.
4. 독립성 증명:
   • 증명 탐색 실패를 통해 특정 OiC 원리들이 서로 독립적임을 (한 원리가 다른 원리를 함의하지 않음) 반례 모델을 구성하여 증명했습니다.

4. 연구 결과 (Results)

• 논리 체계의 위계 구조:
  • Fig. 4 의 격자 (Lattice) 구조를 통해 16 가지 Deontic STIT 계산기 간의 강도 관계를 시각화했습니다.
  • 가장 약한 논리 (G3DSn) 에서 가장 강한 논리 (전통적 Deontic STIT 에 해당하는 G3DSn{D2, D3, D4}) 까지 계층 구조가 형성되었습니다.
• OiC 원리별 최소 논리 체계:
  • 각 OiC 원리가 정리가 되기 위해 필요한 최소한의 프레임 속성 (D2, D3, D4, D5) 을 Fig. 5 를 통해 명시했습니다.
  • 예: 전통적인 STIT 에서의 '능력 (OiA)'은 D3 과 D5 속성이 필요하지만, '통제 (OiCtrl)'와 같은 강한 원리는 D2, D3, D4, D5 가 모두 필요합니다.
• 논리적 독립성 발견:
  • 예를 들어, '규범적 능력 (OiNA)'은 '논리적 가능성 (OiLP)'이나 '실제 가능성 (OiAP)'과 논리적으로 독립적임을 보였습니다. 즉, OiLP 를 수용한다고 해서 OiNA 를 수용해야 하는 것은 아닙니다.
• 승인 원칙 (Endorsement Principle):
  • 특정 OiC 해석 (예: OiA) 을 지지하는 것은 논리적으로 더 약한 해석들 (OiLP, OiAP 등) 을 지지하는 것을 함의함을 보였습니다. 이는 철학적 논의에서 어떤 원칙을 선택할 때의 논리적 함의를 명확히 합니다.

5. 의의 및 중요성 (Significance)

• 철학적 논의의 형식화: 모호했던 '가능성'과 '의무'의 관계를 10 가지 구체적인 논리 체계로 세분화하여, 철학적 논쟁을 정밀한 논리적 분석의 대상으로 만들었습니다.
• 계산적 적용 가능성: 시퀀트 계산 (Sequent Calculus) 을 사용함으로써, 자동화된 규범적 추론 (Automated Normative Reasoning) 이나 증명 도구 개발의 기초를 마련했습니다.
• 이론적 확장성: 제안된 모듈식 프레임워크는 향후 지식 (Epistemic), 시간 (Temporal), 법적 (Juridical) 맥락에서의 STIT 논리 확장에도 쉽게 적용될 수 있는 기반을 제공합니다.
• 새로운 통찰: 기존에 간과되었거나 혼동되었던 OiC 원리들 간의 논리적 관계 (함의, 독립성, 동치) 를 명확히 함으로써, 윤리학과 논리학의 교차 연구에 중요한 기여를 했습니다.

결론적으로, 이 논문은 Deontic STIT 논리를 다양한 OiC 해석을 포괄할 수 있도록 재설계하고, 이를 증명 이론적 도구를 통해 체계적으로 분석함으로써 의무와 가능성의 관계를 규명하는 새로운 기준을 제시했습니다.