РАЗШИРЕНИЕ И СЕЧЕНИЕ НА СЕКВЕНЦИИ

    Ако са дадени три секвенции, ще казваме, че третата от тях е сечение на първата и втората, когато трите секвенции имат съответно вида

    Забележка. Когато са дадени две секвенции и формула j, която принадлежи на предпоставката на първата секвенция и на заключението на втората, то двете секвенции в общия случай имат повече от едно сечение по j (до четири на брой). Това е така, защото кое да е крайно множество Q от формули, съдържащо j, може да се представи по два различни начина във вида Q=QўИ{j}, където Qў е крайно множество от формули: при единия начин Qў=Q\{j}, а при другия Qў=Q. Очевидно всяко от сеченията на двете секвенции по j е разширение на онова, което се получава, когато използваме първия начин на представяне както за предпоставката на първата секвенция, така и за заключението на втората (при конкретни задачи най-често ще използваме именно това сечение). Разбира се, освен отбелязаната неединственост на сечението може да има и друга, дължаща се на наличието на повече от една обща формула в предпоставката на първата секвенция и в заключението на втората (лесно се съобразява, че в този случай всяко от сеченията на двете секвенции е тривиално тъждествено вярно).

    Следното твърдение показва, че верността на секвенциите се запазва при образуване на сечение.

    Лема за семантична коректност на сечението. Ако две секвенции са верни в дадена конфигурация, а трета секвенция е тяхно сечение, тя също е вярна в дадената конфигурация.

    Доказателство. Нека е дадена една конфигурация (S,v) и нека за дадени крайни множества от формули G₁, D₁, G₂, D₂ и дадена формула j двете секвенции G₁И{j}-:D₁ и G₂-:D₂И{j} са верни в (S,v). Ще покажем, че тогава и секвенцията G₁ИG₂-:D₁ИD₂ е вярна в (S,v). И наистина, верността на първата секвенция дава, че някоя формула от G₁ е невярна в (S,v) или j е невярна в (S,v) или някоя формула от D₁ е вярна в (S,v). Аналогично, верността на втората секвенция дава, че някоя формула от G₂ е невярна в (S,v) или някоя формула от D₂ е вярна в (S,v) или j е вярна в (S,v). По такъв начин възникват девет случая, които подлежат на разглеждане. Един от тях обаче е невъзможен, а именно не е възможно едновременно j да е невярна в (S,v) и j да е вярна в (S,v). От друга страна във всеки от останалите случаи някоя формула от G₁ИG₂ е невярна в (S,v) или някоя формула от D₁ИD₂ е вярна в (S,v), т.е. във всички възможни случаи секвенцията G₁ИG₂-:D₁ИD₂ се оказва вярна в (S,v).

    Можем да тълкуваме току-що доказаната лема като обосновка на една определена форма на умозаключение, която в общия си вид едва ли може да бъде срещната в някое реално срещащо се математическо разсъждение. Някои нейни частни случаи обаче съответстват на често използвани начини на разсъждаване. Ще отбележим няколко такива частни случаи.

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

    Ако G и D са крайни множества от формули и j е формула, то секвенциите j-:D и G-:j очевидно имат сечение G-:D. Този случай (и особено подслучаят, когато D се състои от една формула) също съответства на начин на разсъждение, използван в математиката (а и не само там).

    Когато е дадено едно множество M от секвенции, за една секвенция ще казваме, че е c-изводима от M, ако тя може да се получи от някои секвенции, принадлежащи на M, чрез някакъв брой прилагания на сечение (буквата "c" във въведения термин е избрана, понеже е първа буква на думаta "cut" - английската дума за "сечение"). За да следваме досегашния стил на изложение, можем да въведем същото понятие с помощта на следната индуктивна дефиниция:
    c-И1. Всяка секвенция, принадлежаща на M, е c-изводима от M.
    c-И2. Когато една секвенция е сечение на две секвенции, c-изводими от M, тя също е c-изводима от M.

    Благодарение на лемата за семантична коректност на сечението е ясно, че ако M е множество от секвенции и е дадена конфигурация, в която са верни всички секвенции от M, то в тази конфигурация са верни и всички секвенции, c-изводими от M. Тъй като празната секвенция не е вярна в никоя конфигурация, оттук може да се заключи, че ако от дадено множество от секвенции е c-изводима празната секвенция, то това множество е неизпълнимо.

    В съчетание с разглежданията от предходния въпрос заключението, което току-що направихме, дава един формален метод за установяване на  неизпълнимост на безкванторни формули или множества от безкванторни формули. В какво се състои методът ще илюстрираме с един съвсем прост пример (в него неизпълнимостта е и непосредствено очевидна, но методът е приложим успешно и в значително по-сложни случаи). Примерът ще бъде с формулата a«Шa, където a е атомарна формула. В пример 5 от предходния въпрос видяхме, че тази формула е еквивалентна с множеството от двете елементарни секвенции a-: и -:a. Това, че множеството от тези две секвенции е неизпълнимо, а следователно и формулата a«Шa е неизпълнима, може да се види освен директно още и като се използва, че споменатите две секвенции имат за сечение празната секвенция. Ето и един по-интересен пример.

    Пример 1. Нека езикът на предикатното смятане, с който работим, има един нулместен функционален символ a, един едноместен функционален символ f и един двуместен предикатен символ і и нека сме се условили да пишем tіtў вместо і(t,tў). Нека трябва да се изследва дали е изпълнимо множеството от следните пет формули, където x, y и z са различни помежду си променливи:

    Едно множество от секвенции ще наричаме c-противоречиво, ако от него е c-изводима празната секвенция. Това, което видяхме преди малко и след това използвахме в примери, всъщност е фактът, че всяко c-противоречиво множество от секвенции е неизпълнимо. Обратното твърдение на последното би гласило, че ако едно множество от секвенции е неизпълнимо, то е c-противоречиво. В общия случай такова твърдение не е вярно и прост пример за това би могло да бъде множество, състоящо се от една секвенция от вида j-:, където j е тъждествено вярна формула. Скоро ще покажем обаче, че за множество от елементарни секвенции е вярно и въпросното обратно твърдение и то даже в малко по-силна форма. В тази по-силна форма ще използваме един малко по-ограничен вид сечения, които ще наричаме съществени.

    За две секвенции Gў-:Dў и GІ-:DІ ще казваме, че имат съществено сечение, ако са изпълнени следните изисквания за броя на общите формули в двойките от предпоставка и заключение на тези секвенции: множеството GўЗDІ се състои от точно една формула, а множествата GўЗDў, GІЗDў и GІЗDІ са празни. Ако споменатите две секвенции имат съществено сечение и общата формула на Gў и DІ е j, то под съществено сечение на двете секвенции ще разбираме секвенцията

    Пример 2. Секвенциите j-: и -:j, където j е дадена формула, имат съществено сечение и то е празната секвенция (други техни сечения са секвенциите j-:, -:j и j-:j).

    Ако една секвенция е съществено сечение на две дадени секвенции, то тя не е тривиално тъждествено вярна и не е разширение на никоя от двете. И наистина, при условията и означенията от горната дефиниция секвенцията (Gў\{j})ИGІ-:DўИ(DІ\{j}) не е тривиално тъждествено вярна, защото сечението на всяко от множествата Gў\{j} и GІ със всяко от множествата Dў и DІ\{j} е празно. При същите условия и означения тя не е разширение на секвенцията Gў-:Dў, защото формулата j принадлежи на Gў, но не принадлежи на (Gў\{j})ИGІ (в случай, че би принадлежала, тя би принадлежала и на сечението GІЗDІ). По подобен начин се вижда, че секвенцията (Gў\{j})ИGІ-:DўИ(DІ\{j}) не е разширение и на секвенцията GІ-:DІ.

    Лесно се доказва и обратното - ако една секвенция, която е сечение на две дадени секвенции, не е тривиално тъждествено вярна и не е разширение на никоя от двете, то тя е тяхно съществено сечение.

    За една секвенция ще казваме, че е ec-изводима от дадено множество от секвенции, ако тя може да се получи от секвенции, принадлежащи на това множество, чрез някакъв брой прилагания на съществено сечение ("ec" идва от "essential cut"). Разбира се естествено е и тази изводимост да дефинираме индуктивно подобно на c-изводимостта. Съответната дефиниция може да се получи от дефиницията за c-изводимост като навсякъде се замени 'c-" с "ec-".Няма да я изписваме в явен вид, но ще я използваме, когато потрябва. Понеже съществените сечения на секвенции са техни сечения, ясно е, че всяка секвенция, ec-изводима от дадено множество, е същевремено и c-изводима от него (обратното не е вярно, защото например секвенцията j-:j е c-изводима от множеството от двете секвенции j-: и -:j, но не е ec-изводима от него).

    За едно множество от секвенции ще казваме, че е ec-противоречиво, ако от него е ec-изводима празната секвенция. Казаното дотук показва, че всяко ec-противоречиво множество от секвенции е c-противоречиво и следователно е неизпълнимо.  Поради това формалният метод, за който стана дума преди малко, може да се използва и като се работи само със съществени сечения (обикновено това е за предпочитане).

 

Задачи

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