Дәлелдер теориясы: Математикалық логика мен есептеу ғылымының саласы

Кіріспе

Математикалық логиканың саласы Дәлелдер теориясы – математикалық логиканың және теориялық информатиканың маңызды саласы болып табылады, онда дәлелдемелер формальды математикалық объектілер ретінде қарастырылады, бұл оларды математикалық әдістермен талдауға мүмкіндік береді. Дәлелдер әдетте берілген логикалық жүйенің аксиомалары мен логикалық қорытындылар ережелеріне сәйкес құрылған тізімдер, блоктардан тұратын тізімдер немесе ағаштар сияқты индуктивті түрде анықталған дерек құрылымдары түрінде ұсынылады. Осылайша, дәлелдер теориясы синтаксистік сипатқа ие, модельдер теориясынан өзгеше, ол семантикалық сипатта болады. Дәлелдер теориясының негізгі салаларына құрылымдық дәлелдер теориясы, ординалдық талдау, дәлелдеме логикасы, кері математика, дәлелдерді іздеу, теоремаларды автоматты түрде дәлелдеу және дәлелдің күрделігін зерттеу жатады. Көптеген зерттеулер информатика, тіл білімі және философия салаларындағы қолданылуына да бағытталған.

Тәртіптік талдау

Ординалдық талдау – арифметика, анализ және жиын теориясының ішкі жүйелері үшін комбинаторлық тұрақтылықты дәлелдеудің қуатты әдісі. Гёделдің екінші толық еместік теоремасы көбінесе жеткілікті күшті теориялар үшін формалды сәйкестікті дәлелдеудің мүмкін еместігін көрсету ретінде түсіндіріледі. Ординалдық талдау теориялардың тұрақтылығының шексіз мазмұнын нақты өлшеуге мүмкіндік береді. Тұрақты, рекурсивті аксиоматизацияланған теория T үшін, белгілі бір трансфинитті ординалдың негізділігі T теориясының тұрақтылығын білдіреді. Гёделдің екінші толық еместік теоремасы мұндай ординалдың негізділігі T теориясында дәлелденбейтінін көрсетеді.

Ординалдық талдаудың салдары: (1) конструктивті теорияларға қатысты классикалық екінші реттік арифметика мен жиын теориясының кіші жүйелерінің тұрақтылығы, (2) комбинаторлық тәуелсіздік нәтижелері және (3) дәлелденетін жалпы рекурсивті функциялардың және дәлелденетін жақсы негізді ординалдардың жіктелуі. Ординалдық талдауды Генцен бастады, ол трансфинитті индукцияны ε0 ординалына дейін қолданып, Пеано арифметикасының тұрақтылығын дәлелдеді. Ординалдық талдау бірінші және екінші реттік арифметика мен жиын теориясының көптеген фрагменттеріне қарай кеңейтілді. Басты қиындықтардың бірі – алдын ала болжау теорияларының ординалдық талдауы. Бұл бағыттағы алғашқы табыс – Такеутидің ординалдық диаграммалар әдісі арқылы Π CA0 теориясының тұрақтылығын дәлелдеуі болды.

Дәлелдендіру логикасы

Дәлелдеу логикасы – бұл модальдық логика, онда «бокс» операторы «дәлелдеуге болады» деп түсіндіріледі. Мақсаты – нақты бай формальды теориядағы дәлелдеу предикатының ұғымын қамту. Пьяно арифметикасында дәлелденетін нәрсені қамтитын GL (Гёдель-Лёб) дәлелдеу логикасының негізгі аксиомалары ретінде Хилберт-Бернейдің туынды шарттары мен Лёб теоремасының модальдық аналогтары алынады (егер A-ның дәлелденуі A-ны білдірсе, онда A дәлелденеді). Пеано арифметикасы және оған байланысты теориялардың толық еместігі туралы негізгі нәтижелердің кейбіреулері дәлелдеу логикасында аналогтарға ие. Мысалы, GL-де егер қайшылық дәлелденбесе, онда қайшылықтың дәлелденбеуінің дәлелденбеуі – теорема (Гёдельдің екінші толық еместік теоремасы). Тұрақты нүкте теоремасының модальдық аналогтары да бар. Роберт Соловэй GL модальдық логикасының Пьяно арифметикасына қатысты толық екенін дәлелдеді. Яғни, Пьяно арифметикасындағы дәлелдеудің теориялық жүйесі модульдік логика GL арқылы толық бейнеленеді. Бұл тікелей Пьяно арифметикасындағы дәлелдеуге қатысты логикалық ойлаудың толық және шешімді екенін білдіреді. Дәлелдеу логикасындағы басқа зерттеулер бірінші реттік дәлелдеу логикасына, полимодальді дәлелдеу логикасына (объект теориясындағы дәлелдеуді білдіретін бір модальділікпен және метатеориядағы дәлелдеуді білдіретін екінші модальділікпен) және дәлелдеу мен түсіндіру арасындағы өзара әрекеттестікті түсінуге арналған түсіндіру логикасына бағытталған. Кейбір соңғы зерттеулер математикалық теориялардың ординалдық талдауына дәрежеленген дәлелдеу алгебраларын қолдануды қамтиды.

