귀납적 기반 산술(Inductive Grounded Arithmetic): 구드스타인 정리, 하이드라, 그리고 $\Gamma_0$

요약

본 논문은 귀납적 기반 산술(IGA)을 제시하며, 제거 규칙 추가를 통해 시스템의 건전성을 확보합니다. IGA는 이를 바탕으로 구드스타인 정리와 커비-파리 하이드라 게임 같은 중요한 수학적 명제를 증명하는 데 사용됩니다. 또한 $\Gamma_0$와 같은 순서수의 정의 및 접근성 술어의 역할을 깊이 있게 다루며, 논리학의 기반을 탐구합니다.

핵심 포인트

• IGA는 제거 규칙 추가를 통해 시스템의 건전성을 확보함.
• 구드스타인 정리와 하이드라 게임 증명에 활용되는 이론적 틀 제공.
• $\Gamma_0$와 같은 순서수의 정의 및 접근성 술어의 역할을 분석.
• 시스템 전체가 Isabelle/HOL에서 기계적으로 검증됨.