연구 프로그램으로서의 힐버트 계획
Hilbert’s Program as Research Program
0
조회
0
다운로드
1
인용
0
참고문헌
키워드
초록
수리 논리학의 발전은 상당 부분 힐버트 (D. Hilbert, 1862〜1943)의 증명이론(Beweistheorie)에 뿌리를 두고 있다. 흔히 ‘힐버트 계획’ (Hilbert’s program) 으로 불리는 이 계획의 목표는 형식적 공리론적 방법에 의해 수학의 모든 명제와 증명을 형식화하고 이 형식 체계의 완비성과 무모순성 증명을 통해 고전 수학을 ‘구원’ 하고, 수학의 토대를 공고히 하자는 데에 있다. 1931년 괴델의 제 1정리에 의해 결정불가능 명제의 존재가 드러나면서 완전성이 위기를 맞고, 제 2정리에 의해 무모순성의 확립이 무산될 위기에 처한다. 그러나 ‘상대적’ 내지 ‘부분적’ 힐버트 계획은 효과적인 연구 프로그램으로서 살아 있다고 말하는 학자들이 적지 않다. 우리는 특히 힐버트 계획 이 오늘날 구성주의 수학 의 발전에 동력을 제공하고 있다는 점을 커리-하워드 대응 (Curry-Howard Correspondence) 을 통하여 부각시키고자 했다. 자연연역에서 증명 (proof) 이 바로 컴퓨터 프로그램 (computer program) 에 다름 아니라는 사실에 의해 수학의 형식화 (formalization)는 새로운 조명을 받게 된 것이다. 요컨대 힐버트 계획은 컴퓨터 과학에서 알고 리듬 (algorithm) 이라는 핵심개념에 가장 잘 부합되는 것이다.
Abstract
The development of recent Mathematical Logic is mostly originated in Hilbert’s Proof Theory. The purpose of the plan so called Hilbert’s Program lies in the formalization of mathematics by formal axiomatic method, rescuing classical mathematics by means of verifying completeness and consistency of the formal system and solidifying the foundations of mathematics. In 1931, the completeness encounters crisis by the existence of undecidable proposition through the 1st Theorem of G?del, and the establishment of consistency faces a risk of invalidation by the 2nd Theorem. However, relative of partial realization of Hilbert’s Program still exists as a fruitful research program. We have tried to bring into relief through Curry-Howard Correspondence the fact that Hilbert’s program serves as source of power for the growth of mathematical constructivism today. That proof in natural deduction is in truth equivalent to computer program has allowed the formalization of mathematics to be seen in new light. In other words, Hilbert’s program conforms best to the concept of algorithm, the central idea in computer science.
참고문헌 (25)
- Benacerraf P., "Philosophy of Mathematics" (1983), Cambridge University press
- Bernays P., "On Hilbert’s Thoughts Concerning the Grounding of Arithmetics", pp.223~226 (1923), Mancosu
- Bernays P., "Hilbert, David, Encyclopedia of philosophy" (1967), Macmillan Publishing Co
- Bernays P., "The Philosophy of Mathematics and Hilbert’s Proof Theory", pp.234~265 (1930), Mancosu
- Cassou-Noguès Pierre, "Hilbert" (2001), Les Belles Lettres
- Detlefsen M., "Hilbert’s Program" (1986), Dordrecht
- Ewald W. B., "From Kant to Hilbert. A Source book in the foundations of Mathematics" (1996), Oxford University press
- Feferman S., "Hilbert’s Program relativized: Proof-Theoretical and foundational reductions", Journal of Symbolic Logic, 53(2), pp.284~304 (1988)
- Gray J.J., "Le Défi de Hilbert" (2004), Dunod
- Herbrand J., "English translation: ’On the consistency of arithmetic’, IN From Frege to Gödel. A source Book in Mathematical Logic, 1879-1931", pp.620~628 (1967), Harvard University Press
- Hilbert D., "The New Grounding of Mathematics", pp.198~214 (1922), Mancosu
- Hilbert D., "On the infinite", pp.367~392 (1926), Van Heijenoort
- Hilbert D., "The foundation of mathematics", pp.464~479 (1927), Van Heijenoort
- Kreisel G., "Hilbert’s Program, 1983, in philosophy of mathematices", pp.207~238 (1983), Benacerraf and Putnam
- Mancosu P., "From Brouwer to Hilbert. The Debate of the Foundations of Mathematics in the 1920s" (1998), Oxford University press
- Mancosu P., "Hilbert and Berneys on metamathemetics", pp.149~188, Mancosu
- Murawsk: R., "On proofs of the consistency of arithmetic, Studies in logic", grammar and rhetoric, 5(18), pp.41~50 (2002)
- Sieg W., "Hilbert’s Program: 1887-1922", Bulletin of symbolic Logic, 5(1), pp.1~44 (1999)
- Simpson S. G., "Partial realizations of Hilbert’s Program", Journal of Symbolic Logic, 53(2), pp.349~363 (1988)
- Slater B. H., "Epsilon Calculi", Logic Journal of IGPL, 14(4), pp.535~590 (2006)
- Tait W. W., "Finitism", Journal of Philosophy, 78, pp.524~546 (1981)
- Van Heijenoort J., "From Frege to Gödel. A source Book in mathematical Logic, 1897– 1931" (1967), Harvard University press
- Zach R., "Hilbert’s Program" (2003), The Stanford Encyclopedia of Philosophy
- Zach R., "The practice of finitism. Epsilon calculus and consistency proofs in Hilbert’s Program", Synthese, 137, pp.211~259 (2003)