예전에 서강올빼미에서 소개해드렸던 저의 삼위일체 관련 두 편의 철학 논문이, 이번에는 Isabelle/HOL 형식화와 기계 검증을 거친 코드 형태로 **Archive of Formal Proofs (AFP)**에 실리게 되었습니다. 엔트리 제목은 **「Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL」**이고, 2026년 3월 17일자로 공개되었습니다.
이번 작업은 제가 앞서 발표했던 두 편의 한국어 철학 논문을 바탕으로, 존재론적 논증과 삼위일체 필연성 논증을 Higher-Order Logic 안에서 다시 구성한 것입니다. 이 형식화는 HOL의 기본 논리 외에 추가 공리를 도입하지 않고, 보수적 정의 확장을 통해 전개되며, H_{opt}라는 개념을 통해 “그보다 더 확실한 진리는 생각될 수 없는 궁극적 진리”를 구조적으로 정식화합니다. 또한 N=1, N=2, N \ge 4의 경우를 배제하고, 그 결과로 N=3 이 유일한 허용 가능한 구조로 도출되며, Nitpick을 통해 비공허하고 genuine한 triune model의 만족 가능성도 제시합니다.
개인적으로 이번 등재의 의미는, 철학 논증이 더 이상 인간 언어의 해석과 반박에만 머무는 것이 아니라, 명시적 정의·정리·의존관계·모형 탐색이 모두 드러나는 형태로 옮겨 철학적 주장 자체를 기계 검증 가능한 대상으로 다시 세운 시도라고 말씀드릴 수 있을 것 같습니다.
AFP의 Logic/Philosophical aspects 분류에는 이미 Gödel의 존재론적 논증, Anselm의 논증, Lowe의 논증 같은 작업들이 올라와 있습니다. 이번 등재는 그런 흐름 속에서, 삼위일체 필연성 연구를 포함한 논의의 연속으로서 의미가 있을 것 같습니다.
서강올빼미에서 예전에 제 한국어 논문들을 소개드렸기에, 이번에는 그 논의가 어디까지 확장되었는지 함께 나누고 싶어 이렇게 글을 올립니다. 철학이 인간 언어의 사유를 넘어, 논리와 코드의 수준에서도 어디까지 밀고 나갈 수 있는지 관심 있는 분들께 하나의 사례가 되었으면 합니다.^^
document 5.pdf (770.3 KB)