Кері математика

Кері математика – математикалық логикада математикалық теоремаларды дәлелдеу үшін қандай аксиомалар қажет екенін анықтауға бағытталған бағдарлама. Бұл саланың негізін Харви Фридман қалады. Оның ерекше әдісін «теоремалардан аксиомаларға кері жүру» деп сипаттауға болады, бұл аксиомалардан теоремаларды тудырудың дәстүрлі математикалық тәсіліне қайшы келеді. Кері математика бағдарламасы жинақтар теориясындағы нәтижелермен, мысалы, таңдау аксиомасы мен Зорн леммасының ZF жинақтар теориясы бойынша эквивалентті екендігін көрсететін классикалық теоремамен алдын ала болжалды. Алайда, кері математиканың мақсаты жинақтар теориясының мүмкін болатын аксиомаларын емес, математиканың қарапайым теоремаларының мүмкін болатын аксиомаларын зерттеу болып табылады. Кері математикада негізгі тілмен және негізгі теориямен – яғни, теоремалардың көпшілігін дәлелдеуге жеткіліксіз, бірақ оларды тұжырымдауға қажетті анықтамаларды жасауға жететін негізгі аксиомалар жүйесімен басталады. Мысалы, «Кез келген шектелген нақты сандар тізбегінің жоғарғы шегі болады» теоремасын зерттеу үшін нақты сандар мен нақты сандар тізбектері туралы сөйлей алатын негізгі жүйе қолданылуы керек. Негізгі жүйеде тұжырымдалуға болатын, бірақ дәлелденбеген әрбір теорема үшін мақсат – сол теореманы дәлелдеу үшін қажетті нақты аксиомалық жүйені (негізгі жүйеден күштірек) анықтау болып табылады. Теорема T-ны дәлелдеу үшін жүйе S қажет екенін көрсету үшін екі дәлел қажет. Бірінші дәлел T-ның S-тен дәлелденетінін көрсетеді; бұл S жүйесінде оны жүзеге асыруға болатындығын дәлелдеумен бірге қарапайым математикалық дәлелдеу. Екінші дәлел, кері дәлелдеу деп аталады, T-ның өзі S-ті білдіретінін көрсетеді; бұл дәлел негізгі жүйеде жүзеге асырылады. Кері дәлелдеу негізгі жүйені кеңейтетін S′ аксиомалық жүйесі S-тен әлсіз бола алмайтынын, сонымен бірге T-ны дәлелдейтінін анықтайды. Кері математикадағы ең қызықты құбылыстардың бірі – Үлкен Бес аксиомалық жүйенің тұрақтылығы. Күшінің өсу ретімен бұл жүйелер RCA0, WKL0, ACA0, ATR0 және Π CA0 аббревиатураларымен аталады. Кері математикалық талдаудан өткен математиканың дерлік әрбір теоремасы осы бес жүйенің бірімен эквивалентті екені дәлелденді. Жақындағы зерттеулердің көп бөлігі осы шеңберге жақсы сәйкес келмейтін комбинаторлық принциптерге, мысалы, жұптар үшін Рамзи теоремасы (RT) сияқты, бағытталған. Кері математикадағы зерттеулер көбінесе рекурсия теориясының және дәлелдеу теориясының әдістерін қамтиды.

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. The field was founded by Harvey Friedman. Its defining method can be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the axiom of choice and Zorn's lemma are equivalent over ZF set theory. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory. In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems. For example, to study the theorem "Every bounded sequence of real numbers has a supremum" it is necessary to use a base system that can speak of real numbers and sequences of real numbers. For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system S is required to prove a theorem T, two proofs are required. The first proof shows T is provable from S; this is an ordinary mathematical proof along with a justification that it can be carried out in the system S. The second proof, known as a reversal, shows that T itself implies S; this proof is carried out in the base system. The reversal establishes that no axiom system S′ that extends the base system can be weaker than S while still proving T.

