Formal aksiomatik nazariya

MULOHAZALAR HISOBI UCHUN AKSIOMALAR SISTEMASI. DEDUKSIYA TEOREMASI. KELTIRIB CHIQARILADIGAN FORMULALAR
REJA:

1. 
   Formal aksiomatik nazariya
   
2. 
   Mulohazalar hisobi uchun aksiomalar sistemasi
   
3. 
   Deduksiya teoremasi
   
4. 
   nazariyaning asosiy keltirib chiqariladigan formulalari
   

FORMAL AKSIOMATIK NAZARIYA

Matematikada aksiomatik metod eramizdan oldin qadimgi yunon matematiklarining ishlarida paydo bo‘lgan. Ammo aksiomatik metod XIX asrda rus matematigi N.I.Lobachevskiy tomonidan noevklid geometriyasining kashf etilishi bilan o‘zining alohida yo‘nalish sifatida yangi rivojlanish pog‘onasiga o‘tdi. Shunday qilib, aksiomatik metod matematik nazariyalarni qurish va o‘rganishda kuchli apparat ekanligi XIX asr matematiklari tomonidan to‘la-to‘kis e’tirof etildi va bu apparat matematikada keng ko‘lamda qo‘llanila boshlandi.

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.
Endi esa formal aksiomatik nazariyani ifodalashga o‘taylik.
Agar quyidagi shartlar bajarilsa, u holda formal (aksiomatik) nazariya aniqlangan xisoblanadi:

1. 
   Sanoqli simvollar to‘plami- nazariyaning simvollari berilgan bo‘lsa nazariyaning chekli simvollari ketma-ketligi ning ifodasi deyiladi.
   
2. 
   nazariyaning formulalari deb ataluvchi ning ifodalari to‘plami berilgan bo‘lsa. (odatda, berilgan ifodaning formula bo‘lish bo‘lmasligini aniqlovchi effektiv jarayon beriladi).
   
3. 
   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).
   
4. 
   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 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.
Bunday algoritm mavjud bo‘lgan nazariyani echiluvchan nazariya, aks holda esa echilmaydigan nazariya deyiladi.
Biroz oldinga o‘tib shuni aytish mumkinki, mulohazalar xisobi uchun qurilgan formal aksiomatik nazariya echiluvchan nazariya, tor ma’nodagi predikatlar xisobi nazariyasi esa echilmaydigan nazariyadir.
formula nazariyada formulalar to‘plami ning mantiqiy natijasi (mulohazalar xisobida mantiqiy natija) bo‘lishi uchun shunday formulalar ketma-ketligi mavjud bo‘lishi kerakki, bunda formula dan iborat bo‘lib, ixtiyoriy uchun formula yoki aksioma, yoki to‘plamning elementi, yoki birorta keltirib chiqarish qoidasi orqali o‘zidan oldingi formulalarning bevosita natijasi bo‘lishi zarur va etarlidir. Bunday formulalar ketma-ketligi formulalar to‘plamidan ni keltirib chiqarilishi deyilib, ning elementlari esa, keltirib chiqarish gipotenuzalari deyiladi.
qulaylik uchun, « formula formulalar to‘plamning natijasi» degan tasdiqni ├ ko‘rinishda yozamiz.
Agar chekli to‘plam bo‘lsa, ya’ni , u holda ├ yozuvni ├ ko‘rinishda yozamiz. Agar , bo‘lsa, u holda ├ yozuv formula da teorema bo‘lganda va faqat shu xoldagina o‘rinli bo‘ladi. Odatda ├ yozuv o‘rniga, ├ ko‘rinishda yoziladi. Shunday qilib ├ yozuv « formula da teoremadir» degan tasdiqning qisqartirilganidir.
Aniqlangan ├ -keltirib chiqarilishining ba’zi xossalarini ko‘rib o‘taylik.
1-hossa. Agar va ├ , bo‘lsa, u holda ├ bo‘ladi.
Haqiqatan ham, ├ deganda quyidagini tushunamiz: shunday ketma-ketlik mavjudki, bunda formula dan iborat bo‘lib, ixtiyoriy uchun formula, yoki aksioma, yoki ning elementi, yoki o‘zidan oldingi formulalardan birorta keltirib chiqarish qoidasi orqali hosil qilinsa bevosita natijasidir.
Agar formulalar to‘plamga tegishli bo‘lsa, bo‘lgani uchun lar ga ham tegishli bo‘ladi.
Bu esa ├ ekanini bildiradi.