ФОРМАЛНА СИСТЕМА ОТ ГЕНЦЕНОВ ТИП ЗА ИЗВЕЖДАНЕ НА ТЪЖДЕСТВЕНО ВЕРНИ ЗАТВОРЕНИ СЕКВЕНЦИИ

    Един широко използван метод за изграждане на математически дисциплини е тъй нареченият аксиоматичен метод. При този метод се фиксират предварително някакъв набор от понятия на изгражданата дисциплина (нейни първични понятия) и някакъв набор от твърдения на тази дисциплина (нейни аксиоми), а след това се разрешава в нея да се работи само с такива понятия, които в крайна сметка са дефинирани чрез първичните понятия, и само с такива твърдения, които не съдържат други понятия освен първични и дефинирани чрез тях и за които твърдения е показано по логически безупречен начин, че следват от аксиомите на дисциплината. Една от важните задачи на математическата логика е по-задълбоченото изясняване на същността и на възможностите на аксиоматичния метод. Съществена стъпка в тази насока е построяването и изследването на тъй наречени формални системи за извеждане в определени класове обекти на математическата логика (като важен пример за такъв клас обекти можем да посочим класа на тъждествено верните формули на предикатното смятане). Построяването на една такава система става като се посочва определен обозрим подклас на интересуващия ни клас от обекти (елементите на този подклас се наричат аксиоми на формалната система) и се дава обозрима съвкупност от правила (извеждащи правила на системата или, по-кратко  –  нейни правила), чрез които от едни елементи на разглеждания клас могат да се получават други. Когато е построена някоя система от този вид, естествено е да се изследва кои елементи на разглеждания клас могат да бъдат получени от аксиомите чрез прилагане на извеждащите правила.1 Такива елементи се наричат изводими в дадената формална система. Особен интерес представляват онези формални системи, в които са изводими всички елементи на разглеждания клас  –  формалните системи с това свойство се наричат пълни.

    Някои от често използваните формални системи за извеждане в класа на тъждествено верните формули на предикатното смятане са били по същество известни още през първите десетилетия на този век. Пълнотата на тези системи е доказана от Курт Гьодел (Kurt Gödel) през 1930 г.2 С оглед на определени технически удобства в днешно време се използват и формални системи, които вместо с формули работят с по-сложни обекти, наречени секвенции, за които също е дефинирано понятието тъждествена вярност. Формални системи за извеждане в класа на тъждествено верните секвенции на предикатното смятане са предложени през 1934 г. от Герхард Генцен (Gerhard Gentzen). Сега ще се запознаем накратко с една подобна система за класа на тъждествено верните затворени секвенции на предикатното смятане, която ще означим с G°.

    Ще предполагаме, че е дадена една сигнатура Σ, за която по-нататък ще се наложи да направим едно допълнително предположение. Секвенция в сигнатурата Σ ще наричаме всяка наредена двойка (Γ,Δ), където Γ и Δ са крайни множества от формули в тази сигнатура (по-нататък ще си мислим както обикновено, че сигнатурата е фиксирана, и най-често няма да я споменаваме изрично). Секвенцията (Γ,Δ) ще записваме във вида ΓстрелкаΔ (в литературата по-често се използва обикновена стрелка вместо стрелка, но при нас обикновената стрелка служи за означаване на импликация). Множествата Γ и Δ се наричат съответно предпоставка и заключение на секвенцията ΓстрелкаΔ. Една секвенция се нарича затворена, ако всички формули от нейната предпоставка и всички формули от нейното заключение са затворени. Една затворена секвенция се нарича тъждествено вярна, ако не съществува структура, в която всички формули от предпоставката на секвенцията са верни, а всички формули от нейното заключение са неверни (по аналогичен начин се дефинира тъждествена вярност и за произволна секвенция  –  в този случай думата „структура“ трябва да се замени с думата „конфигурация“).

    Установяването дали една затворена секвенция е тъждествено вярна и установяването дали една затворена формула е тъждествено вярна са задачи, които се свеждат една към друга. Очевидно една затворена формула θ е тъждествено вярна точно тогава, когато е тъждествено вярна секвенцията с празна предпоставка и със заключение {θ}. За да покажем, че имаме и обратното свеждане, да разгледаме произволна затворена секвенция ΓстрелкаΔ. Очевидно тази секвенция не е тъждествено вярна в случай, че и двете множества Γ и Δ са празни. Да означим с γ една формула, която е конюнкция на формулите от множеството Γ, в случай, че то не е празно, и да означим с δ една формула, която е дизюнкция на формулите от множеството Δ, в случай, че то не е празно. Лесно се вижда, че ако никое от множествата Γ и Δ не е празно, то секвенцията ΓстрелкаΔ е тъждествено вярна точно тогава, когато е тъждествено вярна затворената формула γ→δ. Още по-просто свеждане имаме в случаите, когато едното от множествата Γ и Δ е празно, а другото не е. Ако Γ е празно, а Δ не е, то ΓстрелкаΔ е тъждествено вярна точно тогава, когато е тъждествено вярна затворената формула δ. Ако Δ е празно, а Γ не е, то ΓстрелкаΔ е тъждествено вярна точно тогава, когато е тъждествено вярна затворената формула ¬γ.

    За да опишем формалната система G°, ще е нужно още да дефинираме кога една константа на сигнатурата Σ участва в дадена секвенция. За тази цел най-напред даваме индуктивна дефиниция, която на всеки терм τ съпоставя множество CONST(τ) на константите, участващи в него. Правим това, като положим CONST(τ) да бъде множеството с единствен елемент τ, когато τ е константа, празното множество, когато τ е променлива, и обединението на множествата CONST(τi), i=1,…,m, при τ=ω(τ1,…,τm), където m е положително цяло число, ω е m-местен функционален символ и τ1, …, τm са термове. След това за произволна формула θ дефинираме индуктивно множество CONST(θ) на константите, участващи в нея. За целта първо приемаме, че множеството CONST(θ) е празно, ако θ е нулместен предикатен символ, че то е обединението на множествата CONST(τi), i=1,…,m, при θ=π(τ1,…,τm), където m е положително цяло число, π е m-местен предикатен символ и τ1, …, τm са термове. Приемаме също, че множеството на константите се запазва без изменение при образуване на отрицание и при поставяне на квантор, докато при образуване на конюнкция и на дизюнкция на две формули множеството на константите, участващи в получената по този начин формула, е обединение на множеството на константите, участващи в първата формула, и множеството на константите, участващи във втората. След като по този начин сме дефинирали кога една константа участва в дадена формула, приемаме, че една константа участва в дадена секвенция точно тогава, когато тази константа участва в някоя формула от предпоставката на секвенцията или в някоя формула от нейното заключение.

    За аксиоми на системата G° обявяваме затворените секвенции, на които предпоставката и заключението имат поне една обща формула (т.е. секвенциите от вида Γ∪{θ}стрелкаΔ∪{θ}, където θ е затворена формула, а Γ и Δ са крайни множества от затворени формули). Извеждащите правила на G° ще представим чрез схеми, като всяка схема ще съдържа хоризонтална черта, под чертата ще бъдe посоченa секвенция, която може да се получи по това правило, a над чертата  –  секвенция или секвенции, от които може да се получи секвенцията, която е под чертата (вляво от чертата ще бъде дадено и условно означение на правилото). Буквите Γ и Δ в схемите ще означават крайни множества от формули, буквите θ, φ и ψ  –  формули, буквите ξ и τ  –  съответно променлива и затворен терм, буквата α  –  константа, която не участва в секвенцията под чертата на съответната схема. Ето въпросните схеми:

    (¬ стрелка)   
