Contents
 

 

ОСНОВНИ ДЕФИНИЦИИ НА ПОНЯТИЯ ОТ МАТЕМАТИЧЕСКАТА ЛОГИКА
(от лекциите на Д. Скордев по Логическо програмиране)

Синтактични понятия

    Предполагаме, че е дадена една азбука, съдържаща измежду своите знаци двете кръгли скоби и запетаята (когато по-нататък конкретни знаци от тази азбука се срещат в рамките на друг текст, за избягване на недоразумения ще ги изобразяваме с получерен шрифт). Тази азбука по-нататък ще я наричаме базисна. Ако W е едно множество от думи над базисната азбука, то някои думи над нея ще наричаме префиксни изрази над W. Дефиницията е индуктивна: така ще наричаме думите от W и всички думи от вида w(T1,T2...,Tn), където n е положително цяло число, w е дума от W и T1, T2, ..., Tn са префиксни изрази над W (при n=1 считаме, че думата  ,T2...,Tn  е празна, докато при n>1 тя очевидно не е празна). Префиксните изрази от втория вид ще наричаме съставни. Ще казваме, че префиксните изрази над W имат еднозначен анализ, ако никой съставен префиксен израз над W не принадлежи на самото W и всеки съставен префиксен израз има само едно представяне във въпросния втори вид. Едно достатъчно (но не необходимо) условие, за да имат префиксните изрази над W еднозначен анализ - това е условието в думите от W да не се срещат нито кръгли скоби, нито запетаи.
    Оттук нататък предполагаме, че е фиксирано някое такова множество W от думи над базисната азбука, щото префиксните изрази над W да имат еднозначен анализ. При това ще се занимаваме със случая, когато W е обединение на множество X (множество на променливите), за което ще искаме да е безкрайно, множества F0,F1,F2, ... (множествa съответно на нулместните, едноместните, двуместните и т.н. функционални символи), множества P0,P1,P2, ... (множествa съответно на нулместните, едноместните, двуместните и т.н. предикатни символи)  и непразно множество L (множество на логическите символи), като множествата X и L нямат общи елементи с никое от множествата Fn и Pn, а също и помежду си (други пресичания на множества измежду споменатите се допускат). Нулместните функционални символи ще наричамe още константи. Двойката от редиците F0,F1,F2,... и P0,P1,P2,... ще наричаме сигнатура. Ще приемем, че множеството L се състои от пет различни думи, които ще означаваме с not, and, or, for_all и for_some.
    Индуктивно се дефинира понятието терм: термове са константите, променливите и всички думи от вида f(T1,Т2...,Тn), където n е положително цяло число, f e n-местен функционален символ и T1, Т2,..., Тn са термове.
    Уславяме се да наричаме атомарни формули нулместните предикатни символи и всички думи от вида p(T1,Т2...,Тn), където n е положително цяло число, p e n-местен предикатен символ и T1, Т2, ..., Тn са термове.
    Индуктивно се дефинира понятието формула: формули са атомарните формули и всички думи, имащи някой от петте вида not(F), and(F1,F2), or(F1,F2), for_all(X,F), for_some(X,F), където F, F1, F2 са формули, а X е променлива. Ако в тази дефиниция  се ограничим с атомарните формули и с формулите от първите три измежду посочените пет вида, получаваме дефиниция на понятието безкванторна формула. Вместо not(F), and(F1,F2), or(F1,F2), for_all(X,F),  for_some(X,F) обикновено пишем съответно ШF, F1&F2, F1ЪF2, "XF, $XF. При използването на знаците Ш, " и $ приемаме, че съответните им операции имат приоритет пред операциите, съответни на знаците & и Ъ. За всеки две формули F1 и F2 полагаме
F1®F2=ШF1ЪF2,     F1«F2=(F1&F2)Ъ(ШF1&ШF2).
При всеки избор на формулите F1, F2, ..., Fn полагаме
F1&F2&...&Fn=(...(F1&F2)&...)&Fn, F1ЪF2Ъ...ЪFn=(...(F1ЪF2)Ъ...)ЪFn.
Една формула наричаме  литерал, ако тя е атомарна или има вида ШF, където F е атомарна формула. Елементарни конюнкции и елементарни дизюнкции наричаме съответно формулите от вида F1&F2&...&Fn и формулите от вида F1ЪF2Ъ...ЪFn, където всяка от формулите F1, F2, ..., Fn е литерал. Хорнова дизюнкция наричаме формула от вида F1ЪF2Ъ...ЪFn, където F1, F2, ..., Fn са литерали и най-много един от тях е атомарна формула.
   За всека дума E, която е терм или формула, дефинираме множество VAR(E), което наричаме множество на променливите на E (или множество на свободните променливи на E). А именно:
        а) при wОF0ИP0 полагаме VAR(w)=Ж;
        б) при XОX полагаме VAR(X)={X};
        в) когато n е положително цяло число, wОFnИPn и T1, Т2, ..., Тn са термове, полагаме
