힐베르트의 프로그램

Hilbert's program

수학에서 힐베르트의 프로그램은 1920년대 초 독일 수학자 데이비드 힐베르트가 고안한 [1]수학의 기초 위기에 대한 제안된 해결책으로, 수학의 기초를 명확히 하려는 초기 시도가 역설과 불일치로 고통받는 것으로 밝혀졌습니다. 힐베르트는 그 해결책으로 현존하는 모든 이론을 유한하고 완전한 일련의 공리에 근거하고, 이 공리들이 일치한다는 증거를 제시할 것을 제안했습니다. 힐버트는 실제 분석과 같이 더 복잡한 시스템의 일관성이 더 단순한 시스템의 측면에서 증명될 수 있다고 제안했습니다. 궁극적으로 모든 수학의 일관성이 기초산술로 떨어질 수 있습니다.

1931년에 발표된 괴델의 불완전성 정리는 힐베르트의 프로그램이 수학의 핵심 영역에서 달성할 수 없다는 것을 보여주었습니다. 괴델은 첫 번째 정리에서 산술을 표현할 수 있는 계산 가능한 일련의 공리를 가진 일관된 시스템은 결코 완전할 수 없다는 것을 보여주었습니다: 사실로 보일 수 있는 문장을 구성할 수 있지만 시스템의 공식 규칙에서 파생될 수는 없습니다. 그의 두 번째 정리에서, 그는 그러한 체계가 그 자체의 일관성을 증명할 수 없다는 것을 보여주었고, 따라서 그것은 확실히 더 강한 것의 일관성을 확실하게 증명하는 데 사용될 수 없다는 것을 보여주었습니다. 이것은 유한 체계가 그 자신의 일관성을 증명하기 위해 사용될 수 있고, 따라서 다른 모든 것을 증명할 수 없다는 힐베르트의 가정을 반박했습니다.

힐베르트의 계획서

힐버트의 프로그램의 주요 목표는 모든 수학에 안전한 기초를 제공하는 것이었습니다. 여기에는 특히 다음이 포함되어야 합니다.

  • 모든 수학의 공식, 즉 모든 수학적 진술은 정확한 공식 언어로 작성되어야 하며, 잘 정의된 규칙에 따라 조작되어야 합니다.
  • 완전성: 모든 참된 수학적 진술이 형식주의에서 증명될 수 있다는 증거입니다.
  • 일관성: 수학의 형식주의에서 어떤 모순도 얻을 수 없다는 증거. 이 일관성 증명은 가급적 유한한 수학적 대상에 대한 " 유한한" 추론만을 사용해야 합니다.
  • 보존: "이상적인 물체"(예를 들어 셀 수 없는 집합)에 대한 추론을 사용하여 얻은 "실제 물체"에 대한 결과는 이상적인 물체를 사용하지 않고 증명할 수 있다는 증거입니다.
  • 결정 가능성: 어떤 수학적 진술의 진위를 결정하는 알고리즘이 있어야 합니다.

괴델의 불완전성 정리

주요 기사: 괴델의 불완전성 정리

Kurt Gödel은 힐베르트 프로그램의 대부분의 목표가 최소한 가장 명백한 방식으로 해석된다면 달성이 불가능하다는 것을 보여주었습니다. 괴델의 두 번째 불완전성 정리는 정수의 덧셈과 곱셈을 암호화할 만큼 강력한 일관된 이론은 그 자체의 일관성을 증명할 수 없다는 것을 보여줍니다. 이것은 힐버트의 프로그램에 대한 도전을 보여줍니다.

  • 공식 체계 내에서 모든 수학적 참 진술을 공식화하는 것은 불가능합니다. 왜냐하면 그러한 형식주의에 대한 시도는 일부 참 진술을 생략할 것이기 때문입니다. 재귀적으로 열거 가능한 일련의 공리에 기초한 페아노 산술의 완전하고 일관된 확장은 없습니다.
  • 페아노 산술과 같은 이론은 그 자체의 일관성을 증명할 수도 없기 때문에, 그것의 제한된 "결정론적" 부분 집합은 집합 이론과 같은 더 강력한 이론의 일관성을 확실히 증명할 수 없습니다.
  • 페아노 산술의 어떤 일관된 확장에서도 진술의 참(또는 증명 가능성)을 결정하는 알고리즘은 없습니다. 엄밀하게 말하면, 엔체이둥 문제에 대한 이 부정적인 해결책은 괴델의 정리 이후 몇 년 후에 나타났는데, 당시에는 알고리즘의 개념이 정확하게 정의되지 않았기 때문입니다.

괴델 이후 힐베르트의 프로그램