ΓстрелкаΔ∪{θ}
Γ∪{¬θ}стрелкаΔ
                        (стрелка ¬)   
Γ∪{θ}стрелкаΔ
ΓстрелкаΔ∪{¬θ}
 
    (& стрелка)   
Γ∪{φ,ψ}стрелкаΔ
Γ∪{φ&ψ}стрелкаΔ
                        (стрелка &)   
ΓстрелкаΔ∪{φ}    ΓстрелкаΔ∪{ψ}
ΓстрелкаΔ∪{φ&ψ}
 
    (∨ стрелка)   
Γ∪{φ}стрелкаΔ    Γ∪{ψ}стрелкаΔ
Γ∪{φ∨ψ}стрелкаΔ
                       (стрелка ∨)   
ΓстрелкаΔ∪{φ,ψ}
ΓстрелкаΔ∪{φ∨ψ}
 
    (∀ стрелка)   
Γ∪{[ξ/τ]θ}стрелкаΔ
Γ∪{∀ξθ}стрелкаΔ
                        (стрелка ∀)   
ΓстрелкаΔ∪{[ξ/α]θ}
ΓстрелкаΔ∪{∀ξθ}
 
    (∃ стрелка)   
Γ∪{[ξ/α]θ}стрелкаΔ
Γ∪{∃ξθ}стрелкаΔ
                        (стрелка ∃)   
