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

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

1. 
   Predikatlar hisobining aksiomalari sistemasi.
   
2. 
   Umumiylik va mavjudlik kvantorlarini kiritish qoidasi.
   

1. 
   Predikatlar hisobining aksiomalari sistemasi.
   

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)

Birinchi guruh aksiomalari:
I₁ .
I₂ .
Ikkinchi guruh aksiomalari:
II₁ .
II₂ .
II₃ .
Uchinchi guruh aksiomalari:
III₁ .
III₂ .
III₃ .
To‘rtinchi guruh aksiomalari:
IV₁ .
IV₂ .
IV₃ .
va ikkita qo‘shimcha
, ,
aksiomalardan iborat sistema bo‘lishi mumkin, bu yerda o‘zgaruvchi o‘zgaruvchini o‘z ichiga olmaydi.
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.
O'zgartirish qoidalari
Agar erkin x o'zgaruvchini o'z ichiga olgan F (x) formulada barcha x o'rniga t atamasini almashtirsak, u holda F (t) formulani hosil qilamiz.
Ushbu fakt quyidagicha yoziladi:
_x ^t F(x)
F(t).
Misol uchun,

1. 
   _x1^x2x₃( P²₁(x₁, x₃) P₂ (x₂))
   

x₃( P²₁(x₂, x₃) P₂ (x₂)).
Bu to'g'ri almashtirishdir, chunki x1 erkin o'zgaruvchidir.

2. 
   _x1^{f(x2, t)} _x3( P²₁(x₁, x₃) P₂ (x₂))
   

_x3( P²₁(f(x2, t), x₃) P₂ (x₂)).
Bu to'g'ri almashtirishdir, chunki x1 erkin o'zgaruvchidir.



3. _x3^x2_x3( P²₁(x₁, x₃) P₂ (x₂))
_x3( P²₁(x₁, x₂) P₂ (x₂)).

Bu noto'g'ri almashtirish. Chunki x3 mavjudlik kvantori bilan bog'langan.

4. _x2^x3_x3( P₁(x₁, x₃) P₂ (x₂))
_x3( P₁(x₁, x₃) P₂ (x₃)).
Bu noto'g'ri almashtirish. Chunki P2 (x3) predikati mavjudlik kvantori doirasiga kiradi.

To'g'ri almashtirish tushunchasi, masalan, umumiylik miqdorni olib tashlash uchun qonunlarni shakllantirish uchun zarurdir

_x F(x)

F(t)

va ekzistensial miqdorni kiritish

F (t)
xF(x).
Kvantorlarni kiritish va olib tashlash qoidalari