Matematika

Keltirib chiqarish (isbotlash) tushunchasi
Ta’rif. Agar B1 ,B2 ,...,Bn chekli formulalar ketma-ketligining har qanday hadi quyidagi:

1)H formulalar majmuasining birorta formulasi;

2) isbotlanuvchi formula;

3) B1 ,B2 ,...,B2ketma-ketlikning istalgan ikkita oldinma-keyin keladigan elementlaridan xulosa qoidasiga asosan hosil qilinadi degan uch shartning birortasini qanoatlantirsa, u holda bu ketma-ketlik H chekli formulalar majmuasidan keltirib chiqarilgan deb aytiladi.

H {A,B} dan quyidagi formulalar chekli ketma-ketligi keltirilib chiqariladi:

A, B, (AA)((AB)(AAB)), B(AB),

A, B, AA, (AB)(AAB)), AB, AAB, A B.

Agar murakkab xulosa qoidasidan foydalansak, u vaqtda (isbot) keltirib chiqarish formulalari quyidagicha bo’ladi:

A, B, (AA)((AB)(AAB)),

B(AB), AA, AB, A B.

Formulani keltirib chiqarish va formulalar majmuasidan keltirib chiqarish ta’riflariga asosan keltirib chiqarishning quyidagi xossalari hosil bo’ladi:

-H formulalar majmuasidan keltirib chiqarilgan chekli ketma-ket-likning boshlang’ich qismi ham H dan keltirib chiqariladigan bo’ladi;

-agar H dan keltirib chiqarilgan ketma-ketlikning ikkita qo’shni hadlari (elementlari) orasiga H dan keltirib chiqarilgan qandaydir boshqa ketma-ketlik qo’yilsa, u vaqtda hosil etilgan yangi formula-lar ketma-ketligi ham H dan keltirib chiqarilishi mumkin.

-H formulalar majmuasidan keltirib chiqarilgan formulalar ketma-ketligining har qanday hadi H dan keltirib chiqariladigan formuladir.

-agar H W bo’lsa, u vaqtda H dan keltirib chiqarilgan har qanday formula W ning ham formulasi bo’ladi.

- B formula H dan keltirib chiqariladigan formula bo’lishi uchun H dan keltirib chiqarilgan ixtiyoriy formulalar ketma-ketligida bu formulaning mavjud bo’lishi yetarli va zarurdir.