ΓстрелкаΔ∪{[ξ/τ]θ}
ΓстрелкаΔ∪{∃ξθ}

(правилата, представени чрез схемите от лявата и от дясната колона, ще наричаме съответно правила за отрицание, конюнкция, дизюнкция, квантор за обшност и квантор за съществуване в предпоставката и в заключението).

    В съгласие с общите бележки, които направихме в началото, едма секвенция ще наричме изводима в G°, ако тя може да бъде получена от аксиоми на G° чрез някакъв (евентуално нулев) брой прилагания на правила на G°.

    Пример 1. Нека Γ и Δ са произволни крайни множества от затворени формули, а φ и ψ са произволни затворени формули. Ще покажем, че секвенцията

Γ∪{φ&ψ}стрелкаΔ∪{ψ&φ}
е изводима от G°. За целта първо отбелязваме, че следните две секвенции са аксиоми на G°:
Γ∪{φ,ψ}стрелкаΔ∪{ψ},    Γ∪{φ,ψ}стрелкаΔ∪{φ}.
От тях по правилото (стрелка &) получаваме секвенцията
Γ∪{φ,ψ}стрелкаΔ∪{ψ&φ}
и накрая към нея прилагаме правилото (& стрелка).

    Пример 2. Нека p е двуместен предикатен символ на сигнатурата Σ, а α1 и α2 са две различни нейни константи. Нека Γ и Δ са крайни множества от затворени формули, в които не участва никоя от константите α1 и α2. Ще покажем, че секвенцията

ΓстрелкаΔ∪{∀x∀y(p(x,y)∨¬p(x,y))}
е изводима от G°. За целта първо отбелязваме, че секвенцията
Γ∪{p(α1,α2)}стрелкаΔ∪{p(α1,α2)}
е аксиома на G°. От нея чрез прилагане на правилата (стрелка ¬), (стрелка ∨) и (стрелка ∀) получаваме последователно секвенциите
ΓстрелкаΔ∪{p(α1,α2),¬p(α1,α2)},
ΓстрелкаΔ∪{p(α1,α2)∨¬p(α1,α2)},
ΓстрелкаΔ∪{∀y(p(α1,y)∨¬p(α1,y))}.
Още едно прилагане на правилото (стрелка ∀) дава желания резултат.

    Поради изискването τ да бъде затворен терм и α да бъде константа последните четири от правилата на системата G° (тези, които се отнасят за кванторите) са неизползваеми в случаите, когато сигнатурата Σ няма нито една константа. В тези случаи (с изключение на онези от тях, когато Σ няма и предикатни символи и поради това не съществуват формули в сигнатура Σ) лесно могат да се посочат затворени секвенции, които са тъждествено верни, но не са изводими в G°. Например, ако Γ е празно, а Δ има за единствен елемент някоя тъждествено вярна затворена формула, започваща с квантор за общност, то ΓстрелкаΔ е тъждествено вярна затворена секвенция, която не е аксиома на G° и не може да бъде получена по никое правило на G°, различно от (стрелка ∀), следователно тя не е изводима в G°, когато въпросното правило е неизползваемо. Ясно е, че за добрата използваемост на системата G° е необходимо сигнатурата Σ да има поне една константа. Това условие обаче не е достатъчно. Нека например Σ има двуместен предикатен символ p и единствена константа a. Тогава