VAR(w(T1,Т2...,Тn)) =VAR(T1)ИVAR(T2)И . . . ИVAR(Tn);
        г) за всяка формула F полагаме VAR(ШF)=VAR(F);
        д) за всеки две формули F1 и F2 полагаме VAR(F1&F2)=VAR(F1ЪF2)=VAR(F1)ИVAR(F2);
        е) за всяка променлива X и всяка формула F полагаме VAR("XF)=VAR($XF)=VAR(F)\{X}.
    Термовете и формулите, на които множеството на променливите е празно, наричаме затворени. Универсално затваряне (екзистенциално затваряне) на една формула F наричаме такава затворена формула, която има вида "X1..."XmF (вида $X1...$XmF) при някой избор на променливите X1, ..., Xm (mі0).
    Множеството на затворените термове наричаме Ербранов универсум, а множеството на всички термове - разширен Ербранов универсум.
    Субституция наричаме такова изображение s на множеството на променливите в разширения Ербранов универсум, че равенството s(X)=X  да е нарушено за най-много краен брой променливи X. Въвеждаме означение за субституцията, която преобразува дадени краен брой променливи в дадени термове, а всички други променливи преобразува в самите тях. Субституцията, която преобразува всяка променлива в самата нея, наричаме тъждествена субституция. По обичайния индуктивен начин дефинираме резултат от прилагането на една субституция към произволен терм и към произволна безкванторна формула; резултата от прилагането на s към E означаваме със s(E). За всеки две субституции s и s0 означаваме с ss0 субституцията s1, определена с условието за всяка променлива  да имаме равенството s1(X)= s(s0(X)); ще я наричаме произведение на s и s0, а също резултат от прилагането на s към s0. Благодарение на това, че така дефинираното умножение на субституции е асоциативно, можем да означаваме и произведения на повече от две субституции без да използваме скоби.
    Ако E е терм, безкванторна формула или субституция, резултатите от прилагането на субституции към E наричаме частни случаи на E. Вариант на E наричаме такъв частен случай Eў на E, че и E да е частен случай на Eў. Ако E1 и E2 са два терма или две атомарни формули, унификатор на E1 и E2 наричаме такава субституция, че резултатите от прилагането й към E1 и E2 да съвпадат. В случай, че такава субституция съществува, казваме, че E1 и E2 са унифицируеми. Най-общ унификатор на E1 и E2 наричаме такъв техен унификатор, че всеки унификатор на E1 и E2 да бъде негов частен случай.
 
 

Семантични понятия

    Нека C е дадено множество, а n е дадено естествено число. Ще наричаме n-местни операции в C изображенията на Cn в C, ако n е различно от 0, и елементите на C в случай, че n=0. Ще считаме, че n-местните предикати в C са изображенията на Cn в двуелементното множество {0,1}, ако n е различно от 0, и числата 0 и 1 в противен случай (числата 0 и 1 играят ролята съответно на "лъжа" и "истина"). Интерпретация в C на n-местните функционални символи ще наричаме всяко съответствие, което съпоставя на тези символи n-местни операции в C, а интерпретация в C на n-местните предикатни символи - всяко съответствие, което съпоставя на тези символи n-местни предикати в C. Структура ще наричаме всяка наредена тройка от непразно множество C и две редици j0,j1,j2,... и p0,p1,p2,..., където за всяко естествено число n jn е интерпретация в C на n-местните функционални символи, а pn е интерпретация в C на n-местните предикатни символи. Множеството C наричаме носител на структурата, а редиците j0,j1,j2,... и p0,p1,p2,... - нейни интерпретационни редици. Оценка на променливите в дадено множество C наричаме всяко изображение на множеството на променливите в C. Очевидно тъждествената субституция е една оценка на променливите в разширения Ербранов универсум; наричаме я Ербранова оценка на променливите.
    Нека S е структура с носител C и интерпретационни редици j0,j1,j2,... и p0,p1,p2,... Когато е дадена една оценка v на променливите в C, на всеки терм T съпоставяме елемент TS,v на C, наречен  стойност на T в S при оценката v. Дефиницията е индуктивна: при cОF0 полагаме cS,v=j0(c), при XОX полагаме XS,v=v(X), a когато n е положително цяло число, fОFn и T1, Т2,...,Тn са термове, полагаме
f(T1,Т2...,Тn)S,v = jn(f)(T1S,v,Т2S,v,...,ТnS,v).
Ако термът T е затворен, то елементът TS,v не зависи от избора на v; този елемент се означава още с TS и се нарича стойност на T в S. За всяка формула дефинираме кога тя е вярна в S при дадена оценка на променливите в C. Дефиницията е пак индуктивна и се състои от следните точки: За да изразим, че дадена формула F е вярна в S при дадена оценка v на променливите, пишем S,vF. Когато формулата F е затворена, това дали е изпълнено условието S,vF не зависи от избора на оценката v, поради което вместо S,vF можем да пишем SF и да казваме, че F е вярна в S, когато това условие е изпълнено. За една формула F казваме, че тя е тъждествено вярна в S, ако F е вярна в S при всяка оценка на променливите, и казваме, че е изпълнима в S, ако е вярна в S при някоя оценка на променливите.
    За една формула казваме, че е тъждествено вярна, ако тя е тъждествено вярна във всяка структура, и казваме, че е изпълнима, ако е изпълнима в някоя структура.
    За две формули казваме, че са еквивалентни, ако винаги, когато едната от тях е вярна в дадена структура S при дадена оценка v на променливите, другата също е вярна в S при оценката v.
    Модел за едно множество от формули наричаме такава структура S, че всички формули от множеството да са тъждествено верни в  S (разбира се, ако формулите от даденото множество са затворени, то думата "тъждествено" може да се пропусне). Едно множество от затворени формули наричаме изпълнимо, ако съществува структура, която е модел за него (т.е. структура, в която всички формули от множеството са верни).
    Когато са дадени една структура S и една субституция s, на всяка оценка v на променливите в носителя на S можем да съпоставим оценката w, дефинирана за всяка променлива X чрез равенството w(X)=s(X)S,v. Така описаното преобразуване на оценки означаваме със sS и наричаме  оператор за присвояване в S, съответен на s.

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