ПРЕДСТАВЯНЕ НА ФОРМУЛИ В ПРЕНЕКСЕН ВИД
По естествен начин се дефинира индуктивно какво значи една формула да има даден брой квантори, при което броят е винаги неотрицателно цяло число. А именно:
БК0. Ако a е атомарна формула, то a има 0 квантори.
БК1. Ако j има n квантора, то Шj също има n квантора.
БК2,3. Ако j има k квантора, а y има l квантора, то всяка от формулите
j&y и jЪy има k+l квантора.
БК4,5. Ако j има n квантора и x е променлива, то всяка от формулите
"xj и $xj има n+1 квантора.
Чрез индукция, съобразена с дефиницията за формула, веднага се получава,
че за всяка формула j съществува точно едно неотрицателно цяло число n, такова, че
j има n квантора (при доказателството за единственост се използва и еднозначността
на синтактичния анализ на формулите). Разбира се, за въпросното n ще
казваме, че е броят на кванторите на j. Пак чрез индукция, съобразена с дефиницията
за формула, се показва още, че една формула е безкванторна точно тогава,
когато броят на кванторите й е 0, и че винаги, когато s е преименуваща
субституция, за всяка формула j съответната й формула s#(j) има същия брой
квантори както j.
За една формула ще казваме, че е в пренексен вид, ако тя има вида
K1K2...Knq,
където q е безкванторна формула, n е неотрицателно цяло число и всяка от думите
K1, K2, ..., Kn е квантор за общност или квантор за съществуване относно
някоя променлива. Ясно е, че универсалните формули (в частност безкванторните
формули) са формули в пренексен вид, но освен тях има и много други в такъв
вид.
Забележка 1. Ако в горната дефиниция поискаме допълнително кванторите K1,
K2, ..., Kn да са относно две по две различни променливи, ние бихме стеснили
обема на понятието формула в пренексен вид, но това ограничение не би било съществено,
защото всяка формула в пренексен вид в първоначалния смисъл би била
еквивалентна на формула в пренексен вид в новия смисъл (получена като в случай
на квантори относно една и съща променлива се остави само най-десният от тях).
Следващата теорема ще играе важна роля в по-нататъшната ни работа.
Теорема за представимост в пренексен вид. Всяка формула е еквивалентна на
някоя формула в пренексен вид, имаща същите свободни променливи както дадената.
Доказателство. Ще използваме следните еквивалентности, където j и q са
произволни формули, x е променлива, K е квантор за общност или квантор за съществуване
относно някоя променлива, която не е свободна променлива на q, а l
е кой да е от знаците "&" и "Ъ":
(1) Ш"xj
$xШj, Ш$xj"xШj,
(2) (Kjlq)K(jlq), (qlKj)K(qlj).
Верността на еквивалентностите (1) беше отбелязана във въпроса "Следване на
една формула от друга. Еквивалентни формули". Тъй като втората от еквивалентностите
(2) следва съвсем лесно от първата, ще се ограничим с доказателство на
първата. Възможни са четири случая според вида на квантора K и на знака l. Ще разгледаме
подробно единия от тях - онзи, в който K е квантор за общност, а l е
знакът "Ъ" (другите три се разглеждат аналогично или по-лесно). Нека K е "x,
където x е дадена променлива, която разбира се не е свободна променлива на q.
Тогава доказваната еквивалентност добива вида
"xjЪq"x(jЪq).
Нека S=(C,I) е произволна структура, а v е произволна оценка в S на променливите.
Целта ни ще бъде да докажем, че формулата "xjЪq е вярна в конфигурацията
(S,v) точно тогава, когато в тази конфигурация е вярна формулата "x(jЪq).
Да предположим най-напред, че "xjЪq е вярна в конфигурацията (S,v). В такъв
случай някоя от формулите "xj и q е вярна в (S,v). С цел да докажем, че и формулата
"x(jЪq) е вярна в (S,v), да означим с vў x,c-модификацията на v, където
c е произволен елемент на C. Споменатата цел ще бъде постигната, ако успеем да
покажем, че някоя от формулите j и q е вярна в конфигурацията (S,vў), защото
тогава и дизюнкцията им ще бъде вярна в тази конфигурация. А положението е наистина
такова - ако "xj е вярна в (S,v), то j ще бъде вярна в (S,vў) по семантиката
на квантора за общност, а ако q е вярна в (S,v), то q ще бъде вярна и в
(S,vў), защото оценките v и vў съвпадат върху свободните променливи на q. Сега
да предположим пък, че формулата "x(jЪq) е вярна в (S,v), и да допуснем, че
формулата "xjЪq не е вярна в (S,v). Тогава никоя от двете формули "xj и q не
е вярна в (S,v). Да означим отново с vў x,c-модификацията на v, където c е
произволен елемент на C. Поради верността на "x(jЪq) в (S,v), дизюнкцията
jЪq ще бъде вярна в (S,vў), а поради съвпадането на v и vў върху свободните
променливи на q формулата q няма да е вярна в (S,vў). Оттук заключаваме, че
формулата j е вярна в (S,vў). Тъй като това заключение е в сила при всеки избор
на елемента c на C, можем да твърдим, че формулата "xj е вярна в конфигурацията
(S,v), а нашето допускане ни беше довело до противоположното твърдение.
Полученото противоречие показва, че допускането е било погрешно и значи
формулата "xjЪq е вярна в (S,v).
Лесно се проверява, че във всяка от еквивалентностите (1) и (2) при направените
преди тях предположения двете страни на еквивалентността имат едни и
същи свободни променливи.
Да наречем временно една формула j редуцируема, ако тя е еквивалентна на
някоя формула със същите свободни променливи, но имаща вида Kc, където K е
квантор относно някоя променлива, а c е формула с брой на кванторите, по-малък
от този на j. Ще покажем, че всяка формула с положителен брой на кванторите е
редуцируема. За целта е достатъчно да докажем помощното твърдение, че всяка
формула е безкванторна или е редуцируема, а това ще направим чрез индукция,
съобразена с дефиницията за формула. За краткост да наречем (пак временно) една
формула нормална, ако тя е безкванторна или е редуцируема. Атомарните формули
са нормални, защото са безкванторни. Формулите от вида "xj и от вида $xj,
където x е променлива, а j е произволна формула, също са нормални, защото са
очевидно редуцируеми. Поради това за провеждането на индукцията остава да се
убедим, че нормалността се запазва при образуване на отрицание, на конюнкция и
на дизюнкция.
За случая на отрицание да предположим, че j е дадена нормална формула. Ще
трябва да покажем, че и формулата Шj е нормална. Ако j е безкванторна, то Шj е
също безкванторна и значи е нормална. Да разгледаме случая, когато j е редуцируема.
Тогава jKc, където K е квантор относно някоя променлива, c е някоя
формула, имаща по-малък брой квантори от j, и формулата Kc има същите свободни
променливи както j. Тогава, използвайки подходяща измежду еквивалентностите
(1), получаваме, че
ШjШKcK~Шc,
където K~ е другият вид квантор относно същата променлива както K, като при
това са верни равенствата
СВО(K~Шc)=СВО(ШKc)=СВО(Kc)=СВО(j)=СВО(Шj).
Като вземем пред вид още, че броят на кванторите се запазва при образуване на
отрицание, виждаме също, че броят на кванторите на Шc е по-малък от броя на
кванторите на Шj. С това е показано, че и формулата Шj е редуцируема, а значи
и нормална.
За случаите на конюнкция и на дизюнкция да предположим, че j и y са нормални
формули, а l е някой от знаците "&" и "Ъ". Ще покажем, че формулата jly
също е нормална. Ако и двете формули j и y са безкванторни, това е ясно, защото
тогава и jly ще бъде безкванторна. Затова да разгледаме случая, когато някоя
от тях е редуцируема. Нека например j е редуцируема. Тогава jKc, където
K е квантор относно някоя променлива, c е някоя формула, имаща по-малък брой
квантори от j, и свободните променливи на Kc са същите както на j. Ако променливата,
относно която е кванторът K, не е свободна променлива на y, оттук, използвайки
първата от еквивалентностите (2), получаваме, че
jlyK(cly),
като при това са налице равенствата
СВО(K(cly))=СВО(Kclj)=СВО(Kc)ИСВО(y)=СВО(j)ИСВО(y)=СВО(jly).
Тъй като броят на кванторите на формулата cly е по-малък от броя на кванторите
на формулата jly, с това е показано, че и jly сигурно е редуцируема, а значи и
нормална в случая, когато променливата, относно която е кванторът K, не е свободна
променлива на y. Случаят, когато въпросната свързана променлива е свободна
променлива на y, може да бъде сведен към него с помощта на теоремата за
преименуване на свързани променливи. Например, нека K="x, където x е свободна
променлива на y. Да изберем някоя променлива xў, която не е свободна променлива
нито на c, нито на y (такава променлива xў съществува, защото свободните
променливи на коя да е формула са крайно много, а множеството X на всички променливи
е безкрайно). Нека s е преименуващата субституция (x,xў:=xў,x). Тогава,
по споменатата теорема, Kcs#(Kc)="xўs#(c) и формулата "xўs#(c) има
същите свободни променливи както Kc. Освен това s#(c) има същия брой квантори
както c. Следователно ще имаме разгледаното преди малко положение, ако в качеството
на ново K вземем "xў, а в качеството на ново c - формулата s#(c).
След като по този начин завършихме доказателството на помощното твърдение,
можем да завършим и доказателството на теоремата за представяне в пренексен
вид. Това можем да направим чрез индукция относно броя на кванторите в разглежданата
формула. Да наречем една формула пренексно представима, ако тя е
еквивалентна на някоя формула в пренексен вид, имаща същите свободни променливи.
Формулите, чийто брой на кванторите е 0, са безкванторни и следователно те
самите имат пренексен вид, поради което разбира се са пренексно представими.
От друга страна, ако при дадено положително цяло число n всички формули с по-малко
от n квантори са пренексно представими, то и формулите с брой n на кванторите
ще бъдат пренексно представими благодарение на своята редуцируемост.
Забележка 2. Всъщност изложеното доказателство на теоремата за представи-
мост в пренексен вид позволява да се твърди, че всяка формула е еквивалентна
на някоя формула в пренексен вид, имаща същите свободни променливи както дадената
и не по-голям брой квантори от нейния. Доказателството на теоремата дава
и начин за намирането на такава еквивалентна формула, при която броят на кванторите
е същият както при дадената формула. Ако вместо част от еквивалентностите
от вида (2) се използват подходящи други еквивалентности, то за някои
формули могат да се намерят еквивалентни на тях формули в пренексен вид със
същите свободни променливи, но с по-малък брой квантори. Две еквивалентности,
които често са подходящи в това отношение, са следните:
"xj&"xy"x(j&y), $xjЪ$xy$x(jЪy)
(в тях x може да бъде произволна променлива, а j и y могат да бъдат произволни
формули; доказателството на еквивалентностите не представлява затруднение). С
помощта на тези еквивалентности могат да се преработват и формули от по-общите
видове "xj&"hy и $xjЪ$hy, където x и h са произволни променливи, а j и y -
произволни формули; това може да се прави като при x№h първо се извърши преименуване
на едната или евентуално на двете свързани променливи.
Пример. Ще представим в пренексен вид формулата "xp(x,y)&"yq(x,y), където x и y са различни променливи, а p и q са двуместни предикатни символи. Можем да си послужим със следната верига от еквивалентности, където z е променлива, различна от x и от y:
"xp(x,y)&"yq(x,y)"zp(z,y)&"zq(x,z)"z(p(z,y)&q(x,z)).
Ако бихме следвали метода, произтичащ от доказателството на теоремата, би
трябвало да си послужим примерно с веригата от еквивалентности
"xp(x,y)&"yq(x,y)"zp(z,y)&"yq(x,y)"z(p(z,y)&"yq(x,y))"z(p(z,y)&"uq(x,u))"z"u(p(z,y)&q(x,u)),
където z и u са две нови променливи; резултатът би съдържал един квантор повече от резултата, получен по другия начин.
Последно изменение: 26.07.1999 г.