∅стрелка{∀x∀y(p(x,y)∨¬p(x,y))}
е тъждествено вярна затворена секвенция, която не е аксиома на G°, а единственият начин тя да бъде получена по някое правило на G° е прилагане на правилото (стрелка ∀) към секвенцията
∅стрелка{∀y(p(a,y)∨¬p(a,y))}.
Тази секвенция, която също не е аксиома на G°, не може обаче да бъде получена по никое от правилата на G°  –  по правилата, различни от (стрелка ∀), очевидно не може, но не може и по него, тъй като не съществува константа на Σ, неучастваща в секвенцията. За да се окаже последната секвенция изводима в G°, необходимо би било сигнатурата Σ да има поне още една константа. Както се вижда от пример 2, за конкретната секвенция, която току-що разглеждахме, това би било и достатъчно, но, модифицирайки я по подходящ начин, лесно се убеждаваме, че в общия случай никакъв фиксиран краен брой константи в Σ не може да осигури изводимостта в G° на всяка тъждествено вярна затворена секвенция. За пълноценното използване на системата G° е нужно сигнатурата Σ да има безбройно много константи.

    Независимо от това коя е сигнатурата Σ и колко са нейните константи в сила е следното твърдение.

    Теорема за коректност на системата G°. Всички секвенции, изводими от G°, са затворени и тъждествено верни.

    Доказателство. Очевидно всяка от аксиомите на G° е тъждествено вярна затворена секвенция. При това положение е достатъчно да покажем, че при прилагане на правилата на G° към тъждествено верни затворени секвенции получените секвенции пак са затворени и тъждествено верни. Това, че при прилагането на тези правила към затворени секвенции се получават пак затворени секвенции, се вижда почти непосредствено (в случая на последните четири правила използваме, че ако при заместването на ξ в θ с τ или с α се получава затворена формула, то θ няма свободни променливи, различни от ξ).

    Като изключим последните четири от правилата на G°, проверката, че при прилагането на правилата към тъждествено верни затворени секвенции се запазва и тъждествената вярност, се свежда до използване на нужните дефиниции. Например да предположим, че за дадени крайни множества Γ и Δ от формули и дадени формули φ и ψ двете секвенции над чертата в правилото (стрелка &) са затворени и тъждествено верни, и да допуснем, че при някой избор на структура S всички формули от предпоставката на секвенцията под чертата са верни в S, а всички формули от заключението на тази секвенция са неверни в S. Тогава всички формули от множеството Γ са верни в S, а всички формули от множеството Δ както и формулата φ&ψ са неверни в S. В такъв случай обаче поради тъждествената вярност на двете секвенции над чертата не е възможно някоя от формулите φ и ψ да бъде невярна в S. Значи допускането ни относно S ни доведе до противоречие със семантиката на конюнкцията.

    Не са трудни разсъжденията и за случаите на правилата (∀ стрелка) и (стрелка ∃). Да предположим например, че за дадени крайни множества Γ и Δ от формули, дадена формула θ, дадена променлива ξ и даден затворен терм τ е затворена и тъждествено вярна секвенцията над чертата в правилото (∀ стрелка), и да допуснем, че при някой избор на структура S всички формули от предпоставката на секвенцията под чертата са верни в S, а всички формули от заключението на тази секвенция са неверни в S. Тогава всички формули от множеството Γ както и формулата ∀ξθ са верни в S, а всички формули от множеството Δ са неверни в S. Знаем обаче, че от формулата ∀ξθ следва всеки резултат от заместване на ξ в θ с терм. Това дава, че в секвенцията над чертата всички формули от предпоставката са верни в S, а всички от заключението са неверни в S  –  в противоречие с предположената тъждествена вярност на тази секвенция. По-подобен начин се постъпва и за правилото (стрелка ∃)  –  използва се, че формулата ∃ξθ следва от всеки резултат от заместване на ξ в θ с терм.

    Остава да се занимаем с правилата (стрелка ∀) и (∃ стрелка). Това ще направим с помощта на едно помощно твърдение, чийто смисъл, грубо казано, е това, че верността и неверността на една формула не зависят от интерпретацията на константите, неучастваши в тази формула. То е следното: ако са дадени една затворена формула θ, една константа α, неучастваща в θ, и две структури с един и същ носител, на които интерпретиращите съответствия съвпадат за всички функционални символи, различни от α, и за всички предикатни символи, то стойността на θ в двете структури е една и съща (за да не разкъсваме изложението, доказателството на това твърдение ще отложим за накрая). Ето как с помощта на току-що изказаното помощно твърдение можем да разгледаме например случая на правилото (стрелка ∀), Да предположим, че за дадени крайни множества Γ и Δ от формули, дадена формула θ, дадена променлива ξ и дадена константа α, неучастваща в секвенцията под чертата, секвенцията над нея е затворена и тъждествено вярна. Да допуснем, че при някой избор на структура S=(Σ,C,I) всички формули от предпоставката на секвенцията под чертата са верни в S, а всички формули от заключението на тази секвенция са неверни в S. Тогава всички формули от Γ са верни в S, а всички формули от Δ както и формулата ∀ξθ са неверни в S. Да означим с v някоя оценка на променливите в S. Поради неверността на формулата ∀ξθ в S, съществува такъв елемент c на C, че θ не е вярна в S при оценката v[ξ→c]. Разглеждаме нова структура S′=(Σ,C,I′), където I′ съпоставя на α елемента c и съвпада с I за всички други функционални символи и за всички предикатни символи. Помощното твърдение позволява да заключим, че и в структурата S′ всички формули от Γ са верни, а всички формули от Δ са неверни. Имаме равенствата

