Кіріспе
Арифметиканы аксиомалау
Математикалық логикада Хейтинг арифметикасы – интуиционизм философиясына сәйкес арифметиканы аксиомалаудың бір түрі. Ол алғаш рет ұсынған Аренд Хейтингтің есімімен аталады.
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
Аксиоматизация
Хейтинг арифметикасы Пеано арифметикасының бірінші реттік теориясы сияқты сипатталуы мүмкін, бірақ ол интуициялық предикат есептеуін шығару үшін пайдаланады. Атап айтқанда, бұл екі рет жоққа шығару принципінің, сондай-ақ қарама-қарсылық принципінің қолданылмауын білдіреді. "Қолданбайды" деудің мағынасы – қарама-қарсылық туралы мәлімдеме барлық ұйғарымдар үшін автоматты түрде дәлелденбейді. Дегенмен, мұндай көптеген мәлімдемелер осы арифметикада дәлелденеді және кез келген мұндай дизъюнкцияның жоқтығына қайшылық тудырады. Хейтинг арифметикасы Пеано арифметикасының теоремаларынан қатаң түрде күшті, себебі барлық Пеано арифметикасы теоремалары Хейтинг арифметикасының теоремалары болып табылады. Хейтинг арифметикасы Пеано арифметикасының аксиомаларын қамтиды және оның мақсатталған моделі – табиғи сандар жиыны. Сигнатураға нөл "0" және ізбасар "S" кіреді, ал теориялар қосу және көбейтуді сипаттайды. Бұл логикаға әсер етеді: , және осылайша әр ұйғарым үшін, терістелуі формасында болады және осылайша тривиальды ұйғарым. Терминдер үшін жазыңыз. Белгілі бір термин үшін теңдік рефлексивтілік арқылы дұрыс, ал ұйғарым эквивалентті болады. Бұл дизъюнкцияларды формалды жою кванторсыз примитивті рекурсивті арифметикада мүмкін емес еді. Теория кез келген примитивті рекурсивті функция үшін функциялық символдармен кеңейтілуі мүмкін, бұл оны осы теорияның фрагменті етеді. Толық функция үшін, көбінесе формадағы предикаттар қарастырылады.
It may be shown that can then be defined as This formal elimination of disjunctions was not possible in the quantifier free primitive recursive arithmetic The theory may be extended with function symbols for any primitive recursive function, making also a fragment of this theory. For a total function , one often considers predicates of the form .
Екі есе терістеу
Кез келген интуиционистік теорияда жарылыс жарамды болған кезде, егер кейбір үшін теорема болса, онда теория сәйкес келмесе ғана анықтама бойынша дәлелденеді. Шындығында, Хейтинг арифметикасында қос терістеу нақты түрде білдіреді. формасындағы теорема, кейбір үшін шын болуы мүмкін емес екенін көрсетеді. Бұл, мұндайдың бар екендігінен әлсіз. Метатеориялық талқылаудың үлкен бөлігі классикалық түрде дәлелденетін барлық талаптарға қатысты болады. Қос терістеу көрсетіп тұрады. Сондықтан, формасындағы теорема әрқашан (оның ішінде оң) мәлімдемелерді нақты жоққа шығарудың жаңа тәсілдерін береді.
Классикалық теңдестірілген мәлімдемелер дәлелдемелері
Естеріңізге сала кетейік, формуласы классикалық түрде кері айналуы мүмкін, және осымен бірге осы да кері айналуы мүмкін. Мұндағы айырмашылық – барлық сандар үшін дұрыс деп есептегенде, сандық қарсы мысалдардың болуы мен абсурдтық қорытындылардың арасындағы келіспеушілік. Екі рет жою теоремаларды теоремаларға айналдырады. Нақтырақ айтқанда, егер бір формула жүйесінде дәлелденсе, оның классикалық эквиваленті Годель-Гентценнің теріс аудармасы да бірдей жүйеде дәлелденеді. Аударма процедурасы формуласын формуласына қайта жазуды қамтиды. Бұл, барлық Пеано арифметикасы теоремаларының дәлелі конструктивті дәлелден кейін классикалық логикалық қайта жазудан тұрады дегенді білдіреді. Шамамен айтқанда, соңғы қадам екі рет жоюды қолдануға келеді. Атап айтқанда, шешілмейтін атомдық ұйғарымдар болмаған жағдайда, экзистенциалдық кванторлар немесе дизъюнкцияларды қамтымайтын кез келген ұйғарым үшін .
Қолданылатын қағидалар мен ережелер
Минималды логика терістелген формулалар үшін қос жойқынды жоюды дәлелдейді. Көбінесе, Хейтинг арифметикасы кез келген Харроп формуласы үшін осы классикалық эквиваленттілікті дәлелдейді. Ал нәтижелер де жақсы қасиеттерге ие: арифметикалық иерархияның ең төменгі деңгейіндегі Марков ережесі – бұл қосымша пікірді қабылдауға болатын ереже, яғни , еркін айнымалысы бар. Кванторсыз предикаттар туралы айтудың орнына, осыны бастапқы рекурсивті предикат немесе Клинидің T предикаты үшін де бірдей тұжырымдауға болады, олар сәйкесінше деп аталады. Тіпті осымен байланысты ереже де қабылдауға болады, онда -тың есептеуге қабілеттілігі синтаксистік шартқа емес, керісінше сол жақ бөлігі де талаптарға сай болуы керек. Ескеріңіз, сөйлемді оның синтаксистік түріне сәйкес жіктегенде, тек классикалық тұрғыдан дұрыс эквиваленттілік негізінде оның күрделілігін төмендетуге қателесуге болмайды.
Instead of speaking of quantifier free predicates, one may equivalently formulate this for primitive recursive predicate or Kleene's T predicate, called , resp. and Even the related rule is admissible, in which the tractability aspect of is not e. g. based on a syntactic condition but where the left hand side also requires
Beware that in classifying a proposition based on its syntactic form, one ought not mistakenly assign a lower complexity based on some only classical valid equivalence.
Ортасы жоқ
Интуициялық логикаға қатысты басқа теориялар сияқты, осы конструктивті арифметикада әртүрлі жағдайлар дәлелдене алады. Дисъюнкцияны енгізу арқылы, егер ұйғарым немесе ұйғарымы дәлелденсе, онда ұйғарымы да дәлелденеді. Мысалы, аксиомалармен және аксиомалардан алынған, біреу "бір" предикаты үшін шеттестік принципін индукциялау үшін алғышартты растай алады, содан кейін нөлге теңдігі шешімді деп айтуға болады. Шындығында, ұйғарымы барлық сандар үшін теңдікті шешімді етеді, яғни, одан да күшті, өйткені теңдік – Хейтинг арифметикасындағы жалғыз предикат символы, сондықтан кез келген сандық еркін формула үшін , онда бос айнымалылар бар, теория барлық ұйғарымдар үшін дәлелденетін минималды логикадан асып түспейтін ереже бойынша жабылады. Кез келген минималды логикадан асып түспейтін теория барлық ұйғарымдар үшін ұйғарымын дәлелдейді. Сондықтан, егер теория тұйық болса, ол шеттестік принципінің жоққа шығарылуын ешқашан дәлелдей алмайды. Іс жүзінде, сияқты консервативті конструктивті жүйелерде, қай түпкі ұйғарымдар алгоритмдік түрде шешілетіні түсінілгенде, шеттестік дизъюнкциясының дәлелденбеуінің нәтижесі ұйғарымның алгоритмдік шешілмейтінін көрсетеді.
Any theory over minimal logic proves for all propositions. So if the theory is consistent, it never proves the negation of an excluded middle statement. Practically speaking, in rather conservative constructive frameworks such as , when it is understood what type of statements are algorithmically decidable, then an unprovability result of an excluded middle disjunction expresses the algorithmic undecidability of .
Консервативтілік
Қарапайым мәлімдемелер үшін теория тек қана классикалық жарамды екілік дихотомияларды растамайды. Фридман аудармасын теоремалардың барлығының : арқылы дәлелденгенін белгілеуге болады. Кез келген және кванторсыз үшін ,
Бұл нәтиже, әрине, ашық әмбебап жабылу арқылы да білдірілуі мүмкін. Шамамен айтқанда, классикалық түрде дәлелденетін есептеуге қабілетті қатынастар туралы қарапайым мәлімдемелер конструктивті түрде де дәлелденеді. Бірақ тоқтату мәселелерінде, кванторсыз ғана емес, сонымен қатар мәлімдемелер де маңызды рөл атқарады, және олар тіпті классикалық түрде тәуелсіз болуы мүмкін. Сол сияқты, шексіз домендегі бірегей болу, яғни , формальды түрде ерекше қарапайым емес. Сондықтан консервативті теорияға қарағанда, Робинсон арифметикасының классикалық теориясы барлық теоремаларды дәлелдейді, ал кейбір қарапайым теоремалар одан тәуелсіз. Индукция Фридманның нәтижесінде де маңызды рөл атқарады: мысалы, тәртіп туралы аксиомалармен күшейтілген және қалау бойынша шешілетін теңдікпен толықтырылған теория, оның интуиционистік әріптесіне қарағанда көбірек мәлімдемелерді дәлелдейді. Бұл талқылау толық емес. Классикалық теореманың конструктивті теориямен байланысты болуына қатысты әртүрлі нәтижелер бар. Сондай-ақ, металлологиялық нәтижелерді алу үшін қолданылған логиканың маңызды болуы мүмкін екенін ескеріңіз. Мысалы, жүзеге асырылуға қатысты көптеген нәтижелер конструктивті металлологияда алынған. Бірақ егер нақты контекст берілмесе, көрсетілген нәтижелер классикалық деп есептелуі керек.
Классикалық тәуелсіз ұғымдар
Гёдельдің толық емес теоремаларын білу, дәлелдемеге ие, бірақ дәлелдемесіз мәлімдемелердің түрін түсінуге көмектеседі. Хилберттің оныншы мәселесін шешу, кейбір нақты полиномдар мен сәйкес полиномдық теңдеулерді ұсынды, осылайша соңғыларының шешімі бар деген талап алгоритмдік тұрғыдан шешілмейтін болып табылады. Бұл ұсынысты былай түсіндіруге болады:
Мұндай нөлдік мән бар екендігі туралы кейбір мәлімдемелерге нақтырақ түсінік беріледі: теориялар, мысалы, немесе, осы ұсыныстардың теориялардың арифметикалық тұжырымдарымен эквивалентті екенін көрсетеді, яғни теорияның өзінің қарама-қайшылығын көрсетеді. Осылайша, мұндай ұсыныстарды тіпті күшті классикалық жиын теориялары үшін де жазуға болады. Үйлесімді және дұрыс арифметикалық теорияда, мұндай барлық талаптар тәуелсіз ұсыныс болып табылады. Содан кейін, квантор арқылы жоғарылатылған жосықсыздық, тәуелсіз Голдбах түріндегі немесе ұсыныс ретінде көрінеді. Нақтырақ айтқанда, қос жосықсыздық (немесе) де тәуелсіз. Ал кез келген үш жосықсыздық, кез келген жағдайда, бір жосықсыздыққа тең болып табылады.
АА-ның ДО-ға қайшы келуі
Келесі мәтін мұндай тәуелсіз тұжырымдамалардың мағынасын ашады. Теорияның барлық дәлелдемелерінің тізіміндегі индекс берілгенде, оның қандай ұйғарымды дәлелдейтінін тексеруге болады. Бұл процедураны дұрыс бейнелейді: абсурдты ұйғарымның бірі екенін көрсететін бастапқы рекурсивті предикат бар. Бұл жоғарыдағы полиномның қайтару мәні нөлге тең болатын, арнайы арифметикалық предикатқа қатысты. Металогиялық тұрғыдан қарағанда, егер жүйе дәйекті болса, онда ол әрбір жеке индекс үшін оны дәлелдейді. Нақты аксиоматизацияланған теорияда, әрбір дәлелді бірінен соң бірін тексеруге болады. Егер теория шынымен дәйекті болса, онда абсурдты дәлелдеу болмайды, бұл аталған "абсурдты іздеу" ешқашан тоқтамайды дегенді білдіреді. Теорияда формальды түрде бұл, арифметикалық қайшылықты жоққа шығаратын ұйғарыммен көрсетіледі. Эквивалентті ұйғарым барлық дәлелдер абсурдты дәлелдемейді деп, іздеудің ешқашан тоқтамайтынын ресми түсіндіреді. Шындығында, дәлелдемелерді дәл көрсететін омега-дәйекті теорияда, абсурдты іздеу тоқтау арқылы аяқталады деген дәлел жоқ (нақты қайшылық шығарылмайды), және, Гёдель көрскендей, абсурдты іздеу ешқашан тоқтамайды деген дәлел де болмайды (дәйектілік шығарылмайды). Қайталайық, абсурдты іздеу ешқашан тоқтамайды деген дәлел жоқ (дәйектілік шығарылмайды), сондай-ақ абсурдты іздеу тоқтамайды деген дәлел де жоқ (дәйектілік жоққа шығарылмайды). Екі дизъюнктивтің де бірі дәлелденбейді, ал олардың дизъюнкциясы тривиальды түрде дәлелденеді. Шындығында, егер жүйе дәйекті болса, онда ол логикалық оң тұжырым болып табылатын ұйғарымды бұзады. Дегенмен, ол тарихи түрде , ал оның жоқтығы - ұйғарым деп белгіленеді. Конструктивтік контексте, жоқтық белгісін осылай қолдану шатастыратын номенклатура болуы мүмкін. Фридман дәлелденбейтін тағы бір қызықты тұжырым жасады, атап айтқанда, дәйекті және жеткілікті теория өзінің арифметикалық дизъюнкциялық қасиетін ешқашан дәлелдей алмайды.
In an effectively axiomatized theory, one may successively perform an inspection of each proof. If a theory is indeed consistent, then there does not exist a proof of an absurdity, which corresponds to the statement that the mentioned "absurdity search" will never halt. Formally in the theory, the former is expressed by the proposition , negating the arithmetized inconsistency claim. The equivalent proposition formalizes the never halting of the search by stating that all proofs are not a proof of an absurdity. And indeed, in an omega consistent theory that accurately represents provability, there is no proof that the absurdity search would ever conclude by halting (explicit inconsistency not derivable), nor—as shown by Gödel—can there be a proof that the absurdity search would never halt (consistency not derivable). Reformulated, there is no proof that the absurdity search never halts (consistency not derivable), nor is there a proof that the absurdity search does not never halt (consistency not rejectible). To reiterate, neither of these two disjuncts is provable, while their disjunction is trivially provable. Indeed, if is consistent then it violates
The proposition expressing the existence of a proof of is a logically positive statement. Nonetheless, it is historically denoted , while its negation is a proposition denoted by In a constructive context, this use of the negation sign may be misleading nomenclature. Friedman established another interesting unprovable statement, namely that a consistent and adequate theory never proves its arithmetized disjunction property.
Дәлелденбейтін классикалық принциптер
Қазірдің өзінде минималды логика логикалық тұрғыдан барлық қарама-қайшылық жоқ талаптарды дәлелдейді, және атап айтқанда, егер де , онда теореманы дәлелденген қос терістелген шеттестік дизъюнкциясы (немесе болу туралы талап) ретінде қарастыруға болады. Бірақ дизъюнкция қасиетіне сүйенсек немесе тиісті Де Морган заңы интуиционистік тұрғыдан орындалмаса, қарапайым шеттестік принципін дәлелдеу мүмкін емес. және принциптерінің бұзылуы түсіндірілді. Ең кіші сан принципі – индукция принципімен теңдес көптеген тұжырымдардың бірі ғана. Төмендегі дәлелдеме көрсеткендей, , демек, бұл принцип те жалпы жарамды бола алмайды. Дегенмен, кез келген тривиальды емес предикат үшін қос терістелген ең кіші санның бар екенін көрсететін схема жалпы жарамды. Гёдельдің дәлеліне сәйкес, осы үш принциптің бұзылуын конструктивтік логиканың дәлелдемелік тұрғыдан қарастырылуымен үйлесетін Хейтинг арифметикасы ретінде түсінуге болады. Марков принципі примитивті рекурсивті предикаттар үшін , тіпті қатаң түрде күшті болғанымен, жоғарыда айтылғандай, қабылданады. Сол сияқты, теория терістелген предикаттар үшін алғышарт тәуелсіздік принципін дәлелдемейді, бірақ ол барлық терістелген ұйғарымдар үшін ереже бойынша жабық, яғни экзистенциалдық кванторды шығаруға болады. Осыған ұқсас, экзистенциалдық тұжырымды қарапайым дизъюнкциямен алмастырған жағдайда да осы принцип сақталады. Дұрыс тұжырымды кері тәртіпте де, дизъюнктивті силогизмді қолдана отырып, дұрыс екенін дәлелдеуге болады. Алайда, қос терістеудің ауысуы интуиционистік тұрғыдан дәлелденбейді, яғни барлық сандар бойынша әмбебап квантификациямен "" коммутативтілігінің схемасы. Бұл қызықты бұзылу, Чирч тезисі туралы бөлімде талқыланғандай, кейбір жағдайларда дәйектілігімен түсіндіріледі.
Шіркеудің тезисі
Шіркеу ережесі – Шіркеудің тезисі қағидасында қабылдануы мүмкін, ал оны қабылдамайды: Ол жоғарыда сипатталған сияқты жорамалды теріске шығаруларды білдіреді. Логикалық мағынада шешілетін барлық предикаттар жалпы есептелетін функция арқылы да шешілетінін көрсететін принципті қарастырайық. Ортаны алып тастаумен қақтығысын көрсету үшін, есептеу арқылы шешілмейтін предикатты анықтау жеткілікті. Осы мақсатта, Клиннің T предикатынан анықталған предикаттар үшін белгіні пайдаланайық. Жалпы есептелетін функциялардың индекстері орындалады. Ал, бастапқы рекурсивті түрде жүзеге асырылуы мүмкін болса да, , яғни диагональда тоқтауын көрсететін куәлікпен жартылай есептелетін функция индекстерінің класы есептеулік тұрғыдан санауға болады, бірақ есептеуге болмайды. арқылы анықталған классикалық толықтыру тіпті есептеулік тұрғыдан санауға да келмейді, тоқтату мәселесін қараңыз. Бұл дәлелденген шешілмейтін мәселе бұзушы мысал болып табылады. Кез келген индекс үшін эквивалентті форма сәйкес функция бағаланғанда ( ), барлық мүмкін бағалау тарихтарының сипаттамалары қолдағы бағалауды сипаттамайды. Нақтырақ айтқанда, функциялар үшін мұның шешілмейтіні, ресми Шіркеу қағидаларының рекурсивтік мектеппен байланысты екенін көрсетеді. Марков принципі осы мектепте және конструктивтік математикада жиі қолданылады. Шіркеу принципінің болуы жағдайында, ол оның әлсіз түрімен эквивалентті болады. Соңғысын әдетте бір аксиома ретінде беруге болады, атап айтқанда, кез келген Хейтинг арифметикасы үшін қос жорамалды жою және анықталатын предикаттар үшін алғышарттың тәуелсіздігін дәлелдеу, бірақ олар дәйекті түрде бірге келе бермейді. Л. Е. Ж. Браувердің интуиционистік мектебі Хейтинг арифметикасын екеуін де жорамалды теріске шығаратын қағидалар жинағымен кеңейтеді.
The formal Church's principles are associated with the recursive school, naturally. Markov's principle is commonly adopted, by that school and by constructive mathematics more broadly. In the presence of Church's principle, is equivalent to its weaker form The latter can generally be expressed as a single axiom, namely double negation elimination for any Heyting arithmetic together with both + prove independence of premise for decidable predicates, But they do not go together, consistently, with also negates The intuitionist school of L. E. J. Brouwer extends Heyting arithmetic by
a collection of principles that negate both as well as .
Бірқалыптылық
Егер теория дәйекті болса, онда ешқандай дәлел абсурд емес. Курт Гёдель кері аударманы енгізіп, Хейтинг арифметикасы дәйекті болса, Пеано арифметикасы да дәйекті болады деп дәлелдеді. Яғни, ол дәйектілік мәселесін Хейтинг арифметикасының дәйектілігіне келтірді. Алайда, Гёдельдің толық еместік теоремалары, кейбір теориялардың өздерінің дәйектілігін дәлелдей алмауы туралы, Хейтинг арифметикасының өзіне де қатысты. Классикалық бірінші реттік теорияның стандартты моделі, сондай-ақ оның стандартты емес модельдерінің кез келгені де Хейтинг арифметикасының моделі болып табылады.
Жинақ теориясы
Толық және оның мақсатты семантикасы үшін құрылымдық жиын теориясының модельдері де бар. Салыстырмалы түрде әлсіз жиын теориясы жеткілікті: олар шексіздік аксиомасын, арифметикалық формулалардың индукциясын дәлелдеу үшін предикативті бөлудің аксиомалық схемасын, сондай-ақ рекурсивті анықтамалар үшін шекті домендердегі функциялық кеңістіктердің болуын қабылдайды. Нақты айтқанда, бұл теориялар , толық бөлу аксиомасы немесе жиынтық индукциясы (тұрақтылық аксиомасын ескермей) немесе жалпы функциялық кеңістіктерді (қуат жиынының толық аксиомасын ескермей) қажет етпейді. Сонымен қатар, ординалдар класы , сондықтан фон Нейман натуралдарының жиынтығы теорияда жиынтық ретінде жоқ. Метатеориялық тұрғыдан алғанда, бұл теорияның домені оның ординалдар класымен шамалас және негізінен табиғи санмен биекциядағы барлық жиынтықтардың класы арқылы беріледі. Бұл аксиома ретінде аталады, ал қалған аксиомалар жиын алгебрасы мен тәртібіне байланысты: Біріктіру және бинарлық қиылыс, ол предикативті бөлу схемасымен тығыз байланысты, кеңейтімділік, жұптастыру және жиынтық индукция схемасы. Бұл теория онда берілген теориямен бірдей, бірақ күшті шексіздік аксиомасы жоқ және шектілік аксиомасы қосылған. Бұл жиын теориясындағы талқылануы модель теориясындағыдай. Ал кері бағытта, жиын теориясының аксиомалары бастапқы рекурсивті қатынасқа қатысты дәлелденеді. Бұл жиынтардың кішкентай ғаламын олардың өзара мүшелігін кодтайтын реттелген біртұтас бинарлық тізбектер жиынтығы ретінде түсінуге болады. Мысалы, "th" жиынында бір басқа жиын бар, ал "th" жиынында төрт басқа жиын бар. BIT предикатын қараңыз.
That small universe of sets can be understood as the ordered collection of finite binary sequences which encode their mutual membership. For example, the 'th set contains one other set and the 'th set contains four other sets. See BIT predicate.
Атқарылуы
Метатеориядағы кейбір сандар үшін зерттелетін объект теориясындағы сан былай белгіленеді. Интуиционистік арифметикада дизъюнкция қасиеті әдетте қолданылады. Сондай-ақ, арифметиканың кез келген c. e. кеңейтуі үшін, егер ол орындалса, сандық болу қасиеті де бар екені теорема болып табылады.
In intuitionistic arithmetics, the disjunction property is typically valid. And it is a theorem that any c. e. extension of arithmetic for which it holds also has the numerical existence property :
So these properties are metalogical equivalent in Heyting arithmetic. The existence and disjunction property in fact still holds when relativizing the existence claim by a Harrop formula , i. e. for provable
Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic. In turn, his student Nels David Nelson established (in an extension of ) that all closed theorems of (meaning all variables are bound) can be realized. Inference in Heyting arithmetic preserves realizability. Moreover, if then there is a partial recursive function realizing in the sense that whenever the function evaluated at terminates with , then This can be extended to any finite number of function arguments
There are also classical theorems that are not provable but do have a realization. Typed versions of realizability have been introduced by Georg Kreisel. With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories. See also BHK interpretation and Dialectica interpretation. In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to is categorical. Categoricity here is reminiscent of Tennenbaum's theorem. The model validates but not and so completeness fails in this context.
Осылайша, бұл қасиеттер Хейтинг арифметикасында металдық эквивалентті. Шындығында, болу туралы талапты Harrop формуласымен салыстыра қарастырғанда, болу және дизъюнкция қасиеттері әлі де сақталады, яғни дәлелдемеге болатын жағдайда. Чирчтің шәкірті Клейн Хейтинг арифметикасының маңызды іске асырылатын модельдерін енгізді. Ал оның шәкірті Нельс Дэвид Нельсон (кеңейтуде) барлық жабық теоремалардың (барлық айнымалылар байланысқан) іске асырылатынын дәлездеді. Хейтинг арифметикасындағы логикалық қорытынды іске асырылуды сақтайды. Сонымен қатар, егер онда функцияның мәні аяқталғанда , яғни функцияны іске асыратын ішінара рекурсивті функция бар. Бұл кез келген шекті сандағы функция аргументтеріне дейін кеңейтілуі мүмкін.
In intuitionistic arithmetics, the disjunction property is typically valid. And it is a theorem that any c. e. extension of arithmetic for which it holds also has the numerical existence property :
So these properties are metalogical equivalent in Heyting arithmetic. The existence and disjunction property in fact still holds when relativizing the existence claim by a Harrop formula , i. e. for provable
Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic. In turn, his student Nels David Nelson established (in an extension of ) that all closed theorems of (meaning all variables are bound) can be realized. Inference in Heyting arithmetic preserves realizability. Moreover, if then there is a partial recursive function realizing in the sense that whenever the function evaluated at terminates with , then This can be extended to any finite number of function arguments
There are also classical theorems that are not provable but do have a realization. Typed versions of realizability have been introduced by Georg Kreisel. With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories. See also BHK interpretation and Dialectica interpretation. In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to is categorical. Categoricity here is reminiscent of Tennenbaum's theorem. The model validates but not and so completeness fails in this context.
Дәлелдемеге келмейтін, бірақ іске асырылатын классикалық теоремалар да бар. Георг Крайзель іске асырылудың типтелген нұсқаларын енгізді. Осы арқылы ол интуиционистік теориялар үшін классикалық түрде жарамды Марков принципіне тәуелсіздігін көрсетті. Сондай-ақ, BHK интерпретациясы мен Dialectica интерпретациясын қараңыз. Тиімді топоста, индукциясымен шектелген Хейтинг арифметикасының шекті аксиомаланатын кіші жүйесі категориялық болып табылады. Бұл жердегі категориялық қасиет Тенненбаум теоремасын еске салады. Модель жарамды екенін, бірақ жарамсыздығын көрсетеді, сондықтан осы контексте толықтық жоқ.
In intuitionistic arithmetics, the disjunction property is typically valid. And it is a theorem that any c. e. extension of arithmetic for which it holds also has the numerical existence property :
So these properties are metalogical equivalent in Heyting arithmetic. The existence and disjunction property in fact still holds when relativizing the existence claim by a Harrop formula , i. e. for provable
Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic. In turn, his student Nels David Nelson established (in an extension of ) that all closed theorems of (meaning all variables are bound) can be realized. Inference in Heyting arithmetic preserves realizability. Moreover, if then there is a partial recursive function realizing in the sense that whenever the function evaluated at terminates with , then This can be extended to any finite number of function arguments
There are also classical theorems that are not provable but do have a realization. Typed versions of realizability have been introduced by Georg Kreisel. With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories. See also BHK interpretation and Dialectica interpretation. In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to is categorical. Categoricity here is reminiscent of Tennenbaum's theorem. The model validates but not and so completeness fails in this context.
Тип теориясы
Түрлер теориясының іске асырылымдары, қорытынды ережелеріне негізделген логикалық формализацияларды шағылыстыратын түрде, әртүрлі тілдерде жүзеге асырылды.
Ұзартулар
Хейтинг арифметикасы примитивті рекурсивті функциялар үшін қосымша функция белгілерімен талқыланды. Бұл теория Аккерман функциясының толықтығын дәлелдейді. Бұдан әрі, аксиомалар мен формализмді таңдау конструктивист аясында да әрдайым пікір-таластың нысаны болды. Дәлелдеу теориясында сандар арасындағы функциялардың түрлері, сондай-ақ олардың арасындағы функциялар және т.б. сияқты көптеген типтелген кеңейтулер жан-жақты зерттелді. Формальдықтар, әрине, функцияларды қолдануды реттейтін әртүрлі аксиомалармен күрделене түседі. Осылайша, функциялардың толық класын байытуға болады. Функцияның экстенсионалдығы және таңдау аксиомасымен біріктірілген ақырғы типтер теориясы, дәл осы арифметикалық формулаларды дәлелдейді және типтік теориялық интерпретацияға ие. Дегенмен, бұл теория Church тезисіне де, барлық функциялардың үздіксіздігіне де қарсы тұрады. Бірақ, мысалы, әртүрлі экстенсионалдық ережелерді, таңдау аксиомаларын, Марковтың және тәуелсіздік принциптерін, тіпті Кёниг леммасын қабылдасақ, бәрін бірге, бірақ әрқайсысын белгілі бір күшпен немесе деңгейде қолдансақ, ол формулалар деңгейінде ортақ жорамалды жоққа шығаруға мүмкін емес. Алғашқы зерттеулерде интенсионалдық теңдік және Брауэрдің таңдау тізбегі бар нұсқалар да қарастырылды. Конструктивті екінші реттік арифметиканың кері математикалық зерттеулері жүргізілді.
Тарих
Теорияның формалды аксиоматизациясы Хейтингке (1930), Гербранд пен Клинеге қатысты. Гёдель 1933 жылы оның дәйектілігін дәлелдеді.
Қарым-қатынас ұғымдары
Хейтинг арифметикасын, Буль алгебраларының интуиционистік аналогы болып табылатын Хейтинг алгебраларымен шатастыруға болмайды.