Теорияда қайшылықтың болмауы

Кіріспе

Теорияның қарама-қайшылықсыздығы

Классикалық дедуктивті логикада, логикалық қарама-қайшылыққа алып келмейтін теория консистентті деп аталады. Қарама-қайшылықтың жоқтығын семантикалық немесе синтаксистік тұрғыдан анықтауға болады. Семантикалық анықтама бойынша, теория консистентті болады, егер оның моделі болса, яғни теориядағы барлық формулалардың дұрыс болатын интерпретациясы болса. Бұл дәстүрлі Аристотельдік логикада қолданылатын мағына, бірақ қазіргі математикалық логикада «қанағаттандырылатындық» термині қолданылады. Синтаксистік анықтама бойынша, теория консистентті болады, егер формула және оның жоқтығы екеуі де жабық сөйлемдер жиынының (формальды түрде «аксиомалар») және белгілі бір (нақты, мүмкін жасырын) формалды дедуктивті жүйе бойынша шығарылатын жабық сөйлемдер жиынының элементтері болмаса. Аксиомалар жиыны консистентті болады, егер формула және оның жоқтығы екеуі де осы жиында болмаса. Егер дедуктивті жүйе болса, онда бұл семантикалық және синтаксистік анықтамалар нақты дедуктивті логикада құрастырылған кез келген теория үшін эквивалентті болады, онда логика толық деп аталады. Сентенциалдық логиканың толықтығын Пол Бернейс 1918 жылы және Эмиль Пост 1921 жылы, ал предикаттық логиканың толықтығын Курт Гёдель 1930 жылы дәлелдеді, ал индукция аксиома схемасына қатысты шектелген арифметиканың консистенттілігін Акерман (1924), фон Нейман (1927) және Гербранд (1931) дәлелдеді. Екінші реттік логика сияқты күшті логикалар толық емес. Консистенттілік дәлелі – нақты теорияның консистентті екенін математикалық түрде дәлелдеу. Математикалық дәлелдеу теориясының бастапқы дамуы Гилберт бағдарламасының бір бөлігі ретінде математиканың барлығы үшін шекті консистенттілік дәлелдерін беру ниетімен жетектелді. Толық еместік теоремалары Гилберт бағдарламасына күшті әсер етті, олар жеткілікті күшті дәлелдеу теориялары өз консистенттіліктерін дәлелдей алмайтынын көрсетті (егер олар консистентті болса). Консистенттілікті модельдік теорияны қолдану арқылы дәлелдеуге болады, бірақ көбінесе бұл логиканың моделіне сілтеме жасамай, тек синтаксистік жолмен жасалады. Кесуді жою (немесе тиісті есептеудің нормалауы, егер ол болса) есептеудің консистенттілігін білдіреді: жалғандықтың кесусіз дәлелі болмағандықтан, жалпы қарама-қайшылық жоқ.

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i. e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of Let be a set of closed sentences (informally "axioms") and the set of closed sentences provable from under some (specified, possibly implicitly) formal deductive system. The set of axioms is consistent when there is no formula such that and
If there exists a deductive system for which these semantic and syntactic definitions are equivalent for any theory formulated in a particular deductive logic, the logic is called complete. The completeness of the sentential calculus was proved by Paul Bernays in 1918 and Emil Post in 1921, while the completeness of predicate calculus was proved by Kurt Gödel in 1930, and consistency proofs for arithmetics restricted with respect to the induction axiom schema were proved by Ackermann (1924), von Neumann (1927) and Herbrand (1931). Stronger logics, such as second order logic, are not complete. A consistency proof is a mathematical proof that a particular theory is consistent. The early development of mathematical proof theory was driven by the desire to provide finitary consistency proofs for all of mathematics as part of Hilbert's program. Hilbert's program was strongly impacted by the incompleteness theorems, which showed that sufficiently strong proof theories cannot prove their consistency (provided that they are consistent). Although consistency can be proved using model theory, it is often done in a purely syntactical way, without any need to reference some model of the logic. The cut elimination (or equivalently the normalization of the underlying calculus if there is one) implies the consistency of the calculus: since there is no cut free proof of falsity, there is no contradiction in general.