([ξ/α]θ)S′ = ([ξ/α]θ)S′,v = θS′,[ξ/α]S′(v) = θS′,v[ξ→c] = θS,v[ξ→c] = 0, 
като предпоследното от тях пак се основава на помощното твърдение. От тях виждаме, че и формулата [ξ/α]θ е невярна в структурата S′, а това противоречи на тъждествената вярност на секвенцията над чертата. По подобен начин се разглежда и случаят на правилото (∃ стрелка).

    За да завършим доказателството на теоремата, трябва да докажем и използваното помощно твърдение. Да предположим, че са дадени една константа α на сигнатурата Σ и две структури S и S′ с тази сигнатура, които имат един и същ носител и са с интерпретиращи съответствия, съвпадащи за всички функционални символи, различни от α, и за всички предикатни символи. Тогава лесно е да се докаже индуктивно, че за всеки терм τ е в сила следното условно твърдение: ако константата α не участва в τ, то при всяка оценка v на променливите в S имаме равенството τS,v=τS′,v. След като се направи това, не е трудно да се докаже индуктивно аналогично твърдение и за формули: ако константата α не участва в дадена формула θ, то при всяка оценка v на променливите в S имаме равенството θS,v=θS′,v. Използваното помощно твърдение отговаря на частния случай, когато формулата θ е затворена.  □

    Както вече видяхме, не винаги е вярно обратното твърдение на доказаната теорема, т.е. твърдението, че всяка тъждествено вярна затворена секвенция е изводима в системата G°. За сигнатури, които имат безбройно много константи, то обаче е вярно и значи в случая на такава сигнатура системата G° е една пълна система за извеждане на тъждествено верни затворени секвенции.

 

Бележки
    1 Без ограничения относно броя на прилаганията  –  той може да бъде произволно естествено число (включително и нула).

    2 Гьодел е особено известен с един друг свой резултат, който пак се отнася до въпрос за пълнота на формални системи, обаче е отрицателен. Това е прочутата Гьоделова теорема за непълнота, според която (при определени естествени уточнявания на понятията) не е възможна например пълна формална система за извеждане в класа на формулите на предикатното смятане, тъждествено верни в дадена достатъчно богата структура с носител множеството на естествените числа.

  Последно изменение: 14.02.2008 г.