Higher-order Kripke models for intuitionistic and non-classical modal logics

비크토르 바르소우나시멘토의 논문"직관주의 및 비고전적 모달 논리를 위한 고차 크립키 모델"에 대한 설명을 일상적인 언어와 창의적인 비유로 번역한 것입니다.

큰 그림: "모델의 모델"을 구축하기

사람들이 필수적(반드시 일어나야 함) 인 것이나 가능적(일어날 수 있음) 인 것에 대해 어떻게 결정을 내리는지 이해하려고 노력한다고 상상해 보세요.

표준 논리 (고전 수학에서 사용하는 논리) 에서는 크립키 모델이라는 도구를 사용합니다. 크립키 모델을 다양한 가능한 세계들의 지도라고 생각하세요.

• 세계: 사실들이 참이거나 거짓인 특정 상황 (예: "비가 오고 있다").
• 지도: 이러한 세계들을 연결하는 네트워크. 세계 A 가 세계 B 와 연결되어 있다면, B 는 A 의"가능한 대안"이라는 뜻입니다.
• 규칙: 세계 A 에서 무언가가"필수적"이라면, A 와 연결된 모든 세계들에서 참이어야 합니다.

문제점:
이 논문은 직관주의 논리에 초점을 맞추고 있습니다. 이는 증명 없이는"참이거나 거짓이다"라고 말할 수 없다고 믿는 사람들이 사용하는 수학의 한 종류입니다. 이 논리에서 진리는 시간이 지남에 따라 자라납니다 (수학자가 새로운 정리를 발견하는 것처럼).

이러한 진리가 성장하는 시스템 내에서"가능성"을 다루는 전통적인 방식은 messy 합니다. 두 가지 다른 유형의 연결 (관계) 이 얽힌 모델을 필요로 합니다. 마치 도시를 항해할 때 두 개의 서로 다른 지도를 동시에 사용하는 것과 같습니다: 하나는 도로용이고 다른 하나는 지하철용인데, 이 둘이 어떻게 상호작용하는지에 대한 규칙은 복잡하고 시각화하기 어렵습니다.

해결책:"중첩"접근법

저자 비크토르 바르소우나시멘토는 관점의 근본적인 변화를 제안합니다. 두 개의 지도를 하나로 접어 넣는 대신, 모델의 모델을 구축할 것을 제안합니다.

비유: 타임라인 도서관
수학자의 삶을 타임라인으로 기록한 책들이 있는 도서관을 상상해 보세요.

• 책 내부 (모델): 아침, 오후, 저녁과 같은 시간의 다른 순간들을 나타내는 장들이 있습니다. 아침에서 저녁으로 이동함에 따라 수학자는 더 많은 정리를 증명합니다. 이것이 표준"크립키 모델"입니다.
• 도서관 (새로운 모델): 이제 도서관 자체가 지도라고 상상해 보세요. 이 새로운 지도의"세계"들은 단순히 시간의 순간이 아니라 **전체 책 (타임라인)**입니다.

이 새로운 시스템에서:

1. "세계"는 타임라인입니다: "아침에 비가 오는가?"라고 묻는 대신, "타임라인 A 의 아침에서 이것이 참인가?"라고 묻습니다.
2. 연결: 우리는 책들 사이에 선을 그립니다."타임라인 A"가"타임라인 B"와 연결되어 있다면, 타임라인 B 는 타임라인 A 의 유효한 대안 버전이라는 뜻입니다.
3. 마법 같은 트릭: 타임라인 A 의 아침에 무언가가"가능"한지 결정하려면, 타임라인 A 의 오후를 보지 않습니다. 대신 타임라인 B 의 아침을 봅니다.

왜 이것이 더 나은가요?
기존의 messy 한 시스템에서는"가능성"에 대한 규칙이"성장하는 진리"규칙 안에 딱 맞게 정교하게 설계되어야 했습니다. 하지만 이 새로운"중첩"시스템에서는 규칙이 간단하고 자연스럽습니다.

