The calculus of neo-Peircean relations

1. 문제 제기 (Problem)

• 관계 미적분학 (CR) 의 역사적 한계: 19 세기 데 모건 (De Morgan) 과 피어스 (Peirce) 가 도입한 CR 은 불 대수 (Boolean algebra) 를 관계로 확장한 것으로, 양화사 (quantifiers) 없이 관계만을 연산하여 논리를 표현합니다. 그러나 CR 은 1 차 논리보다 표현력이 낮고 (strictly less expressive), 완전한 유한 공리화가 불가능하다는 것이 타르스키 (Tarski) 와 후속 연구들 (Mon64 등) 에 의해 증명되었습니다.
• 기존 접근법의 결함: CR 의 부정적 결과 (no-go theorems) 는 전통적인 **카르테시안 (Cartesian) 구문 (syntax)**에 기반한 관계의 표현 방식에서 비롯됩니다. 이 방식은 변수 바인딩, 스코프, 캡처 방지 치환 등의 복잡성을 피하기 위해 양화사를 제거했으나, 그 대가로 표현력과 완전성을 잃었습니다.
• 목표: CR 의 장점 (양화사 없음, 순전히 대수적 추론) 을 유지하면서, 1 차 논리와 동등한 표현력을 가지며 완전한 공리화를 가능하게 하는 새로운 체계 개발.

2. 방법론 (Methodology)

저자들은 전통적인 구문 (term-based syntax) 을 버리고 **도식적 구문 (diagrammatic syntax)**인 **스트링 다이어그램 (String Diagrams)**을 기반으로 한 범주론적 구조를 도입합니다.

• 범주론적 구조의 결합:
  1. 카르테시안 바이카테고리 (Cartesian Bicategories): 존재적 양화 ($\exists$) 와 논리곱 ($\land$) 을 표현. (흰색 배경 다이어그램)
  2. 코카르테시안 바이카테고리 (Cocartesian Bicategories): 보편적 양화 ($\forall$) 와 논리합 ($\lor$) 을 표현. (검은색 배경 다이어그램)
  3. 선형 바이카테고리 (Linear Bicategories): 위 두 구조를 통합하고, 두 가지 합성 연산 ($\circ$ 와 $\bullet$) 간의 선형 분배 법칙을 정의.
• First-Order Bicategories (fo-bicategories) 의 정의:
  • 위의 세 가지 구조를 통합하여 fo-bicategories를 정의합니다.
  • 핵심 아이디어는 흰색 (카르테시안) 과 검은색 (코카르테시안) 구조가 선형 쌍대 (linear adjunction) 관계를 형성하고, **선형 프로베니우스 법칙 (linear Frobenius laws)**을 만족하도록 하는 것입니다.
  • 이를 통해 관계의 반대 (converse) 와 여집합 (complement) 연산이 자연스럽게 도출됩니다.
• NPR$\Sigma$ (Neo-Peircean Relations):
  • 위 axioms 를 기반으로 정의된 계산 체계입니다.
  • 변수가 없으며, 복사 (copier) 와 삭제 (discharger) 연산자를 명시적으로 다룹니다.
  • 다이어그램의 색상을 반전 (photographic negative) 시키면 논리적 부정 (negation) 을, 거울상 (mirror image) 을 취하면 반대 관계 (converse) 를 표현합니다.

3. 주요 기여 (Key Contributions)

1. 완전한 공리화 (Complete Axiomatisation):
   • NPR$\Sigma$는 1 차 논리 (FOL) 와 동등한 표현력을 가지면서도, 유한한 공리 집합으로 완전하게 공리화될 수 있음을 증명했습니다.
   • 이는 기존 CR 에 대한 "완전한 유한 공리화는 불가능하다"는 부정적 정리를 우회한 것입니다. 우회 이유는 NPR$\Sigma$가 CR 보다 더 표현력이 풍부하기 때문입니다.
