17-Ma’ruza. Deduksiya teoremasi. Mos keltirib chiqarish haqida lemma. To’liqlik haqida Gyodel teoremasi

4.1.2. Keltirib chiqarish (isbotlash) tushunchasi.
2- ta’rif. Agar chekli formulalar ketma-ketligining har qanday hadi quyidagi uch shartning birortasini qanoatlantirsa, u holda bu ketma-ketlik chekli formulalar majmuasidan keltirib chiqarilgan deb ataladi:
1) formulalar majmuasining birorta formulasi;
2) isbotlanuvchi formula;
3) ketma-ketlikning istalgan ikkita oldinma-keyin keladigan elementlaridan xulosa qoidasiga asosan hosil qilinadi.
Oldingi paragrafdagi misolda ko‘rsatildiki, formulalar majmuasidan quyidagi formulalar chekli ketma-ketligi keltirilib chiqariladi:
, , , , , , , , .
Agar murakkab xulosa qoidasidan foydalansak, u holda (isbotlash) keltirib chiqarish formulalari quyidagicha bo‘ladi:
, , ,
, , , .
Formulani keltirib chiqarish va formulalar majmuasidan keltirib chiqarish ta’riflariga asosan keltirib chiqarishning quyidagi xossalari hosil bo‘ladi.
1) formulalar majmuasidan keltirib chiqarilgan chekli ketma-ketlikning boshlang‘ich qismi ham dan keltirib chiqariladigan bo‘ladi.
2) Agar dan keltirib chiqarilgan ketma-ketlikning ikkita qo‘shni hadlari (elementlari) orasiga dan keltirib chiqarilgan biror boshqa ketma-ketlik qo‘yilsa, u holda hosil etilgan yangi formulalar ketma-ketligi ham dan keltirib chiqarilishi mumkin.
Haqiqatan ham, masalan, agar va lar dan keltirib chiqarilsa, u vaqtda, keltirib chiqarish ta’rifiga asosan,
ham dan keltirib chiqariladigan bo‘ladi.
3) formulalar majmuasidan keltirib chiqarilgan formulalar ketma-ketligining har qanday hadi dan keltirib chiqariladigan formuladir.
4) Agar bo‘lsa, u holda dan keltirib chiqarilgan har qanday formula ning ham formulasi bo‘ladi.
5) formula dan keltirib chiqariladigan formula bo‘lishi uchun dan keltirib chiqarilgan ixtiyoriy formulalar ketma-ketligida bu formulaning mavjud bo‘lishi yetarli va zarurdir.