Previous | Next | Contents |
Закон за въвеждане на квантор за общност в предпоставката. Нека G и D са крайни множества от формули, x е променлива, j е формула, а t е такъв терм, че субституцията (x:=t) е приложима към j. Тогава, ако секвенцията
Доказателство. Знаем, че формулата (x:=t)(j) следва от формулата "xj. Да предположим сега, че секвенцията GИ{(x:=t)(j)}-:D е вярна в дадена конфигурация (S,v), и да допуснем, че секвенцията GИ{"xj}-:D не е вярна в (S,v). Тогава всички формули от множеството GИ{"xj} ще бъдат верни в (S,v), а всички формули от множеството D ще бъдат неверни в (S,v). Като използваме отбелязаното преди малко следване, оттук получаваме, че всички формули от множеството GИ{(x:=t)(j)} са верни в конфигурацията (S,v), а всички формули от множеството D са неверни в нея. Това обаче противоречи на верността на секвенцията GИ{(x:=t)(j)}-:D в (S,v).
Закон за квантор за общност в предпоставката. Нека G и D са крайни множества от формули, x е променлива, j е формула, а t е такъв терм, че субституцията (x:=t) е приложима към j. Тогава, за да бъде секвенцията
Разбира се, всяко от горните две твърдения остава в сила, ако вместо вярност на секвенциите в дадена конфигурация се разглежда тяхната тъждествена вярност в дадена структура. В твърдението, което сега ще изкажем, направо ще става дума за тъждествена вярност в дадена структура. За по-удобното изказване на това и на някои други твърдения се уславяме да казваме за една променлива h, че е свободна променлива на дадена секвенция, ако h е свободна променлива на някоя формула, принадлежаща на предпоставката или на заключението на секвенцията; по аналогичен начин, макар засега това не ни е нужно, дефинираме кога една променлива е свързана променлива на дадена секвенция.
Закон за квантор за общност в заключението. Нека G и D са крайни множества от формули, x е променлива, j е формула, а h е такава променлива, че субституцията (x:=h) е приложима към j. Нека освен това h не е свободна променлива на секвенцията
Законите, отнасящи се до квантор за съществуване, са аналогични на горните, като обаче се отличават от тях по това, че се разменят ролите в тях на предпоставката и заключението. Само ще формулираме тези закони, защото доказателствата им са аналогични на изложените по-горе.
Закон за въвеждане на квантор за съществуване в заключението. Нека G и D са крайни множества от формули, x е променлива, j е формула, а t е такъв терм, че субституцията (x:=t) е приложима към j. Тогава, ако секвенцията
Закон за квантор за съществуване в заключението. Нека G и D са крайни множества от формули, x е променлива, j е формула, а t е такъв терм, че субституцията (x:=t) е приложима към j. Тогава, за да бъде секвенцията
Закон за квантор за съществуване в предпоставката. Нека G и D са крайни множества от формули, x е променлива, j е формула, а h е такава променлива, че субституцията (x:=h) е приложима към j. Нека освен това h не е свободна променлива на секвенцията
Навсякъде в отбелязаните тук закони за квантори в секвенции би могло вместо за вярност в конфигурация или за тъждествена вярност в структура да се говори просто за тъждествена вярност. Поради това въпросните закони и споменатите в началото други закони, отнасящи се до съждителни операции в секвенции, могат да служат за установяване на тъждествена вярност на някои секвенции (разбира се за целта бихме могли да използваме и изучените преди това други методи, като заменим интересуващите ни секвенции с еквивалентни на тях формули).
Бележка
1 Виждаме даже, че ако първата от двете секвенции е вярна в S при дадена
оценка на променливите, то втората е вярна в S при същата оценка на променливите; при това в тази част от разсъжденията не се използва предположението h да не е свободна променлива на първата секвенция.
Последно изменение: 9.01.2001 г.
Previous | Next | Contents |