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

    Някои от често използваните формални системи за извеждане в класа на тъждествено верните формули на предикатното смятане са били по същество известни още през първите десетилетия на този век. Пълнотата на тези системи е доказана от Курт Гьодел през 1930 г.² Формални системи за извеждане в класа на тъждествено верните секвенции на предикатното смятане са предложени през 1934 г. от Генцен и ние сега ще се запознаем съвсем накратко с една такава система.

    Предполагайки, че е даден някой език на предикатното смятане, ще разгледаме формална система G, чиито извеждащи правила отговарят на законите за различните логически операции в предпоставката и в заключението. Аксиоми на G ще бъдат секвенциите, на които предпоставката и заключението имат обща формула (знаем, че всички такива секвенции са тъждествено верни). Извеждащите правила на G ще представим чрез схеми, като всяка схема ще съдържа хоризонтална черта, под чертата и над чертата ще бъдат посочени съответно секвенция, която може да се получи по това правило, и секвенция или секвенции, от които може да се получи тя, а вляво от чертата ще бъде дадено условно означение на правилото (словесните наименования на правилата ще бъдат същите както на съответните закони с тази разлика, че вместо думата "закон" сега ще имаме думата "правило" - например правилото (Ш -:) ще наричаме правило за отрицание в предпоставката). Буквите G и D в схемите ще означават крайни множества от формули, буквите j и y - формули, буквите x и h - променливи, буквата t - терм (за последните четири правила накрая ще бъдат написани и допълнителни условия, които се изискват, за да са приложими тези правила). Системата G ще има следните 10 извеждащи правила:

(при правилата (" -:) и (-: $) се изисква субституцията (x:=t) да бъде приложима към j, а при правилата ($ -:) и (-: ") - h да не е свободна променлива на секвенцията под чертата и субституцията (x:=h) да е приложима към j).

    Както може да се види от някои примери, фактическото получаване на една секвенция от аксиоми на G с помощта на правила на G може да изглежда доста различно от обичайните математически доказателства. С цел да се постигне по-голяма близост с обичайните доказателства предложени са някои по-подходящи в това отношение формални системи, които за разлика от G са системи за извеждане в по-тесен клас от тъждествено верни секвенции - в класа на онези от тях, на които заключението съдържа най-много формула. Ще опишем една такава система, която ще означим с Gў.

    Системата Gў ще има за аксиоми всички секвенции от следните видове, където j и y са формули, x е променлива и t е такъв терм, че субституцията (x:=t) е приложима към j:

Правила за извеждане на Gў ще бъдат някои частни случаи на правила на G (изброени по-надолу) и следните три правила, където c е формула, G и Gў са крайни множества от формули, D е празното множество или множество от една формула:

(правила за разширяване)	G-:D ѕѕѕѕѕѕ GИ{c}-:D		G-: ѕѕѕѕ G-:c
(правило за сечение)	GИ{c}-:D    Gў-:c ѕѕѕѕѕѕѕѕѕѕ GИGў-:D

