Проблем за разрешимостта на предикатната логика
1)Изявление на проблема:
Има ли алгоритъм, който би позволил да се съди по формата на предикатната логическа формула какъв е нейният характер (например дали е тавтология или формулата е просто осъществима).
Както е доказано (през 1936 г., Чърч), задачата има отрицателен отговор, т.е. предикатната логика е неразрешима.
2) Причината за неразрешимостта е наличието на безкрайни предметни области и, най-общо казано, различното поведение на формулата върху безкрайни и крайни множества. Така например има формула, която е приложима за безкраен набор, но не е приложима за нито един краен набор.
3) Въпреки това, при определени "преценки" на логиката на предикатите, ние получаваме разрешимостта на този проблем. Така, например, ако разгледаме само ограничени предметни области M=< а1, а2,... am >, тогава логиката на предиката ще бъде разрешима в този случай. Това следва от следната теорема.
Теорема.За всеки предикат Р(х) има еквивалентности: (xР(х))ó(P(a1)/\P(a2)/\. /\P(am)) (1)
( xP(x))—(P(a1) \/P(a2) \/. \/P(am)) (2)
Значението на твърдението е, че кванторните операции върху крайни множества не са последователни, а се изразяват чрез логически връзки /\, \/.
Доказателство.Докажете (1), (2) по същия начин.
а) P(x) е идентично вярно на M. В този случай и двете части на (1) приемат стойностите на истината.
b) В противен случай за всяко P(x) има невярно твърдение, но има „фалшив компонент“ в дясната страна на (1) като част от връзката, т.е. връзката е невярна.
И в двата възможни случая са получени твърдения с една и съща стойност на истината, което доказва еквивалентността на (1). Всяка формула върху краен набор, съгласно теорема (1), може да бъде"освободени" от кванторни операции. Но в този случай всеки компонент, включен във формулата на елементите на крайно множество, може да бъде реализиран само като верен или неверен, което означава, че механизмът на таблицата на истината в случай на крайно М се оказва приложим, като по този начин определя характера на формулите и следователно посоченият проблем е положително решен.
4) Оказва се, че логиката на едноместните предикати също е разрешима, тъй като ограничавайки се до едноместни предикати, можем да намалим проблема до случая на крайни множества (без доказателство).
5) И така, логиката на предикатите не е противоречива в смисъл, че една формула не може да бъде тавтология и опровержима (противоречие и осъществимо). Логиката на предикатите е завършена теория, т.е. всяка формула е или тавтология, или опровержима. И накрая, тя е неразрешима, т.е. няма нито един съответен алгоритъм. Това обаче не означава, че е невъзможно да се намери техника за определяне на същността й за определена формула: тази техника просто ще бъде приложима конкретно за нея или за цял клас формули, но не и за цялата логика като цяло.
Концепцията за предикатно смятане (PC).
1) Синтаксисът на теорията е същият като синтаксиса на предикатната логика.
Синтаксис - концепция за азбука и формула:
Субектна променлива, предикатна променлива 0 е локална, n е локална, логически връзки, ┐,→ и символи , .
Формулата е предикатна променлива и също така, ако P и Q са формули, тогава P→Q, xP, xQ са формули, където в последните два случая x трябва свободно да влиза във формулите P и Q.
2) Аксиомите на теорията, които се приемат като първоначално изводими формули:
б) както и аксиомите ( xP(x))→P(t) и P(t)→( xP(x)).
3) Правилото за извеждане на други формули:
B) Още две правила:
-Ако B→P(x) е изведено, тогава B→( xP(x))производен.
- Ако B→P(x) е изведено, тогава ( xP(x))→B е изведено.
Изводимостта на формула в LP се превръща в свойства на нейната тавтология. По-специално, IP аксиомите, приложими като извеждащи формули, се оказват тавтологии в LP, тъй като е лесно да се провери.
Правилата за извод в IP се трансформират в LP в правила за конструиране на нови тавтологии.
5)Метатеория.
а) IP не е противоречив;
b) IP е пълен, в смисъл, че всяка IP формула е или изведена, или не притежава това свойство.
в) IP е неразрешима теория (в противен случай цялата му семантика би била неразрешима, което не е вярно поради неразрешимостта на LP).