СЕМАНТИЧНИ ТАБЛИЦИ. ЛЕМА НА БЕТ

    Понятието семантична таблица е въведено и успешно използвано от холандския логик Еверт Бет (Evert W. Beth).

    Ще разглеждаме термове, формули и секвенции над дадена сигнатура, в която има поне една константа, като една избрана измежду константите ще означаваме с α (в следващите въпроси ще стане нужда да са налице безбройно много константи). За краткост ще се занимаваме само с формули, построени без използуване на други логически знаци освен ¬, & и , и под думата "формула" по-нататък ще разбираме съответно формула от този вид, а под думата "секвенция"    секвенция, съставена от такива формули (за произволни формули и секвенции разглежданията се разпространяват без да възникват трудности от принципен характер).

    Една наредена двойка (Γ,Δ) от множества от формули (в частност, една секвенция) ще наричаме затворена, ако всички формули от множеството ΓΔ са затворени. За една константа ще казваме, че участва в  (Γ,Δ), ако участва в някоя формула от множеството ΓΔ. Ако е дадена една затворена двойка (Γ,Δ) от множества от формули, нейно съответно множество от константи ще наричаме множеството на константите, участващи в нея, при условие, че то не е празно, и множеството с единствен елемент α в противен случай. Един терм ще наричаме допустим за такава двойка (Γ,Δ), ако той е затворен и всички участващи в него константи принадлежат на множеството от константи, съответно на (Γ,Δ) (т.е. ако принадлежи на ербрановия универсум, отговарящ на въпросното множество от константи и евентуално наличните в сигнатурата функционални символи с ненулев брой аргументи).

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

    Пример 1. Ако a е константа, p и q са едноместни предикатни символи, а r е двуместен предикатен символ, то секвенциите

x¬(p(x)&q(x)), x p(x), p(a), ¬(p(a)&q(a)) -: ¬x p(x), p(a)&q(a), q(a),
x¬y r(x,y), ¬y r(a,y) -: y r(a,y), r(a,a)
са семантични таблици.

    Пример 2. Ако S е такава структура, че всеки елемент на нейния носител е стойност в S на някой затворен терм, Γ е множеството на всички затворени формули, които са верни в S, а Δ е множеството на всички затворени формули, които не са верни в S, то наредената двойка (Γ,Δ) е семантична таблица.

    Забележка 1. Лесно се вижда, че условието ST( ) при наличието на останалите условия от дефиницията е равносилно с изискването Γ и Δ да нямат общи атомарни формули.

    Забележка 2. В условието ST( -: ) вместо "терм τ, допустим за (Γ,Δ)" би могло да се напише "затворен терм τ". Това е така, защото всички термове, допустими за (Γ,Δ) са затворени, а от друга страна, ако за даден затворен терм τ формулата [ξ/τ]φ принадлежи на Δ, то без ограничение на общността можем да смятаме, че термът τ е допустим за (Γ,Δ)    той очевидно е такъв, когато ξ е свободна променлива на φ, а в останалите случаи можем да го заменим с кой да е терм, допустим за (Γ,Δ).

    Лема на Бет. Ако (Γ,Δ) е семантична таблица, то съществува такава структура S, че всички формули от Γ са верни в S, а всички формули от Δ са неверни в S.

    Доказателство. Нека наредената двойка (Γ,Δ) е семантична таблица и нека H е множеството на всички термове, допустими за (Γ,Δ). Благодарение на това, че Γ и Δ нямат общ елемент, можем да построим такава ербранова структура S с носител H, че всички атомарни формули, принадлежащи на Γ, да бъдат верни в S, а всички атомарни формули, принадлежащи на Δ, да бъдат неверни в S. Ще докажем, че всички формули от Γ са верни в S, а всички формули отΔ са неверни в S. За целта да наречем логическа дължина на една формула естественото число, дефинирано чрез следната индуктивна дефиниция: логическата дължина на атомарна формула е 0, логическата дължина на ¬φ и на ξφ е с 1 по-голяма от логическата дължина на φ, логическата дължина на φ&ψ е равна на сбора от логическите дължини на φ и ψ, увеличен с 1. Очевидно логическата дължина на една формула се запазва при субституция. С индукция относно логическата дължина ще покажем, че за всяка формула θ са верни следните твърдения: а) ако θΓ, то θ е вярна в S; б) ако θΔ, то θ е невярна в S.

    За формулите θ с логическа дължина 0 тези твърдения са верни благодарение на избора на S. Предполагайки, че твърденията а) и б) са верни за формули θ, чиято логическа дължина не надминава дадено естествено число h, да разгледаме формула θ с логическа дължина h+1.

    Ако θ има вида ¬φ, то верността на твърденията а) и б) се получава лесно с използуване съответно на условията ST(¬ -: ) и ST( -: ¬) и на индуктивното предположение. Аналогично е положението и в случая, когато θ е конюнкция на две формули.

    Ще разгледаме по-подробно случая, когато θ е от вида ξφ. За да докажем верността на твърдението а), да предположим, че θΓ. Ще трябва да докажем, че θ е вярна в S, а за това е достатъчно да покажем, че формулата φ е вярна в S при произволна оценка на променливите. Нека v е такава оценка и нека τ е термът v(ξ). Благодарение на условието ST( -: ) формулата [ξ/τ]φ принадлежи на Γ, а оттук с помощта на индуктивното предположение заключаваме, че тя е вярна в S. Следователно формулата φ е вярна в S при оценката [ξ/τ]S(v), която обаче съвпада с v поради равенството τS=τ. Аналогично се доказва и верността на твърдението б) (правим предположение, че θΔ, след което прилагаме условието ST( -: ) и избираме терм τ от H, за който [ξ/τ]φΔ). 

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

x¬(p(x)&q(x)) -: ¬x p(x),
x¬y p(x,y) -: ,
което показва, че от формулата x¬(p(x)&q(x)) не следва формулата ¬x p(x), а формулата x¬y p(x,y) е изпълнима. Оказва се, че използуването на лемата в подобен дух може да се развие до систематичен метод, който да позволява и установяване на тъждествена вярност за всяка тъждествено вярна затворена секвенция. Това ще бъде показано в следващия въпрос.

 

Последно изменение във файла:  9 януари 2006 г.