Споменатите преди малко частни случаи на правила на G са случаите с празно D на правилата (Ш -:), (-: Ш), (-: &), (-: ") и случаите с празно или едноелементно D на правилата (Ъ -:), ($ -:). Ще означаваме тези частни случаи с (-: Ш)ў, (-: &)ў и т.н.

    Може да се докаже, че системата Gў е пълна, а системата G е, тъй да се каже, почти пълна - в нея са изводими поне онези тъждествено верни секвенции, за които никоя променлива не е едновременно тяхна свободна и тяхна свързана променлива.

    Две от правилата на системата G - правилата (-: Ъ) и (-: $) очевидно не са подходящи за системата Gў, защото дори и при празно D първото от тях използва секвенция с повече от една формула в заключението винаги освен само в специалния случай, когато j=y, а второто използва такава секвенция винаги без изключение. Останалите правила на G, частни случаи на които не бяха включени в Gў, са правилата (& -:) и (" -:). Ще покажем, че съответните им частни случаи могат все пак да се използват в Gў (това, както и други по-нататъшни твърдения, следва и от споменатата пълнота на Gў, но тя трудно би могла да се докаже, без да се докажат предварително подобни свойства на изводимостта в Gў).

    Лема за допустимост на правило (& -:)ў в системата Gў. Нека j и y са формули, G е крайно множество от формули, D е празното множество или е множество от една формула. Тогава ако секвенцията GИ{j,y}-:D е изводима в системата Gў, то и секвенцията GИ{j&y}-:D е изводима в Gў.

    Доказателство. От секвенцията GИ{j,y}-:D и аксиомата j&y-:j на Gў по правилото за сечение се получава секвенцията GИ{y,j&y}-:D, а от нея и аксиомата j&y-:y на Gў пак по правилото за сечение - секвенцията GИ{j&y}-:D.

    Лема за допустимост на правило (" -:)ў в системата Gў. Нека j е формула, x е променлива, t е такъв терм, че субституцията (x:=t) е приложима към j, G е крайно множество от формули, D е празното множество или е множество от една формула. Тогава ако секвенцията GИ{"xj,(x:=t)(j)}-:D е изводима в системата Gў, то и секвенцията GИ{"xj}-:D е изводима в Gў.

    Доказателство. Втората секвенция може да бъде получена от първата и от аксиомата "xj-:(x:=t)(j) на Gў по правилото за сечение.

    В сила е още следното твърдение:

    Лема за изводимост в Gў на някои аксиоми на G. Онези от аксиомите на G, на които заключенията са от по една формула, са изводими в системата Gў.

    Доказателство. Всяка от тези аксиоми може да се получи от секвенция от вида j-:j чрез известен брой прилагания на първото правило за разширяване.

    Горните три леми понякога са достатъчни дадено конкретно установяване на изводимост в системата G да може да се използва за установяване на изводимост и в системата Gў. В други случаи е полезна и следната лема.

    Лема за допустимост на контрапозиция в системата Gў. Нека G е крайно множество от формули, j и y са формули и секвенцията GИ{j}-:y е изводима в Gў. Тогава секвенцията GИ{Шy}-:Шj също е изводима в Gў.

    Доказателство. Втората секвенция може да се получи от първата чрез последователно прилагане на правилата (Ш -:)ў и (-: Ш)ў.

    С помощта на доказаните леми ще докажем следната обща теорема.

    Теорема за запазване на изводимост при преминаване от G към Gў. Ако една секвенция G-:D е изводима в системата G и множеството D има не повече от един елемент, тази секвенция е изводима и в системата Gў.

    Доказателство. За кое да е крайно множество от формули D да означим с ШD множеството на формулите от вида Шj, където jОD. Да наречем превод на произволна секвенция G-:D съответната секвенция GИШD-:. Очевидно преводът на секвенция с празно заключение съвпада със самата нея, а за произволна секвенция G-:j, имаща едноелементно заключение, нейният превод е GИ{Шj}-:. Поради това, за да докажем теоремата, достатъчно е да докажем следните две помощни твърдения: а) преводът на всяка секвенция, изводима в G, е изводим в Gў; б) ако за дадено крайно множество от формули G и дадена формула j секвенцията GИ{Шj}-: е изводима в Gў, то секвенцията G-:j също е изводима в Gў. Помощното твърдение б) се доказва, като се забележи, че от секвенцията GИ{Шj}-: по правилото (-: Ш)ў се получава секвенцията G-:ШШj, а от аксиомата ШШj-:j на Gў и последната секвенция по правилото за сечение се получава секвенцията G-:j. За да докажем помощното твърдение а), да наречем легитимни онези секвенции, изводими в G, на които преводите са изводими в Gў. Тогава твърдението а) може да бъде изказано като твърдение, че всички секвенции, изводими в G, са легитимни. Ще го докажем, като покажем, че всички аксиоми на G са легитимни и че при прилагане на правилата на G към легитимни секвенции получените секвенции винаги са пак легитимни. Очевидно преводът на коя да е аксиома на G е секвенция от вида BИ{j,Шj}-:, където B е крайно множество от формули, а j е формула. Такава секвенция е изводима в Gў, защото може да се получи по правилото (Ш -:)ў от секвенцията BИ{j}-:j, която от своя страна е изводима в Gў според лемата за изводимост в Gў на някои аксиоми на G. Остава за всички правила на системата G да покажем, че прилагането им към легитимни секвенции дава пак легитимни секвенции. За целта ще разгледаме поотделно всяко от правилата.

    (Ш -:)  Нека G -:DИ{j} е легитимна секвенция. Неин превод е секвенцията GИШDИ{Шj}-: и значи последната е изводима в Gў. Очевидно обаче секвенцията GИ{Шj}-:D има същия превод. Следователно и тя е легитимна.

    (-: Ш)  Нека GИ{j}-:D е легитимна секвенция. Тогава секвенцията GИ{j}ИШD-: е изводима в Gў. Трябва да докажем, че е легитимна и секвенцията G-:DИ{Шj}, което ще означава в Gў да бъде изводима секвенцията GИШDИ{ШШj}-:. Това условие е изпълнено, защото последната секвенция може да се получи от GИ{j}ИШD-: чрез последователно прилагане на правилото (-: Ш)ў и правилото (Ш -:)ў.

    (& -:)  Нека GИ{j,y}-:D е легитимна секвенция. Тогава GИ{j,y}ИШD-: е секвенция, изводима в Gў. Лемата за допустимост на правило (& -:)ў в системата Gў позволява оттук да заключим, че е изводима в Gў и секвенцията GИ{j&y}ИШD-:. Тя обаче е превод на секвенцията GИ{j&y}-:D, значи последната е също легитимна.

    (-: &)  Нека G-:DИ{j} и G-:DИ{y} са легитимни секвенции. Тогава секвенциите GИШDИ{Шj}-: и GИШDИ{Шy}-: са изводими в Gў. Помощното твърдение б), което вече доказахме, позволява оттук да заключим, че в Gў са изводими и секвенциите GИШD-:j и GИШD-:y. От тях обаче чрез последователно прилагане на правилата (-: &)ў и (Ш -:)ў се получава секвенцията GИШDИ{Ш(j&y)}-: и значи тя също е изводима в Gў. Следователно секвенцията G-:DИ{j&y} е легитимна.

    (Ъ -:)  Нека GИ{j}-:D и GИ{y}-:D са легитимни секвенции. Тогава секвенциите GИ{j}ИШD- и GИ{y}ИШD-: са изводими в Gў. От тях по правилото (Ъ -:) се получава секвенцията GИ{jЪy}ИШD-:, която значи също е изводима в Gў. Следователно секвенцията GИ{jЪy}-:D е легитимна.

    (-: Ъ)  Нека G-:DИ{j,y} е легитимна секвенция. Тогава в Gў е изводима секвенцията GИШDИ{Шj,Шy}-:. Като вземем предвид лемата за допустимост на контрапозиция в Gў и обстоятелството, че j-:jЪy и y-:jЪy са аксиоми на Gў, виждаме, че в Gў са изводими секвенциите Ш(jЪy)-:Шj и Ш(jЪy)-:Шy. От тях и секвенцията GИШDИ{Шj,Шy}-: чрез двукратно прилагане на правилото за сечение се получава секвенцията GИШDИ{Ш(jЪy)}-:. Значи секвенцията G-:DИ{jЪy} е легитимна.

    (" -:)  Нека при предположенията, при които може да се прилага това правило, секвенцията GИ{"xj,(x:=t)(j)}-:D е легитимна. Тогава съответната секвенция GИ{"xj,(x:=t)(j)}ИШD-: е изводима в Gў. Оттук по лемата за допустимост на правило (" -:)ў в системата Gў получаваме, че в Gў е изводима и секвенцията GИ{"xj}ИШD-:. Следователно секвенцията GИ{"xj}-:D е легитимна.

    (-: ")  Нека при предположенията, при които може да се прилага това правило, секвенцията G-:DИ{(x:=h)(j)} е легитимна. Тогава в Gў е изводима секвенцията GИШDИ{Ш(x:=h)(j)}-:. Помощното твърдение б) позволява оттук да заключим, че и секвенцията GИШD-:(x:=h)(j) е изводима в Gў. От нея с последователно прилагане на правилата (-: ") и (Ш -:) можем да получим секвенцията GИШDИ{Ш"xj}-: и значи секвенцията G-:DИ{"xj} е легитимна.

    ($ -:)  Нека при предположенията, при които може да се прилага това правило, секвенцията GИ{(x:=h)(j)}-:D е легитимна. Тогава в Gў е изводима секвенцията GИ{(x:=h)(j)}ИШD-:. От нея обаче по правилото ($ -:)ў се получава секвенцията GИ{$xj}ИШD-: и значи секвенцията GИ{$xj}-:D е легитимна.

    (-: $)  Нека при предположенията, при които може да се прилага това правило, секвенцията G-:DИ{$xj,(x:=t)(j)} е легитимна. Тогава в Gў е изводима секвенцията GИШDИ{Ш$xj,Ш(x:=t)(j)}-:. От лемата за допустимост на контрапозиция в Gў и обстоятелството, че (x:=t)(j)-:$xj е аксиома на Gў, се получава, че секвенцията Ш$xj-:Ш(x:=t)(j) е изводима в Gў. С прилагане на правилото за сечение към споменатите две секвенции, изводими в Gў, можем да получим секвенцията GИШDИ{Ш$xj}-:. Значи секвенцията G-:DИ{$xj} е легитимна.

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

Previous

Contents