First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

당신이 이사벨(Isabelle)이라는 이름의 초지능 로봇에게, 어떤 곳에서는 참이지만 다른 곳에서는 거짓일 수 있는 세상, 그리고 그 장소들에서 "모든 사람"이나 "누군가"에 대해 이야기할 수 있는 세상을 가르치려 한다고 상상해 보십시오. 이것이 바로 **1차 양상 논리(First-Order Modal Logic, FML)**의 세계입니다. 이것은 "만약 ~라면 어떨까?"라는 질문과 모든 가능한 존재들에 대한 출석 체크가 결합된 게임과 같습니다.

문제는 이사벨이 매우 정밀하고 고차원적인 언어인 **고차 논리(Higher-Order Logic, HOL)**를 사용한다는 점입니다. 이사벨에게 우리의 "만약 ~라면 어떨까?" 게임을 이해시키기 위해, 저자들은 우리의 논리를 이사벨의 언어로 번역하는 세 가지 서로 다른 다리(임베딩)를 구축해야 했습니다.

세 가지 다리

1. 깊은 다리 (설계도 - The Deep Bridge): 이것은 마치 논리의 모든 규칙, 모든 "그리고(and)", 모든 "아니오(not)", 모든 "모든(for all)"을 하나의 거대한 구조물 속의 개별적인 벽돌로 만드는 것과 같은, 논리의 물리적 모델을 직접 구축하는 것입니다. 매우 무겁고 상세하며, 논리의 형태 자체를 연구하기에는 완벽하지만, 로봇이 그 위에서 빠르게 달리기는 어렵습니다.
2. 무거운 얕은 다리 (풀 서비스 호텔 - The Heavyweight Shallow Bridge): 이 다리는 마치 고급 호텔과 같아서, 모든 투숙객(모든 공식)은 자신만의 방을 배정받으며, 그 방에는 세계의 지도, 모든 사람의 명단, 그리고 특정 안내서가 함께 제공됩니다. 모든 것을 명시적으로 운반합니다. 매우 명확하지만, 들고 다니기에 다소 육중합니다.
3. 가벼운 얕은 다리 (미니멀리스트 텐트 - The Lightweight Shallow Tent): 이 논문의 주인공은 바로 이것입니다. 이것은 아주 작고 휴대 가능한 텐트입니다. 전체 지도와 사람들의 명단을 다 들고 다니는 대신, 오직 하나의 "세계"와 하나의 "안내자"만을 가집니다. 나머지 가구들은 이미 그곳에 있다고 가정하는 것입니다. 매우 가볍기 때문에 로봇이 자신의 자동 추론 도구(예: "Sledgehammer"나 "Nitpick")를 매우 빠르게 실행할 수 있게 해줍니다.

큰 장애물: 전사성 문제 (The Surjectivity Problem)

여기서 이야기가 까다로워집니다. 저자들은 가벼운 텐트와 깊은 설계도가 실제로 똑같은 것을 말하고 있다는 것을 증명하고 싶었습니다. 즉, 설계도에서 어떤 문장이 참이라면 텐트에서도 참이어야 하고, 그 반대도 마찬가지임을 보여주고 싶었습니다.

하지만 문제가 생겼습니다. 가벼운 텐트는 셀 수 있는(countable) 수의 사람들(예: 자연수 1, 2, 3...)만을 가리킬 수 있는 안내자(변수 할당)를 사용합니다. 그러나 깊은 설계도는 셀 수 없는(uncountable) 수의 사람들(예: 직선 위의 모든 실수)이 존재하는 우주를 허용합니다.

만약 우주가 거대하고 셀 수 없이 크다면, 셀 수 있는 목록만을 담을 수 있는 안내자는 결코 모든 사람에게 닿을 수 없습니다. 이는 마치 1,000명의 이름만 적을 수 있는 명단을 가지고 수십억 명의 관중이 모인 경기장에서 출석 체크를 하려는 것과 같습니다. 저자들은 만약 안내자가 셀 수 없는 우주의 모든 사람에게 닿도록 강제한다면, 증명이 무너질 것이라는 사실을 깨달았습니다.

