Гёдельдің толықтық теоремасының заманауи тұжырымдамасы

Гёдельдің толықтық теоремасының дәлелі: қазіргі логика тілінде түсіндірілген, 1929 жылғы диссертация негізіндегі мақала. Бірінші реттік логика, функциялар, қатынастар.

9 мин оқу

100%

Дереккөз: Original proof of Gödel's completeness theorem — Wikipedia

Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.

Мазмұны

Кіріспе

Гёдельдің толықтық теоремасының дәлелі Курт Гёдельдің 1929 жылғы докторлық диссертациясында келтірілген (және дәлелдің қысқартылған нұсқасы 1930 жылы "Логикалық функционалдық есептеудің аксиомаларының толықтығы" (неміс тілінде) деген мақала ретінде жарияланған), қазіргі таңда оқуы қиын; ол қазір қолданылмайтын түсініктер мен формализмдерді, сондай-ақ көбінесе түсініксіз терминологияны пайдаланады. Төмендегі нұсқа дәлелдегі барлық қадамдар мен маңызды идеяларды нақты бейнелеуге, сонымен бірге дәлелді математикалық логиканың заманауи тілімен қайта баяндауға тырысады. Бұл жоба теореманың қатаң дәлелі ретінде қарастырылмауы керек.

Қорытындылар

Біз бірінші реттік предикат есептеуімен жұмыс істейміз. Біздің тілдеріміз тұрақты, функция және қатынас символдарына мүмкіндік береді. Құрылымдар (бос емес) домендерден және тиісті символдардың осы домендегі тұрақты мүшелер, функциялар немесе қатынастар ретінде интерпретацияларынан тұрады. Біз классикалық логиканы қабылдаймыз (мысалы, интуиционистік логикадан өзгеше). Біз предикат есептеуінің кейбір аксиоматизациясын (яғни, синтаксис негізінде, машинамен басқарылатын дәлелдеу жүйесі) белгілейміз: логикалық аксиомалар мен шешінді шығару ережелері. Бірнеше жақсы белгілі эквивалентті аксиоматизациялардың кез келгені жарайды. Гёдельдің бастапқы дәлелі Хилберт-Аккерманның дәлелдеу жүйесін қолданды. Біз формализміміз туралы барлық негізгі белгілі нәтижелерді, мысалы, нормальды форма теоремасын немесе дұрыстық теоремасын дәлелсіз қабылдаймыз. Біз теңдіксіз (кейде жаңсақ деп те аталатын) предикат есептеуін аксиоматизациялаймыз, яғни (объект) теңдіктің қасиеттерін білдіретін ерекше аксиомалар жоқ. Теореманың негізгі түрі дәлелденгеннен кейін, оны теңдігі бар предикат есептеуіне кеңейту оңай болады.

Теореманың тұжырымдамасы және оның дәлелі

Келесіде теореманың екі эквивалентті түрін келтіріп, олардың эквиваленттігін көрсетеміз. Кейін теореманы дәлелдейміз. Бұл келесі қадамдармен жасалады:

Теореманы сөйлемдерге (еркін айнымалысы жоқ формулаларға) prenex түрінде, яғни барлық кванторлары (∀ және ∃) басында болатын сөйлемдерге келтіру. Сонымен қатар, біз оны бірінші кванторы ∀ болатын формулаларға дейін қысқартамыз. Бұл мүмкін, өйткені әр сөйлем үшін бірінші кванторы ∀ болатын эквивалентті prenex түріндегі сөйлем бар. Теореманы ∀x₁ ∀x₂ … ∀xₖ ∃y₁ ∃y₂ … ∃yₘ φ(x₁ … xₖ, y₁ … yₘ) түріндегі сөйлемдерге дейін келтіру. Кванторларды жай ғана қайта орналастыру арқылы мұны істей алмасақ та, теореманы осы түрдегі сөйлемдер үшін дәлелдеу жеткілікті екенін көрсетеміз. Соңында теореманы осы түрдегі сөйлемдер үшін дәлелдейміз. Бұл, мысалы, сөйлемнің жоққа шығарылатынын (оның жоқтығы әрқашан рас) немесе қанағаттандырылатынын атап өту арқылы жасалады, яғни оны қанағаттандыратын модель бар (ол тіпті әрқашан рас болуы мүмкін, яғни тавтология); бұл модель жай ғана B құрамына кіретін субпропозицияларға шындық мәнін тағайындау арқылы құрылады. Мұның себебі – экзистенциалдық кванторлар ешқандай рөл атқармайтын, сөйлемдік логиканың толықтығы. Біз осы нәтижені B-ден құрылған, күрделі және ұзын сөйлемдерге Dn (n = 1, 2, ...) дейін кеңейтеміз, сондықтан олардың кез келгені жоққа шығарылатын болса, φ да жоққа шығарылады, немесе олардың барлығы жоққа шығарылмайтын болса, әрқайсысы қандай да бір модельде рас болады. Соңында, φ-ны қанағаттандыратын модельді құру үшін Dn-ды қанағаттандыратын модельдерді қолданамыз (барлығы жоққа шығарылмайтын жағдайда).

