다양한 논리, 하나의 방법론: 형식화된 추론에서의 논리적 다원주의를 위한 호소 (preprint)

본 입장 성명(position statement)은 고전적 고차 논리 (HOL) 내에서 비고전 논리 (non-classical logics)의 얕은 임베딩 (shallow embeddings)에 관한 지난 20년간의 연구를 되돌아봅니다. 이 연구 흐름은 HOL 내의 다양한 논리 임베딩 (logic embeddings)으로 확장되었으며, LogiKEy 논리적 다원주의 지식 표현 및 추론 (logic-pluralistic knowledge representation and reasoning) 방법론에 영감을 주었습니다. 본 논문은 계산 형이상학 (computational metaphysics)에 근거하여, LogiKEy와 같은 통합적인 메타 논리 프레임워크 (meta-logical framework) 내에서 대상 논리 (object-logic) 수준의 논리적 다원주의 (logical pluralism)를 옹호합니다. 더 넓게는, 현대적 증명 보조기 (proof assistants)에서 논리적 다원주의에 대한 원칙적인 지원을 주장하며, 논리적 제국주의 (logical imperialism) — 대규모 이론 개발을 위해 단일한 기초 논리를 경직되게 채택하는 것 — 에 대해 경고합니다. 이러한 제국주의는 LogiKEy가 가능하도록 설계된 학제 간 재사용 (interdisciplinary reuse)을 저해합니다.