Когато F и G са формули, казваме, че от F следва G, и пишем F ⊨ G, ако винаги, когато формулата F е вярна в дадена конфигурация, формулата G също е вярна в тази конфигурация. Т.е. приемаме, че F ⊨ G, ако не съществува конфигурация, в която формулата F да е вярна, а формулата G да не е вярна. Разбира се ще пишем F ⊭ G, за да изразим, че от F не следва G  (т.е. че съществува конфигурация, в която формулата F е вярна, а формулата G не е вярна). Лесно се съобразява, че съотношението F ⊨ G е налице точно тогава, когато за всяка конфигурация (S,v) е в сила неравенството F^S,v ≤ G^S,v. Ясно е, че ако формулите F и G са затворени, то навсякъде в гореказаното конфигурациите могат да се заменят със структури.

      Пример 1. Ако една формула е неизпълнима, от нея следва всяка формула, а ако дадена формула е тъждествено вярна, тя следва от всяка формула. Всяка формула, от която следва някоя неизпълнима формула, също е неизпълнима, а всяка формула, която следва от някоя тъждествено вярна формула, също е тъждествено вярна,

      Пример 2. За всяка n-ка от формули  F₁, …, F_n  са налице съотношенията

      Пример 3. Нека са дадени формули  F₁, …, F_n  и  G.  Ако  G ⊨ F_i  за  i=1,…,n,  то  G ⊨ F₁ & … & F_n,  а ако  F_i ⊨ G  за  i=1,…,n,  то  F₁ ∨ … ∨ F_n ⊨ G.

      Пример 4. За всяка формула F и всяка променлива ξ имаме съотношенията  ∀ξ F ⊨ F  и  F ⊨ ∃ξ F  (проверката се извършва лесно, като се използва обстоятелството, че за всяка конфигурация  (S,v)  имаме равенството  v = v[ξ→v(ξ)] ).

      Пример 5. Нека ξ и η са две различни променливи, а F е произволна формула. Ще покажем, че  ∃ξ ∀η F ⊨ ∀η ∃ξ F. Действително, нека формулата  ∃ξ ∀η F  е вярна в дадена конфигурация (S,v). Тогава съществува елемент x на носителя на S, такъв, че  S,v[ξ→x] ⊨ ∀η F и следователно  S, v[ξ→x][η→y] ⊨ F за всяко y от носителя на S. Тъй като обаче  v[ξ→x][η→y] = v[η→y][ξ→x],  това гарантира, че за всяко y от носителя на S е налице съотношението  S,v[η→y] ⊨ ∃ξ F  и значи  S,v ⊨ ∀η ∃ξ F.

      Пример 6. Нека ξ и η да са пак две различни променливи, но F да е формула от вида π(ξ,η), където π е двуместен предикатен символ. Тогава  ∀ξ ∃η F ⊭ ∃η ∀ξ F.  За да се убедим в това, достатъчно е да разгледаме например такава структура S с носител D, състоящ се от поне два елемента, че предикатът  π^S  да приема стойност 1 за двойките от D² с равни членове и стойност 0 за останалите двойки от D²  -  при такъв избор на S затворената формула  ∀ξ ∃η F  е вярна в S, а затворената формула  ∃η ∀ξ F  не е вярна в S.

      От дефиницията на отношението следване веднага се вижда, че това отношение е рефлексивно, т.е  F ⊨ F  за всяка формула F,  и е транзитивно, т.е. винаги, когато за три формули F, G и H имаме съотношенията  F ⊨ G  и  G ⊨ H,  имаме и съотношението  F ⊨ H.

      Ще отбележим още следните лесно проверими свойства (първото от тях се нарича закон за контрапозиция):
        1. Ако за две формули F и G имаме съотношението  F ⊨ G,  то за тях е налице и съотношението  ¬ G ⊨ ¬ F.
        2. Ако за две n-ки от формули   F₁, …, F_n  и  G₁, …, G_n  имаме съотношенията  F_i ⊨ G_i  при  i=1,…,n,  то са налице и съотношенията

      Ще казваме, че от едно множество от формули Γ следва дадена формула G, ако G е вярна във всяка конфигурация, с която са верни формулите от Γ, т.е. ако не съществува конфигурация, в която са верни формулите от Γ, а G не е вярна (разбира се, ако всички формули от Γ са затворени и формулата G също е затворена, то вместо с вярност в конфигурации можем да си служим с вярност в структури). Наличието на гореописаната семантична връзка между Γ и G ще записваме чрез означението  Γ ⊨ G,  а отсъствието й  -  чрез означението  Γ ⊭ G. Ясно е, че в случая, когато Γ се състои от точно една формула F, условието  Γ ⊨ G  е равносилно с условието   F ⊨ G,  а ако Γ е празно, то условието  Γ ⊨ G  е равносилно с изискването G да е тъждествено вярна. В сила е и следното обобщение на първото от тези твърдения: ако Γ е множеството на членовете на дадена конюнкция, то една формула следва от Γ точно тогава, когато следва от тази конюнкция.

      В края на предходния въпрос стана дума за това, че в логическото програмиране възникват някои задачи за изследване дали дадена формула е изпълнима във всеки модел на дадено множество от формули. Като заменим дадената формула с нейно екзистенциално затваряне, а формулите от даденото множество  -  с техни универсални затваряния, винаги можем да сведем този въпрос до въпрос дали дадена затворена формула следва от дадено множество от затворени формули.
 

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

Previous  Next  Contents