Bajardi: Bozorov Odilbek

Keltirib chiqariluvchi formulalar.
Mulohazalar hisobini qurishning keyingi bosqichi isbotlanuvchi formulalarni ajratib olishdan iborat. Avval aksiomalarni bayon qilamiz, keyin aksiomalardan keltirib chiqariluvchi, ya’ni isbotlanuvchi formulalarni keltirib chiqarish qoidalari ni beramiz.
1. Mulohazalar hisobining aksiomalari.
Mulohazalar hisobining aksiomalari 4 ta guruhga bo‘lingan ro‘yxatdagi 11 aksiomadan iborat.
I guruù aksiomalari :
I1. A Þ ( V Þ A ) .
I2. ( A Þ ( B Þ C )) Þ (( A Þ B ) Þ ( A Þ C )).
II guruù aksiomalari :
II1. A & B Þ A .
II2. A & B Þ B .
II3. ( A Þ B ) Þ (( A Þ C ) Þ ( A Þ B & C )).
III guruù aksiomalari :
III1. A Þ A Ú B .
III2. B Þ A Ú B .
III3. ( A Þ C ) Þ (( B Þ C ) Þ ( A Ú B Þ C )) .
IY guruù aksiomalari :
IY1. ( A Þ B ) Þ ( ù B Þ ù A ) .
IY2. A Þ ù ù A .
IY3. ù ù A Þ A .
II.2.2. Keltirib chiqarish qoidalari .
1. O‘rniga qo‘yish qoidasi.
MH ning tarkibida A o‘zgaruvchi mulohaza qatnashgan
ℑ ( A ) , hamda iùtiyoriy ℬ formulalari berilgan bo‘lsin. Agar ℑ ( A ) mulohazalar hisobining keltirib chiqariluvchi (k.ch.) formulasi bo‘lsa, u holda ℑ ( ℬ ) formula ham mulohazalar hisobining keltirib chiqariluvchi formulasi bo‘ladi.
Bu qoida qisqacha sxematik ravishda ℑ ( A ) ℑ ( ℬ )
ko‘rinishda belgilanadi.
Xulosa chiqarish ( Modus ponens –MR ) qoidasi.
Agar ℑ Þ ℬ va ℑ formulalar MH ning keltirib chiqariluvchi formulalari bo‘lsa, u holda ℬ formula ham MH ning keltirib chiqariluvchi formulasidir. Bu qoida qisqacha quyidagi ko‘rinishda belgilanadi : ℑ , ℑ Þ ℬ
ℬ .
3 - ta’rif. 1º. 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.
II.2.4 - ta’rif. 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.
II.2.5 - teorema. ⊢ A Þ A .
Isbot. quyidagi ketma-ketlikni =araylik :
A Þ ( V Þ A ) .
( A Þ ( V Þ A )) Þ (( A Þ V ) Þ ( A Þ A )) .
( A Þ V ) Þ ( A Þ A ) .
( A Þ ( V Þ A )) Þ ( A Þ A ) .
A Þ A .
A Þ A .
Bu ketma-ketlik A Þ A formulaning formal isboti ekanligini ko‘rish qiyin emas. Haqiqatdan ham,
A Þ (V Þ A)- formula I1 aksioma;
( A Þ (V Þ A )) Þ (( A Þ V ) Þ (A Þ A ))- formula I2 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 I1 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.
ℱ Þ ù ù A .
ℱ Þ ù ù ℑ .