Съдържание 
 

ПРЕДИКАТНО СМЯТАНЕ С РАВЕНСТВО

    В повечето от математическите теории наред с други математически понятия играе роля и понятието равенство. Равенството е едно отношение между обекти на теорията, на което свойствата могат да се опишат в подходящ вариант на предикатното смятане, наречен предикатно смятане с равенство (досега разглежданото предикатно смятане ще наричаме общо предикатно смятане).

    Можем да считаме, че езикът на предикатното смятане с равенство е същият, както на общото предикатно смятане, но при условие, че множеството на двуместните предикатни символи не е празно и сред тях е избран един, който ще наричаме символ за равенство . За определеност ще приемем, че това е символът eq (aтомарна формула от вида eq(τ,τ'), където τ и τ' са термове, ще си позволяваме да записваме и във вида (τ=τ')). Ще предполагаме, че е дадена една сигнатура Σ, в която eq е двуместен предикатен символ, и ще считаме, че всички структури, които разглеждаме, са с тази сигнатура. Ще считаме също, че всички разглеждани термове и формули са при сигнатура Σ, и т.н.

    Една структура S ще наричаме нормална, ако eqS е предикатът за равенство в носителя на S. Редица понятия, които въведохме за общото предикатно смятане, като използвахме произволни структури, имат свои аналози за предикатното равенство с равенство, дефинирани по подобен начин, но с използването само на нормални структури. Например на досегашното понятие тъждествено вярна формула ще съответства понятието тъждествено вярна формула на предикатното смятане с равенство  –  то ще означава формула, която е тъждествено вярна във всяка нормална структура. Под модел в предикатното смятане с равенство на едно множество Γ от формули ще разбираме нормална структура, в която са тъждествено верни всички формули от Γ. Аналогично се дефинират за предикатното смятане с равенство изпълнимост на формула и на множество от формули, следване на една формула от дадено множество от формули и еквивалентност на две формули.

    Разбира се, всяка формула, която е тъждествено вярна в общото предикатно смятане, ще бъде тъждествено вярна и в предикатното смятане с равенство. Обратното обаче не е вярно и като пример за това може да послужи формулата eq(x,x).

    Ще изброим някои затворени формули, тъждествено верни в предикатното смятане с равенство, които ще наричаме аксиоми на равенството (всяка от тези формули е универсално затваряне на някоя безкванторна формула и проверката на тъждествената вярност в нормалните структури се свежда до такава проверка за въпросната безкванторна формула). Приемаме за аксиоми на равенството формулите от следните пет вида (за краткост и за по-голяма интуитивна яснота сме ги записали с използване на знак за равенство вместо с използване на символа eq, който те фактически съдържат):
    1) ∀ξ(ξ=ξ), където ξ е коя да е променлива.
    2) ∀ξ∀η((ξ=η)→(η=ξ)), където ξ и η са различни помежду си променливи.
    3) ∀ξ∀η∀ζ(((ξ=η)&(η=ζ))→(ξ=ζ)), където ξ, η и ζ са различни помежду си променливи.
    4) ∀ξ1…∀ξn∀η1…∀ηn(((ξ1=η1)&…&(ξn=ηn))→(ω(ξ1,…,ξn)=ω(η1,…,ηn)), където ω e n-местен функционален символ с n>0 и ξ1, …, ξn, η1,…, ηn са различни помежду си променливи.
    5) ∀ξ1…∀ξn∀η1…∀ηn(((ξ1=η1)&…&(ξn=ηn)&π(ξ1,…,ξn))→π(η1,…,ηn)), където π e n-местен предикатен символ с n>0, различен от eq, и ξ1, …, ξn, η1,…, ηn са различни помежду си променливи.

    Формулите от първите три вида се наричат съответно аксиоми за рефлексивност, за симетрия, за транзитивност, а формулите от последните два вида се наричат съответно аксиоми за замяна за функционалните символи и аксиоми за замяна за предикатните символи. Конкретният избор на променливите във всяка една от изброените формули не е съществен  –  ако вместо едни променливи изберем други, ще получим формула, еквивалентна на дадената в общото предикатно смятане (а следователно и в предикатното смятане с равенство). Например нека при даден избор на различните променливи ξ и η формулата от вида 2), т.е. формулата

∀ξ∀η(eq(ξ,η)→ eq(η,ξ)),
е вярна в дадена структура S (не непременно нормална). Тогава в тази структура ще бъде тъждествено вярна безкванторната формула (eq(ξ,η)→ eq(η,ξ)). Ако ξ' и η' са друга двойка от различни променливи, то формулата (eq(ξ',η')→ eq(η',ξ')) е неин частен случаи (получава се от нея чрез прилагане на субституцията [ξ/ξ',η/η']) и следователно също е тъждествено вярна в структурата S. Оттук обаче можем да заключим, че в тази структура ще бъде вярна затворената формула
∀ξ'∀η'(eq(ξ',η')→ eq(η',ξ')).

    Забележка. Формулите от петия вид, които биха се получили при π = eq, имат вида

