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

      Предполагайки, че е дадена една структура S=(Σ,D,I), ние за всяка формула F ще дефинираме нейна стойност F^S,v в произволна конфигурация (S,v), като тази стойност ще бъде винаги някое от числата 0 и 1 (интуитивно те ще играят ролите на "лъжа" и "истина"). Ако можехме да се ограничим само с безкванторни формули, дефиницията би била в същия дух както дефиницията за стойност на терм, но при разглеждането на произволни формули нещата са по-сложни и е подходящо да въведем първо едно спомагателно понятие. А именно, за произволна оценка v на променливите в множеството D, произволна променлива ξ и произволен елемент d на D ние ще въведем наименование и означение за онази оценка на променливите в D, която съпоставя на променливата ξ елемента d, а за всички други променливи съвпада с v. Ще наричаме така описаната оценка модификация на v върху ξ чрез d и ще я означаваме с v[ξ→d]. Eто как изглежда дефиницията за стойност на формула при използване на въведеното спомагателно понятие там, където е подходящо (коректността на дефиницията се обосновава с еднозначния прочит на формулите):
          а) ако F = π(T₁,…,Т_n), където n е положително цяло число, π е n-местен предикатен символ на Σ и T₁, …, Т_n са термове, полагаме F^S,v = π^S(T₁^S,v,…,Т_n^S,v)  (т.е. F^S,v = I(π)(T₁^S,v,…,Т_n^S,v) ), a ako F е нулместен предикатен символ на Σ, полагаме F^S,v = F^S  (т.е. F^S,v = I(F) );
          б) ако F = true, то F^S,v = 1, а ако F = fail, то F^S,v = 0;
          в) ако F = not(F₀) за дадена формула F₀, то F^S,v = 1 − F₀^S,v;
          г) ако F = (F₁,…,F_n), където n е цяло число, по-голямо от 1, а F₁, …, F_n са формули, то F^S,v = min { F₁^S,v, …, F_n^S,v  };
          д) ако F = (F₁;…;F_n), където n е цяло число, по-голямо от 1, а F₁, …, F_n са формули, то F^S,v = max { F₁^S,v, …, F_n^S,v };
          е) ако F = (,ξ)F₀ за дадена променлива ξ и дадена формула F₀, то F^S,v = min { F₀^S,v[ξ→d] | d∈D };
          ж) ако F = (;ξ)F₀ за дадена променлива ξ и дадена формула F₀, то F^S,v = max { F₀^S,v[ξ→d] | d∈D }.

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

      Дадените по-горе дефиниции осигуряват, че отрицанието на една формула е вярно в дадена конфигурация точно тогава, когато самата формула не е вярна в тази конфигурация, че конюнкцията на какъв да е даден краен брой формули е вярна в дадена конфигурация точно тогава, когато в нея са верни всичките тези формули, а дизюнкцията на въпросните формули е вярна в дадена конфигурация точно тогава, когато в нея е вярна някоя от тези формули. Дефинициите осигуряват още следното: генерализацията на една формула по една променлива ξ е вярна в дадена конфигурация (S,v) точно тогава, когато самата формула е вярна във всяка от конфигурациите (S,v[ξ→d]), където d принадлежи на носителя на S, а екзистенциализацията на формулата е вярна в конфигурацията (S,v) точно тогава, когато формулата е вярна в поне една от споменатите други конфигурации.

      Дотук се занимавахме със стойности на термове и формули при една фиксирана сигнатура. Да предположим сега, че са дадени структура S със сигнатура Σ и нейно обогатяване S′, което е със сигнатура Σ′. Понеже Σ′ съдържа Σ, термовете и формулите при сигнатура Σ същевременно са съответно термове и формули при сигнатура Σ′. Освен това, тъй като S и S′ имат един и същ носител, всяка оценка на променливите в S е тяхна оценка в S′ и обратно. С индукция се доказва, че за всеки терм T в сигнатура Σ и всяка оценка v на променливите в S имаме равенството T^S,v = T^S′,v, а след това с още една индукция се установява, че F^S,v = F^S′,v за всяка формула F в сигнатура Σ и всяка оценка v на променливите в S.
 

Previous  Next  Contents

Дата на предходната версия:	12.08.2004
Дата на настоящата версия:	28.02.2005