ТОЛЫМСЫЗДЫҚ ТЕОРЕМАСЫНА ЕКІ ҚОСЫМША

Аннотация: Де Йонгтың қозғалмайтын нүкте теоремасына жаңа дәлелдеу берілді. Консерватизм туралы бінеше нәтиже алынды.

Кілтті сөздер: Қозғалмайтын нүкте, модальді оператор, консервативті, салыстырмалы қайшылықсыздық

§1 Қозғалмайтын нүкте туралы теорема

Диагонализацияның көмегімен ,  ұсыныстарын оңай табуға болады

,

Екінші толымсыздық теорема мен Леб теоремасының дәлелдері қызықты жағдайды анықтайды, олар тек жалғыз ғана емес, сонымен бірге нақты анықталады:

,

,

мұндағы  – ақиқат. Леб теоремасының ескі дәлелі қозғалмайтын нүктені пайдаланады

кез келген берілген  формула үшін. Қарапайым алгебралық манипуляциялар мұны көп ұзамай көрсетеді

осыдан  формуласы қайтадан, бұл жолы қалған айнымалы бойынша анық анықталуы мүмкін. Бұл оқшауланған мысалдар емес, жалпы нәтиженің ерекше жағдайлары екендігі белгілі болды.

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

, ;

, .

Егер – пропозициялық тілдің формуласы болса және біз  сөйлемдерін  айнымалыларына сәйкес келтірсек, онда біз – сөйлемін түрінде жазамыз, яғни ауыстыру нәтижесі әр  орнына тиісті  және  бірге. □

1.1. (де Йонгтың қозғалмайтын нүкте туралы теоремасы¹).  болсын,  тек □ қолданылу аясында ғана кездеседі. Содан кейін кейбір  және барлық  ұсыныстары үшін,  теориясының тілі

.

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

Бұл бекітудің дәлелі мұнда қайта шығару үшін тым күрделі. Дегенмен, біз келесі нақты жағдайды дәлелдей аламыз.

1.2. Т е о р е м а.  болсын, мұндағы  формуласында  айнымалысы □ қолданылу аясында кездеспейді. Сонда  формуласының қозғалмайтын нүктелері формула бойынша параметрлік түрде анықталады

,

Д ә л е л д е у.  айнымалылары  ұсыныстарымен алмастырылатын нәтижені анықтауға қызығушылық танытқанымызбен, пропозициялық жазба ыңғайлы.  өрнегі сәйкесінше түсініледі.

Диагонализация туралы лемма болғандықтан, бізде  бар деп болжауға болады. Осыдан кейін  болады.

1.3. Л е м м а. Барлық , ,  үшін ,  бар.

Бұл  формула ұзындығы бойынша индукция арқылы шығару шарттарынан алынады. Біз дәлелдемені жоққа шығарамыз.

1.2 теореманы дәлелдеу үшін алдымен көрсетеміз

                                                                      (*)

 – қозғалмайтын нүкте болғандықтан, онда . Енді,  – □ қозғалыс аясында  енгізбегендіктен, бізде

,

                             (**)

Шығару шарттары береді

                        (***)

Лемманы (**), (***) қолданып, біз бірден аламыз

яғни

.

Формалды Леб теоремасы бойынша бізде

,

бұл бекітуді дәлелдеуді аяқтайды (*).

Дәлелдеуді аяқтау үшін (*) күшін ескереміз

Соңғы эквиваленттілік  таңдауына сәйкес дұрыс. □

1.4. М ы с а л. Біз (і) ; (іі) ; (ііі) ; (іv) ; (v)  және (vі) кестесінде (v) формуласын түпкілікті жеңілдету нәтижесін береміз:

(і)
(іі)
(ііі)
(іv)
(v)
(vі)

§2. Консервативті нәтижелер

Бұл бөлімде біз Крейзелге байланысты консерватизм туралы кейбір нәтижелерді ұсынамыз.

