Атомарните формули не са достатъчни за изразяване на много от твърденията и условията, които е желателно да бъдат изразени. Затова ще дефинираме един по-широк клас от думи над базисната азбука, които ще наричаме логически формули (или още формули на предикатното смятане, а за краткост просто формули). Дефиницията е индуктивна: 
    0. Всяка атомарна формула е логическа формула.
    1. Логическите символи and и or са логически формули (наричат се съответно празна конюнкция и празна дизюнкция).
    2. При всеки избор на положително цяло число n и на логически формули F₁, F₂, ..., F_n думите and(F₁,F₂...,F_n) и or(F₁,F₂...,F_n) също са логически формули (наричат се съответно конюнкция на F₁, F₂, ..., F_n и дизюнкция на F₁, F₂, ..., F_n, а споменатите n формули се наричат членове на конюнкцията и на дизюнкцията).
    3. За всяка логическа формула F думата not(F) също е логическа формула (нарича се отрицание на F).
    4. За всяка променлива X и всяка логическа формула F думите for_all(X,F) и for_some(X,F) също са логически формули (наричат се съответно генерализация на F по X и екзистенциализация на F по X).

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

    Ще използваме и следните означения за логически формули: формулата and ще означаваме още с true, формулата or - с false или fail, формулите and(F₁,F₂...,F_n) и or(F₁,F₂...,F_n) - съответно с F₁ & F₂ & ... & F_n и с F₁ Ъ F₂ Ъ ... Ъ F_n (знаците & и Ъ се четат съответно като "и" и "или"), формулата not(F) - с Ш F (знакът Ш се чете "не"), формулите for_all(X,F) и for_some(X,F) - съответно с "X F и с $X F (знаците " и $ се четат съответно като "за всяко" и "за някое").

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

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

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

    Променливата X, използвана при прилагането на последната точка от дефиницията за формула, играе по-особена роля в двете формули, които се строят по тази точка. От гледна точка на описаната преди малко интуитивна семантика на формулите верността на коя да е от двете споменати формули не зависи от предварително дадена стойност на въпросната променлива (за разлика да речем от наличната в общия случай зависимост на стойността на една атомарна формула от стойностите на нейните променливи). Поради тази особеност ние ще съпоставим на всяка формула F две множества от променливи, които ще означаваме с FVAR(F) и с BVAR(F); променливите от първото множество ще наричаме свободни променливи на F, а променливите от второто - свързани променливи на F (буквите F и B пред VAR идват съответно от думите "free" и "bound", с които на английски език започват термините за двата вида променливи). Дефиницията на двете множества е индуктивна и се състои от следните точки: 
    1. Ако F е атомарна формула, то FVAR(F)=VAR(F), BVAR(F)=Ж.
    2. Ако F е някоя от формулите and и or, то FVAR(F)=BVAR(F)=Ж.
    3. Ако F е някоя от формулите and(F₁,F₂...,F_n) и or(F₁,F₂...,F_n), където n е положително цяло число и F₁, F₂, ..., F_n са дадени формули, то

    Току-що дадената дефиниция е коректна благодарение на еднозначното прочитане на логическите формули. Индуктивно се доказва, че за всяка формула F множествата FVAR(F) и BVAR(F) са крайни. Може да се случи за някоя формула F тези две множества да имат непразно сечение. Например ако X е свободна променлива на дадена формула F₀, а F е формулата F₀ & $X Ш F₀, то X О FVAR(F) З BVAR(F). Понякога обаче наличието на променливи, които са едновременно свободни и свързани променливи на една формула, създава известни технически неудобства. Поради това нерядко използването на формули с такива променливи се избягва (например ако споменатата преди малко F₀ е формулата p(X), където p е едноместен предикатен смисъл, то съответната формула F би имала вида p(X) & $X Ш p(X), но се предпочита вместо с нея да се работи с формула от вида p(X) & $ YШ p(Y), където Y е някоя променлива, различна от X).

    Формула, която няма свободни променливи, се нарича затворена, а формула, която няма свързани променливи, се нарича отворена. Разбира се за атомарни формули дефинираното сега понятие за затвореност съвпада с по-раншното. Можем да отбележим още, че всички атомарни формули са отворени, тъй че не е трудно да се даде пример за формула, която е едновременно отворена и затворена, а също и пример за формула, която е отворена, но не е затворена (разбира се, най-прост пример за формули, които са едновременно отворени и затворени - това са празната конюнкция и празната дизюнкция). Като пример за формула, която е затворена, но не е отворена, бихме могли да посочим формула от вида "X p(X), където X и p са съответно променлива и едноместен предикатен смисъл. Ако X и Y са различни помежду си променливи, а q е двуместен предикатен символ, то формулата $Y q(X,Y) пък не е нито затворена, нито отворена.

    Понятието отворена формула допуска и индуктивна дефиниция. А именно нека дефинираме понятието безкванторна формула по следния индуктивен начин (фактически използваме дефиницията за логическа формула без т. 4 и със замяна на думите "логическа формула" и "логически формули" съответно с думите "безкванторна формула" и "безкванторни формули"): 
    0. Всяка атомарна формула е безкванторна формула.
    1. Логическите символи and и or са безкванторни формули.
    2. При всеки избор на положително цяло число n и на безкванторни формули F₁, F₂, ..., F_n думите and(F₁,F₂...,F_n) и or(F₁,F₂...,F_n) също са безкванторни формули.
    3. За всяка безкванторна формула F думата not(F) също е безкванторна формула.

    Ясно е, че всяка безкванторна формула е отворена логическа формула, а лесно се доказва и обратното (за целта е достатъчно индуктивно да докажем за произволна логическа формула, че тя е безкванторна или има поне свързана променлива). Следователно отворените формули и безкванторните формули всъщност образуват едно и също множество.

    От току-що казаното следва, че една формула е едновременно отворена и затворена точно тогава, когато тя е затворена безкванторна формула. Лесно се вижда, че множеството на затворените безкванторни формули съвпада с множеството на формулите без променливи, където понятието формула без променливи се въвежда чрез следната индуктивна дефиниция (получена чрез прости изменения в дефиницията за безкванторна формула):
    0. Всяка затворена атомарна формула е формула без променливи.
    1. Логическите символи and и or са формули без променливи.
    2. При всеки избор на положително цяло число n и на формули без променливи F₁, F₂, ..., F_n думите and(F₁,F₂...,F_n) и or(F₁,F₂...,F_n) също са формули без променливи.
    3. За всяка формула без променливи F думата not(F) също е формула без променливи.
 

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

Previous  Next  Contents