Следващите две твърдения ще играят съществена роля в по-нататъшната ни работа.

    Запазване на тъждествената вярност при преминаване към частен случай. Нека E е атомарна формула или клауза, тъждествено вярна в дадена структура S. Тогава всички частни случаи на E също са тъждествено верни в S.

    Доказателство. Нека s е произволна субституция. Ще докажем тъждествената вярност на s(E) в S. Първо ще разгледаме случая, когато E е атомарна формула. Нека v е произволна оценка в S на променливите. От необходимото и достатъчно условие за вярност на резултата от прилагане на субституция към атомарна формула знаем, че условието S,vs(Е) е равносилно с условието S,vўЕ, където vў=s_S(v). Второто от тези две условия обаче със сигурност е изпълнено благодарение на тъждествената вярност на A в S, следователно първото също е изпълнено. С това е доказано, че атомарната формула s(Е) наистина е тъждествено вярна в S. Преминаваме към случая, когато E е клауза. Нека главата и тялото на E да бъдат съответно H и B; тогава s(Е) е клаузата с глава s(H) и тяло s(B). Нека v е такава оценка в S на променливите, че в S при оценката v да е изпълнена целта s(B). Ще трябва да покажем, че S,vs(H). Да положим отново vў=s_S(v). Тогава по споменатото по-горе необходимо и достатъчно условие за вярност на резултат от прилагане на субституция можем да твърдим, че условието S,vs(H) е равносилно с условието S,vўH. Вследствие на тъждествената вярност в S на клаузата E последното условие сигурно ще бъде изпълнено, ако в S при оценката vў е изпълнена целта B. Ние обаче сме предположили, че в S при оценката v е изпълнена целта s(B), а оттук по следствието от същото необходимо и достатъчно условие се получава, че наистина целта B е изпълнена в S при оценката vў.  _ї 

    Изпълнимост на цел, имаща изпълним частен случай. Нека G е цел и нека някой частен случай на G е изпълним в дадена структура S. Тогава и целта G е изпълнима в S.

    Доказателство. Нека s е такава субституция, че целта s(G) да е изпълнима в S. Да означим с v такава оценка в S на променливите, че s(G) да е изпълнена в S при оценката v. Тогава G е изпълнена в S при оценката s_S(v) съгласно следствието от необходимото и достатъчно условие за вярност на резултата от прилагане на субституция към атомарна формула.  _ї

    Измежду частните случаи на термовете, атомарните формули, целите и клаузите особено внимание заслужават онези, които са затворени. Затова ще изкажем изрично онова, което дават доказаните по-горе две твърдения в тази насока. А именно, получаваме следните две твърдения:
    1. Нека E е атомарна формула или клауза, тъждествено вярна в дадена структура S. Тогава всички затворени частни случаи на E са верни в S.
    2. Нека G е цел и нека някой затворен частен случай на G е изпълнен в дадена структура S. Тогава целта G е изпълнима в S.

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

    Пример 1. Нека X₀ е променлива, c е константа, а f е едноместен функционален символ. Тогава са в сила равенствата

    Пример 2. Нека s₀ е произволна субституция. Тогава са в сила равенствата

    Пример 3. Нека U и V са две различни променливи. Тогава е в сила равенството

    Пример 4. Предполагайки отново, че U и V са две различни променливи, да приложим установеното в пример 3 с разменени роли на U и V. Получаваме равенството [V=:U][U=:V] = [V=:U], а значи и още един пример, че произведението на две субституции може да зависи от реда на множителите (това, че субституциите [U=:V] и [V=:U] са различни, се вижда например като сравним стойностите им за променливата U).

    Пример 5. Нека пак U и V са две различни променливи. Тогава е в сила равенството

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

    Прилагане на произведение на две субституции към термове, атомарни формули, цели и клаузи. Нека E е терм, атомарна формула, цел или клауза. Тогава за всеки две субституции s₁ и s₂ е в сила равенството

    Доказателство. Ако E е променлива, горното равенство следва направо от дефиницията на s₂s₁. Ако E е константа, равенството пак е вярно, защото тогава и двете му страни са равни на E. Нека сега E=f(E₁,E₂...,E_n), където n е положително цяло число, f e n-местен функционален символ и E₁, E₂, ...,E_n са такива термове, че при i=1,2,...,n е в сила равенството

    Следствие 1 (транзитивност на отношението "е частен случай на"). Нека E е терм, атомарна формула, цел или клауза. Нека Eў е частен случай на E, а Eўў от своя страна е частен случай на Eў. Тогава Eўў е частен случай на E.

    Доказателство. За някои субституции s₁ и s₂ имаме равенствата Eў=s₁(E),Eўў=s₂(Eў). Това дава

    Следствие 2 (асоциативен закон на умножението на субституции). За всеки три субституции s₁,s₂ и s₃ е в сила равенството

    Доказателство. За всяка променлива X имаме

    Благодарение на асоциативния закон можем без опасност от недоразумение всяко от двете произведения s₃(s₂s₁) и (s₃s₂)s₁ да запишем във вида s₃s₂s₁. Ще можем да пропускаме скоби и в по-сложни изрази, получени чрез по-голям брой прилагания на умножението на субституции.
 

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

Previous  Next  Contents