Ta’rif.Agar chekli formulalar ketma-ketligining har qanday hadi quyidagi: 1) formulalar majmuasining birorta formulasi; 2) isbotlanuvchi formula; 3) ketma-ketlikning istalgan ikkita oldinma-keyin keladigan elementlaridan xulosa qoidasiga asosan hosil qilinadi degan uch shartning birortasini qanoatlantirsa, u holda bu ketma-ketlik chekli formulalar majmuasidan keltirib chiqarilgan deb aytiladi. Oldingi paragrafdagi misolda ko‘rsatildiki, dan quyidagi formulalar chekli ketma-ketligi keltirilib chiqariladi.
Aksiomatik nazariya. Keltirib chiqarish. 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.
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).