1-теорема. Әрбір дұрыс формула (барлық құрылымдарда дұрыс) дәлелденуге болады.

Бұл толық теореманың ең қарапайым түрі. Біз оны біздің мақсаттарымызға сәйкес, көбірек қолайлы нысанда қайтадан тұжырымдаймыз: "Барлық құрылымдар" дегенде, аталған құрылымдардың классикалық (Тарскилік) I интерпретациялары екенін нақтылау маңызды, мұнда I = <U, F> (U – бос емес (мүмкін шексіз) объектілер жиыны, ал F – интерпретацияланған символизмнің өрнектерінен U-ға функциялар жиыны). [Керісінше, "еркін логика" деп аталатындар U үшін бос жиындарға рұқсат береді. Еркін логика туралы толық ақпарат алу үшін Карел Ламберттің еңбектерін қараңыз.]

Теорема 2. φ формуласының әрқайсысы қандай да бір құрылымда жоққа шығарылуы немесе қанағаттандырылуы мүмкін.

"φ жоққа шығарылатын" дегеніміз, анықтама бойынша "¬φ дәлелденетін" дегенді білдіреді.

Екі теореманың теңдігі

Егер 1-теорема орындалса, ал φ ешбір құрылымда қанағаттандырылмаса, онда ¬φ барлық құрылымдарда жарамды және демек, дәлелденеді, осылайша φ жоққа шығарылады және 2-теорема орындалады. Егер керісінше, 2-теорема орындалса және φ барлық құрылымдарда жарамды болса, онда ¬φ ешбір құрылымда қанағаттандырылмауға тиіс және демек, жоққа шығарылады; содан кейін ¬¬φ дәлелденеді, ал содан кейін φ да дәлелденеді, осылайша 1-теорема орындалады.

2-теореманың дәлелі: бірінші қадам

2-теореманың дәлелін φ формулаларының барлық класын біртіндеп шектеу арқылы іздейміз, осыған "φ жоққа шығарылатын немесе қанағаттандырылатын" екенін дәлелдеу қажет. Бастапқыда, біз бұл тұжырымды φ формуласының барлық мүмкін нұсқалары үшін дәлелдеуіміз керек. Дегенмен, әрбір φ формуласы үшін, C формулаларының шектеулі класынан алынған ψ формуласы бар деп есептейік, мұнда "ψ жоққа шығарылатын немесе қанағаттандырылатын" → "φ жоққа шығарылатын немесе қанағаттандырылатын" болады. Осы талапты (алдыңғы сөйлемде айтылған) дәлелдегеннен кейін, тек C класына жататын φ үшін ғана "φ жоққа шығарылатын немесе қанағаттандырылатын" екенін дәлелдеу жеткілікті болады. Егер φ, ψ-ге дәлелді түрде эквивалент болса (яғни (φ ≡ ψ) дәлелденсе), онда "ψ жоққа шығарылатын немесе қанағаттандырылатын" → "φ жоққа шығарылатын немесе қанағаттандырылатын" екендігі рас (мұны көрсету үшін дұрыстық теоремасы қажет). Функциялар немесе тұрақты символдарды қолданбайтын кез келген формуланы қосымша кванторларды енгізу есебінен қайта жазудың стандартты әдістері бар; сондықтан барлық формулалар мұндай символдардан бос деп есептейміз. Гёдельдің еңбегінде функциялары немесе тұрақты символдары жоқ бірінші реттік предикаттық логиканың нұсқасы қолданылады. Келесіде біз жалпы формула φ (онда енді функциялар немесе тұрақты символдар қолданылмайды) қарастырамыз және пенекс формасы теоремасын қолданып, φ ≡ ψ болатындай, ψ формуласын қалыпты түрінде табамыз (ψ қалыпты түрінде болуы, ψ-дегі барлық кванторлар, егер бар болса, ψ-нің басында орналасқандығын білдіреді). Осыдан кейін, 2-теореманы тек қалыпты түріндегі φ формулалары үшін ғана дәлелдеу жеткілікті. Содан кейін, φ-ден барлық еркін айнымалыларды экзистенциалды кванторлармен квантификациялап алып тастаймыз: егер, мысалы, x1, ..., xn φ-де еркін болса, онда: Егер ψ M құрылымында қанағаттандырылса, онда φ да сөзсіз қанағаттандырылады, ал егер ψ жоққа шығарылса, онда ¬ψ дәлелденеді, содан кейін ¬φ да дәлелденеді, демек φ жоққа шығарылады. φ-ні сөйлемге дейін шектеуге болатынын көреміз, яғни еркін айнымалысы жоқ формулаға. Соңында, техникалық ыңғайлылық үшін, φ префиксінің (яғни φ-нің басындағы кванторлар тізбегі, ол қалыпты түрінде) әмбебап квантормен басталып, экзистенциалды квантормен аяқталуын қалаймыз. Бұған жету үшін, жалпы φ үшін (бұрын дәлелдеген шектеулерге байланысты), біз φ-де қолданылмаған бір орынды қатынас символын F және екі жаңа айнымалыны y және z аламыз. Егер φ = (P)Φ болса, онда (P) φ префиксін, ал Φ – матрицаны (φ-нің қалған, кванторсыз бөлігін) білдіреді, онда біз құрастырамыз. Егер ¬(∃y∃z F(y,z) ∧ Φ) дәлелденсе, онда ¬Φ да дәлелденеді, демек Φ жоққа шығарылады.

