1-Mavzu: mulohazalar hisobi uchun aksiomalar sistemasi reja

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.