WikiDer > Консервативті кеңейту

Conservative extension

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

Ресми түрде айтылған теория ${ displaystyle T_ {2}}$ Бұл (дәлелдеу теоретикалық) теорияның консервативті кеңеюі ${ displaystyle T_ {1}}$ егер әр теорема ${ displaystyle T_ {1}}$ теоремасы болып табылады ${ displaystyle T_ {2}}$ және кез келген теоремасы ${ displaystyle T_ {2}}$ тілінде ${ displaystyle T_ {1}}$ теоремасы қазірдің өзінде ${ displaystyle T_ {1}}$ .

Жалпы, егер ${ displaystyle Gamma}$ жиынтығы формулалар жалпы тілде ${ displaystyle T_ {1}}$ және ${ displaystyle T_ {2}}$ , содан кейін ${ displaystyle T_ {2}}$ болып табылады ${ displaystyle Gamma}$ -консервативті аяқталды ${ displaystyle T_ {1}}$ егер әрбір формула ${ displaystyle Gamma}$ дәлелденетін ${ displaystyle T_ {2}}$ да дәлелденеді ${ displaystyle T_ {1}}$ .

А-ның консервативті кеңеюі екенін ескеріңіз тұрақты теория сәйкес келеді. Егер ол болмаса, онда жарылыс принципітіліндегі әрбір формула ${ displaystyle T_ {2}}$ теоремасы болар еді ${ displaystyle T_ {2}}$ , сондықтан тілдегі әрбір формула ${ displaystyle T_ {1}}$ теоремасы болар еді ${ displaystyle T_ {1}}$ , сондықтан ${ displaystyle T_ {1}}$ үйлесімді болмас еді. Демек, консервативті кеңейтулер жаңа қарама-қайшылықтардың пайда болу қаупін тудырмайды. Мұны а ретінде қарастыруға болады әдістеме үлкен теорияларды жазу және құрылымдау үшін: теориядан бастаңыз, ${ displaystyle T_ {0}}$ , бұл белгілі (немесе болжамды) дәйекті және дәйекті түрде консервативті кеңейтулер жасайды ${ displaystyle T_ {1}}$ , ${ displaystyle T_ {2}}$ , ... оның.

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

Консервативті емес кеңейту а деп аталуы мүмкін дұрыс кеңейту.

Мысалдар

ACA₀ (ішкі жүйесі екінші ретті арифметика) бірінші ретті консервативті кеңейту болып табылады Пеано арифметикасы.
Фон Нейман-Бернейс-Годель жиынтығы теориясы консервативті кеңейту болып табылады Цермело-Фраенкель жиынтығы теориясы бірге таңдау аксиомасы (ZFC).
Ішкі жиынтық теориясы консервативті кеңейту болып табылады Цермело-Фраенкель жиынтығы теориясы бірге таңдау аксиомасы (ZFC).
Анықтамалар бойынша кеңейтулер консервативті болып табылады.
Шектелмеген предикат немесе функция белгілері бойынша кеңейту консервативті болып табылады.
IΣ₁ (тек индукциясы бар Peano арифметикасының ішкі жүйесі Σ⁰₁-формулалар) - бұл Π⁰₂-консервативті кеңейту қарабайыр рекурсивті арифметика (PRA).^[1]
ZFC - бұл Π¹₃-ZF-ді консервативті кеңейту Шуинфилдтің абсолюттік теоремасы.
ZFC үздіксіз гипотеза бұл Π²₁- ZFC консервативті кеңеюі.

Модельдік-теоретикалық консервативті кеңейту

Бірге модельдік-теориялық дегеніміз неғұрлым күшті түсінік алынады: кеңейту ${ displaystyle T_ {2}}$ теория ${ displaystyle T_ {1}}$ болып табылады модельдік-теориялық тұрғыдан консервативті егер ${ displaystyle T_ {1} subseteq T_ {2}}$ және әрбір моделі ${ displaystyle T_ {1}}$ моделіне дейін кеңейтуге болады ${ displaystyle T_ {2}}$ . Әрбір модель-теоретикалық консервативті кеңейту сонымен қатар жоғарыдағы мағынадағы (дәлел-теоретикалық) консервативті кеңейту болып табылады.^[2] Модельдік теоретикалық ұғымның дәлелдеу теориясынан артықшылығы бар, ол қолда бар тілге онша тәуелді емес; екінші жағынан, модельдік теоретикалық консервативтілікті орнату әдетте қиынырақ.