Както обикновено, по-нататък ще пропускаме словосъчетанието „при сигнатура Σ“, но ще го подразбираме там, където е нужно.

      Пример 1. Всеки литерал е формула. Ako λ е отрицателен литерал, то думата not(λ) е формула, която не е литерал.

      Пример 2. Нека сигнатурата Σ има триместен предикатен символ m. Тогава думата

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

      Ще използваме следните означения за формули:
          1. Формулата not(φ) ще означаваме с  ¬φ  (такъв начин на нейното означаване сме използвали и досега в случая, когато φ е атомарна формула; и в разглеждания тук по-общ случай знакът  ¬  се чете като „не“).
          2. Формулите (φ,ψ) и (φ;ψ) ще означаваме съответно с  φ & ψ  и с  φ ∨ ψ  (знаците  &  и  ∨  се четат съответно като „и“ и „или“, като вместо първия от тях понякога се използва още и знакът  ∧ ; наричат се съответно знак за конюнкция и знак за дизюнкция).
          3. Уславяйки се да пишем ∀ξ  вместо (,ξ) и ∃ξ  вместо (;ξ), формулите (,ξ)φ и (;ξ)φ ще означаваме съответно с  ∀ξ φ  и с  ∃ξ φ  (знаците  ∀  и  ∃  се четат съответно като „за всяко“ и „за някое“; наричат се съответно квантор за общност и квантор за съществуване, като думите ∀ξ  и ∃ξ  се наричат квантор за общност по ξ и квантор за съществуване по ξ).

      Пример 3. Ако φ е произволна формула, то формулата not(not(φ)) може да бъде записана във вида ¬¬φ и да бъде прочетена „не не φ“. Интуитивно описаната по-горе семантика на формулите дава, че тя е вярна точно тогава, когато е вярна формулата φ.

      Пример 4. Формулите от пример 2 могат да бъдат записани по следния начин:

      С индукция, съобразена с дефиницията за формула, се показва, че всички формули са силно допустими думи (вж. въпроса „Осигуряване на еднозначен прочит с помощта на скоби и разделители“). Лесно се вижда, че не може да се случи една формула да бъде същевременно и терм  –  за атомарните формули това вече сме го проверили, а за останалите то следва от обстоятелството, че празната дума и думата not не са функционални символи. Като използваме лемата за еднозначнния прочит в съчетание с обстоятелството, че споменатите в предното изречение две думи не са и предикатни символи, виждаме, че за формулите е налице еднозначен прочит в следния смисъл: всяка формула може да се получи само по една от точките на индуктивната дефиниция на понятието и то само по един начин (за да покажем, че никоя формула, получена по точка 3 от дефиницията, не би могла да се получи по точка 2, можем да използваме това, че всяка формула започва с малка латинска буква или с лява скоба).

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

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

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

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

      Пример 5. Формулите, за които става дума в пример 1, са безкванторни, а формулите от пример 2 не са.

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