Кіріспе
Логикалық жүйенің түрі. Бірінші реттік логика (предикаттық логика, сандық логика және бірінші реттік предикаттық есептеу) – математика, философия, лингвистика және компьютерлік ғылымда қолданылатын формальды жүйелер жиынтығы. Бірінші реттік логика логикалық емес объектілерге қатысты сандық айнымалыларды қолданады және айнымалыларды қамтитын сөйлемдерді пайдалануға мүмкіндік береді. Сондықтан, "Сократ – адам" сияқты мәлімдемелердің орнына "x бар, онда x – Сократ және x – адам" түріндегі өрнектер кездеседі, мұнда "бар" – сандық анықтауыш, ал x – айнымалы. Бұл оны сандық белгілер мен қатынастарды қолданбайтын мәлімдемелік логикадан ерекшелендіреді; осы мағынада мәлімдемелік логика – бірінші реттік логиканың негізі болып табылады. Жиын теориясы, топтар теориясы немесе арифметиканың формальды теориясы сияқты бір тақырыпқа қатысты теория әдетте бірінші реттік логика болып табылады, сонымен қатар нақтылы сөйлеу саласы (квантифицирленген айнымалылардың диапазоны), осы саладан өзіне шекті сандағы функциялар, осы сала бойынша шекті сандағы предикаттар және оларға қатысты аксиомалар жиынтығы да болады. "Теория" кейде формальды мағынада бірінші реттік логикадағы сөйлемдер жиынтығы ретінде түсініледі. "Бірінші реттік" термині бірінші реттік логиканы жоғары реттік логикадан ажыратады, онда аргумент ретінде предикаттар немесе функциялар бар предикаттар болады немесе онда предикаттар, функциялар немесе екеуі бойынша сандық анықтамаларға рұқсат етіледі. Бірінші реттік теорияларда предикаттар көбінесе жиындармен байланысты болады. Интерпретацияланған жоғары реттік теорияларда предикаттар жиындар жиыны ретінде интерпретациялануы мүмкін. Бірінші реттік логика үшін көптеген дедуктивтік жүйелер бар, олар дұрыс (барлық дәлелденген мәлімдемелер барлық модельдерде дұрыс) және толық (барлық модельдерде дұрыс мәлімдемелер дәлелденеді). Логикалық салдар қатынасы жартылай шешілетін болғанымен, бірінші реттік логикада теоремаларды автоматты түрде дәлелдеуде үлкен жетістіктерге қол жеткізілді. Бірінші реттік логика сондай-ақ Лёвенгейм-Сколем теоремасы және ықшамдық теоремасы сияқты дәлелдеу теориясындағы талдауларға бейімделетін бірнеше металогикалық теоремаларды қанағаттандырады. Бірінші реттік логика – математиканы аксиомаларға формализациялаудың стандарты және математика негіздерінде зерттеледі. Пеано арифметикасы және Цермело-Френкель жиын теориясы сәйкесінше сан теориясы мен жиын теориясының бірінші реттік логикаға аксиомалық түрлендірулері болып табылады. Дегенмен, бірінші реттік теорияның табиғи сандар немесе нақты сызық сияқты шексіз саласы бар құрылымды бірегей түрде сипаттауға жеткілікті күші жоқ. Бұл екі құрылымды толық сипаттайтын аксиомалық жүйелер, яғни категориялық аксиомалық жүйелер, екінші реттік логика сияқты күшті логикада алынуы мүмкін. Бірінші реттік логиканың негіздерін Готлоб Фреге және Чарльз Сандерс Пирс тәуелсіз түрде әзірледі. Бірінші реттік логиканың тарихы және оның формальды логикаға қалай үстемдік еткені туралы Хосе Феррейрос (2001) еңбегін қараңыз.
First order logic—also known as predicate logic, quantificational logic, and first order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First order logic uses quantified variables over non logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first order logic. A theory about a topic, such as set theory, a theory for groups, or a formal theory of arithmetic, is usually a first order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first order logic. The term "first order" distinguishes first order logic from higher order logic, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted. In first order theories, predicates are often associated with sets. In interpreted higher order theories, predicates may be interpreted as sets of sets. There are many deductive systems for first order logic which are both sound, i. e. all provable statements are true in all models, and complete, i. e. all statements which are true in all models are provable. Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first order logic. First order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem. First order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics. Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first order logic. No first order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axiom systems that do fully describe these two structures, i. e. categorical axiom systems, can be obtained in stronger logics such as second order logic. The foundations of first order logic were developed independently by Gottlob Frege and Charles Sanders Peirce. For a history of first order logic and how it came to dominate formal logic, see José Ferreirós (2001).
Кіріспе
Ұсыныстық логика қарапайым мәлімдемелермен айналысса, бірінші реттік логика предикаттар мен квантификацияны қосымша қамтиды. Предикат сөздік домендегі бір немесе бірнеше объект үшін шындық немесе жалған мәнін береді. «Сократ – философ» және «Платон – философ» деген екі сөйлемді қарастырайық. Ұсыныстық логикада бұл сөйлемдердің өзі зерттеу нысандары ретінде қарастырылады және мысалы, p және q сияқты айнымалылармен белгіленуі мүмкін. Олар нақты объектіге предикаттың қолданылуы ретінде емес, тек шын немесе жалған айтылған сөз ретінде қарастырылады. Дегенмен, бірінші реттік логикада бұл екі сөйлем белгілі бір жеке немесе логикалық емес объектінің қасиетін білдіретін мәлімдемелер ретінде берілуі мүмкін. Бұл мысалда екі сөйлем де белгілі бір жеке тұлға үшін ортақ формаға ие, бірінші сөйлемде x айнымалысының мәні «Сократ», ал екінші сөйлемде «Платон» болып табылады. Логикалық емес жеке тұлғалар туралы сөйлеу мүмкіндігі, түпнұсқа логикалық байланыстармен бірге, бірінші реттік логикаға ұсыныстық логиканы қосады. «x – философ» сияқты формуланың шындығы x арқылы белгіленген объектіге және «философ» предикатының интерпретациясына байланысты. Сәйкесінше, «x – философ» өзі шындық мәнін анықтай алмайды және сөйлемнің бөлігіне ұқсайды. Мысалы, логикалық символ әрқашан «және» дегенді білдіреді; ол ешқашан «немесе» деп интерпретацияланбайды, ол логикалық символмен белгіленеді. Алайда, Phil(x) сияқты логикалық емес предикат символы «x – философ», «x – Филипп есімді адам» немесе қолданылып жатқан интерпретацияға байланысты кез келген басқа да бірлік предикаты ретінде интерпретациялануы мүмкін.
Еркін және байланған айнымалылар
Формулада айнымалы еркін немесе байланған (немесе екеуі де) болуы мүмкін. Бұл ұғымның бір формалдауын Куайн жасаған, онда ең алдымен өзгермелінің кездесуі анықталады, содан кейін өзгермелінің кездесуі еркін немесе байланған, ал содан кейін жалпы өзгермелі символ еркін немесе байланған екені анықталады. Бірдей символдың әртүрлі кездесуін ажырату үшін, φ формуласындағы x айнымалы символының әр кездесуі, сол символдың x пайда болатын жеріне дейін φ формуласының бастапқы бөлігімен сәйкестендіріледі. 297-бет. Содан кейін, x-тің кездесуі байланған деп есептеледі, егер x-тің кездесуі кем дегенде бір немесе операторының қолданыс аймағында болса. Егер φ формуласындағы x-тің барлық кездесуі байланған болса, онда x φ формуласында байланған болып саналады. z тек еркін кездеседі, ал w формулада кездеспегендіктен, ол да еркін емес. Формуланың еркін және байланған айнымалылары әрқашан бөлек жиынтықтар болуы міндетті емес: P(x) → ∀x Q(x) формуласында x-тің бірінші кездесуі P аргументі ретінде еркін, ал екіншісі Q аргументі ретінде байланған. Еркін айнымалы кездеспейтін бірінші реттік логикадағы формула бірінші реттік сөйлем деп аталады. Осы формулалар интерпретацияда нақты шындық мәніне ие болады. Мысалы, Phil(x) сияқты формуланың шындығы x нені білдіретініне байланысты болуы керек. Ал ∃x Phil(x) сөйлемі берілген интерпретацияда дұрыс немесе жалған болады.
Мысал: реттелген абельдік топтар
Математикада реттелген абельдік топтардың тілінде бір тұрақты символ 0, бір унарлық функция символы −, бір екілік функция символы + және бір екілік қатынас символы ≤ бар. Сонда: +(x, y) және +(x, +(y, −(z))) өрнектері терминдер болып табылады. Бұл әдетте x + y және x + y − z деп жазылады. +(x, y) = 0 және ≤(+(x, +(y, −(z))), +(x, y)) өрнектері атомдық формулалар болып табылады. Бұл әдетте x + y = 0 және x + y − z ≤ x + y түрінде жазылады. Бұл өрнек – формула, әдетте былай жазылады: . Бұл формулада бір бос айнымалы бар, z. Реттелген абельдік топтар үшін аксиомалар тілде сөйлемдер жиынтығы ретінде берілуі мүмкін. Мысалы, топтың коммутативті екенін көрсететін аксиома әдетте былай жазылады.
The expressions +(x, y) and +(x, +(y, −(z))) are terms. These are usually written as x + y and x + y − z. The expressions +(x, y) = 0 and ≤(+(x, +(y, −(z))), +(x, y)) are atomic formulas. These are usually written as x + y = 0 and x + y − z ≤ x + y. The expression is a formula, which is usually written as This formula has one free variable, z. The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written
Семантика
Бірінші реттік тілдің түсіндірмесі, сол тілдегі әрбір логикалық емес символға (предикат символы, функция символы немесе тұрақты символ) мағына тағайындайды. Ол сонымен қатар, сандық көрсеткіштердің ауқымын анықтайтын сөздік доменді анықтайды. Нәтижесінде, әрбір терминге ол көрсететін объект беріледі, әрбір предикатқа объектілердің қасиеттері, ал әрбір сөйлемге – шындық мәні тағайындалады. Осылайша, түсіндірме тілдің терминдеріне, предикаттарына және формулаларына семантикалық мағына береді. Формальді тілдердің түсіндірмелерін зерттеу формальді семантика деп аталады. Бұдан әрі бірінші реттік логиканың стандартты, немесе Тарски семантикасының сипаттамасы келтіріледі. (Бірінші реттік логика үшін ойын семантикасын да анықтауға болады, бірақ таңдау аксиомасын қажет етуден басқа, ойын семантикасы бірінші реттік логика үшін Тарски семантикасымен сәйкес келеді, сондықтан ойын семантикасы бұл жерде кеңінен қарастырылмайды.)
Шындық мәндерін бағалау
Формуланың мәні нақты немесе жалған деп бағаланады, интерпретация мен μ айнымалысының тағайындалуы берілгенде, бұл айнымалының әрбір айнымалысына сөйлеу доменінің элементін байланыстырады. Айнымалы тағайындалуының қажеттілігі – еркін айнымалылары бар формулаларға мағына беру, мысалы, осы формуланының нақтылық мәні x және y-нің білдіретін мәндеріне байланысты өзгереді. Біріншіден, μ айнымалы тағайындауын тілдің барлық терминдеріне кеңейтуге болады, нәтижесінде әрбір термин сөйлеу доменінің бір ғана элементіне сәйкес келеді. Бұл тағайындауды жасау үшін келесі ережелер қолданылады: Айнымалылар. Әрбір x айнымалы μ(x) мәніне бағаланады. Функциялар. Егер терминдер доменнің элементтеріне бағаланған болса және f n-арғы функция символы берілген болса, онда термин келесіге бағаланады. Келесіде, әрбір формулаға нақтылық мәні тағайындалады. Бұл тағайындауды жасау үшін қолданылатын индуктивті анықтама T-схемасы деп аталады. Атомдық формулалар (1). Формуланың мәні нақты немесе жалған, оның мәні терминдердің бағалануына және түсіндірмеге байланысты болады, мұнда түсіндірме – , атомдық формулалардың (2) кіші жиыны болып табылады. Формула нақты болады, егер және evaluate бірдей домен элементіне бағаланса (теңдік туралы бөлімді қараңыз). Логикалық байланыстар. , және т.б. пішіндегі формулалар сөйлемдік логикадағыдай, байланыстырушының шындық кестесіне сәйкес бағаланады. Экзистенциалдық кванторлар. Формула M бойынша нақты болады және егер x-тің бағалауына қатысты және φ M түсіндірмесі мен айнымалы тағайындауы бойынша нақты болатын, x-тен ең көп айырмашылығы бар айнымалылардың бағалауы болса. Бұл формалды анықтама φ(x) қанағаттандырылатын x үшін мәнді таңдаудың жолы болса ғана нақты болады деген идеяны қамтиды. Универсалды кванторлар. Формула M бойынша нақты болады және егер φ(x) интерпретация M және x мәнінен ең көп айырмашылығы бар кейбір айнымалы тағайындауынан тұратын әрбір жұп үшін нақты болса. Бұл егер x үшін кез келген мәнді таңдау φ(x)-ты нақты етсе, бұл идеяны нақты етеді. Егер формула еркін айнымалыларды қамтымаса, яғни сөйлем болса, бастапқы айнымалы тағайындауы оның нақтылық мәніне әсер етпейді. Басқаша айтқанда, сөйлем M бойынша нақты болады және тек егер ол M және басқа кез келген айнымалы тағайындауы бойынша нақты болса. Мүмкін болатын екінші тәсіл – шындық мәнін анықтау үшін айнымалы тағайындау функцияларын пайдаланбау. Оның орнына, M интерпретациясы берілгенде, алдымен қолтаңбаға тұрақты символдар жинағын қосады, М-дегі сөйлеу доменінің әрбір элементі үшін біреуін; домендегі әр d үшін тұрақты символ cd белгіленеді делік. Түсіндірме кеңейтіледі, сондықтан әрбір жаңа тұрақты символ доменнің тиісті элементіне тағайындалады. Қазір квантталған формулалар үшін шындықты синтаксистік түрде келесідей анықтаймыз: Экзистенциалдық кванторлар (балама). Формула M бойынша нақты болады, егер сөйлеу доменінде d болса. Бұл φ-де x-тің әрбір еркін пайда болуын cd-мен алмастыру нәтижесі. Универсалды кванторлар (балама). Формула M бойынша нақты болады, егер сөйлеу доменіндегі әрбір d үшін M бойынша нақты болса. Бұл баламалы тәсіл барлық сөйлемдерге айнымалы тағайындаулар арқылы алынған тәсілмен дәл бірдей шындық мәндерін береді.
Variables. Each variable x evaluates to μ(x)
Functions. Given terms that have been evaluated to elements of the domain of discourse, and a n ary function symbol f, the term evaluates to
Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the T schema. Atomic formulas (1). A formula is associated the value true or false depending on whether , where are the evaluation of the terms and is the interpretation of , which by assumption is a subset of Atomic formulas (2). A formula is assigned true if and evaluate to the same object of the domain of discourse (see the section on equality below). Logical connectives. A formula in the form , , etc. is evaluated according to the truth table for the connective in question, as in propositional logic. Existential quantifiers. A formula is true according to M and if there exists an evaluation of the variables that differs from at most regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment This formal definition captures the idea that is true if and only if there is a way to choose a value for x such that φ(x) is satisfied. Universal quantifiers. A formula is true according to M and if φ(x) is true for every pair composed by the interpretation M and some variable assignment that differs from at most on the value of x. This captures the idea that is true if every possible choice of a value for x causes φ(x) to be true. If a formula does not contain free variables, and so is a sentence, then the initial variable assignment does not affect its truth value. In other words, a sentence is true according to M and if and only if it is true according to M and every other variable assignment
There is a second common approach to defining truth values that does not rely on variable assignment functions. Instead, given an interpretation M, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse in M; say that for each d in the domain the constant symbol cd is fixed. The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. One now defines truth for quantified formulas syntactically, as follows:
Existential quantifiers (alternate). A formula is true according to M if there is some d in the domain of discourse such that holds. Here is the result of substituting cd for every free occurrence of x in φ. Universal quantifiers (alternate). A formula is true according to M if, for every d in the domain of discourse, is true according to M.
This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments.
Дұрыс, қанағаттанарлық және логикалық салдары
Егер φ сөйлем берілген M түсіндірмесінде шындыққа сай келсе, онда M сөйлемді қанағаттандырады делінеді; бұл A сөйлемнің қанағаттандырылатыны, егер ол бір түсіндірмеде шын болса. Бұл модель теориясындағы символдан өзгеше, онда модельде қанағаттанушылықты білдіреді, яғни " ' доменіне өзгермелі символдарға тиісті мәндер тағайындалған". Бос айнымалылары бар формулалардың қанағаттандырылуы күрделірек, себебі түсіндірме өздігінен мұндай формуланың шындық мәнін анықтай алмайды. Ең көп тараған конвенция бойынша, егер формула φ бос айнымалылары , , үшін түсіндірмемен қанағаттандырылса, онда формула φ дискурс доменінен осы бос айнымалыларға тағайындалған индивидтар қандай болса да шын болып қала береді. Бұл формула φ қанағаттандырылса және тек оның жалпы жабылуы қанағаттандырылса ғана қанағаттандырылады дегендей әсер етеді. Формула логикалық жарамды (немесе жай ғана жарамды) егер ол кез келген түсіндірмеде шын болса. Бұл формулалар сөйлемдік логикадағы тавтологиялармен салыстырылатын рөл атқарады. Егер ψ шындыққа келтіретін кез келген түсіндірме φ шындыққа келтірсе, онда φ формуласы ψ формуласының логикалық салдары болып табылады. Бұл жағдайда φ формуласы ψ арқылы логикалық түрде туындайды делінеді.
Бірінші реттік теориялар, модельдер және элементарлық кластар
Белгілі бір қолтаңбаның бірінші реттік теориясы – сол қолтаңбаның символдарынан құралған аксиомалар жиынтығы. Аксиомалар жиыны көбінесе шекті немесе рекурсивті түрде саналатын болады, мұндай жағдайда теория тиімді деп аталады. Кейбір авторлар теорияларға аксиомалардың барлық логикалық салдарының да кіруін талап етеді. Аксиомалар теория ішінде дұрыс деп есептеледі және олардан теория ішінде дұрыс болатын басқа да сөйлемдер шығарылуы мүмкін. Белгілі бір теориядағы барлық сөйлемдерді қанағаттандыратын бірінші реттік құрылым сол теорияның моделі деп аталады. Элементарлық сынып – нақты бір теорияны қанағаттандыратын барлық құрылымдардың жиынтығы. Бұл сыныптар модель теориясының негізгі зерттеу нысаны болып табылады. Көптеген теориялардың мақсатталған интерпретациясы бар, яғни теорияны зерттегенде ескерілетін нақты модель. Мысалы, Пеано арифметикасының мақсатталған интерпретациясы – әдеттегі амалдары бар әдеттегі натурал сандардан тұрады. Алайда, Лёвенхайм-Сколем теоремасы көптеген бірінші реттік теорияларда басқа да, стандартты емес модельдердің де болатынын көрсетеді. Теория сәйкес келеді, егер оның аксиомаларынан қайшылықты дәлелдеу мүмкін болмаса. Теория толық болады, егер оның қолтаңбасындағы әрбір формула үшін, сол формула немесе оның жоқтығы теория аксиомаларының логикалық салдары болса. Гёдельдің толық еместік теоремасы, натурал сандар теориясының жеткілікті бөлігін қамтитын тиімді бірінші реттік теориялардың тұтастығы мен толықтығын бірдей қамтамасыз ете алмайтынын көрсетеді.
Дедуктивті жүйелер
Дедуктивті жүйе бір формуланың екінші формуланың логикалық салдары екенін таза синтаксистік негізде көрсету үшін қолданылады. Бірінші реттік логика үшін мұндай көптеген жүйелер бар, оның ішінде Гильберт стиліндегі дедуктивті жүйелер, табиғи дедукция, тізбекті есептеу, кестелік әдіс және шешім табу әдісі. Бұл жүйелердің ортақ қасиеті – дедукция шекті синтаксистік объекті болып табылады; осы объектінің форматы және құрылу тәсілі әртүрлі болуы мүмкін. Дәлел теориясында осы шекті дедукциялар жиі туынды деп аталады. Олар көбінесе дәлелдер деп те аталады, бірақ табиғи тілдегі математикалық дәлелдерден айырмашылығы, толыққанды ресмилендірілген. Дедуктивті жүйе дұрыс деп есептеледі, егер жүйеде туындырылған кез келген формула логикалық тұрғыдан дұрыс болса. Керісінше, дедуктивті жүйе толық болады, егер әрбір логикалық тұрғыдан дұрыс формула туындырылатын болса. Осы мақалада талқыланған барлық жүйелер дұрыс және толық. Олар сондай-ақ, күдікті жарамды дедукцияның нақты дедукция екенін тиімді тексеруге болатын қасиетті бөліседі; мұндай дедукция жүйелері тиімді деп аталады. Дедуктивті жүйелердің маңызды қасиеті – олар таза синтаксистік болып табылады, сондықтан туындыларды ешқандай интерпретацияны ескермей тексеруге болады. Осылайша, дұрыс аргумент тілдің барлық мүмкін интерпретацияларында дұрыс болады, бұл интерпретация математика, экономика немесе басқа сала туралы болсын. Жалпы, бірінші реттік логикадағы логикалық салдар тек жартылай шешіледі: егер A сөйлем B сөйлемін логикалық түрде білдірсе, онда оны анықтауға болады (мысалы, тиімді, дұрыс және толық дәлелдеу жүйесін пайдаланып, дәлелді табуға дейін іздеу арқылы). Алайда, егер A логикалық түрде B-ні білдірмесе, бұл A логикалық түрде B-нің жоқтығын білдіреді дегенді білдірмейді. A және B формулалары берілген жағдайда, A логикалық түрде B-ні білдіре ме, білдірмей ме, әрқашан дұрыс шешетін тиімді процедура жоқ.
Қорытындылау ережесі
Шешімделу ережесі белгілі бір қасиетке ие гипотеза ретінде берілген нақты формуланың (немесе формулалар жиынтығының) негізінде, басқа нақты формуланың (немесе формулалар жиынтығының) қорытынды ретінде алынуын көрсетеді. Егер кез келген интерпретация гипотезаны қанағаттандырса, онда сол интерпретация қорытындыны да қанағаттандыратын болса, ереже дұрыс (немесе шындықты сақтайтын) болып есептеледі, яғни жарамдылықты сақтайды. Мысалы, жиі қолданылатын шешімделу ережесі – алмастыру ережесі. Егер t – термин болса, ал φ – x айнымалысын қамтитын формула болса, онда φ[t/x] – φ формуласындағы x айнымалысының барлық еркін кездесулерін t-мен алмастыру нәтижесі. Алмастыру ережесіне сәйкес, кез келген φ және кез келген t термині үшін, егер алмастыру процесінде t терминінің еркін айнымалысы байланбаса, онда φ-ден φ[t/x] қорытындысын шығаруға болады. (Егер t терминінің бірнеше еркін айнымалысы байланса, онда x-ті t-мен алмастыру үшін алдымен φ формуласының байланған айнымалыларын t терминінің еркін айнымалыларынан өзгеше етіп өзгерту қажет.) Байланған айнымалыларға қойылатын шектеудің қажеттілігін түсіну үшін, арифметиканың (0,1,+,×,=) қолтаңбасында берілген логикалық жарамды φ формуласын қарастырайық. Егер t термині "x + 1" болса, онда φ[t/y] формуласы , көптеген интерпретацияларда бұл жалған болады. Мұның себебі – t терминінің еркін айнымалысы x алмастыру кезінде байланған. Көзге көрінетін алмастыруды φ формуласының байланған айнымалысы x-ті басқа бір символға, мысалы z-ге өзгерту арқылы алуға болады, сонда алмастырудан кейінгі формула , бұл қайтадан логикалық жарамды болады. Алмастыру ережесі шешімделу ережелерінің бірнеше жалпы ерекшеліктерін көрсетеді. Ол толығымен синтаксистік болып табылады; оны дұрыс қолданғанын кез келген интерпретацияға жүгінбей-ақ анықтауға болады. Ол (синтаксистік тұрғыдан анықталған) қолданылу шектеулеріне ие, оларды сақтау арқылы шығарудың дұрыстығын қамтамасыз ету керек. Сонымен қатар, көбінесе болатындай, бұл шектеулер шешімделу ережесіне қатысты формулалардың синтаксистік манипуляциялары кезінде еркін және байланған айнымалылар арасындағы өзара әрекеттесулердің нәтижесі болып табылады.
To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by , in the signature of (0,1,+,×,=) of arithmetic. If t is the term "x + 1", the formula φ[t/y] is , which will be false in many interpretations. The problem is that the free variable x of t became bound during the substitution. The intended replacement can be obtained by renaming the bound variable x of φ to something else, say z, so that the formula after substitution is , which is again logically valid. The substitution rule demonstrates several common aspects of rules of inference. It is entirely syntactical; one can tell whether it was correctly applied without appeal to any interpretation. It has (syntactically defined) limitations on when it can be applied, which must be respected to preserve the correctness of derivations. Moreover, as is often the case, these limitations are necessary because of interactions between free and bound variables that occur during syntactic manipulations of the formulas involved in the inference rule.
Гилберт стилі жүйелері және табиғи шегерім
Гильберт стиліндегі дедуктивтік жүйедегі дедукция – формулалардың тізімі, олардың әрқайсысы логикалық аксиома, ағымдағы шығарылым үшін қабылданған гипотеза немесе қорытынды шығару ережесі арқылы бұрынғы формулалардан туындайтын нәрсе. Логикалық аксиомалар логикалық тұрғыдан дұрыс формулалардың бірнеше аксиомалық схемаларынан тұрады; олар пропозициялық логиканың маңызды бөлігін қамтиды. Қорытынды шығару ережелері кванторларды манипуляциялауға мүмкіндік береді. Типтік Гильберт стиліндегі жүйелерде логикалық аксиомалардың бірнеше шексіз схемаларымен қатар, аздаған қорытынды шығару ережелері болады. Әдетте, тек modus ponens және жалпыламалау ережелері қолданылады. Табиғи дедукция жүйелері Гильберт стиліндегі жүйелерге ұқсас, себебі дедукция – формулалардың шекті тізімі. Дегенмен, табиғи дедукция жүйелерінде логикалық аксиомалар жоқ; олар дәлелдемедегі формулалардағы логикалық байланыстарды манипуляциялауға арналған қосымша қорытынды шығару ережелерін қосу арқылы толықтырылады.
Тізбекті есептеу
Кезекті есептеу табиғи шегерім жүйелерінің қасиеттерін зерттеу үшін жасалды. Бір формуламен бір уақытта жұмыс істеудің орнына, ол реттіліктерді қолданады, олар мынадай түріндегі өрнектер:
мұнда A1, …, An, B1, …, Bk – формулалар, ал турникте белгісі екі бөліктің арасын бөлу үшін қолданылатын тыныш белгі ретінде пайдаланылады. Интуитивті түрде, реттілік -ның -дан шығатынын көрсетеді.
Таблеакс әдісі
Тақырыбында сипатталған әдістерден айырмашылығы, кестелік әдіс бойынша туындылар формулалар тізімі емес. Керісінше, туынды – формулалар ағашы. Формула А-ның дәлелді екенін көрсету үшін, кестелік әдіс А-ның жоқтығы қанағаттандырылмайтынын көрсетуге тырысады. Туынды ағашының түбірінде басталады; ағаш формуланың құрылымын көрсететіндей етіп тармақталады. Мысалы, егер оны қанағаттандыру мүмкін емес екенін көрсету керек болса, C және D әрқайсысы да қанағаттандырылмайтынын көрсету қажет; бұл ағаштағы тармақталу нүктесіне сәйкес келеді, онда C және D – түбірдің балалары.
Қаулы
Резолюция ережесі – біріктірумен бірге бірінші реттік логика үшін дұрыс және толық болатын жалғыз логикалық қорытынды ереже. Табло әдісі сияқты, формуланың жоқтығын көрсету арқылы оның терістелуі қанағаттандырылмайтыны дәлелденеді. Резолюция әдісі автоматты түрде теоремаларды дәлелдеуде кеңінен қолданылады. Резолюция әдісі тек атомдық формулалардың дизъюнкциясы түріндегі формулалармен жұмыс істейді; кез келген формулалар алдымен Сколемизация арқылы осы түріне келтірілуі керек. Резолюция ережесі гипотезалардан және , деген қорытынды алуға болатынын көрсетеді.
Теңдіксіз бірінші реттік логика
Басқа тәсіл теңдік қатынасын логикалық емес символ деп қарастырады. Бұл конвенция теңдіксіз бірінші реттік логика деп аталады. Егер теңдік қатынасы қолтаңбаға енгізілсе, қалаған жағдайда, логика ережелері ретінде қарастырылмай, теңдік аксиомалары қарастырылып жатқан теорияларға қосылуы керек. Бұл әдіс пен теңдіктің бірінші реттік логикасының негізгі айырмашылығы – интерпретация енді екі әртүрлі объектіні "тең" деп түсіндіре алады (бірақ Лейбниц заңына сәйкес, олар кез келген интерпретацияда дәл бірдей формулаларды қанағаттандырады). Яғни, теңдік қатынасы енді интерпретацияның функциялары мен қатынастарына қатысты үйлесімді болатын кездейсоқ эквиваленттілік қатынасымен түсіндірілуі мүмкін. Осы екінші конвенция қолданылғанда, нормальді модель термині екі әртүрлі объекті a және b үшін a = b теңдігі орындалмаған интерпретацияны білдіреді. Теңдіктің бірінші реттік логикасында тек нормальді модельдер қарастырылады, сондықтан нормальді модельден өзге модельді атауға арналған термин жоқ. Теңдіксіз бірінші реттік логика зерттелген кезде, Лёвенхайм-Школем теоремасы сияқты нәтижелердің тұжырымдамасын тек нормальді модельдерді қарастыру үшін өзгерту қажет. Теңдіксіз бірінші реттік логика көбінесе екінші реттік арифметика және басқа жоғары реттік арифметика теорияларының контекстінде қолданылады, онда табиғи сандар жиындары арасындағы теңдік қатынасы әдетте алынып тасталады.
Металдық қасиеттері
Бірінші дәрежелі логиканы жоғары дәрежелі логикадан гөрі пайдаланудың бір себебі – бірінші дәрежелі логиканың күшті логикаларда жоқ көптеген металогиялық қасиеттерінің болуы. Бұл нәтижелер нақты теориялардың қасиеттеріне емес, бірінші дәрежелі логиканың өзінің жалпы қасиеттеріне қатысты. Олар бірінші дәрежелі теориялардың модельдерін құруға арналған негізгі құралдарды қамтамасыз етеді.
Толықтығы және шешілмеуі
1929 жылы Курт Гёдель дәлелдеген Гёдельдің толықтық теоремасы бірінші реттік логика үшін дұрыс, толық және тиімді дедуктивті жүйелердің бар екенін, сондай-ақ бірінші реттік логикалық салдарын шекті дәлелдеумен анықтайтынын көрсетеді. Көзге жақын тұрғысынан, φ формуласы ψ формуласын логикалық тұрде білдіреді деген тұжырым, φ-ның барлық модельдеріне байланысты; мұндай модельдердің кардиналдығы кез келгендей үлкен болуы мүмкін, сондықтан логикалық салдарын әрбір модельді тексеру арқылы тиімді растауға болмайды. Дегенмен, барлық шекті туындыларды санап шығуға және φ-дан ψ туындысын іздеуге болады. Егер ψ логикалық тұрде φ-тан шықса, онда мұндай туынды әрине табылады. Осылайша, бірінші реттік логикалық салдарын жартылай шешуге болады: ψ, φ-ның логикалық салдары болатын (φ, ψ) сөйлемдерінің барлық жұптарын тиімді санауға болады. Ұйғарымдық логикадан өзгеше, бірінші реттік логика шешілмейді (бірақ жартылай шешіледі), егер тілде теңдіктен өзге кемінде 2 аргументі бар бір предикат болса. Бұл, кез келген формуланың логикалық жарамдылығын анықтайтын шешім қабылдау процедурасының жоқтығын білдіреді. Бұл нәтижені Алонзо Черч пен Алан Тьюринг 1936 және 1937 жылдары тәуелсіз түрде дәлелдеді, осылайша Дэвид Хилберт пен Вильгельм Акерманның 1928 жылы қойған Entscheidungsproblem мәселесіне теріс жауап берді. Олардың дәлелдемелері бірінші реттік логика үшін шешім мәселесінің шешілмейтіндігі мен тоқтату мәселесінің шешілмейтіндігі арасындағы байланысты көрсетеді. Бірінші реттік логикадан әлсіз жүйелер бар, олар үшін логикалық салдарын анықтауға болады. Мұндай жүйелерге ұйғарымдық логика және монадтық предикат логикасы жатады, ол тек бір аргументі бар предикаттармен және функцияларсыз бірінші реттік логиканың шектеулі түрі болып табылады. Функцияларсыз шешілетін басқа логикаларға бірінші реттік логиканың қорғалған фрагменті және екі айнымалы логика жатады. Бірінші реттік формулалардың Бернейс-Шенфинкель класы да шешіледі. Бірінші реттік логиканың шешілетін ішкі жиынтықтарын сипаттамалық логика аясында да зерттеуге болады.
Лёвенхайм-Сколем теоремасы
Лёвенхайм-Сколем теоремасы λ кардиналдығының бірінші реттік теориясы шексіз модельге ие болса, онда ол λ-дан үлкен немесе оған тең әрбір шексіз кардиналдықтағы модельдерге де ие болады екенін көрсетеді. Модель теориясының ең ерте нәтижелерінің бірі болып табылатын бұл теорема, саналатын қолтаңбасы бар бірінші реттік тілде саналатындықты немесе саналмайтындықты сипаттау мүмкін емес екенін көрсетеді. Яғни, М кездейсоқ құрылымының домені саналатын (немесе екінші жағдайда саналмайтын) болса ғана φ(x) деген бірінші реттік формулаға қанағаттандырады; басқаша айтқанда, мұндай формула жоқ. Лёвенхайм-Сколем теоремасы шексіз құрылымдарды бірінші реттік логикада категориялық түрде аксиоматизациялауға болмайтынын білдіреді. Мысалы, жалғыз моделі нақты сан түзуі болатын бірінші реттік теория жоқ: шексіз моделі бар кез келген бірінші реттік теорияда континуумнан үлкен кардиналдығы бар модель де болады. Нақты сан түзуі шексіз болғандықтан, нақты сан түзуіне қанағаттандыратын кез келген теория стандартты емес кейбір модельдерге де қанағаттандырады. Лёвенхайм-Сколем теоремасы бірінші реттік жиын теорияларына қолданылғанда, интуицияға қайшы келетін салдары Сколемнің парадоксы деп аталады.
Қатылық теоремасы
Компакттылық теоремасы бірінші реттік сөйлемдер жиынының моделі бар екенін, және тек қана егер оның кез келген шекті ішкі жиынының моделі болса, күйейді. Бұл, егер формула шексіз бірінші реттік аксиомалар жиынының логикалық салдары болса, онда ол сол аксиомалардың кейбір шекті санының логикалық салдары болады дегенді білдіреді. Бұл теорема алғаш рет Курт Гёдель толықтық теоремасының салдары ретінде дәлелденді, бірақ содан бері көптеген қосымша дәлелдер алынды. Бұл модель теориясының орталық құралы болып табылады және модельдерді құрудың негізгі әдісін ұсынады. Компакттылық теоремасы бірінші реттік құрылымдардың қай топтамалары элементарлық сыныптар болатынына шектеу қояды. Мысалы, компакттылық теоремасы кез келген теорияның кез келген үлкен шекті модельдері болса, онда оның шексіз модельі де болады екенін білдіреді. Осылайша, барлық шекті графтардың класы элементарлық класс емес (осыған ұқсас жағдай көптеген басқа алгебралық құрылымдар үшін де орынды). Компакттылық теоремасымен түсіндірілетін бірінші реттік логиканың тағы да күрделі шектеулері бар. Мысалы, компьютерлік ғылымда көптеген жағдайларды күйлердің (түйіндердің) және байланыстардың (бағытталған қабырғалардың) бағытталған графы ретінде модельдеуге болады. Мұндай жүйені тексеру үшін "жақсы" күйден ешқандай "жаман" күйге жету мүмкін емес екенін көрсету қажет болуы мүмкін. Осылайша, "жақсы" және "жаман" күйлер графиктің әртүрлі байланысқан компоненттерінде орналасқан ба дегенді анықтауға тырысады. Алайда, компакттылық теоремасын байланысқан графтардың бірінші реттік логикада элементарлық класс еместігін көрсету үшін қолдануға болады, және графтар логикасында x-тен y-ге дейін жол бар екенін білдіретін φ(x,y) сияқты бірінші реттік логика формуласы жоқ. Бірақ байланыс екінші реттік логикада берілуі мүмкін, бірақ ғана экзистенциалды жиынтық кванторларымен емес, сондай-ақ компакттылыққа ие.
Линдстрем теоремасы
Пер Линдстрем металлологиялық қасиеттерді талқылағанда, олардың бірінші реттік логиканы сипаттайтынын және одан күшті логиканың мұндай қасиеттерге ие бола алмайтынын көрсетті (Ebbinghaus and Flum 1994, XIII тарау). Линдстрем абстрактілі логикалық жүйелер класын және осы кластың мүшелерінің салыстырмалы күшін қатаң түрде анықтады. Ол осы типтегі жүйелер үшін екі теорема дәлелдеді: Линдстремнің анықтамасын қанағаттандыратын және бірінші реттік логиканы қамтитын, сондай-ақ Лёвенхайм-Школем теоремасы мен тығыздық теоремасын қанағаттандыратын логикалық жүйе бірінші реттік логикаға эквивалентті болуы керек. Линдстремнің анықтамасын қанағаттандыратын, жартылай шешілетін логикалық салдар қатынасына ие және Лёвенхайм-Школем теоремасын қанағаттандыратын логикалық жүйе де бірінші реттік логикаға эквивалентті болуы керек.
A logical system satisfying Lindström's definition that contains first order logic and satisfies both the Löwenheim–Skolem theorem and the compactness theorem must be equivalent to first order logic. A logical system satisfying Lindström's definition that has a semidecidable logical consequence relation and satisfies the Löwenheim–Skolem theorem must be equivalent to first order logic.
Шектеулер
Бірінші реттік логика математиканың көп бөлігін формалдауға жеткілікті және компьютерлік ғылымда және басқа да салаларда кеңінен қолданылатын болса да, оның белгілі бір шектеулері бар. Оларға оның көлемділігінің шектеулері және табиғи тілдердің қандай бөліктерін сипаттау мүмкіндігінің шектеулері жатады. Мысалы, бірінші реттік логика шешілмейді, яғни оның дұрыстығын, толықтығын және нәтижелілігін қамтамасыз ететін дәлелдеу алгоритмі жоқ. Бұл қызықты шешілетін фрагменттерді зерттеуге әкелді, мысалы C2: екі айнымалысы және сандық кванторлары бар бірінші реттік логика.
Экспрессивтілік
Лёвенхайм-Сколем теоремасы, егер бірінші реттік теорияда шексіз модель болса, онда оның кез келген кардиналдылықтағы шексіз модельдері болады екенін көрсетеді. Атап айтқанда, шексіз модельі бар ешбір бірінші реттік теория категориалды бола алмайды. Демек, жалғыз моделі табиғи сандар жиыны домен ретінде немесе жалғыз моделі нақты сандар жиыны домен ретінде болатын бірінші реттік теория жоқ. Бірінші реттік логиканың көптеген кеңейтімдері, соның ішінде шексіз логика және жоғары реттік логика, табиғи сандар немесе нақты сандардың категориялық аксиоматизациясына мүмкіндік береді. Алайда, бұл экспрессивтілік металлогикалық құнмен төленеді: Линдстрем теоремасы бойынша, тығыздық теоремасы және төменгі Лёвенхайм-Сколем теоремасы бірінші реттік логикадан күштірек ешқандай логикада сақталмайды.
Табиғи тілдерді ресмилендіру
Бірінші реттік логика табиғи тілдегі көптеген қарапайым квантификаторлық құрылымдарды, мысалы, "Пертте тұратын әр адам Австралияда тұрады" деген сияқты формальдастыруға қабілетті. Сондықтан, бірінші реттік логика FO(.) сияқты білімді ұсыну тілдерінің негізі ретінде қолданылады. Дегенмен, табиғи тілдің бірінші реттік логикамен өрнектеуге болмайтын күрделі ерекшеліктері бар. "Табиғи тілді талдау құралы ретінде қолданылатын кез келген логикалық жүйе бірінші реттік предикаттық логикадан әлдеқайда бай құрылымды қажет етеді".
Түрі Мысал Түсіндірме
Қасиеттер бойынша квантификация Егер Джон өзін-өзі қанағаттандырса, онда оның Петірмен кем дегенде бір ортақ нәрсесі бар. Мысал предикаттар бойынша квантификацияны талап етеді, оны бір реттік бірінші реттік логикада іске асыру мүмкін емес:
Қасиеттер бойынша квантификация Санта-Клаус садисттің барлық қасиеттеріне ие. Мысал предикаттар бойынша квантификацияны талап етеді, оны бір реттік бірінші реттік логикада іске асыру мүмкін емес:
Предикаттық сөз тіркесі Джон жылдам жүріп жатыр. Мысал түс сияқты екінші реттік предикаттар сияқты емес, сондықтан оны осылай талдауға болмайды.
Салыстырмалы сын есім Жумбо кішкентай піл. Мысал түс сияқты екінші реттік предикаттар сияқты емес, сондықтан оны осылай талдауға болмайды.
Предикаттық сөз тіркесін өзгертуші Джон өте жылдам жүріп жатыр.
Салыстырмалы сын есімді өзгертуші Жумбо өте кішкентай. "Өте" сияқты сөз "кішкентай" сияқты салыстырмалы сын есімге қолданылғанда, "өте кішкентай" сияқты жаңа құрама салыстырмалы сын есім пайда болады.
Алдын ала сөздер Мэри Джонның қасында отыр. "Жоханның" жанына "қасында" деген сөз тіркесін қолданғанда, "Жоханның қасында" деген предикаттық сөз тіркесі пайда болады.
Шектеулер, кеңейтулер және өзгерістер
Бірінші реттік логиканың көптеген нұсқалары бар. Олардың кейбіреулері маңызды емес, себебі олар тек белгілеуді өзгертеді, бірақ мағынасын өзгерте алмайды. Ал енді басқалары семантиканы қосымша кванторлар немесе басқа жаңа логикалық символдар арқылы кеңейту арқылы өрнектеу мүмкіндігін айтарлықтай өзгертеді. Мысалы, шексіз логикалар шексіз өлшемдегі формулаларға рұқсат береді, ал модальдық логикалар мүмкіндік және қажеттілік үшін символдарды қосады.
Көп сұрыпталатын логика
Кәдімгі бірінші реттік интерпретациялардың барлық кванторлары бір ғана сөздік доменде қолданылады. Көп сортты бірінші реттік логика айнымалыларға әртүрлі домендері бар әртүрлі сорттарға ие болуға мүмкіндік береді. Бұл сондай-ақ типтелген бірінші реттік логика деп аталады, мұнда сорттар типтер деп аталады (мысалы, дерек типі), бірақ ол бірінші реттік типтер теориясымен бірдей емес. Көп сортты бірінші реттік логика екінші реттік арифметиканы зерттеуде жиі қолданылады. Егер теорияда тек шектеулі түрлер болса, көп сортты бірінші реттік логиканы бір сортты бірінші реттік логикаға дейін келтіруге болады. Бір сортты теорияға әр сорт үшін бірлік предикаттық символ енгізіледі және бұл бірлік предикаттар сөздік доменді бөледі деген аксиома қосылады. Мысалы, егер екі сорт болса, онда предикаттық символдар мен аксиома қосылады: . Онда -ны қанағаттандыратын элементтер бірінші сорттың элементтері ретінде, ал -ны қанағаттандыратын элементтер екінші сорттың элементтері ретінде қарастырылады. Әр сорт бойынша квантификациялау үшін тиісті предикаттық символ қолданылып, квантификацияның ауқымы шектеледі. Мысалы, φ(x) формуласын қанағаттандыратын бірінші сорттың элементі бар екенін айту үшін былай жазады: .
.
Қосымша сандық белгілер
Бірінші реттік логикаға қосымша сандық белгілерді қосуға болады. Кейде "P(x) дәл бір x үшін орындалады" деу пайдалы, оны ∃!x P(x) деп көрсетеді. Бұл белгі, бірегейлік сандық белгілеуі деп аталады, мысалы, 1=∃x (P(x) ∧∀y (P(y) → (x = y))) сияқты формуланың қысқартылған түрі ретінде қарастырылуы мүмкін. Қосымша сандық белгілері бар бірінші реттік логикада Qx сияқты жаңа сандық белгілер болады, олардың мағынасы "көптеген x бар, мұндай..." болып табылады. Сондай-ақ, Джордж Булос және басқалардың тармақталған сандық белгілері мен көптік сандық белгілерін қараңыз. Шектелген сандық белгілер жинақтар теориясы немесе арифметиканы зерттеуде жиі қолданылады.
Шексіз логика
Шексіз логика шексіз ұзын сөйлемдерге мүмкіндік береді. Мысалы, шексіз көп формулалардың біріктірілуіне немесе ажыратылуына, немесе шексіз көп айнымалыларға қатысты квантификацияға рұқсат етуге болады. Шексіз ұзын сөйлемдер математиканың, оның ішінде топология және модель теориясы салаларында кездеседі. Шексіз логика, шексіз ұзындықтағы формулаларға рұқсат беру үшін бірінші реттік логиканы кеңейтеді. Формулалардың шексіз болуының ең көп таралған жолы – шексіз біріктірулер мен ажыратулар арқылы. Дегенмен, функция және қатынас белгілерінің шексіз арлықтарына рұқсат беретін, немесе кванторлар шексіз көп айнымалыларды байланыстыра алатын, кеңейтілген қолтаңбаларды қабылдау да мүмкін. Шексіз формуланы шекті тізбек түрінде көрсету мүмкін болмағандықтан, формулаларды көрсетудің басқа тәсілін таңдау қажет; осы контекстегі әдеттегі тәсіл – ағаш. Осылайша, формулалар, негізінен, талданған тізбектермен емес, олардың талдау ағаштарымен сәйкестендіріледі. Ең көп зерттелген шексіз логикалар Lαβ деп белгіленеді, мұнда α және β әрқайсысы кардинал сандар немесе ∞ символы болып табылады. Осы белгілеуде, қалыпты бірінші реттік логика Lωω болып табылады. L∞ω логикасында формулаларды құрастыру кезінде кез келген біріктірулер немесе ажыратулар рұқсат етіледі және айнымалылардың шексіз қоры бар. Көбірек жалпылаған түрде, κ-дан кем компоненттері бар біріктірулер мен ажыратуларға рұқсат беретін логика Lκω деп аталады. Мысалы, Lω1ω санаулы біріктірулер мен ажыратуларға рұқсат береді. Lκω формуласындағы бос айнымалылар жиыны κ-дан кіші кез келген кардиналдылыққа ие болуы мүмкін, бірақ олардың тек шекті саны ғана формула басқа формуланың субформуласы ретінде пайда болғанда, кез келген квантордың қол жеткізілген аймағында болуы мүмкін. Басқа шексіз логикаларда, субформула шексіз көп квантордың қол жеткізілген аймағында болуы мүмкін. Мысалы, Lκ∞-да бір ғана жалпылама немесе барлық айнымалы кванторы бір мезгілде шексіз көп айнымалыларды байланыстыра алады. Сол сияқты, Lκλ логикасы λ-дан кем айнымалыларға қатысты бір мезгілде квантификациялауға, сондай-ақ κ-тан кіші өлшемдегі біріктірулер мен ажыратуларға мүмкіндік береді.
Классикалық емес және модальдық логикалар
Интуициялық бірінші реттік логика классикалық емес, интуициялық қорытынды шығаруды қолданады; мысалы, ¬¬φ φ-ға эквивалентті болуы міндетті емес және ¬ ∀x.φ жалпы жағдайда ∃x.¬φ-ға эквивалентті емес. Бірінші реттік модальдық логика бізге басқа мүмкін әлемдерді, сондай-ақ біз тұратын осы мүмкін болатын әлемді сипаттауға мүмкіндік береді. Кейбір нұсқаларында, мүмкін әлемдер жиыны адам қай мүмкін әлемде болғанына байланысты өзгереді. Модальдық логикада қосымша модальдық операторлар бар, олардың мағынасын шамамен былай сипаттауға болады, мысалы, "φ қажет" (барлық мүмкін әлемдерде шын) және "φ мүмкін" (кейбір мүмкін әлемдерде шын). Стандартты бірінші реттік логикада бізде бір домен бар, және әр предикатқа бір ғана мән беріледі. Бірінші реттік модальдық логикада әр мүмкін әлемге өз доменін тағайындайтын домен функциясы бар, сондықтан әр предикат тек осы мүмкін әлемдерге қатысты мән алады. Бұл бізге, мысалы, Алекс философ болған, бірақ математик болуы мүмкін еді, тіпті мүлдем болмауы мүмкін еді деген жағдайларды модельдеуге мүмкіндік береді. Бірінші мүмкін әлемде P(a) шын, екіншісінде P(a) жалған, ал үшінші мүмкін әлемде доменде a мүлдем жоқ. Бірінші реттік бұлыңғыр логикалар – классикалық үкімдік есептеудің орнына, үкімдік бұлыңғыр логиканың бірінші реттік кеңейтулері.
Фикстік нүкте логикасы
Фикстік нүкте логикасы оң операторлардың ең кіші тұрақты нүктелері бойынша жабылуды қосу арқылы бірінші реттік логиканы кеңейтеді.
Автоматтандырылған теоремаларды дәлелдеу және ресми әдістер
Автоматтандырылған теоремаларды дәлелдеу – математикалық теоремалардың туындыларын (формалды дәлелдемелерін) іздейтін және табатын компьютерлік бағдарламаларды әзірлеу. Туындыларды табу қиын, өйткені іздеу кеңістігі өте үлкен болуы мүмкін; теориялық тұрғыдан әрбір мүмкін туындыны толық іздеу мүмкін, бірақ математиканың көптеген маңызды жүйелері үшін есептеу жүргізу мүмкін емес. Сондықтан күрделі эвристикалық функциялар соқыр іздеуге қарағанда аз уақытта туынды табуға тырысу үшін жасалады. Автоматтандырылған дәлелдеуді тексеруге байланысты сала компьютерлік бағдарламаларды пайдаланып, адам жасаған дәлелдемелердің дұрыстығын тексеруге арналған. Күрделі автоматтандырылған теорема дәлелдеушілерден өзгеше, тексеру жүйелерінің дұрыстығын қолмен де, автоматтандырылған бағдарламалық қамтамасыз ету арқылы да тексеруге болатындай кішкентай болуы мүмкін. Дәлел тексерушінің осы растауы, "дұрыс" деп белгіленген кез келген туындының шынымен дұрыс екендігіне сенімділік беру үшін қажет. Кейбір дәлелдеушілер, мысалы, Metamath толық туындыны енгізуді талап етеді. Mizar және Isabelle сияқты басқалары жақсы форматталған дәлелдеу эскизін (ол әлі де өте ұзын және егжей-тегжейлі болуы мүмкін) қабылдап, жоғалған бөліктерді қарапайым дәлелдеу іздеулері арқылы немесе белгілі шешімдер процедураларын қолдану арқылы толықтырады: нәтижеде алынған туынды кішкентай ядролық "ядро" арқылы тексеріледі. Мұндай жүйелердің көпшілігі математиктердің интерактивті пайдалануы үшін көзделеді: олар дәлелдеуге көмектесушілер деп аталады. Олар сондай-ақ бірінші реттік логикадан күшті формальды логиканы, мысалы типтік теорияны қолдануы мүмкін. Бірінші реттік дедуктивті жүйедегі кез келген маңызды емес нәтиженің толық туындысын адам үшін жазу өте ұзаққа созылады, сондықтан нәтижелер көбінесе жеке туындылар құрастырылатын леммалар сериясы түрінде формальдастырылады. Автоматтандырылған теорема дәлелдеушілер компьютерлік ғылымда формальды тексеруді жүзеге асыру үшін де қолданылады. Бұл жағдайда теорема дәлелдеушілер бағдарламалардың және процессорлар сияқты аппараттардың дұрыстығын формальды сипаттамаға сәйкес тексеру үшін пайдаланылады. Мұндай талдау көп уақытты қажет ететіндіктен және қымбат болғандықтан, әдетте ақаулық адам немесе қаржылық салдарларға әкелетін жобалар үшін қолданылады. Модельді тексеру мәселесі үшін кіріс шекті құрылымының бірінші реттік формулаға сәйкес келетінін анықтау үшін тиімді алгоритмдер белгілі, сонымен қатар есептеу күрделілігінің шектері де бар: қараңыз.