▲

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

 (math.stackexchange.com)
1P by GN⁺ 1일전 | ★ favorite | 댓글 1개
  • 페아노 산술(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는 계산 자체를 인코딩할 수 있는 완전한 논리 기반임
▲
GN⁺ 1일전  [-]
Hacker News 의견
  • 이 글은 제가 Stack Overflow에서 질문했던 내용을 블로그 포스트로 만든 것 Peano 공리계로 증명할 수 있는 한계와 어떻게 Peano 공리계 내에서 Lisp를 부트스트랩할지 설명이 포함됨 농담은 대부분 두 번째 섹션에 있음 수정이나 추가 질문도 환영함
    • 이 글을 읽으면서 "Why Lisp?" 섹션에서 괄호가 맞지 않는 부분을 발견함 (defun not (x) (if x false true) 예시 참고) 누군가 괄호를 사용하기 시작하면 본능적으로 맞게 닫혀 있는지 확인하게 됨 이후에 "괄호가 균형을 이루는지 컴퓨터로 프로그램하기 쉽다"고 언급한 것을 보고 크게 웃음 이런 농담이 정말 재미있었고, "Basic Number Theory" 섹션에서 ; After a while, you stop noticing that stack of closing parens. 코멘트도 인상적임 오랜만에 Lisp를 다시 접했는데 글이 정말 재미있었음
    • 이 글이 정말 흥미로움 아직 도입부밖에 안 읽었지만, Peano 공리계(PA) 안에서 Goodstein 수열의 모든 특수한 경우가 0에 도달한다는 사실은 증명할 수 있지만 ‘모든’ 경우가 0에 도달한다는 것은 증명할 수 없는 점이 흥미로움 (사실 당연한 결과이긴 해도 흥미 진진함) 그리고 Peano 공리계만으로도 계산을 인코딩할 수 있다는 사실이 정말 이상함 (원론적으로 보면 당연하지만, 이전엔 한 번 더 자기 참조를 생각해보지 않음) 마침 최근에 집합론을 좀더 공부해보려 Intro to Set Theory 교재에서 Goodstein 수열 부분까지 학습한 경험이 있음 혹시 추천해줄만한 고급 집합론 교재나 Peano 산술 깊이 파고든 교재가 있으면 알려주면 고맙겠음 Goodstein 정리 증명에 PA가 왜 부족한지 이해하는 것이 작은 목표이지만, 대신 추천해줄만한 다른 길도 환영함
    • 글의 오메가(omega) 중 두 군데에서 \omega로 표기하는 걸 깜빡한 부분이 있음
  • Boyer-Moore 이론과 매우 유사함 이 이론은 Peano 공리계 수준에서 수학을 쌓아 올리는 것 Boyer와 Moore는 이 이론을 구현한 자동 정리 증명기를 개발했고, GNU Common LISP로 작동하는 사본도 가지고 있음 "A Computational Logic" 논문과 nqthm 구현물 링크도 참고 가치 있음 논문에서 예로, Peano 공리로 시작할 때 소수의 곱셈처럼 복잡한 정리는 어렵지만, 덧셈의 교환법칙, 곱셈의 분배법칙, GCD 함수 관련 정리 등은 충분히 증명 가능하다는 내용이 인상적임
  • 나는 수학과 프로그래밍 모두 배경이 있는데, 개인적으로 Goodstein 정리의 독립성 부분을 자기 지시적으로 우회 가능하다는 점이 더 흥미로움 PA+"PA가 오메가 일관적(omega-consistent)이다"라는 전제를 추가하면 Goodstein 정리를 증명할 수 있지 않을까 생각됨, 그리고 이는 epsilon_0까지 초한귀납법(transfinite induction)도 가능하지 않을까 추측함 EDIT: 어쩌면 "PA가 일관적이다"만으로도 충분하지 않을까?
    • 아쉽게도 그렇지 않음 그리고 Con(PA) 뿐 아니라 임의의 보편적으로 수량화된 공식만 가지고도 충분하지 않다는 사실이 있음 관련 Math StackExchange 답변 참고 첫 번째 질문과 관련해, 오메가 일관성을 PA의 공식으로 어떻게 인코딩하는지 궁금함 바로 떠오르지 않아 호기심이 생김
    • 내가 Stack Overflow에서 질문자임 질문에 몇 가지 답변 링크를 추가로 적어 두었음 본질적으로 "PA가 일관적이다"만으로는 충분하지 않지만, "PA에서 증명되면 참"이라는 일종의 "균일 반영 원리(uniform reflection principle)"가 있으면 충분함 이 원리가 오메가 일관성과 완전히 같다고 확신할 수는 없지만, 위키피디아의 설명 상으론 같다고 읽힘 T가 오메가 일관적이면 "T + RFN_T + 모든 참인 공식의 집합이 일관적"이라는 의미이고, 이는 "T + RFN_T가 참"이라는 것과 동치로 해석됨
    • 나는 이런 귀납(재귀) 구조도 마음에 듦 결국 PA가 어떤 걸 증명하는지에 대한 메타-증명을 만들고, PA를 신뢰한다면 이 메타-증명도 신뢰할 수 있다고 생각함 단순히 "PA가 일관적이다"로 충분하다는 부분은 확실하게 이해되진 않음 내 생각에 PA+"PA 일관성"은 표준 자연수 범위에서는 Goodstein 정리가 참인 모델이 존재하지만, 동시에 어떤 비표준 정수 N에 대해 Goodstein 정리가 거짓인 모델도 존재하게 허용할 것 같음 오메가-일관성의 더 강한 명제로 이런 케이스를 배제할 수 있다고 봄
    • math exchange 게시글에선 PA+초한귀납법(epsilon_0) 증명이 PA 자체를 증명한다고 언급함 내 생각에 PA+"PA 일관성"이면 epsilon_0까지 초한귀납법을 증명 가능할 것 같음
    • 이제 이 주제는 내가 편하게 발언할 수 있는 디테일을 넘어가는 것 같음 ChatGPT에 따르면 "PA+PA 일관성"만으로는 충분하지 않다는 설명임 ChatGPT가 워낙 논리학 책들을 많이 소화했을 테니, 그런 주장이라면 믿을 수 있을 듯함
  • Stack Overflow에서 JoJoModding에게 쓴 댓글이 올바르지 않음 "비표준 PA 모델에는 무한한 자연수가 있기 때문에 PA가 자신이 어떤 증명을 만들었는지를 증명해도 그것이 유한한 길이라는 것을 증명하지 못한다"고 했지만, 실제로 PA가 "PA가 X를 증명했다"고 증명하면 PA가 X 자체도 증명함 중요한 점은 비표준 모델 존재가 아니라, 표준 자연수 모델이 PA의 모델이라는 점임 그래서 "PA가 X를 증명함을 증명하면" 실질적으로 표준 유한 자연수에 해당하는 증명이 하나 생성되며, 이 수를 이용해 PA 내에서 X에 대한 실제 증명을 만들 수 있음
    • 논리를 더 자세히 검토해볼 시간은 없지만, 자연어로 보면 "PA가 'forall n, G(n)'을 증명함"이 아니라 "PA가 'forall n, Provable(G(n))'을 증명함"이라는 차이가 핵심임 논리에 약한 편이라 누군가 왜 "forall n, Provable(P(n))"을 증명한다고 해서 "Provable(forall n, P(n))"을 증명할 수 없는지, 구체적으로 설명해주면 고맙겠음
    • "PA가 'PA가 X를 증명한다'를 증명하면 PA가 X를 증명한다"는 명제는 맞지 않음 PA로 모든 가능 증명을 검색하는 함수를 만들 수 있고, 실제로 답변 마지막 부분에 이 방식을 스케치했음 이로부터 will-return, opposite-return 같은 함수도 만들 수 있고, 이는 할팅 문제 표준 증명과 일치함 opposite-return(opposite-return, opposite-return) 케이스를 생각해 보면, PA가 opposite-return이 리턴함을 증명하면 실제로 리턴하지 않는다는 것 역시 증명함, 반대로 리턴하지 않음을 증명하면 리턴함을 증명함 만약 PA가 "증명 가능한 것은 모두 실제로 증명가능하다"는 식의 더 강한 명제를 채택하면 이는 곧 Gödel의 2차 불완전성 정리로, PA가 모순임을 뜻하게 됨 따라서 단순히 "PA가 증명함"과 "PA가 자신이 증명함을 증명함"은 반드시 구분되어야 함
  • 순수 람다 계산법만으로도 충분함 람다 계산법 자체가 계산을 인코딩하기 때문임
  • 누군가와 귀납적 데이터 타입에 대해 얘기하다 zero/succ로 만든 Nat 정의(Lean이나 Rocq에서 볼 수 있음)를 보여줌 상대는 "이것만으로 충분한가?", "Peano 공리계가 필요한가? 귀납적 데이터 타입보다 더 원시적인 무언가가 있는가?" 등 궁금증을 가졌음 Peano 공리계가 본질적으로 당연하다 생각하지 말고, 하나의 설계일 뿐이라는 점을 자주 되짚어 보는 것이 좋다고 생각하게 됨
    • "귀납 데이터 타입보다 더 근본적인 게 있는가?"에 대한 답변으로, 자연수 자체가 귀납 데이터 타입보다 더 원시적이라고 생각함 모든 귀납 데이터 타입은 자연수와 그 외 소수의 원시적 타입 생성자(Π, Σ, =, Ω)만 있으면 만들 수 있음
  • Kirby-Paris 정리에 대한 Q&A 참고
  • PA 일관성 관련해서, PA 내에서 증명 가능하다는 영상 자료 공유 유튜브 링크
    • 비논리학자들에게 필수로 설명이 필요한 부분임 Gödel의 2차 불완전성 정리에 따르면 만약 PA가 자신의 일관성을 증명할 수 있다면 PA는 모순이 됨(거짓도 포함해 무엇이든 증명 가능해짐) 본 영상은 PA가 모순임을 증명하지 않고, PA가 보다 약한 의미에서 "자신의 일관성"을 증명할 수 있음을 보임 논리학의 기초를 알지 못한다면 정확히 이해하긴 어려운 내용이지만 충분히 흥미로움
  • 이 주제가 123 포인트를 얻고 있는데, 정작 SO에 올라온 본문은 11업로드밖에 없음
    • Stack Overflow는 15 포인트가 있어야 업보팅 가능함 평판 문제 때문에 사람들이 글을 올리고 싶어하지 않기도 하고, 15포인트 제한이 업보팅을 막는 것 같음
  • 컴퓨테이션 만으로 충분한가? 계산 가능한 실수는 실수 전체의 부분집합임
    • "실수"란 이름 자체가 오해를 불러일으키는 명칭이라고 생각함 실수는 실제 물리적 비율(비)를 의미한다고 해석할 수도 있음 예를 들어, 180.255파운드라고 하면, 존스의 실제 몸무게와 표준 파운드 사이의 실제 물리적 비율이라는 의미임 이러한 비율도 물리적으로 존재한다는 것 즉, 실수는 물리적 비로 해석될 수 있음 반면 지금은 숫자를 현실과 분리된 추상적 개념으로 보는 입장이 우세하고, 이는 대표적으로 플라톤주의적 견해임 하지만 현실에서는 무한정한 정밀도로 무엇을 측정하거나 표현하는 것은 불가능함 예컨대, 50자리 이상의 정밀도 측정은 양자역학적 제한으로 불가능함 만약 태양계 천체의 궤도를 오차 없이 측정하려면 50자리 이상으로 가면 인접 별의 질량효과, 100자리 이상은 은하 전체를 모델링해야 하며, 결국 실측 불가능한 물리적 영향까지 고려해야 함 그래서 현실에서는 유한한 정밀도의 수학만이 가능함 즉, 원리상 모든 것은 계산 가능하지만 무한대로 갈수록 수학적 모델 자체도 무의미해짐
    • 정말 그런가? 사실 비가산(uncountable)이 더 많다는 개념은 오해에서 출발함 내 설명 글 참고 비가산이 많다는 걸 받아들이면 "존재"에 관해 논쟁적 입장을 채택할 수밖에 없음 관련 토론 참고 마지막으로 우리가 끝까지 논리 전개를 해도, 컴퓨터로 모두 표현 가능함 ZFC에 큰 집합들을 더해도 PA로 출발해 임의의 결론까지 모두 추론 가능하기에 실질적으로 PA만으로 충분하다고 판단함 좀 더 설득이 필요하다면 Gödel, Escher, Bach 책을 추천함
    • 내 방식은 조금 다름 실수 일반은 계산, 기호화, 기록 등 어떤 형태로도 다룰 수 없지만, 실수에 대한 ‘명제’ 자체는 유용하게 표현하고 계산할 수 있는 경우가 많음 Harvey Friedman이나 이번 글의 저자처럼 단순한 체계에서 상상 이상의 복잡한 값을 만들어내는 시도가 정말 흥미로움 (참고: audiomulch 웹사이트는 접속 안 됨)
    • "충분하다"에 어떤 목표가 붙지 않는 한 이 질문은 정의가 모호함 무엇을 위해 충분한지가 중요함
    • "컴퓨테이션만으로 충분한가?"라는 질문 자체가 틀렸다고 생각함 당연히 충분하지 않음, 만약 충분하다면 현실을 믿기 쉬운 시계태엽처럼 여기는 쪽 일부의 생각이 모두 맞아버림 현실은 그보다 훨씬 흥미롭고 복잡함
답변달기