Teng kuchli formulalar va asosiy teng kuchliliklar Ta’rif

FORMAL AKSIOMATIK NAZARIYA
Mulohazalar algebrasini o‘rganganimizda bu asosan rostlik jadvali orqali ko‘pgina savollarga javob olgan edik. Mantiqning ba’zi qiyinroq masalalarini bu metod bilan xal qilish mumkin bo‘lmaganligi sababli, biz endi aksiomatik metodni qo‘llaymiz va aynan rost formulalar to‘plamini deduktiv sistema yordamida aniqlaymiz. Boshqacha aytganda, biz «dastlabki» aynan rost formulalar sifatida mulohazalar xisobi aksiomalarini aniqlaymiz va shu aksiomalardan xuddi shunday formulalarni keltirib chiqarish mumkin bo‘ladigan keltirib chiqarish qoidalarini ifodalaymiz. Bunday qoidalar mantiqa xizmat qilib, keltirib chiqarish jarayonini sof mexanik xisoblashlarga aylantirgani uchun ham mulohazalar mulohazalar xisobi atamasi paydo bo‘lgan.
Agar quyidagi shartlar bajarilsa, u holda formal (aksiomatik) nazariya aniqlangan xisoblanadi:

• 
  Agar quyidagi shartlar bajarilsa, u holda formal (aksiomatik) nazariya aniqlangan xisoblanadi:
  
• 
  Sanoqli simvollar to‘plami- nazariyaning simvollari berilgan bo‘lsa nazariyaning chekli simvollari ketma-ketligi ning ifodasi deyiladi.
  
• 
  nazariyaning formulalari deb ataluvchi ning ifodalari to‘plami berilgan bo‘lsa. (odatda, berilgan ifodaning formula bo‘lish bo‘lmasligini aniqlovchi effektiv jarayon beriladi).
  
• 
  nazariyaning aksiomalari deb ataluvchi formulalar majmuasi to‘plami ajratilgan bo‘lsa. (ko‘pgina hollarda nazariyaning berilgan formulasi aksioma bo‘lish yoki bo‘lmasligini effektiv aniqlash mumkin bo‘ladi; bu holda ni effektiv aksiomalashtirilgan yoki aksiomatik nazariya deyiladi).
  
• 
  Formulalar orasida keltirib chiqarish qoidalari deb ataluvchi chekli munosabatlar ketma-ketligi berilgan bo‘lsin. Har bir uchun shunday musbat butun soni topiladiki, ta formulalardan iborat xar qanday to‘plam uchun hamda ixtiyoriy formula uchun, berilgan ta formulalar formula bilan munosabatda bo‘ladimi, degan savol effektiv xal etilishi kerak. Agar bu savolga xa deb javob olinsa, u holda formula berilgan ta formulalarning qoidasi bo‘yicha bevosita natijasi deyiladi.
  

Agar formulalar ketma-ketligi berilgan bo‘lib, har qanday uchun formula yoki aksioma bo‘lsa, yoki o‘zidan oldingi qandaydir formulalarning bevosita natijasi bo‘lsa, u holda berilgan formulalar ketma-ketligi da keltirib chiqarish deyiladi.

• 
  Agar formulalar ketma-ketligi berilgan bo‘lib, har qanday uchun formula yoki aksioma bo‘lsa, yoki o‘zidan oldingi qandaydir formulalarning bevosita natijasi bo‘lsa, u holda berilgan formulalar ketma-ketligi da keltirib chiqarish deyiladi.
  
• 
  Agar da keltirib chiqarish mavjud bo‘lib, bu keltirib chiqarishning oxirgi formulasi formula bilan ustma-ust tushsa, u holda formula nazariyaning teoremasi deyiladi; bunday keltirib chiqarish formulaning keltirib chiqarishi deyiladi. (Berilgan nazariyaga nisbatan).
  
• 
  Xatto, effektiv aksiomalashtirilgan nazariyada ham, teorema tushunchasi effektiv bo‘lishi shart emas, chunki umuman olganda berilgan formulaning da keltirib chiqarilishi mavjudligini aniqlovchi effektiv algoritm mavjud bo‘lmasligi ham mumkin.
  

 Biz endi mulohazalar hisobining aksiomatik nazariyasini kiritamiz. (38-bet)

• 
   Biz endi mulohazalar hisobining aksiomatik nazariyasini kiritamiz. (38-bet)
  
• 
  (1) ning simvollari sifatida , va butun musbat indeksli propozitsional xarflarni olamiz: .
  
• 
  Bu erda va lar primitiv bog‘lovchilar deyiladi. Mulohazalar xisobining muhim tushunchasi hisoblangan formula tushunchasini kiritamiz.
  
• 
  (2) (a) Barcha propozitsional harflar formulalardir:
  
• 
  (b) agar va lar formulalar bo‘lsa, u holda lar ham formulalardir.
  
• 
  (3) nazariyaning formulalari qanday bo‘lishidan qat’iy nazar quyidagi formulalar ning aksiomalaridir:
  
• 
  (4) Yagona keltirib chiqarish qoidasi bo‘lib, u ham bo‘lsa, modus ponens qoidasi xizmat qiladi: va formulalarning bevosita natijasi dir. Bu qoidani qisqacha ko‘rinishda belgilaymiz. (71-bet)