We approach the proof of Theorem 2 by successively restricting the class of all formulas φ for which we need to prove "φ is either refutable or satisfiable". At the beginning we need to prove this for all possible formulas φ in our language. However, suppose that for every formula φ there is some formula ψ taken from a more restricted class of formulas C, such that "ψ is either refutable or satisfiable" → "φ is either refutable or satisfiable". Then, once this claim (expressed in the previous sentence) is proved, it will suffice to prove "φ is either refutable or satisfiable" only for φ's belonging to the class C. If φ is provably equivalent to ψ (i. e., (φ ≡ ψ) is provable), then it is indeed the case that "ψ is either refutable or satisfiable" → "φ is either refutable or satisfiable" (the soundness theorem is needed to show this). There are standard techniques for rewriting an arbitrary formula into one that does not use function or constant symbols, at the cost of introducing additional quantifiers; we will therefore assume that all formulas are free of such symbols. Gödel's paper uses a version of first order predicate calculus that has no function or constant symbols to begin with. Next we consider a generic formula φ (which no longer uses function or constant symbols) and apply the prenex form theorem to find a formula ψ in normal form such that φ ≡ ψ (ψ being in normal form means that all the quantifiers in ψ, if there are any, are found at the very beginning of ψ). It follows now that we need only prove Theorem 2 for formulas φ in normal form. Next, we eliminate all free variables from φ by quantifying them existentially: if, say, x1 xn are free in φ, we form If ψ is satisfiable in a structure M, then certainly so is φ and if ψ is refutable, then is provable, and then so is ¬φ, thus φ is refutable. We see that we can restrict φ to be a sentence, that is, a formula with no free variables. Finally, we would like, for reasons of technical convenience, that the prefix of φ (that is, the string of quantifiers at the beginning of φ, which is in normal form) begin with a universal quantifier and end with an existential quantifier. To achieve this for a generic φ (subject to restrictions we have already proved), we take some one place relation symbol F unused in φ, and two new variables y and z If φ = (P)Φ, where (P) stands for the prefix of φ and Φ for the matrix (the remaining, quantifier free part of φ) we form Since is clearly provable, it is easy to see that is provable.

1-дәрежелі формулалар үшін теореманы дәлелдеу

Жоғарыда келтірілген леммада көрсетілгендей, бізге φ формуласы үшін теоремамызды дәлелдеу ғана қажет, φ R дәрежесінде 1 болғанда. φ 0 дәрежесінде бола алмайды, өйткені R формулаларында бос айнымалылар жоқ және тұрақты символдар қолданылмайды. Сонымен, φ формуласының жалпы түрі:

