Formulalar. Asosiy teng kuchli formulalar. Normal formalar. Mulohazalar hisobini qurish. Teng kuchli almashtirishlar. Normal formalar. Mulohazalar algebrasi

4º. Mulohazalar hisobining boshqa keltirib chiqariluvchi formulalari yo‘q.
II.2.4 - ta’rif. Agar formulalarning chekli ketma-ketligi ℑ₁, ℑ₂, . . . , ℑ_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.
II.2.5 - teorema. ⊢ A Þ A .
Isbot. quyidagi ketma-ketlikni =araylik :

1. 
   A Þ ( V Þ A ) .
   
2. 
   ( A Þ ( V Þ A )) Þ (( A Þ V ) Þ ( A Þ A )) .
   
3. 
   ( A Þ V ) Þ ( A Þ A ) .
   
4. 
   ( A Þ ( V Þ A )) Þ ( A Þ A ) .
   
5. 
   A Þ A .
   
6. 
   A Þ A .
   

Bu ketma-ketlik A Þ A formulaning formal isboti ekanligini ko‘rish qiyin emas. Haqiqatdan ham,
A Þ (V Þ A)- formula I₁ aksioma;
( A Þ (V Þ A )) Þ (( A Þ V ) Þ (A Þ A ))- formula I₂ aksiomadagi S ni A bilan almashtirish natijasida hosil qilingan;
( A Þ V ) Þ ( A Þ A ) formula 2 - formulaga MR qoidasini qo‘lllash natijasida hosil qilingan;
( A Þ ( V Þ A )) Þ ( A Þ A ) formula ûzidan oldingi formulada V ni V Þ A formula bilan almashtirish natijasida hosil qilingan;
A Þ A formula 4 – formulaga MR qoidasini qo‘lllash natijasida hosil qilingan;
A Þ A formula A ni A bilan almashtirish natijasida hosil qilingan.
Bundan keyin mulohazalar hisobining keltirib chiqariluvchi formulasini ℛ xarfi, ù ℛ ni ℱ xarfi bilan belgilab olamiz.

II.2.6 - teorema. ℑ mulohazalar hisobining iùtiyoriy formulasi bo‘lsin. U holda ℑ Þ ℛ mulohazalar hisobining keltirib chiqariluvchi formulasi bo‘ladi, ya’ni ⊢ ℑ Þ ℛ.

Isbot. 1. A Þ ( V Þ A ).
2. ℛ Þ ( V Þ ℛ ).
3. V Þ ℛ .
4. ℑ Þ ℛ.
Bu ketma - ketlik teoremaning formal isbotidir. Haqiqatdan ham, 1 - formula I₁ aksioma. 2 - formula 1 -formuladan A ni ℛ bilan almashtirish natijasida hosil qilingan. 3 - formula 2 - formuladan MR qoida yordamida hosil qilingan. 4 - formula esa 3 - formulada V ni ℑ formula bilan almshtirish natijasida hosil qilingan.
II.2.7 - teorema. ⊢ ℱ Þ ù ù ℑ.
Isbot. 1. ( A Þ V ) Þ ( ù V Þ ù A ).
2. ( ù A Þ V ) Þ ( ù V Þ ù ù A ).
3. ( ù A Þ ℛ ) Þ ( ù ℛ Þ ù ù A ).
4. ù ℛ Þ ù ù A.

1. 
   ℱ Þ ù ù A .
   
2. 
   ℱ Þ ù ù ℑ .