Доказателство. Ще използваме индукция, съобразена с индуктивната дефиниция на понятието затворен терм. Ако cОF₀, то c^S=j₀^H(c)=c. Да предположим сега, че fОF_n, където n>0, и T₁,T₂,...,T_n са затворени термове, за които имаме равенствата T₁^S=T₁,T₂^S=T₂,...,T_n^S=T_n. Тогава

    Следствие 1. При предположенията на горната лема всеки два различни затворени терма (ако съществуват такива) имат различни стойности в S.

    Забележка 1. Уговорката, добавена в скоби в горното следствие, е по повод на това, че би могло да се случи при n>0 да няма n-местни функционални символи и същевременно множеството F₀ да се състои точно от един елемент - очевидно в такъв случай споменатият единствен елемент на F₀ би бил и единственият затворен терм (това е всъщност случаят, когато Ербрановият универсум се състои само от един елемент).

    Следствие 2. Нека S е произволна ербранова структура и нека в S за произволно неотрицателно цяло число n интерпретацията на n-местните предикатни символи да бъде p_n. Тогава при n>0, pОP_n и (T₁,T₂,...,T_n)ОHⁿ, за да бъде вярна в S атомарната формула p(T₁,T₂...,T_n), необходимо и достатъчно е да е в сила равенството p_n(p)(T₁,T₂,...,T_n)=1.

    Забележка 2. Разбира се за произволна структура S (не непременно ербранова) с интерпретация p₀ на нулместните предикатни символи може да се твърди (въз основа на съответните дефиниции), че ако pОP₀, то p е затворена атомарна формула и за да бъде тя вярна в S, необходимо и достатъчно е да е в сила равенството p₀(p)=1.

    Втора основна лема за ербрановите структури. Нека F₀№Ж и нека е дадено едно множество M от затворени атомарни формули. Тогава съществува точно една ербранова структура S със свойството, че в S са верни онези и само онези затворени атомарни формули, които принадлежат на M.

    Доказателство. Нека S е произволна ербранова структура. За произволно неотрицателно цяло число n да означим с p_n интерпретацията на n-местните предикатни символи в тази структура. От следствие 2 и забележка 2 е ясно, че структурата S ще има изказаното в лемата свойство точно тогава, когато са изпълнени следните две условия: а) приn>0 и pОP_n равенството p_n(p)(T₁,T₂,...,T_n)=1 е в сила за онези и само за онези (T₁,T₂,...,T_n) от Hⁿ, за които съответната атомарна формула p(T₁,T₂...,T_n) принадлежи на множеството M; б) равенството p₀(p)=1 е в сила точно за онези и само за онези p от P₀, които принадлежат на M. Лесно е да се види обаче, че съществува точно една ербранова структура S, за която са изпълнени условията а) и б). Действително, дефиницията за ербранова структура определя еднозначно носителя на структурата и интерпретациите на функционалните символи, а пък условията а) и б) определят еднозначно интерпретациите на предикатните символи.  _ї

     Ще направим аналогични разглеждания, работейки с произволни термове, а не само със затворени. Множеството на всички термове ще наричаме разширен Ербранов универсум и ще го означаваме с Hў (това множество със сигурност не е празно). За всяко неотрицателно цяло число n дефинираме изображение j_n^Hў на множеството F_n в множеството на n-местните операции в Hў, което изображение ще наричаме разширена Ербранова интерпретация на n-местните функционални символи. Дефиницията е аналогична на дефиницията на изображението j_n^H - разликата е в това, че при n>0 става дума за произволни термове, а не само за затворени. Ще наричаме разширена ербранова структура всяка структура с носител разширения Ербранов универсум Hў, в която за всяко неотрицателно цяло число n интерпретация на n-местните функционални символи е тяхната разширена Ербранова интерпретация j_n^Hў. Под Ербранова оценка на променливите ще разбираме тъждественото изображение на множеството X в себе си.

     Първа основна лема за разширените ербранови структури. Нека S е произволна разширена ербранова структура, а v е Ербрановата оценка на променливите. Тогава T^S,v=T за всеки терм T.

     Доказателство. Ще използваме индукция, съобразена с индуктивната дефиниция на понятието терм. Ако cОF₀, то c^S=j₀^Hў(c)=c. Ако XОX, то X^S,v=v(X)=X. Да предположим сега, че fОF_n, където n>0, и T₁,T₂,...,T_n са  термове, за които имаме равенствата T₁^S,v=T₁,T₂^S,v=T₂,...,T_n^S,v=T_n. Тогава

    Следствие 3. При предположението на горната лема всеки два различни терма имат различни стойности в S при оценката v.

    Следствие 4. Нека S е произволна разширена ербранова структура, нека v е Ербрановата оценка на променливите и нека в S за произволно неотрицателно цяло число n интерпретацията на n-местните предикатни символи да бъде p_n. Тогава при n>0, pОP_n и (T₁,T₂,...,T_n)ОHўⁿ, за да бъде вярна в S при оценката v атомарната формула p(T₁,T₂...,T_n), необходимо и достатъчно е да е в сила равенството p_n(p)(T₁,T₂,...,T_n)=1.

    Втора основна лема за разширените ербранови структури. Нека е дадено едно множество M от атомарни формули. Тогава съществува точно една разширена ербранова структура S със свойството, че в S при Ербрановата оценка на променливите са верни онези и само онези атомарни формули, които принадлежат на M.

    Доказателство. Нека S е произволна разширена ербранова структура. Да означим с v Ербрановата оценка на променливите, а за произволно неотрицателно цяло число n да означим с p_n интерпретацията на n-местните предикатни символи в тази структура. От следствие 4 и забележка 2 е ясно, че структурата S ще има изказаното в лемата свойство точно тогава, когато са изпълнени следните две условия: а) приn>0 и pОP_n равенството p_n(p)(T₁,T₂,...,T_n)=1 е в сила за онези и само за онези (T₁,T₂,...,T_n) от Hўⁿ, за които съответната атомарна формула p(T₁,T₂...,T_n) принадлежи на множеството M; б) равенството p₀(p)=1 е в сила за онези и само за онези p от P₀, които принадлежат на M. Лесно е да се види обаче, че съществува точно една разширена ербранова структура S, за която са изпълнени условията а) и б). Действително, дефиницията за разширена ербранова структура определя еднозначно носителя на структурата и интерпретациите на функционалните символи, а пък условията а) и б) определят еднозначно интерпретациите на предикатните символи.  _ї
 

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

Previous  Next  Contents