Арифметика мен жинақ теориясының бірізділігі мен толықтығы

Арифметика теорияларында, мысалы, Пеано арифметикасында, теорияның дәйектілігі мен толықтығы арасында күрделі байланыс бар. Теория толық болады, егер оның тіліндегі кез келген φ формуласы үшін, φ немесе ¬φ-ның кем дегенде біреуі теорияның логикалық салдары болса. Пресбургер арифметикасы – қосу амалы бойынша натурал сандар үшін аксиомалық жүйе. Ол дәйекті де, толық та. Гёдельдің толық емес теоремалары арифметиканың жеткілікті күшті, рекурсивті саналатын кез келген теориясы бір мезгілде толық та, дәйекті де бола алмайтынын көрсетеді. Гёдель теоремасы Пеано арифметикасы (PA) және примитивті рекурсивті арифметика (PRA) теорияларына қолданылады, бірақ Пресбургер арифметикасына емес. Сонымен қатар, Гёдельдің екінші толық емес теоремасы арифметиканың жеткілікті күшті, рекурсивті саналатын теорияларының дәйектілігін белгілі бір тәсілмен тексеруге болатынын көрсетеді. Мұндай теория дәйекті болады, егер және тек қана ол теорияның Гёдель сөйлемі деп аталатын нақты бір сөйлемді дәлелдей алмаса, бұл сөйлем теорияның дәйекті екенін формалды түрде көрсетеді. Осылайша, жеткілікті күшті, рекурсивті саналатын, дәйекті арифметика теориясының дәйектілігі сол жүйеде өзінде ешқашан дәлелденбеуі мүмкін. Бұл нәтиже арифметиканың жеткілікті күшті фрагментін сипаттайтын рекурсивті саналатын теориялар үшін де дұрыс – оның ішінде Зермело-Фрэнкель жинақтар теориясы (ZF) сияқты жинақтар теориялары да. Бұл теориялар өздерінің Гёдель сөйлемдерін дәлелдей алмайды, егер олар дәйекті болса, және бұл жалпыға сенімді мәселе. ZF-тың дәйектілігі ZF-та дәлелденбейтіндіктен, жинақтар теориясында (және басқа да жеткілікті экспрессивті аксиомалық жүйелерде) әлсіз ұғым қызығушылық тудырады. Егер T теория болса, ал A қосымша аксиома болса, T + A теориясы T-ға қатысты дәйекті деп есептеледі (немесе жай ғана A теориясы T-мен дәйекті) егер T дәйекті болса, онда T + A да дәйекті болады деп дәлелдеуге болады. Егер A және ¬A екеуі де T-мен дәйекті болса, онда A теориясы T-дан тәуелсіз деп айтылады.

Нөмірлік

Математикалық логиканың келесі контекстінде, турниктегі символ "шығарылады" дегенді білдіреді. Яғни, b, a-дан шығарылады (нақты белгіленген формальды жүйеде).

Анықтама

Бірінші реттік логикадағы формулалар жиыны сәйкесті (жазылады ) егер мұндай формула болмаса, онда және басқа жағдайда сәйкессіз (жазылады ). Жиын жай ғана сәйкесті деп аталады, егер жиындағы ешқандай формула үшін, оның өзі де, оның жоқтығы да теорема болмаса. Жиын абсолютті сәйкесті немесе Post-сәйкесті деп аталады, егер тіліндегі кем дегенде бір формула теорема болмаса. Жиын максималды сәйкесті деп аталады, егер ол сәйкесті болса және кез келген формула үшін, егер , онда . Жиын куәгерлерді қамтиды деп айтылады, егер түріндегі әрбір формула үшін, мұндағы әрбір айнымалыны бір терминмен алмастыруды білдіреді, сонда теорема болады; қараңыз, Бірінші реттік логика.

Дәлелдің сызбасы

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

Үлгі теориясы

ZFC жинақтар теориясында классикалық бірінші реттік логика қолданылған жағдайда, қарама-қайшы теория дегеніміз – онда бір жабық формула және оның жоқтығы бар теория. Ал тұрақты теория – келесі логикалық түрде тең шарттар орындалатын теория.