Енді біз k натурал саннан тұратын топтамалардың ретін былай анықтаймыз: егер, немесе, және лексикографиялық тәртіппен алдыңғы орында тұрса, сақталуы керек. [Бұл жерде топтама мүшелерінің қосындысы көрсетіледі.] N-ші топтаманы осы ретпен белгілеңіз. Формуланы былай қойыңыз: . Содан кейін лемманы былай қойыңыз: Әр n үшін .

Дәлелдеу: n бойынша индукция қолданамыз; бізде бар, мұнда соңғы импликация айнымалыны алмастыру арқылы алынады, өйткені топтамалардың реті осындай. Бірақ соңғы формула φ-ге тең. Базалық жағдайда, φ-нің де нәтижесі болады. Сонымен, лемма дәлелденді. Егер n үшін қайта қарулану мүмкін болса, онда φ да қайта қаруланады. Екінші жағынан, егер бұл кез келген n үшін болмаса, онда әр n үшін әртүрлі субпропозицияларға (олардың бірінші пайда болуы бойынша реттелген; "әртүрлі" мұнда бөлек предикаттарды немесе бөлек шектелген айнымалыларды білдіреді) шындық мәндерін тағайындаудың бір жолы бар, сонда әрбір ұйғарым осылай бағаланғанда шын болады. Бұл негізгі сөйлемдік логиканың толықтығынан туындайды. Енді біз шындық мәндерін тағайындаудың осындай жолы бар екенін көрсетеміз, сонда барлығы да шын болады: олар әрқайсысында бірдей тәртіппен пайда болады; біз оларға жалпы тағайындауды индуктивті түрде "көпшілік дауыс беру" арқылы анықтаймыз: шексіз көп тағайындамалар болғандықтан (әрқайсысы үшін бір) әсер ететін , немесе шексіз көп оны шын етеді, немесе шексіз көп оны жалған етеді және тек шекті саны оны шын етеді. Бірінші жағдайда, біз оны жалпыға бірдей дұрыс деп таңдаймыз; екіншісінде, біз оны жалпы жалған деп қабылдаймыз. Содан кейін n-нің шексіз көп санынан жалпы тағайындамадағыдай шындық мәні тағайындалады, біз жалпы тағайындаманы сол тәсілмен таңдаймыз. Бұл жалпы тағайындаманың барлығын және шындыққа алып келуі керек, өйткені егер жалпы тағайындаманың бірі жалған болса, онда әр n > k үшін де жалған болады. Бірақ бұл , жалпы тағайындамалардың шекті жиынтығы үшін шексіз көп n бар екендігіне қайшы келеді. Осы жалпы тағайындамадан, яғни барлық шындықты жасайтын, біз φ шындықты жасайтын тілдің предикаттарының түсіндірмесін құрастырамыз. Модельдің ғаламы табиғи сандар болады. Әрбір i-арлық предикат натуралдарға дәл сол кезде дұрыс болуы керек, егер ұйғарым жалпы тағайындамада дұрыс болса немесе ол оны тағайындамаса (себебі ол ешқашан пайда болмайды). Бұл модельде формулалардың әрқайсысы құрылымы бойынша дұрыс. Бірақ бұл φ-нің өзі модельде шындық екенін білдіреді, өйткені табиғи сандардың барлық мүмкін k топтамалары бойынша ауқым жабады. Сонымен, φ қанағаттандырылатындықтан, есеп аяқталды.

Lemma: For every n,
Proof: By induction on n; we have , where the latter implication holds by variable substitution, since the ordering of the tuples is such that But the last formula is equivalent to φ. For the base case, is obviously a corollary of φ as well. So the Lemma is proven. Now if is refutable for some n, it follows that φ is refutable. On the other hand, suppose that is not refutable for any n. Then for each n there is some way of assigning truth values to the distinct subpropositions (ordered by their first appearance in ; "distinct" here means either distinct predicates, or distinct bound variables) in , such that will be true when each proposition is evaluated in this fashion. This follows from the completeness of the underlying propositional logic. We will now show that there is such an assignment of truth values to , so that all will be true: The appear in the same order in every ; we will inductively define a general assignment to them by a sort of "majority vote": Since there are infinitely many assignments (one for each ) affecting , either infinitely many make true, or infinitely many make it false and only finitely many make it true. In the former case, we choose to be true in general; in the latter we take it to be false in general. Then from the infinitely many n for which through are assigned the same truth value as in the general assignment, we pick a general assignment to in the same fashion. This general assignment must lead to every one of the and being true, since if one of the were false under the general assignment, would also be false for every n > k. But this contradicts the fact that for the finite collection of general assignments appearing in , there are infinitely many n where the assignment making true matches the general assignment. From this general assignment, which makes all of the true, we construct an interpretation of the language's predicates that makes φ true. The universe of the model will be the natural numbers. Each i ary predicate should be true of the naturals precisely when the proposition is either true in the general assignment, or not assigned by it (because it never appears in any of the ). In this model, each of the formulas is true by construction. But this implies that φ itself is true in the model, since the range over all possible k tuples of natural numbers. So φ is satisfiable, and we are done.