One striking phenomenon in reverse mathematics is the robustness of the Big Five axiom systems. In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and Π CA0. Nearly every theorem of ordinary mathematics that has been reverse mathematically analyzed has been proven equivalent to one of these five systems. Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT (Ramsey's theorem for pairs). Research in reverse mathematics often incorporates methods and techniques from recursion theory as well as proof theory.

Функционалдық түсіндірме

Функционалдық түсіндірмелер – конструктивті емес теорияларды функционалдық теорияларға түрлендіру. Функционалдық түсіндірулер әдетте екі кезеңнен тұрады. Біріншіден, классикалық теория C интуициялық теория I-ге "қайтадан жазылады". Яғни, C теориясының теоремаларын I теориясының теоремаларына аударатын конструктивті бейнелеу жасалады. Екіншіден, интуициялық теория I функционалдардың кванторсыз теориясы F-ке дейін азайтылады. Бұл түсіндірулер Хилберт бағдарламасының бір түріне үлес қосады, себебі олар классикалық теориялардың конструктивті теорияларға қатысты дұрыстығын дәлелдейді. Сәтті функционалдық түсіндірулер шексіз теорияларды шекті теорияларға, ал алдын ала болжаушы теорияларды болжаушы теорияларға азайтуға мүмкіндік берді. Функционалдық түсіндірулер сондай-ақ қысқартылған теориядағы дәлелдерден конструктивті ақпаратты алуға жол береді. Түсіндірудің тікелей салдары ретінде, әдетте, I немесе C-де толықтығы дәлелденген кез келген рекурсивті функция F терминімен көрсетіледі. Егер F-тің I-де қосымша түсіндірілуін ұсына алса, бұл кейде мүмкін, онда бұл сипаттама нақты болып шығады. Көбінесе F терминдері функциялардың табиғи класымен сәйкес келеді, мысалы, примитивті рекурсивті немесе полиномиалдық уақытта есептелетін функциялар. Функционалдық түсіндірулер теориялардың реттік талдауларын жүргізу және олардың дәлелденген рекурсивті функцияларын жіктеу үшін де қолданылған. Функционалдық түсіндірулерді зерттеу Курт Гёдельдің шекті типтегі функционалдардың кванторсыз теориясындағы интуициялық арифметиканы түсіндіруімен басталды. Бұл түсіндіру әдетте "Диалектика" түсіндіруі деп аталады. Классикалық логиканың интуициялық логикадағы екі жойғыш теріс түсіндіруімен бірге, ол классикалық арифметиканы интуициялық арифметикаға азайтуды қамтамасыз етеді.

Ресми және бейресми дәлелдеу

Күнделікті математикалық практикадағы бейресми дәлелдемелер, дәлелдеу теориясының ресми дәлелдемелерінен өзгеше. Олар, негізінен, сарапшыға жеткілікті уақыт пен шыдамдылық болғанда, ресми дәлелдемені қайта құруға мүмкіндік беретін жоғары деңгейдегі сызбаларға ұқсайды. Көптеген математиктер үшін толыққанды ресми дәлелдеме жазу тым ұзақ және егжей-тегжейлі болып келеді, сондықтан ол кеңінен қолданылмайды. Формалды дәлелдемелер интерактивті теореманы дәлелдеу кезінде компьютерлердің көмегімен құрастырылады. Ерекшелігі, мұндай дәлелдемелерді компьютер арқылы автоматты түрде тексеруге болады. Формалды дәлелдемелерді тексеру әдетте оңай, бірақ дәлелдемелерді табу (автоматтандырылған теореманы дәлелдеу) көбінесе қиынға соғады. Ал математикалық әдебиеттегі бейресми дәлелдемелерді тексеру үшін бірнеше апталық сарапшылардың қарауы қажет, және оларда қателіктер кездесуі мүмкін.

Дәлелдік-теориялық семантика

Тіл білімінде типтік логикалық грамматика, категориялық грамматика және Монтегю грамматикасы формальды табиғи тіл семантикасын беру үшін құрылымдық дәлелдеу теориясына негіделген формализмдерді қолданады.