Един терм се нарича затворен, ако множеството на променливите му е празно (понякога затворените термове се наричат още основни). От тази дефиниция и дефиницията за множество на променливите на един терм следва, че константите са затворени термове, а променливите не са. Следва още такова твърдение: ако T = φ(T₁,…,Т_n), където n е положително цяло число, φ е n-местен функционален символ и T₁, …, Т_n са термове, то термът T е затворен точно тогава, когато е затворен всеки от термовете T₁, …, Т_n. Току-що отбелязаните следствия от дефиницията позволяват на понятието затворен терм да се даде и директна индуктивна дефиниция  -  без да се използва понятието за множество на променливите на един терм.

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

      От лемата за базисна роля на променливите на един терм се вижда, че ако T е затворен терм, а S е структура, то за всеки две оценки v и v' в S на променливите имаме равенството T^S,v=T^S,v' (тъй като в този случай по тривиални причини v и v' съвпадат върху множеството FVAR(T)). С други думи стойността на един затворен терм в дадена конфигурация (S,v) не зависи от избора на оценката v, а може да зависи само от избора на структурата S. Приемаме за произволен затворен терм T и произволна структура S да означаваме с T^S независещата от избора на оценката v в S стойнист T^S,v; ще я наричаме стойност на T в S. В случая, когато T е константа, означението T^S имаше смисъл и досега (то означаваше съответния на тази константа чрез интерпретиращото съответствие на структурата S елемент на носителя на S). Дефиницията за стойност на терм в дадена конфигурация показва, че новият смисъл, който даваме на означението сега, се съгласува със стария в споменатия случай. От същата дефиниция получаваме още следното: ако T = φ(T₁,…,Т_n), където n е положително цяло число, φ е n-местен функционален символ и T₁, …, Т_n са затворени термове, то T^S = φ^S(T₁^S,…,Т_n^S). Това равенство дава възможност за директна индуктивна дефиниция за стойност на затворен терм в структура  -  без да се използва понятието за стойност на произволен терм в конфигурация.

      Една формула се нарича затворена, ако е празно множеството на нейните свободни променливи. За безкванторни формули това изискване е равносилно с изискването да е празно множеството на всички променливи на формулата, но в общия случай двете условия не са равносилни. Например, ако π е едноместен предикатен символ на дадената сигнатура, а ξ е променлива, то формулата  ∀ξ π(ξ)  е затворена, въпреки че има променлива ξ.

      От току-що дадената дефиниция и дефиницията за множество на свободните променливи на една формула следват такива твърдения:
          0. Нулместните предикатни символи и формулите true и fail са затворени формули, а ако F = π(T₁,…,Т_n), където n е положително цяло число, π е n-местен предикатен символ и T₁, …, Т_n са термове, то формулата F е затворена точно тогава, когато е затворен всеки от термовете T₁, …, Т_n.
          1. Отрицанието на една формула е затворено точно тогава, когато самата формула е затворена.
          2. Ако F = F₁ & … & F_n или F = F₁ ∨ … ∨ F_n, където n е цяло число, по-голямо от 1, и F₁, …, F_n са формули, то формулата F е затворена точно тогава, когато е затворена всяка от формулите F₁, …, F_n.

      Горните твърдения позволяват да се даде за случая на безкванторни формули директна индуктивна дефиниция за затвореност  -  без да се използва понятието за множество на свободните променливи на една формула. В случая на произволни формули обаче даването на такава дефиниция се препятства от обстоятелството, че при построяването на една затворена формула може да бъде използувана и някоя преди това построена незатворена формула (например при построяването на затворената формула  ∀ξ π(ξ)  се използва преди това построената незатворена формула  π(ξ) ).

      От лемата за базисна роля на свободните променливи на една формула се вижда, че ако F е затворена формула, а S е структура, то за всеки две оценки v и v' в S на променливите имаме равенството F^S,v=F^S,v', т.е. стойността на една затворена формула в дадена конфигурация (S,v) не зависи от избора на оценката v, а може да зависи само от избора на структурата S. Приемаме за произволна затворена формула F и произволна структура S да означаваме с F^S независещата от избора на оценката v в S стойност F^S,v; ще я наричаме стойност на F в S. В случая, когато F е нулместен предикатен символ, означението F^S имаше смисъл и досега (то означаваше съответния на този символ чрез интерпретиращото съответствие на структурата S елемент на множеството {0,1}). Дефиницията за стойност на формула в дадена конфигурация показва, че новият смисъл, който даваме на означението сега, се съгласува със стария в споменатия случай. От същата дефиниция получаваме още:
          а) ако F = π(T₁,…,Т_n), където n е положително цяло число, π е n-местен предикатен символ и T₁, …, Т_n са затворени термове, то F^S = π^S(T₁^S,…,Т_n^S);
          б) ако F = true, то F^S = 1, а ако F = fail, то F^S = 0;
          в) ако F = not(F₀) за дадена затворена формула F₀, то F^S = 1 − F₀^S;
          г) ако F = (F₁,…,F_n), където n е цяло число, по-голямо от 1, а F₁, …, F_n са затворени формули, то F^S = min { F₁^S, …, F_n^S  };
          д) ако F = (F₁;…;F_n), където n е цяло число, по-голямо от 1, а F₁, …, F_n са затворени формули, то F^S = max { F₁^S, …, F_n^S };

      Горните твърдения позволяват да се даде и директна индуктивна дефиниция за стойност на затворена безкванторна формула в дадена структура  -  без да се използва понятието за стойност на една формула в дадена конфигурация.

      За една затворена формула F ще казваме, че е вярна (или изпълнена) в дадена структура S, ако е изпълнено равенството F^S = 1. За да изразим, че F е вярна в структурата S, ще си служим и с означението S ⊨ F. Чрез означението S ⊭ F ще изразяваме пък това, че F не е вярна в структурата S, т.е. че имаме равенството F^S = 0.

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

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

Previous  Next  Contents