Кіріспе
Барлық математиканы формализациялауға жасалған әрекет, аксиомалардың шекті жиынтығына негізделген. 1920-жылдардың басында неміс математигі Давид Гильберт ұсынған Гильберт бағдарламасы, математиканың негізін түсіндіруге жасалған алғашқы әрекеттер парадокстар мен үйлесімсіздіктерге тап болған кезде математиканың іргетастық дағдарысын шешуге бағытталған ұсыныс болды. Шешім ретінде Гильберт барлық қолданыстағы теорияларды шекті, толық аксиомалар жиынтығына негіздеуді және осы аксиомалардың дұрыс екенін дәлелдеуді ұсынды. Гильберт күрделі жүйелердің, мысалы, нақты талдаудың, дұрыстығын қарапайым жүйелер арқылы дәлелдеуге болатынын айтты. Соңында, барлық математиканың дұрыстығы негізгі арифметикаға дейін келтірілуі мүмкін еді. 1931 жылы жарияланған Гёдельдің толық емес теоремалары Гильберт бағдарламасының математиканың маңызды салалары үшін іске аспайтынын көрсетті. Бірінші теоремасында Гёдель арифметиканы білдіре алатын және есептелетін аксиомалар жиынтығына ие кез келген жүйе толық бола алмайтынын көрсетті: шындыққа сай екені көрсетілген, бірақ жүйенің формалды ережелерінен шығарылмаған бір мәлімдеме жасау мүмкін. Екінші теоремасында ол мұндай жүйе өзінің дұрыстығын дәлелдей алмайтынын көрсетті, сондықтан оны одан да күшті нәрсенің дұрыстығын дәлелдеу үшін пайдалануға болмайды. Бұл Гильберттің шекті жүйені өзінің дұрыстығын дәлелдеу үшін қолдануға болатындығы туралы болжамын жоққа шығарды, демек, оның көмегімен басқаның бәрін дәлелдеу мүмкін емес еді.
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early 1920s, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic. Gödel's incompleteness theorems, published in 1931, showed that Hilbert's program was unattainable for key areas of mathematics. In his first theorem, Gödel showed that any consistent system with a computable set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger with certainty. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of itself, and therefore could not prove everything else.
Гилберт бағдарламасының мазмұны
Гилберт бағдарламасының басты мақсаты – барлық математиканың берік негізін қалыптастыру болды. Атап айтқанда, оған мыналар кіруі керек: Барлық математиканың формалдануы; яғни, барлық математикалық тұжырымдар нақты, формалды тілде жазылып, анықталған ережелер бойынша қолданылуы тиіс. Толықтығы: барлық дұрыс математикалық тұжырымдар формализмде дәлелдене алатындығының дәлелі. Үйлесімділігі: математика формализмінде ешқандай қайшылыққа жол бермейтіндігінің дәлелі. Бұл үйлесімділікті дәлелдеу, барынша, тек қана шекті математикалық объектілер туралы "финитистік" ой-пікірді қолдануы керек. Сақталуы: "идеалдық объектілер" (мысалы, санауға келмейтін жиындар) туралы ойлар арқылы алынған "нақты объектілер" туралы кез келген нәтиже, идеалдық объектілерді пайдаланбастан дәлелдене алатындығының дәлелі. Шешімділігі: кез келген математикалық тұжырымның дұрыстығын немесе жалғандығын анықтау үшін алгоритм болуы керек.
A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules. Completeness: a proof that all true mathematical statements can be proved in the formalism. Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects. Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects. Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.
Гёдельдің толық емес теоремалары
Курт Гёдель Гилберт бағдарламасының көптеген мақсаттарына қол жеткізу мүмкін емес екенін, кемінде, ең түсінікті жолмен қарастырылса, көрсетті. Гёдельдің екінші толық еместік теоремасы, бүтін сандардың қосылуы мен көбейтілуін кодтауға жеткілікті күшті кез келген дәйекті теория өзінің дәйектілігін дәлелдей алмайтынын көрсетеді. Бұл Гилберт бағдарламасына үлкен қиындық туғызады:
Барлық математикалық шындықтарды формальды жүйеде ресмилеу мүмкін емес, себебі мұндай формализмға жасалған кез келген әрекет кейбір шындық математикалық мәлімдемелерді қамтымайды. Пеано арифметикасының рекурсивті түрде саналатын аксиомалар жинағына негізделген толық және дәйекті кеңейтілісі жоқ. Пеано арифметикасы сияқты теория тіпті өзінің дәйектілігін дәлелдей алмайды, сондықтан оның шектеулі "финитистік" ішкі жиыны жинақтар теориясы сияқты күшті теориялардың дәйектілігін дәлелдей алмайды. Пеано арифметикасының кез келген дәйекті кеңейтіліміндегі мәлімдемелердің шындығын (немесе дәлелделуін) анықтауға арналған алгоритм жоқ. Қатаң айтқанда, Entscheidungsproblem-ге бұл теріс жауап Гёдель теоремасынан кейін бірнеше жыл өткен соң пайда болды, өйткені сол кезде алгоритм ұғымы нақты анықталмаған еді.
Гёдельден кейінгі Гилберт бағдарламасы
Математикалық логикадағы қазіргі көптеген зерттеу бағыттары, мысалы, дәлелдеу теориясы және кері математика, Гилберттің бастапқы бағдарламасының табиғи жалғасы ретінде қарастырылуы мүмкін. Оның көп бөлігін мақсаттарын сәл өзгерту арқылы сақтап қалуға болады (Zach 2005), ал келесі түзетулермен оның кейбіреулері сәтті аяқталды: Барлық математиканы формалдау мүмкін болмаса да, кез келген адам қолданатын математиканың негізгі бөлігін формалдауға болады. Атап айтқанда, Зермело-Франкельдің жиын теориясы, бірінші реттік логикамен біріктірілгенде, қазіргі математиканың басым бөлігі үшін қанағаттанарлық және кеңінен қабылданған формализмді ұсынады. Пеано арифметикасын (немесе, жалпы алғанда, аксиомалардың есептелетін жиынтығын) білдіре алатын жүйелер үшін толықтықты дәлелдеу мүмкін болмаса да, көптеген басқа қызықты жүйелер үшін толықтықтың түрлерін дәлелдеуге болады. Толықтығы дәлелденген тривиальді емес теорияның мысалы – берілген сипаттағы алгебралық жабық өрістер теориясы. Күшті теориялардың шекті тұтастығын дәлелдеуге бола ма деген сұраққа жауап беру қиын, себебі «шекті дәлелдеу» үшін жалпыға қабылданған анықтама жоқ. Дәлелдеу теориясындағы көптеген математиктер шекті математиканы Пеано арифметикасының ішінде деп санайды, және осы жағдайда жеткілікті күшті теориялардың шекті дәлелдемелерін беру мүмкін емес. Екінші жағынан, Гёдельдің өзі Пеано арифметикасында формалдауға болмайтын шекті әдістерді қолдана отырып, шекті тұтастықты дәлелдеу мүмкіндігін ұсынды, сондықтан ол шекті әдістерге қатысты көбірек еркіндікпен қараған сияқты. Бірнеше жылдан кейін, Гентцен Пеано арифметикасының тұтастығын дәлелдеді. Бұл дәлелдеменің анық шекті емес жалғыз бөлігі – ε0 ординалына дейінгі белгілі бір трансфиниттік индукция болды. Егер бұл трансфиниттік индукция шекті әдіс ретінде қабылданса, онда Пеано арифметикасының тұтастығының шекті дәлелі бар деп айтуға болады. Гайси Такеути және басқалар екінші реттік арифметиканың күштірек жиынтықтарына тұтастық дәлелдемелерін берді, және осы дәлелдемелердің қаншалықты шекті немесе конструктивті екендігі туралы пікірталас жалғасуы мүмкін. (Бұл әдістермен тұтастығы дәлелденген теориялар өте күшті және «қалыпты» математиканың көп бөлігін қамтиды.) Пеано арифметикасындағы мәлімдемелердің шындығын анықтауға арналған алгоритм болмаса да, мұндай алгоритмдер табылган көптеген қызықты және тривиальді емес теориялар бар. Мысалы, Тарски аналитикалық геометриядағы кез келген мәлімдеменің шындығын анықтай алатын алгоритмді тапты (дәлірек айтқанда, ол нақты жабық өрістер теориясының шешілетінін дәлелдеді). Кантор-Дедекинд аксиомасын ескере отырып, бұл алгоритмді Евклид геометриясындағы кез келген мәлімдеменің шындығын анықтауға арналған алгоритм ретінде қарастыруға болады. Бұл маңызды, өйткені Евклид геометриясын тривиальді теория деп санайтындар аз.
Although it is not possible to formalize all mathematics, it is possible to formalize essentially all the mathematics that anyone uses. In particular Zermelo–Fraenkel set theory, combined with first order logic, gives a satisfactory and generally accepted formalism for almost all current mathematics. Although it is not possible to prove completeness for systems that can express at least the Peano arithmetic (or, more generally, that have a computable set of axioms), it is possible to prove forms of completeness for many other interesting systems. An example of a non trivial theory for which completeness has been proved is the theory of algebraically closed fields of given characteristic. The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand, Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, Gentzen gave a consistency proof for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite induction up to the ordinal ε0. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of second order arithmetic have been given consistency proofs by Gaisi Takeuti and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.) Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non trivial theories for which such algorithms have been found. For example, Tarski found an algorithm that can decide the truth of any statement in analytic geometry (more precisely, he proved that the theory of real closed fields is decidable). Given the Cantor–Dedekind axiom, this algorithm can be regarded as an algorithm to decide the truth of any statement in Euclidean geometry. This is substantial as few people would consider Euclidean geometry a trivial theory.