증명 이론과 역수학과 같은 수학 논리학의 많은 현재 연구 노선은 힐베르트의 원래 프로그램의 자연스러운 연속으로 볼 수 있습니다. 목표를 약간 변경하면 상당 부분을 구할 수 있으며(Zach 2005), 다음과 같은 수정을 통해 일부는 성공적으로 완료되었습니다.

  • 모든 수학을 공식화할 수는 없지만, 본질적으로 누구나 사용하는 모든 수학을 공식화할 수 있습니다. 특히 1차 논리학과 결합된 저멜로-프란켈 집합 이론은 현재 거의 모든 수학에 대해 만족스럽고 일반적으로 받아들여지는 형식주의를 제공합니다.
  • 적어도 페아노 산술(또는 더 일반적으로 계산 가능한 일련의 공리를 가진)을 표현할 수 있는 시스템에 대해 완전성을 증명할 수는 없지만, 다른 많은 흥미로운 시스템에 대해 완전성의 형태를 증명할 수 있습니다. 완전성이 증명된 사소한 이론의 한 예는 주어진 특성의 대수적으로 닫힌 장 이론입니다.
  • 강력한 이론의 최종 일관성 증명이 있는지에 대한 질문은 대답하기 어려우며, 주로 "최종 증명"에 대한 일반적으로 받아들여지는 정의가 없기 때문입니다. 증명 이론의 대부분의 수학자들은 유한 수학을 페아노 산술에 포함된 것으로 간주하는 것으로 보이며, 이 경우 합리적으로 강한 이론의 유한 증명을 제공할 수 없습니다. 반면 괴델 자신은 페아노 산술에서 형식화할 수 없는 유한한 방법을 사용하여 유한한 일관성 증명을 할 수 있는 가능성을 제시했으므로 어떤 유한한 방법이 허용될 수 있는지에 대해 좀 더 자유주의적인 견해를 가졌던 것으로 보입니다. 몇 년 후, Gentzen은 Peano 산술에 대해 일관성 있는 증거를 제시했습니다. 이 증거에서 명확하게 최종적이지 않은 유일한 부분은 서수 ε까지의 특정 트랜스피니트 유도였습니다. 만약 이 초미세 귀납법이 유한한 방법으로 받아들여진다면, 페아노 산술의 일관성에 대한 유한한 증거가 있다고 주장할 수 있습니다. 가이시 다케우티 등은 2차 산술의 더 강력한 부분집합들이 일관성 있는 증명을 내놓았는데, 이 증명들이 정확히 얼마나 유한적인지 또는 건설적인지에 대해 다시 한 번 논의할 수 있습니다. (이 방법들로 일관성이 입증된 이론들은 매우 강력하며, 대부분의 "보통" 수학을 포함합니다.)
  • 페아노 산술에는 진술의 진실을 결정하는 알고리즘이 없지만, 그런 알고리즘이 발견된 흥미롭고 사소한 이론들이 많이 있습니다. 예를 들어, Tarski는 분석기하학에서 어떤 진술의 참값을 결정할 수 있는 알고리즘을 발견했습니다(더 정확하게는, 그는 실제 닫힌 장 이론이 결정 가능하다는 것을 증명했습니다). 칸토어-데케킨드 공리를 고려할 때, 이 알고리즘은 유클리드 기하학에서 어떤 진술의 진리를 결정하는 알고리즘으로 간주될 수 있습니다. 이것은 유클리드 기하학을 사소한 이론으로 생각하는 사람이 거의 없기 때문에 실질적입니다.

참고 항목

참고문헌

  1. ^ Zach, Richard (2023), Zalta, Edward N.; Nodelman, Uri (eds.), "Hilbert's Program", The Stanford Encyclopedia of Philosophy (Spring 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 2023-07-05
  • G. Gentzen, 1936/1969. 다이 위더스프루크 프라이 데어 리넨 자렌테리오리. Mathematische Annalen 112:493–565. '산술의 일관성'으로 번역된, 게르하르트 젠젠의 논문, M. E. Szabo(ed.), 1969.
  • D. 힐버트. 'Die Grundlegung der element는 Zahlenlehere입니다.' Mathematische Annalen 104:485–94. W. Ewald에 의해 '초등수 이론의 기초'로 번역됨, 만코스에서 266-273쪽 (에드., 1998) 브루어에서 힐베르트까지: 1920년대 수학의 기초에 대한 논쟁, 옥스퍼드 대학 출판부. 뉴욕.
  • S.G. 심슨, 1988. 힐베르트 프로그램의 부분적 실현(pdf). 기호 논리학 저널 53:349–363.
  • R. Zach, 2006. 그때나 지금이나 힐버트의 프로그램. 논리철학 5:411–447, arXiv:math/0508572 [math.LO].

외부 링크