Knowing-Value Logic with Successor Arithmetic

기술 요약: 후속자 산술을 포함한 지식-값 논리(Knowing-Value Logic)

문제 제기
본 논문은 기존의 "지식-값(knowing-value)" 논리, 특히 Wang과 Fan이 제안한 조건부 지식-값 논리($ELKvr$)와 그 공고(public announcement) 확장형($PALKvr$)의 한계를 다룬다. 이러한 체계들은 "에이전트$i$가$\phi$라는 조건 하에$c$의 값을 안다"라는 문장을 형식화하지만, 산술 연산과 등호를 직접 처리할 수 있는 구문론적 기제를 결과적으로 결여하고 있다. 따라서 이들은 연속된 정수 사이의 관계와 같은 숫자 관련 명제의 내부 구조를 포착할 수 없다. 자연어 시나리오와 논리 퍼즐(예: "연속된 숫자" 퍼즐)에서 추론은 종종 에피스데믹(epistemic) 연산자, 등호, 그리고 산술 함수(특히 후속자 함수) 사이의 상호작용에 의존한다. 기존 프레임워크는 수치적 조건을 불투명한 명제 기호로 취급함으로써, 자연어에서는 자명한 함축(예: 어떤 수가 4자리임을 아는 것과 "만약 4자리라면 1111이다"라는 함축을 아는 것이 1111의 값을 안다는 것을 함축한다는 사실)을 도출하는 데 실패한다. 또한, 구조화되지 않은 객체 집합에 기반한 기존 논리들의 표준 의미론은 후속자 함수를 가진 자연수와 같은 특정 수학적 구조를 모델링하기에 불충분하다.

방법론
저자는 다음과 같은 요소들을 조건부 지식-값 논리에 통합한 새로운 논리인 **$ELKvSAr$**($PALKvSAr$의 공고 제거 파편)를 도입한다:

1. 항(Terms): 고정 상수 $0$, 비고정 상수$C$, 그리고 후속자 함수$S$를 포함한다.
2. 원자 명제(Atomic Formulas): 항들 사이의 등호($t_1 \approx t_2$).
3. 의미론(Semantics): 본 논문은 두 가지 구별된 모델 클래스를 정의한다:
   • 표준 모델(Standard Models): 표준 자연수 $(\mathbb{N}, S)$에 기반한다.
   • 비표준 모델(Non-Standard Models): 표준 자연수와 더불어 무수히 많은 "Z-체인"(정수의 복사본)을 포함하는 특정 비표준 후속자 산술 모델 $(\mathbb{N}^\star, S^\star)$에 기반한다. 이러한 확장은 이 논리가 표준 모델 클래스에 대해 컴팩트(compact)하지 않기 때문에 필요하다.

기술적 접근 방식은 다음과 같다:

• 공리화(Axiomatization): 등호, 후속자 산술(예: $\neg Sx \approx 0$, $S$의 단사성), 그리고 지식-값과 산술을 연결하는 특정 공리 및 규칙(예: $KvrS$, $KVE1$, $KVE2$)을 포함하는 시스템 **$ELKVSAr$**를 제안한다. 핵심적인 특징은 존재 양화사 제거와 유사하게 작동하여 유도 과정 중에 상대화된 지식-값 연산자를 제거할 수 있게 해주는 **$Kvr\text{-}Elim$** 규칙이다.
• 완전성 증명(Completeness Proof): 비표준 모델에 대한 강한 완전성(strong completeness)을 증명한다. 이 증명은 표준적인 정준 모델(canonical model) 대신 새로운 트리 형태의 정준 프레임(tree-like canonical frame) 구축을 활용한다. 이는 극대 일관 집합(maximal consistent sets)의 히스토리를 구성하고, 지식-값 연산자와 산술 구조에 의해 유도되는 동치 관계를 준수하면서 상수를 원소로 매핑하는 가치 함수(valuation function)를 정의하는 과정을 포함한다.
• 유한 모델 성질 및 결정 가능성(Finite Model Property and Decidability): 임의의 충족 가능한 공식이 유한한 비표준 모델을 가짐을 입증하며, 이를 산술적 거리를 보존하고 구성 요소를 분리하는 단사 사상(injective mapping)을 통해 유한한 표준 모델로 매핑할 수 있음을 보여준다. 이를 통해 유한 모델 성질과 결정 가능성을 확립한다.
• 응용(Application): 공고 연산자($PALKvSAr$)를 사용하여 에이전트의 지식이 산술적 추론을 통해 어떻게 진화하는지를 보여줌으로써 "연속된 숫자" 퍼즐을 형식화한다.

주요 기여 및 결과

1. 논리 확장: 등호와 후속자 함수를 조건부 지식-값 논리에 통합한 $ELKvSAr$및$PALKvSAr$을 도입하였다.
2. 공리계: **$ELKVSAr$**를 정의하였으며, 이는 다음이 증명되었다:
   • 비표준 모델 클래스에 대해 **강하게 완전(strongly complete)**하다.
   • 표준 모델 클래스에 대해 **약하게 완전(weakly complete)**하다.
3. 메타 논리적 성질:
   • 유한 모델 성질(FMP): 이 논리는 표준 모델과 비표준 모델 모두에 대해 FMP를 갖는다.
   • 결정 가능성(Decidability): $ELKvSAr$의 충족 가능성 문제는 결정 가능하다.
4. 비컴팩트성(Non-Compactness): 본 논문은 $ELKvSAr$이 표준 모델에 대해 컴팩트하지 않음을 증명하여, 완전성 증명을 위한 비표준 모델 도입의 필요성을 입증하였다.
5. 퍼즐 해결: "연속된 숫자" 퍼즐을 시스템 내에서 성공적으로 형식화하고 해결함으로써, 이 논리가 산술적 제약과 에피스데믹 업데이트에 기반한 가능성의 단계적 제거를 포착할 수 있음을 입증하였다.

의의
본 논문은 에피스데믹 논리와 산술을 통합하는 새로운 프레임워크를 제공한다고 주장한다. 지식-값 논리에 후속자 함수를 풍부하게 함으로써, 이 시스템은 이전 접근법들의 거친 입도(coarse-grained) 문제를 극복하고, 수치적 명제의 내부 구조에 의존하는 추론을 형식화할 수 있게 한다. 이 연구는 표현력(산술 및 에피스데믹 상호작용 처리)과 계산 복잡도(결정 가능성 유지) 사이의 균형을 확립한다. 저자들은 이 프레임워크가 "합과 곱(Sum and Product)"과 같은 퍼즐을 해결하는 데 필요한 더 복잡한 산술 구조(덧셈 및 곱셈)를 포함하는 향려 연구의 토대를 마련했다고 언급하며, 그러한 확장은 완전성과 결정 가능성에 있어 상당한 과제를 안겨줄 것임을 시사한다.