Atomarni formuli

АТОМАРНИ ФОРМУЛИ

Наред с термовете още някои думи над азбуката A, разширена със знаците лява кръгла скоба, дясна кръгла скоба и запетая, ще играят съществена роля в нашите разглеждания. Сега ще дадем съответните дефиниции.

Ще наричаме атомарни формули думите от P₀ и думите от вида p(t₁,...,t_n), където n>0, pОP_n и t₁, ..., t_n са термове. Затворени атомарни формули ще наричаме думите от P₀ и думите от вида p(t₁,...,t_n), където n>0, pОP_n и t₁, ..., t_n са затворени термове.

Очевидно затворените атомарни формули са атомарни формули. За да съществува поне една затворена атомарна формула, необходимо и достатъчно е множеството W₀ИP₀ да не е празно. Като се използва обстоятелството, че никой предикатен символ не е същевременно функционален символ или променлива и че функционалните и предикатните символи и променливите не съдържат лява кръгла скоба, веднага се вижда, че никоя дума не е едновременно терм и атомарна формула.

Вярно е следното твърдение за еднозначност на синтактичния анализ на атомарните формули: никоя дума от P₀ не може да има вида p(t₁,...,t_n), и ако p(t₁,...,t_n)=pў(t₁ў,...,t_nўў), където n>0, nў>0, pОP_n, pўОP_nў и t₁, ..., t_n, t₁ў, ..., t_nўў са термове, то имаме и равенствата p=pў, n=nў, t₁=t₁ў, ..., t_n=t_nў. Това се доказва с използване на същите две леми, с чиято помощ установихме, че термовете имат еднозначен синтактичен анализ.

Ако S=(C,I) е структура, то на всяка затворена атомарна формула a ще съпоставим число a^S от множеството {0,1}, което число ще наричаме стойност на a в S. Това ще направим, като положим p^S=I(p) за всеки нулместен предикатен символ p и положим p(t₁,...,t_n)^S=I(p)(t₁^S,...,t_n^S) всеки път, когато n>0, pОP_n и t₁, ..., t_n са затворени термове. Когато a^S=1, ще казваме, че a е вярна в S, а когато a^S=0 - че a е невярна в S.

Ако S=(C,I) е структура, а v е оценка в S на променливите, то на всяка атомарна формула a ще съпоставим число a^S,v от множеството {0,1}, което число ще наричаме стойност на a в конфигурацията (S,v), а също и стойност на a в S при оценка v. Това ще направим, като положим p^S,v=I(p) за всеки нулместен предикатен символ p и положим

p(t₁,...,t_n)^S,v=I(p)(t₁^S,v,...,t_n^S,v) всеки път, когато n>0, pОP_n и t₁, ..., t_n са термове. Когато a^S,v=1, ще казваме, че a е вярна в (S,v) а когато a^S,v=0 - че a е невярна в (S,v) (вместо "в (S,v)" ще казваме също "в S при оценка v").

Сега ще формулираме и докажем едно твърдение, което ще играе много важна роля в по-нататъшната ни работа.

Основна лема за осъществимост. Нека T и F са две непресичащи се множества от атомарни формули. Тогава съществува Ербранова конфигурация, в която всички елементи на T са верни, а всички елементи на F са неверни. Ако множеството W₀ не е празно и елементите на T и F са затворени атомарни формули, то съществува и Ербранова структура, в която елементите на T са верни, а елементите на F са неверни.

Доказателство. Нека h е функция от множеството на атомарните формули към множеството {0,1}, приемаща стойност 1 за всички елементи на T и стойност 0 за всички елементи на F (такава функция съществува поради това, че T и F не се пресичат). Разглеждаме Ербрановата конфигурация (S,v), където интерпретиращото съответствие I на S е такова, че

I(p)(t₁,...,t_n)=h(p(t₁,...,t_n)) всеки път, когато pОP_n, n>0 и t₁, ..., t_n са елементи на Hў, и I(p)=h(p) за всеки нулместен предикатен символ p. Ще покажем, че така определената Ербранова конфигурация има нужното свойство. За целта е достатъчно да проверим, че за всяка атомарна формула a е в сила равенството a^S,v=h(a). Проверката е лесна: ако a=p(t₁,...,t_n), където pОP_n, n>0 и t₁, ..., t_n са термове, то a^S,v=I(p)(t₁^S,v,...,t_n^S,v)=I(p)(t₁,...,t_n)=h(p(t₁,...,t_n))=h(a), а ако p е нулместен предикатен символ, то a^S,v=I(p)=h(p)=h(a). Да предположим сега, че множеството W₀ не е празно и елементите на T и F са затворени атомарни формули. Разглеждаме Ербрановата структура S₀, при която интерпретиращото съответствие се определя върху предикатните символи по същия начин, както беше определено по-горе интерпретиращото съответствие I, но с тази разлика, че вместо произволни термове се разглеждат затворени. Тогава за всяка затворена атомарна формула a е в сила равенството a^S₀=h(a) и следователно в S₀ елементите на T са верни, а елементите на F - неверни.

Следствие. Нека T и F са две множества от атомарни S-формули. За да съществува конфигурация, в която всички елементи на T са верни, а всички елементи на F са неверни, необходимо и достатъчно е множествата T и F да нямат общи елементи. В случай, че множеството W₀ не е празно и елементите на T и F са затворени атомарни формули, същото условие е необходимо и достатъчно и за съществуването на структура, в която всички елементи на T са верни, а всички елементи на F - неверни.

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

Contents