마법 같은 해결책: 하향 뢰벤하임-스콜렘 정리 (The Downward Löwenheim–Skolem Theorem)

이를 해결하기 위해, 저자들은 안내자가 셀 수 없는 군중에 닿도록 만드는 대신, (셀 수 있는) 하향 뢰벤하임-스콜렘 정리라는 수학적 마법을 사용했습니다.

이렇게 생각해 보십시오. 저자들은 거대하고 셀 수 없는 우주에 대해서도, 그 논리가 다루는 내용에 대해서는 똑같이 작동하는 더 작고 셀 수 있는 "그림자" 우주가 존재한다는 것을 증명했습니다. 이것은 마치 거대한 도시와 똑같이 작동하면서도 책상 위에 올려놓을 수 있을 만큼 작은, 도시의 완벽한 미니어처 모델을 찾는 것과 같습니다.

그들은 설령 실제 세계가 셀 수 없이 거대할지라도, 우리는 항상 이 셀 수 있는 그림자로 축소할 수 있다는 것을 보여주었습니다. 우리의 가벼운 텐트의 안내자가 이 셀 수 있는 그림자 속의 모든 사람에게 닿을 수 있기 때문에, 텐트와 설계도 사이의 다리는 다시 견고해졌습니다. 저자들은 단순히 추측하거나 시뮬레이션한 것이 아니라, 이사벨 안에서 엄격한 수학적 논거를 구축하여 이것이 작동함을 증명했습니다.

하지 않은 것들 ("아니오" 목록)

이 논문이 무엇을 하지 않았는지 아는 것이 중요합니다. 그래야 오해를 피할 수 있습니다:

• 변하는 영역 (No Varying Domains): 그들은 어떤 세계에서는 사람들이 태어나고 어떤 세계에서는 죽는 것처럼, 세계마다 사람들의 목록이 변하는 문제를 해결하지 않았습니다. 그들은 고정된 영역(constant domain), 즉 모든 가능한 세계에 동일한 사람들의 집합이 존재하는 상황을 유지했습니다.
• 동등성 (No Equality): 그들은 이 논리에 특수한 "같다($=$)" 기호를 포함하지 않았습니다. 그들은 사물들 사이의 관계에 집중했지, 두 사물이 동일한지 여부에 집중하지 않았습니다.
• 무한한 세계 (아직은 아님): 이들의 셀 수 있는 그림자가 작동하게 하기 위해, 그들은 세계의 개수 또한 셀 수 있어야 한다고 가정해야 했습니다. 그들은 셀 수 없는 수의 세계를 다루는 것은 향후 과제로 남겨두었습니다.

결과: 검증된 연결

저자들은 이것이 작동한다고 제안만 한 것이 아니라, 이사벨 내부에서 **증명을 기계화(mechanized the proof)**했습니다. 그들은 치환 기계(변수를 파괴하지 않고 교체하는 도구)를 구축했고, 다음을 증명했습니다:

1. 깊은 설계도와 가벼운 텐트는 서로에게 충실(faithful)합니다.
2. 당신은 빠르고 가벼운 텐트에서 무언가를 증명할 수 있으며, 그 증명들은 깊고 상세한 설계도에서도 반드시 참임이 보장됩니다.
3. 그들은 유명한 논리 규칙들(K-공리 및 Barcan 공식 등)을 확인하여 이 규칙들이 잘 작동하는지 테스트함으로써 이를 검증했습니다.

요약하자면, 저자들은 컴퓨터가 양화사(quantifiers)가 포함된 복잡한 "만 if" 시나리오를 추론할 수 있도록 매우 효율적이고 가벼운 방법을 만들었으며, 이 지름길이 우주가 무한히 클 때조차 중요한 세부 사항을 놓치지 않는다는 것을 수학적으로 증명했습니다. 그들은 (셀 수 없는 도메인 문제라는) 잠재적인 막다른 골목을 영리한 수학적 축소 기법을 사용하여 해결된 퍼즐로 바꾸어 놓았습니다.