Атомарните формули не са достатъчни за изразяване на много от твърденията и условията, които е желателно да бъдат изразени. Затова ще дефинираме един по-широк клас от думи над базисната азбука, които ще наричаме логически формули (или още формули на предикатното смятане, а за краткост просто формули). Дефиницията е индуктивна: 
    0. Всяка атомарна формула е логическа формула.
    1. Логическите символи true и false са логически формули.
    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 думата not(F) също е логическа формула (нарича се отрицание на F).
    4. За всяка променлива X и всяка логическа формула F думите for_all(X:F) и for_some(X:F) също са логически формули (наричат се съответно генерализация на F по X и екзистенциализация на F по X).

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

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

    Ще използваме и следните означения за логически формули: при n>1 формулите (F₁,F₂...,F_n) и (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 (знаците " и $ се четат съответно като "за всяко" и "за някое"). Току-що въведените означения за конюнкция и дизюнкция биха могли да се използват и при n=1 благодарение на уславянето, което приехме относно конюнкция и дизюнкция на едночленна редица от форнули. Ние ще си служим и с още един вид означения на конюнкцията и на дизюнкцията на n формули при n≥1, а именно ще означаваме конюнкцията и дизюнкцията на F₁, F₂, ..., F_n съответно с and(F₁, F₂,...,F_n) и с or(F₁, F₂,...,F_n). Празната конюнкция и празната дизюнкция ще означаваме още с and и с or без аргументи.

    Забележка 1. Всички логически формули са префиксни изрази над множеството W (в частта на съответното индуктивно доказателство, отговаряща на т. 2 от горната дефиниция, играе роля това, че празната дума е причислена към логическите символи). Като използваме еднозначния анализ на префиксните изрази над 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", с които на английски език започват термините за двата вида променливи). Дефиницията на двете множества е индуктивна и се състои от следните точки: 
    0. Ако F е атомарна формула, то FVAR(F)=VAR(F), BVAR(F)=Ж.
    1. Ако F е някоя от формулите true и false, то FVAR(F)=BVAR(F)=Ж.
    2. Ако F е някоя от формулите (F₁,F₂...,F_n) и (F₁;F₂...;F_n), където n е цяло число, по-голямо от 1, и 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. Логическите символи true и false са безкванторни формули.
    2. При всеки избор на цяло число n, по-голямо от 1, и на безкванторни формули F₁, F₂, ..., F_n думите (F₁,F₂...,F_n) и (F₁;F₂...;F_n) също са безкванторни формули.
    3. За всяка безкванторна формула F думата not(F) също е безкванторна формула.

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

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

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

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

Previous  Next  Contents