Түсініктемесі

Біз әр Bi-ді Φ(x1 xk, y1 ym) түрінде жаза аламыз, мұнда xs-ті "алғашқы аргументтер", ал ys-ті "соңғы аргументтер" деп атаймыз. Мысалы, B1-ді қарастырайық. Оның "соңғы аргументтері" z2, z3, ..., zm+1 болып табылады, және осы айнымалылардың кез келген мүмкін комбинациясы үшін, біз үшін кейбір j бар, сонда олар Bj-де "алғашқы аргументтер" ретінде кездеседі. Осылайша, n1 жеткілікті үлкен болса, Dn1 мына қасиетке ие: B1-дің "соңғы аргументтері" олардың кез келген k комбинациясында Dn ішіндегі басқа Bjs-де "алғашқы аргументтер" ретінде кездеседі. Әрбір Bi үшін осыған сәйкес қасиеттері бар Dni бар. Сондықтан, барлық Dns-ді қанағаттандыратын модельде z1, z2, ..., zm сәйкес келетін объектілер бар, және олардың кез келген k комбинациясы кейбір Bj-де "алғашқы аргументтер" ретінде кездеседі, яғни осы объектілердің кез келген k саны zp1, ..., zpk үшін zq1, ..., zqm бар, бұл Φ(zp1, ..., zpk, zq1, ..., zqm) қанағаттандырылатынын білдіреді. Осы z1, z2, ..., zm объектілерінен ғана тұратын қосалқы модельді алып, φ-ны қанағаттандыратын модель аламыз.

Теңдікпен бірінші реттік предикат калькуліне кеңейту

Гёдель теңдік предикатының мысалдары бар формуласын кеңейтілген тілде одан жоқ формулаға дейін қысқартты. Оның әдісі теңдіктің кейбір мысалдарын қамтитын φ формуласын,

формуласымен алмастыруды қамтиды. Мұнда φ формуласында кездесетін предикаттар (сәйкес арлықтарымен) көрсетілген, ал φ' – бұл φ формуласы, онда теңдіктің барлық кездесулері жаңа Eq предикатымен алмастырылған. Егер осы жаңа формула жоққа шығарылса, бастапқы φ да жоққа шығарылған болар еді; қанағаттандырылатындық үшін де осы айтуға болады, себебі біз жаңа формуланың қанағаттандырылатын моделін Eq өкілдігіндегі эквиваленттілік қатынасы бойынша бөле аламыз. Бұл бөлу басқа предикаттарға қатысты дұрыс анықталған, сондықтан бастапқы φ формуласын қанағаттандырады.

Формулалардың саналатын жиынтықтарына кеңейту

Гёдель сонымен қатар формулалардың санауға болатын шексіз жиынтығы бар жағдайды да қарастырды. Жоғарыда айтылғандай, ол әрбір формула 1-дәрежелі болып, теңдік белгісін қамтымайтын жағдайларды ғана қарастыра алды. 1-дәрежелі формулалардың санауға болатын жиынтығы үшін, жоғарыда көрсетілгендей анықтай аламыз; содан кейін, осының жабылуын анықтаймыз. Дәлелдің қалған бөлігі де бұрынғысынша жүзеге асырылды.

Формулалардың кездейсоқ жиынтықтарына кеңейту

Формулалардың санаусыз шексіз жиынтығы болғанда, таңдау аксиомасы (немесе оның кем дегенде әлсіз түрі) қажет болады. Толық таңдау аксиомасын (АС) пайдаланып, формулаларды жақсы реттеуге болады және санаулы жағдайды дәлелдеу үшін қолданылған аргументті трансфинитті индукция арқылы санаусыз жағдайға да қолдануға болады. Басқа тәсілдерді де қолдануға болады, олар бұл жағдайда толықтық теоремасының, АС-тың әлсіз түрі болып табылатын Бульдік жайқы идеал теоремасымен эквивалентті екенін дәлелдейді.