• 필수성: "아침에 정리 X 를 증명하는 것이 필수적인가?" -> "내 타임라인과 연결된 모든 대안 타임라인의 아침에서 정리 X 가 증명되었는가?"
• 가능성: "아침에 정리 X 를 증명하는 것이 가능한가?" -> "아침에 정리 X 를 증명하는 적어도 하나의 대안 타임라인이 있는가?"

저자는 이를 고차 크립키 모델이라고 부릅니다. 러시아 인형처럼 중첩되어 있습니다:

• 레벨 0: 단일 세계 (진리 할당).
• 레벨 1: 레벨 0 세계들로 구성된 모델 (표준 크립키 모델).
• 레벨 2: 레벨 1 모델들로 구성된 모델 (새로운"고차"모델).

두 가지 주요 캐릭터: IK 와 MK

이 논문은 저자가 IK와 MK라고 부르는 두 가지 특정 논리 시스템에 대해 이 새로운 시스템을 테스트합니다.

1. IK (보수적인 것): 이 논리는 조금 신중합니다. 무언가가 필수적인지 확인하려면 대안 타임라인과 그 타임라인 내의 모든 미래 순간을 모두 살펴봅니다. 마치"어떤 대안 날의 아침에 X 를 증명할 수 없다면, 그것은 필수적이지 않다"라고 말하는 것과 같습니다.
2. MK (대담한 것): 이 논리는 더 강력합니다. 대안 타임라인의 특정 순간만 봅니다. 그 대안의"미래 성장"은 무시합니다. 마치"그날 이후에 무슨 일이 일어나든 상관없이, 대안 날의 아침에 X 를 증명할 수 있다면, 그것은 가능하다"라고 말하는 것과 같습니다.

저자는 그의 새로운"타임라인 도서관"시스템이 이 두 논리 모두에 완벽하게 작동함을 증명합니다. 사실, 이 새로운 시스템은 настолько 깔끔해서 기존 시스템의 복잡한 규칙들 (이중 관계 규칙) 이 억지로 넣은 것이 아니라 자연스럽게 나타나게 합니다.

"대규모 일반화"

이 논문에서 가장 흥미로운 부분은 마지막 섹션입니다. 저자는 이"모델의 모델"아이디어가 직관주의 논리뿐만 아니라 더 넓은 영역에 적용될 수 있다고 제안합니다.

그는 가설(더 많은 증명이 필요한 강력한 추측) 을 제시합니다:

• 기존 문제: 표준 크립키 모델 (레벨 1) 이 완전히 설명할 수 없는 기이하고 복잡한 논리 시스템들이 있습니다. 이들은"불완전"합니다.
• 새로운 희망: 모델을 계속 중첩한다면 (레벨 2, 레벨 3 등), 존재하는 모든 논리 시스템을 설명할 수 있을지도 모릅니다.

비디오 게임 그래픽을 생각해 보세요.

• 표준 모델 (레벨 1): 8 비트 그래픽과 같습니다. 간단한 게임에는 작동하지만 복잡한 장면에서는 흐릿하고 블록처럼 보입니다.
• 고차 모델 (레벨 2, 3...): 4K 또는 8K 그래픽과 같습니다. 더 많은 세부 정보 층 (모델 안에 모델) 을 추가함으로써 논리가 얼마나 복잡해지든 어떤 장면도 완벽하게 렌더링할 수 있습니다.

요약

이 논문은 우리가 논리 모델을 잘못 바라보고 있다고 주장합니다. 서로 다른 두 가지 규칙을 하나의 지도에 억지로 끼워 넣으려 하기보다는, 모델들이 새로운 모델들의 구성 요소가 되는 위계 구조를 구축해야 합니다.

• 구식 방식: 두 가지 유형의 도로가 섞인 messy 한 지도.
• 새로운 방식: 가능한 것이 무엇인지 이해하기 위해 지도 사이를 이동하는 지도들의 도서관.

이 접근법은 수학적으로 우아하고, 개념적으로 사울 크립키의 원래"가능한 세계"아이디어에 더 가깝으며, 수십 년간 수학자들을 당혹스럽게 해 온 논리의 가장 어려운 문제들을 해결할 만큼 강력할 가능성이 있습니다.