2. 도식적 추론 (Diagrammatic Reasoning):
   • 증명 과정이 방정식 치환이 아닌 **도형의 재작성 (diagram rewriting)**으로 수행됩니다.
   • 이는 "Deep Inference" (깊은 추론) 와 유사하며, 증명 보조 도구 (proof assistants) 에 적용하기에 매우 적합합니다.
3. 비어 있는 모델 (Empty Models) 의 허용:
   • 전통적인 FOL 은 정의역이 비어있지 않음을 가정하지만, NPR$\Sigma$는 **비어 있는 모델 (empty domain)**을 허용합니다.
   • 이는 논리 체계의 일반성을 높이며, 비어 있는 모델의 경우 NPR$\Sigma$가 명제 논리 (Propositional Logic) 로 축소됨을 보여줍니다.
4. 범주론적 의미론 (Functorial Semantics):
   • NPR$\Sigma$는 Free First-Order Bicategory로 정의되며, 이는 레어베어 (Lawvere) 의 대수적 이론의 의미론을 관계론적 맥락으로 확장한 것입니다.
   • 모델은 fo-bicategories 사이의 사상으로 정의됩니다.

4. 주요 결과 (Results)

• 완전성 정리 (Completeness Theorem, Theorem 3.5):
  • NPR$\Sigma$의 모든 항 $c, d$에 대해, $c \preceq d$ (문법적 포함) 일 필요충분조건은 모든 모델에서 $c$의 의미론적 값이 $d$의 값에 포함되는 것입니다 ($c \leq d$).
  • 증명 방법은 헨킨 (Henkin) 의 증명법을 도식적으로 적응화한 것으로, 비어 있는 모델을 다루기 위해 추가적인 단계를 거칩니다.
• 표현력 등가성:
  • NPR$\Sigma$는 1 차 논리 (FOL), 관계 미적분학 (CR), 퀸의 술어 함수 논리 (PFL), 피어스의 존재적 그래프 (EGs) 를 모두 인코딩할 수 있습니다.
  • 특히, CR 을 NPR$\Sigma$로 인코딩하면 CR 의 포함 관계를 NPR$\Sigma$의 공리들을 사용하여 검증할 수 있게 됩니다.
• 공리 체계의 구조:
  • 공리들은 카르테시안 바이카테고리, 코카르테시안 바이카테고리, 선형 바이카테고리의 상호작용을 통해 도출됩니다.
  • "논리의 도 (Tao of Logic)"라고 불리는 다이어그램은 이 복잡한 구조를 직관적으로 보여줍니다.

5. 의의 및 중요성 (Significance)

• 논리학의 대수적 뿌리 복귀: 논리학을 양화사와 변수 바인딩의 복잡성에서 해방시켜, 순수한 대수적/도식적 구조로 되돌려 놓았습니다.
• 컴퓨터 과학적 응용:
  • 데이터베이스 이론: 관계 대수와의 밀접한 연결.
  • 프로그래밍 언어 의미론: 비동기적 계산, 양자 계산 (정보 복사 불가), 이동 계산 (mobile computation) 등 전통적인 구문으로 다루기 어려운 영역을 스트링 다이어그램으로 자연스럽게 표현 가능.
  • 증명 보조 도구 (Proof Assistants): 변수 바인딩 처리의 복잡성이 제거되어 자동화 추론에 유리합니다.
• 피어스의 직관 현대화: 19 세기 피어스가 제안했던 관계 대수와 존재적 그래프의 직관들이 현대 범주론 (바이카테고리, 선형 논리) 을 통해 정교하게 정립되었음을 보여줍니다.

결론적으로, 이 논문은 "관계의 미적분학"을 1 차 논리와 동등한 표현력을 가지면서도 완전한 공리화가 가능한 체계로 재탄생시켰으며, 이는 범주론적 도구 (스트링 다이어그램, 바이카테고리) 를 통해 논리학의 새로운 지평을 열었다는 점에서 큰 의의가 있습니다.