∀ξ1∀ξ2∀η1∀η2(((ξ1=η1)&(ξ2=η2)&(ξ1=ξ2))→(η1=η2)),
където ξ1, ξ2, η1, η2 са различни помежду си променливи. Те също са тъждествено верни в предикатното смятане с равенство, но не се причисляват към аксиомите на равенството, защото следват в общото предикатно смятане от аксиомите за симетрия и за транзитивност. Действително нека в дадена структура S са верни формулите
∀ξ∀η(eq(ξ,η)→ eq(η,ξ)),   ∀ξ∀η∀ζ((eq(ξ,η)& eq(η,ζ)) → eq(ξ,ζ)),
където ξ, η и ζ са различни помежду си променливи, и нека ξ1, ξ2, η1, η2 са различни помежду си променливи. Ще покажем, че в S е тъждествено вярна формулата
((eq(ξ1,η1)& eq(ξ2,η2)& eq(ξ1,ξ2)) → eq(η1,η2))
и следователно е вярна формулата, получена от нея чрез добавяне отляво на думата ∀ξ1∀ξ2∀η1∀η2. За целта ще използваме, че в S са тъждествено верни формулите
(eq(ξ,η)→ eq(η,ξ)),   ((eq(ξ,η)& eq(η,ζ)) → eq(ξ,ζ))
и следователно са тъждествено верни техните частни случаи
(eq(ξ1,η1)→ eq(η1,ξ1)),   ((eq(ξ1,ξ2)& eq(ξ2,η2)) → eq(ξ1,η2)),   ((eq(η1,ξ1)& eq(ξ1,η2)) → eq(η1,η2)).
Да предположим сега, че конюнкцията (eq(ξ1,η1)& eq(ξ2,η2)& eq(ξ1,ξ2)) е вярна в S при дадена оценка v. Тогава в S при оценката v ще бъдат верни формулите eq(ξ1,η1), eq(ξ2,η2) и eq(ξ1,ξ2), а оттук и от тъждествената вярност в S на отбелязаните преди малко три импликации лесно заключаваме, че в S при оценката v ще бъде вярна и формулата eq(η1,η2)).

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

    Основна теорема за структурите, в които са верни аксиомите на равенството. Ако S е структура, в която са верни всички аксиоми на равенството, то съществува такава конгруентност R в S, че фактор-структурата S/R е нормална.

    Доказателство. Нека S е структура, в която са верни аксиомите на равенството. Да означим с R множеството на истинност на предиката eqS. Ще покажем, че така дефинираното R е конгруентност в S. Като използваме верността в S на първите четири вида аксиоми на равенството, лесно виждаме, че R има свойствата рефлексивност, симетричност, транзитивност и съгласуваност с функциите на S. Например проверката на симетричността изглежда така: ако d и d' са елементи на носителя на S, удовлетворяващи условието dRd', то, като вземем две различни променливи ξ и η и оценка v в S, за която v(ξ) = d, v(η) = d', можем да твърдим, че формулата eq(ξ,η) е вярна в S при оценката v, а оттук и от тъждествената вярност в S на импликацията (eq(ξ,η)→ eq(η,ξ)) е ясно, че формулата eq(η,ξ) също е вярна в S при оценката v и значи имаме съотношението d'Rd. Като имаме пред вид забележка 1 от текста „Факторизация на структура относно конгруентност в нея“, за да завършим доказателството, че R е конгруентност в S, достатъчно е да покажем, че е налице вариантът на съгласуваността с предикатите на S, при който знакът за равенство е заменен със знака  ≤ . Това можем да направим, като използваме, че всеки път, когато π e n-местен предикатен символ с n>0 и ξ1, …, ξn, η1,…, ηn са различни помежду си променливи, в S е вярна формулата

