Понятието терм при дадена сигнатура Σ се дефинира индуктивно по следния начин: термове са променливите, константите на Σ и всички думи от вида φ(T₁,Т₂,…,Т_n), където n е положително цяло число, φ e n-местен функционален символ на Σ и T₁, Т₂, …, Т_n са термове. Множеството на всички термове при сигнатура Σ ще означаваме с T_Σ. След като разполагаме с понятието терм, уславяме се да наричаме атомарни формули на предикатното смятане при сигнатура Σ нулместните предикатни символи на Σ и всички думи от вида π(T₁,Т₂,…,Т_n), където n е положително цяло число, π e n-местен предикатен символ на Σ и T₁, Т₂, …, Т_n са термове.

      Пример 1. Ako Σ е сигнатурата от пример 1 от въпроса за сигнатури и структури, то думите b(s(a(a(e)))) и a(s(b(X))) са термове, а думите p(e,e), d(a(a(b(b(e))))) и p(X,a(Y)) са атомарни формули.

      Пример 2. Ako Σ е сигнатурата от пример 2 от въпроса за сигнатури и структури, то думата union(singleton(a),singleton(b)) е терм, а думата belongs(X,union(A,B)) е атомарна формула.

      Пример 3. Ako Σ е сигнатурата от пример 5 от въпроса за сигнатури и структури, то думите

      Забележка 1. Очевидно е, че ако сигнатурата Σ е с празно множество на функционалните символи, то единствените термове са променливите, а ако Σ е с празно множество на предикатните символи, то не съществуват атомарни формули.

      Като се използват свойствата на уравновесените и на силно уравновесените думи, с индукция, съобразена с дефиницията за терм, се показва, че всички термове са силно уравновесени думи, а оттам се получава същото и за атомарните формули. Това, че термовете и атомарните формули при дадена сигнатура са силно уравновесени думи, заедно с лемата за еднозначното разпадане и с обстоятелството, че никоя дума не е едновременно константа и променлива, осигурява еднозначното прочитане на термовете и на атомарните формули в следния смисъл: трите случая в дефиницията за терм се изключват взаимно, като в третия от тях числото n, функционалният символ φ и термовете T₁, Т₂, …, Т_n се определят еднозначно по дадения терм, а също двата случая в дефиницията за атомарна формула се изключват взаимно и във втория от тях числото n, предикатният символ π и термовете T₁, Т₂, …, Т_n се определят еднозначно по дадената атомарна формула. Освен това никоя атомарна формула не е терм, тъй като никой предикатен символ не е същевременно функционален символ или променлива.

      Ако са дадени две сигнатури Σ и Σ′, където Σ′ съдържа Σ, една проста индукция показва, че всеки терм при сигнатура Σ е терм и при сигнатура Σ′, а оттук пък следва, че всяка атомарна формула при сигнатура Σ е атомарна формула и при сигнатура Σ′.

      Общото понятие за формула при сигнатура Σ ще въведем чрез следната индуктивна дефиниция, като множеството на всички формули при сигнатура Σ ще означаваме с F_Σ:
          0. Атомарните формули при сигнатура Σ и думите true и fail са формули при сигнатура Σ.
          1. За всяка формула F при сигнатура Σ думата not(F) също е формула при сигнатура Σ (нарича се отрицание на F).
          2. При всеки избор на цяло число n, по-голямо от 1, и на формули F₁, F₂, …, F_n при сигнатура Σ думите (F₁,F₂,…,F_n) и (F₁;F₂;…;F_n) също са формули при сигнатура Σ (наричат се съответно конюнкция на F₁, F₂, …, F_n и дизюнкция на F₁, F₂, …, F_n, а споменатите n формули се наричат членове на конюнкцията и на дизюнкцията).
          3. За всяка променлива ξ и всяка формула F при сигнатура Σ думите (,ξ)F и (;ξ)F също са формули при сигнатура Σ (наричат се съответно генерализация на F по ξ и екзистенциализация на F по ξ).

      Пример 4. Ako Σ е сигнатурата от пример 2 от предходния въпрос, то думите not(belongs(X,A)), (not(belongs(X,A));belongs(X,union(A,B))) и (,X)belongs(X,singleton(X)) са формули.

      В следващия въпрос семантиката на термовете и формулите ще бъде дефинирана по един прецизен начин. Засега ще се ограничим със следното интуитивно нейно описание. Термовете ще служат за означаване на някои елементи на носителя на дадена структура. Атомарните формули ще изразяват някои тъй да се каже прости твърдения за такива елементи. Отрицанието на една формула е вярно тогава, когато тази формула не е вярна. Конюнкцията на дадени формули е вярна тогава, когато всичките тези формули са верни, а дизюнкцията им е вярна, когато поне една от тях е вярна. Генерализацията на една формула по дадена променлива е вярна тогава, когато самата формула е вярна за всички допустими стойности на променливата, а екзистенциализацията на една формула по дадена променлива е вярна тогава, когато самата формула е вярна за поне една допустима стойност на променливата.

      С дефиницията, която приехме, ние всъщност определихме какво да разбираме под конюнкция и под дизюнкция на произволна крайна редица от формули, имаща поне два члена. Удобно е да определим какво да разбираме под конюнкция и под дизюнкция още и на едночленна и на празна редица от формули, като при това да останат в сила изказаните преди малко условия за вярност на конюнкцията и на дизюнкцията. Това ще направим по следния начин: под конюнкция и под дизюнкция на едночленна редица от формули ще разбираме нейния единствен член, а под конюнкция и под дизюнкция на празна редица от формули ще разбираме съответно формулата true и формулата fail (ще ги наричаме празна конюнкция и празна дизюнкция).

      Ще използваме и следните означения за формули:
          1. Формулата not(F) ще означаваме с  ¬ F  (знакът  ¬  се чете "не" и се нарича знак за отрицание).
          2. При n>1 формулите (F₁,F₂,…,F_n) и (F₁;F₂;…;F_n) ще означаваме съответно с F₁ & F₂ & … & F_n и с F₁ ∨ F₂ ∨ … ∨ F_n  (знаците  &  и  ∨  се четат съответно като "и" и "или", като вместо първия от тях понякога се използва още и знакът  ∧ ; наричат се съответно знак за конюнкция и знак за дизюнкция).
          3. Уславяйки се да пишем ∀ξ  вместо (,ξ) и ∃ξ  вместо (;ξ), формулите (,ξ)F и (;ξ)F ще означаваме съответно с  ∀ξ F  и с  ∃ξ F  (знаците  ∀  и  ∃  се четат съответно като "за всяко" и "за някое"; наричат се съответно квантор за общност и квантор за съществуване, като думите ∀ξ  и ∃ξ  се наричат квантор за общност по ξ и квантор за съществуване по ξ).

      Забележка 2. Означенията  F₁ & F₂ & … & F_n  и  F₁ ∨ F₂ ∨ … ∨ F_n  за конюнкция и дизюнкция биха могли да се използват и при n=1 благодарение на уславянето, което приехме относно конюнкция и дизюнкция на едночленна редица от формули. В някои общи разглеждания, при които n не е фиксирано и може да бъде и 0, ние ще използваме тези означения и без да изключваме нулата.

      С индукция, съобразена с дефиницията за формула, се показва, че всички формули са силно уравновесени думи. Лесно се вижда, че не може да се случи една формула да бъде същевременно и терм  -  за атомарните формули това вече го проверихме, а за останалите то следва от обстоятелството, че празната дума и думите true, fail, not не са нито функционални символи, нито променливи. Като използваме още веднъж лемата за еднозначното разпадане, но този път в съчетание с обстоятелството, че изброените в предното изречение четири думи не са и предикатни символи, виждаме, че за формулите е налице еднозначно прочитане в смисъл аналогичен на онзи, който имахме при термовете (за да покажем, че никоя формула, получена по точка 3 от дефиницията, не би могла да се получи по точка 2, можем да използваме това, че всяка формула започва с малка латинска буква или с лява скоба).

      Ако са дадени две сигнатури Σ и Σ′, където Σ′ съдържа Σ, с проста индукция се вижда, че всяка формула при сигнатура Σ е формула и при сигнатура Σ′.

      Забележка 3. Понятието за логическа формула, което въведохме, представлява само един от многото приемливи варианти на това понятие, различаващи се в едно или друго отношение, но свеждащи се по същество един към друг. Всъщност един по-обичаен подход е в дефиницията за логическа формула конюнкциите и дизюнкциите да са само с по два члена, а след това с помощта на такива конюнкции и дизюнкции да се определят конюнкции и дизюнкции и с друг брой членове - например F₁ & F₂ & F₃ да се определи като (F₁ & F₂) & F₃. Освен това невинаги се въвеждат формули от рода на true и fail, което обаче създава някои малки затруднения във връзка с празната конюнкция и празната дизюнкция.

      Забележка 4. В дадената по-горе дефиниция поставянето на квантор пред формула е осъществено по нетрадиционен начин, но това не води до несъгласие с означенията на езика Пролог, понеже нито в него се използват квантори, нито пък формулите, получени по последната точка на дефиницията, означават нещо в Пролог. Разбира се не е никак съществено, че поставянето на кванторите е осъществено именно по този конкретен начин.

      В много от нашите разглеждания ще имаме работа с един по-тесен клас от формули, които ще наричаме безкванторни. Казано накратко, това са формулите, които могат да се получат, без да се използва последната точка от индуkтивната дефиниция за формула. Точната дефиниция и на този клас от формули също е индуктивна и тя може да се изкаже така: атомарните формули при сигнатура Σ и формулите true и fail са безкванторни формули при сигнатура Σ, отрицанието на безкванторна формула при сигнатура Σ е пак безкванторна формула при сигнатура Σ, конюнкцията и дизюнкцията на безкванторни формули при сигнатура Σ са пак безкванторни формули при сигнатура Σ.

      Пример 5. От трите формули, споменати в пример 4, първите две са безкванторни, а последната не е.
 

Previous  Next  Contents

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