Mavzu15. Predikatlar hisobining aksiomalari sistemasi. Umumiylik va mavjudlik kvantorlarini kiritish qoidasi. Reja

Eng keng tarqalgan qoidalar:

1. 
   Umumiy kvantorini kiritish: "agar F₁(t) F₂(x) ketirib chiqariluvchi formula bo'lsa va F₁(t) tarkibida erkin x o'zgaruvchisi bo'lmasa, u holda F₁(t) x(F₂(x)) ham shuningdek, keltirib chiqariluvchi», ya'ni
   

(F₁(t) F₂(x))

(F₁(t) _x(F₂(x))).

2. 
   Umumiy kvantorini olib tashlash: "agar x(F(x)) ketirib chiqariluvchi formula bo'lsa, u holda x erkin o’zgaruvchining o'rniga t atamani almashtirib, F (t) ketirib chiqariluvchi formulasini olish mumkin, ya'ni,
   

x(F(x))
. F (t).

3. 
   Mavjudlik kvantorini kiritish: "agar t o’zgaruvchisi F(t) predikatiga kiritilgan bo'lsa, u holda , hech bo’lmaganda bitta shunday x predmrtli o’zgaruvchi mavjudki, u x(F(x)) predikat talablarini qanoatlantiradi” ya’ni
   

F(t)
x(F(x)).

4. 
   Kvantolarni o’zgartirish;
   

x(F(x)) x(F(x))
x(F(x)); x(F(x)).
Isbot:
x(F(x))=  (x(F(x)))=  x( F(x)) ya’ni matematik isbotlasak,
x(F(x))=F₁(a₁)  F₁(a₁)  F₂(a₂) …xє{ a_1, a_2…}
 x( F(x))=  (F₁(a₁)  F₁(a₁)  F₂(a₂) …xє{ a_1, a_2…}

1. 
   
2. 
   5) t o’zgaruvchi x o’zgaruvchini o’z ichiga olmagan holda kvantorni o’tkazish:
   
3. 
   
4. 
   a) _x(F₁(x)) F₂(t)
   

_x(F₁(x) F₂(t));



b) _x(F₁(x))F₂(t)
_x(F₁(x) F₂(t);

c)
F₁(t) _x(F₂(x))

_x(F₁(t)F₂(x));



d) _x(P(x))F(t)
_x(P(x)F(t));
e)
_x(P(x))F(t)

_x(P(x)F(t)).

6) yangi o'zgaruvchini kiritish:


a) _x(F₁(x))_x(F₂(x))
_y_x(F₁(y) F₂(x));


b) _x(F₁(x))_x( F₂(x))
_y_x(F₁(y)  F₂(x)).


Xulosa qoidalari
Xulosa chinligini aniqlash uchun ikkita asosiy qoidalar mavjud:

1. 
   agar F1 va (F₁F₂) keltirib chiqariladigan formulalar bo'lsa, unda F2 ham keltirib chiqariladigan formula bo'ladi. Bu modus ponens (m.p) qoidasidir.
   

F₁; (F₁F₂)
F_2.

2. 
   agar F₂ va (F₁F₂) keltirib chiqariladigan formulalar bo'lsa, u holda F₁ ham keltirib chiqariladigan formula bo'ladi. Bu modus tollens (m.t) qoidasidir.
   

F₂; (F₁F₂)
F_1.
Ushbu qoidalar xulosa sxemasini belgilaydi va almashtirish qoidalaridan foydalanishga imkon beradi, kvantorlarni kiritish va olib tashlash va xulosaning chinligi to'g'risida xulosa qilish imkonini beradi.


Aksiomatik predikatlar hisobi haqida. Aksiomatik predikatlar nazariyasini ham xuddi aksiomatik mulohazalar nazariyasi kabi yaratish mumkin. Bu yerda quyidagilarni ko‘rsatish zarur:
1. Predikatlar hisobi formulasining ta’rifi predikatlar mantiqi formulasining ta’rifi bilan bir xil.
2. Predikatlar hisobi aksiomalar sistemasini tanlashni (xuddi mulohazalar hisobidagidek) har xil amalga oshirish mumkin. Shunday aksiomalar sistemasidan bittasi quyidagi: mulohazalar hisobining o‘n bir aksiomasi (4ta guruh aksiomalar) va ikkita qo‘shimcha aksioma
, ,
aksiomalardan iborat sistema bo‘lishi mumkin, bu yerda o‘zgaruvchi o‘zgaruvchini o‘z ichiga olmaydi.
3. Mulohazalar hisobidagi keltirib chiqarish qoidasiga yana ikkita qoida qo‘shiladi:
a) umumiylik kvantorini kiritish qoidasi


;
b) mavjudlik kvantorini kiritish qoidasi –
, agar ga bog‘liq bo‘lmasa.
4. Xulosa va isbotlanuvchi formula tushunchalari xuddi mulohazalar hisobidagi kabi aniqlanadi.
5. Xuddi hamma aksiomatik nazariyalardagidek ushbu muammolar ko‘riladi:
a) yechilish, b) zidsizlik, d) to‘liqlik, e) erkinlik.


Muammoli masala va topshiriqlar

1. 
   Ushbu kvantorli mulohazalarning inkorlarini toping:
   

a) ; b) ;
d) ; e) ;
f) ;
g) ; h) ;
i) ;
j) ; k) .