∀ξ1…∀ξn∀η1…∀ηn(eq(ξ1,η1)&…& eq(ξn,ηn)& π(ξ1,…,ξn)) → π(η1,…,ηn))
(когато предикатният символ π е различен от eq, тази формула е една от аксиомите на равенството, а когато π е символът eq, верността й се вижда от забележката по-горе). След като по този начин доказахме, че R наистина е конгруентност в S, можем да се възползваме от забележка 2 от текста „Факторизация на структура относно конгруентност в нея“, вземайки в качеството на π символа eq.  □

    Току-що доказаната теорема позволява редица въпроси за предикатното смятане с равенство да се свеждат към въпроси за общото предикатно смятане. Два примера за такова свеждане се посочват от следващата теорема.

    Сводимост на въпросите за тъждествена вярност и за съществуване на модел в предикатното смятане с равенство към въпроси за общото предикатно смятане. Нека Ε е такова подмножество на аксиомите на равенството, че всяка от тях е еквивалентна в общото предикатно смятане на някоя формула от Ε. Тогава:
      1. Една формула е тъждествено вярна в предикатното смятане с равенство точно тогава, когато тя следва от Ε в общото предикатно смятане.
      2. Едно множество от формули Γ притежава модел в предикатното смятане с равенство точно тогава, когато обединението на множествата Γ и Ε притежава модел в общото предикатно смятане.

    Доказателство. Множеството Ε се състои от затворени формули, които са верни във всяка нормална структура. Поради това, ако една формула следва от Ε в общото предикатно смятане, тя ще бъде тъждествено вярна във всяка нормална структура, т.е. ще бъде тъждествено вярна в предикатното смятане с равенство. Също така, ако едно множество от формули Γ притежава модел в предикатното смятане с равенство, този модел е нормална структура, в която са тъждествено верни всички формули от Γ, и следователно в тази структура са тъждествено верни всички формули от обединението на Γ и Ε, т.е. тя е модел за това обединение. Остава да се убедим, че ако ако една формула е тъждествено вярна в предикатното смятане с равенство, то тя следва от Ε в общото предикатно смятане, и ако обединението на множествата Γ и Ε притежава модел в общото предикатно смятане, то множеството Γ притежава модел в предикатното смятане с равенство. За доказателството на първото от тези две твърдения да предположим, че една формула φ е тъждествено вярна в предикатното смятане с равенство, и да разгледаме произволна структура S, в която формулите от Ε са верни. Тогава в S са верни всички аксиоми на равенството и благодарение на това съществува конгруентност R в S, за която фактор-структурата S/R е нормална. Поради направеното предположение за формулата φ тя е тъждествено вярна в S/R, а оттук по теоремата за елементарна еквивалентност на структурата и фактор-структурата заключаваме, че φ е тъждествено вярна и в S. Значи при въпросното предположение φ следва от Ε в общото предикатно смятане. За доказателството на второто от твърденията да предположим, че обединението на множествата Γ и Ε притежава някакъж модел S в общото предикатно смятане. Понеже в структурата S отново са верни всички аксиоми на равенството, пак съществува конгруентност R в S, за която фактор-структурата S/R е нормална. Тази нормална структура е модел за Γ, тъй като формулите от Γ, бидейки тъждествено верни в S, ще бъдат тъждествено верни и в S/R. Значи S/R е модел за Γ в предикатното смятане с равенство.  □

    Фактически и двата въпроса за общото предикатно смятане, към които става свеждането в горната теорема, по същество са въпроси за съществуване или несъществуване на модел в общото предикатно смятане. За втория от въпросите това е ясно направо, а за първия то се вижда, като забележим, че след замяна на разглежданата формула с нейно универсално затваряне можем да считаме, че тя е затворена, а тогава нейното следване от множеството Ε е равносилно с несъществуване на модел за множеството, получено от Ε чрез добавяне на нейното отрицание. При това положение за решаването на тези въпроси по принцип могат да се използват изучените дотук методи, които в крайна сметка довеждат нещата до прилагане на метода на резолюцията. Оказва се обаче, че дизюнктите, произлизащи от повечето аксиоми на равенството, често увеличават силно обема на работата по този метод и практическото му използване става затруднително. Ето защо в такива случаи се оказва целесъобразно от дизюнктите, произлизащи от аксиоми на равенството, да се включи само един, а именно някой дизюнкт от вида { eq(ξ,ξ)}, където ξ е променлива, но пък освен извършването на резолюция да се разреши още едно действие, наречено парамодулация. Няма да се спираме на неговото описание, а само ще споменем, че то има връзка с един специален случай (случая, когато φ е литерал) на следното твърдение.

    Закон за замяна във формула. Нека φ е формула, ξ е променлива, а и са такива термове, а τ1 и τ2 са такива термове, че субституциите [ξ/τ1] и [ξ/τ2] са приложими към φ. В такъв случай формулите ((τ1=τ2)&[ξ/τ1]φ)→[ξ/τ2]φ и ((τ1=τ2)&[ξ/τ2]φ)→[ξ/τ1]φ са тъждествено верни в предикатното смятане с равенство.

    Доказателство. Ще се ограничим с твърдението за първата от формулите в заключението, защото положението при втората е съвсем аналогично. Да предположим, че в дадена нормална структура S формулата (τ1=τ2)&[ξ/τ1]φ е вярна при дадена оценка v. Тогава имаме равенството τ1S,v = τ2S,v и формулата φ е вярна в S при оценката v[ξ→τ1S,v]. Тъй като току-що споменатата оценка съвпада с оценката v[ξ→τ2 S,v], получаваме, че и формулата [ξ/τ2]φ е вярна в S при оценката v.  □

    По подобен начин се доказва и следното твърдение.

    Закон за замяна в терм. Нека τ, τ1 и τ2 са термове, а ξ е променлива. Тогава формулата (τ1=τ2)→([ξ/τ1]τ=[ξ/τ2]τ) е тъждествено вярна в предикатното смятане с равенство.

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