페아노 산술은 충분하다, 왜냐하면 페아노 산술은 계산을 인코딩할 수 있기 때문임

• 페아노 산술(PA) 은 기계적인 계산 과정을 표현할 수 있으므로, 모든 단일 Goodstein 수열의 소멸을 PA에서 증명 가능함
• Cantor 표준형과 유전적 기수 표기법을 통해 Goodstein 수열과 그 하강성 등을 표현하며, 이로 인해 유한한 길이의 증명 구성이 가능함
• 귀납법(강한 귀납/초월적 귀납) 을 통해 특정 차수의 기수까지 증명을 각각 확장 가능함
• PA는 모든 자연수 n에 대해 “G(n)이 0에 도달한다” 는 것을 증명할 수 있으나, Goodstein 정리 전체(모든 n)에 대한 총체적 증명은 불가함
• PA로 계산, 데이터 구조(List, Pair 등), 심지어 프로그래밍 언어(Lisp) 자체의 인코딩 및 자체 증명 과정 인코딩도 충분히 구현 가능함

서론 및 문제 배경

• 이 글은 페아노 산술(PA)이 Goodstein 수열의 “각 n에 대해 0에 도달함(G(n) terminates)” 을 증명할 수 있음을 기술함
• 이는 논리학자에게는 자명해 보이지만, 프로그래머가 이해할 수 있도록 계산 인코딩의 관점에서 설명함
• Goodstein 수열의 각 경우에 대해 PA 내부에서 구체적 증명 루틴을 구성할 수 있음

Ordinals(순서수)와 Goodstein 수열

• Von Neumann 방식으로 순서수(Sets as Ordinals) 를 생성함
  • 0은 공집합, 1은 {0}, 2는 {0,1}, ω는 {0,1,2,…}, ω+1은 {0,1,2,…,ω} 등 순서가 잘 정의됨
• Goodstein 수열은 Cantor 표준형을 사용한 유전적 진법 표기법을 통해 기술됨
  • 예: ω^ω는 ((1,ω)), 즉 ((1,(1,1)))
  • < 순서는 각 항의 기수/계수에 대해 사전식 비교로 판단함

귀납법과 초월적 귀납(Transfinite Induction)

• 페아노 산술의 귀납법: 0에 대해 성립, n→n+1에 대해 성립하면 전체 자연수에 성립함
• 강한 귀납법 또한 PA로 증명 가능함
• 초월적 귀납(Transfinite induction): ZFC 등에서는 무한 기수에 대해 확장 가능하며, Cantor 표준형으로 쓰인 수에 대해 적용 가능함
  • Theorem 1: Cantor 표준형 내 하강 수열은 항상 유한함
  • Theorem 2: Cantor 표준형 수에 대해 초월적 귀납법 사용 가능함

PA에서의 초월적 귀납과 Goodstein 수열 증명 길이

• PA는 임의의 n에서 Goodstein 수열의 소멸 증명을 생성할 수 있음
  • Cantor 표준형의 타워 높이 m=O(log* n)(iterated log)에 따라 증명 구성 가능함
  • 각 단계별로 m번의 증명을 조합하여 전체 증명 길이 O(m^2) 또는 특별한 표기법(ω[m]) 도입 시 O(m log m)으로 단축 가능함
• 단, 전체 Goodstein 정리(모든 n)에 대한 증명은 PA에서 불가능함(ε0에 대한 초월귀납 불가)
  • 만약 가능하다면 PA의 무모순성도 증명 가능해져 Gödel 제2불완전성과 충돌함

PA의 프로그램, 데이터 구조 인코딩

• PA는 계산/프로그램/데이터 구조(숫자, 쌍, 리스트, 그 외 모든 구조) 를 충분히 인코딩 가능함
• 다음과 같은 방식으로 다양한 기능 구현 가능함:
  • 기초 논리 및 연산(+, *, pow, //, %, min, max 등)
  • 패턴 매칭과 조건 분기(if, cond 등)
  • 숫자를 두 개의 숫자(쌍)로 인코딩하거나, 쌍에서 다시 리스트 등 더 복잡한 구조로 반복 확장(재귀적 리스트, 트리, 텍스트 등)
• 이러한 데이터 구조 인코딩으로 임의의 가상 머신/프로그래밍 언어(Lisp 등) 해석기까지 구축 가능함

Lisp로의 부트스트랩과 인코딩

• Lisp를 예시로 하여, 기초적인 수치 및 논리 연산, 데이터 구조, 프로그래밍 언어 해석기/인터프리터 구현법을 설명함
• Lisp의 구조(명령/인자 매핑, 특수형, macro 등) 모두 PA에서 적절한 함수 조합으로 구현 가능함
• 더 나아가 PA 내에서 PA 증명 과정 자체, 논리 증명 절차, 자기지시적 구조까지 모두 기호적으로 인코딩 및 구현할 수 있음

PA 내에서의 논리 자체 인코딩

• 수리논리학에서의 First-Order Logic의 증명 과정을 PA 수의 데이터로 인코딩 가능함
• 각 증명 단계/명제/추론 규칙/올바른 증명 체크를 일련의 수치 함수/리스트 처리로 인식 및 처리
• 이런 메타적, 자기지시적 인코딩은 Gödel의 불완전성 및 Halting 문제 증명까지 연결됨

결론

• 계산, 데이터 구조, 프로그램, 논리 증명 과정까지 PA에서 충분히 인코딩, 증명, 해석 가능함
• 따라서 임의의 Goodstein 수열(n에 대해 G(n) 소멸) 는 PA 내부에서 구체적으로 증명 가능함
• 단, 전체 Goodstein 정리(모든 n)에 대해 "PA가 PA 내에서 Goodstein 정리를 증명한다"는 증명은 논리의 한계상 불가함
• 프로그래머 관점에서 PA는 계산 자체를 인코딩할 수 있는 완전한 논리 기반임