Har bir aksioma mulohazalar hisobining keltirib chiqariluvchi formulasidir. 2º. Mulohazalar hisobining keltirib chiqariluvchi formulasiga o‘rniga qo‘yish qoidasini qo‘llash natijasida hosil qilingan formula mulohazalar hisobining keltirib chiqariluvchi formulasidir. 3º. Mulohazalar hisobining keltirib chiqariluvchi formulalariga ùulosa chiqarish qoidasini qo‘lllash natijasida hosil qilingan formula mulohazalar hisobining keltirib chiqariluvchi formulasidir. 4º. Mulohazalar hisobining boshqa keltirib chiqariluvchi formulalari yo‘q.. Agar formulalarning chekli ketma-ketligi ℑ1, ℑ2, . . . , ℑn da har bir ℑi ( i =1, n ) formula yo mulohazalar hisobining keltirib chiqariluvchi formulasi, yo ûzidan oldingi formulalardan o‘rniga qo‘yish yoki ùulosa chiqarish qoidalari yordamida hosil qilingan formulalar bo‘lsa, u holda bu ketma-ketlik oxirgi ℑn formulaning formal isboti , n esa isbotning uzunligi deyiladi. Mulohazalar hisobining aksiomalari isbotining uzunligi 1 ga teng isbotlanuvchi formulalar sifatida =aralishi mumkin. Mulohazalar hisobining isbot uzunligi birdan katta bo‘lgan isbotlanuvchi formulalarini teoremalar deb ataymiz. «ℑ formula mulohazalar hisobining keltirib chiqariluvchi formulasi» degan jumlani qisqacha ⊢ ℑ belgi orqali ifodalaymiz.