Естеріңізге сала кетейік, Гилберт консерватизмді құру бағдарламасы идеалды мәлімдемелер мен дерексіз тұжырымдарды қолдану жаңа нақты Теоремаларға әкелмейтіндігін дәлелдеуді талап етті. Толымсыздық теоремалар бұл жалпы жағдайда мүмкін емес екенін көрсеткенімен, олар ерекше жағдайларда жетістікке жету мүмкіндігін жоққа шығармайды. Шындығында, біз консерватизм туралы бір нәтижені анықтау үшін екінші толымсыздық теореманы қолданамыз.

Алдымен біз негізгі нәтижені сипаттаймыз.

2.1. К о н с е р в а т и з м  т у р а л ы  т е о р е м а.  болсын. Онда .

Д ә л е л д е у.  болсын және бұл  делік.  шарты  береді. Бірақ 4.1.4 теоремасы бойынша -ке қатысты  эквивалентті , осыдан . □

Төмендегі екі нәтиже 2.1-нің салдары болып табылады.

2.2. Т е о р е м а.  болсын. Онда .

Д ә л е л д е у.

 2.1 теоремасы бойынша

формальды екінші толымсыздық теоремасы (2.2.4) бойынша. Бірақ бізде бар

, , мұндағы . □

2.3. Т е о р е м а. ,  құрамында  болсын және болсын

                           (*)

кейбір қарапайым рекурсивті  терм үшін. сонда .

Д ә л е л д е у. Консерватизм теоремасы бойынша

контрапозиция көмегімен. Енді -ті  көмегімен контрапозицияны қайта жасайық. □

2.4. С а л д а р. (салыстырмалы қайшылықсыздық теоремасы). ,  құрамында  болсын және болсын

кейбір қарапайым рекурсивті  терм үшін. сонда .

Бұл нәтиже түсіндіруге лайық. Екінші толымсыздық теоремаға сәйкес, әлсіз теориялардың ішіндегі күшті теориялардың қайшылықсыздығын дәлелдей алмаймыз. Кейде күшті теорияның қайшылықсыздығы күмән тудырады және біз нәтижені салыстырмалы қайшылықсыз түрде дәлелдей аламыз, мысалы

                                           (**)

Гильберттің қайшылықсыздық орнату бағдарламасынан біз (**) бекітуді дәлелдеу мүмкін болатын әлсіз жүйеде жүзеге асырылуы туралы талапты мұра қалдырдық. Эпистемологиялық тұрғыдан, -да (**) бекітуді дәлелдеудің қажеті жоқ. Шынында да, (**) құндылықтар толығымен  жүйесін қабылдауға байланысты және біз соңғы (**) теорияда техникалық жағынан оңай екенін дәлелдей аламыз. Дегенмен, біз философиялық сұрыптаудан аулақ бола аламыз, өйткені 2.4-тің қорытындысы бойынша, егер ол орындалса, автоматты түрде (**) әлсіз теорияда, атап айтқанда -да дәлелдеуге болады. Осылайша, бұл туралы дауласатын ештеңе жоқ.

Алдыңғы абзацта біз қайшылықсыздық нәтижелерінің бірі ықтимал философиялық мәселені қалай жойғанын көрсеттік. Әдетте консерватизм нәтижелерінің мәні – бұл бізге дәлелдерді азайту және энергиямызды сақтау үшін күшті аппаратты пайдалануға мүмкіндік береді. Сандық ақпарат алу үшін оқырманды 3-тарауға жібереміз.

Пайдаланылған әдебиеттер:

1. Ерослов (Jeroslow R. G.)

1. Redundancies in the Hilbert – Bernays derivability conditions for Gödel’s second incompleteness theorem. – J. Symbolic Logic, 1973, 38, p. 359–367.

• Крайзель и Леви (Kreisel G., Levy A.)

1. Reflection principles and their use for establishing the complexity of axiomatic systems. – Z. math. Logik Grundl. Math., 1968, 14, S. 97–1421.

• Самбин (Sambin G.)

1. An effective fixed–point theorem in intuitionistic diagonalizable algebras.– Studia Logica, 1976, 35, p. 345–361.

Кушанова Гульдана

Ғылыми жетекші: Мулдагалиев Вали Садыкович, ф.-м.ғ.к,  доцентМ.Өтемісов атындағы Батыс Қазақстан университеті