Muloxazalar xisobi va uning aksiomalari

Echilishi:  Isbot ketma-ketligini quramiz:
(1) (A ((B A)A))((A(BA))(AA)). (A2 aksioma).
(2) (A ((B A)A). (A1 aksioma).
(3) (A(BA))(AA). ((1), (2) dan MP buyicha).
(4) (A(BA)). (A1 aksioma).
(5) AA. ((3), (4) dan MP buyicha).
SHunday qilib biz AA formula uchun ta’rifda aytilgan isbot ketma-ketligini qura oldik. Bu ketma-ketlik (1), (2), (3), (4), (5) formulalar ketma-ketligidan iborat. Bu erda isbot uzunligi n5 ga teng.
L nazariyaning formulalaridan tashkil topgan biror tuplam berilgan bulsin. Bu formulalar tuplamidan keltirib chiqariluvchanlik tushunchasi quyidagicha aniqlanadi.
Ta’rif; L nazariyaning A formulasi AA_n buladigan A₁,...,A_n formulalar ketma-ketligi mavjud bulib, bunda i{1,...,n}da xar bir A_i yoki L ning aksiomasi, yoki ning formulasi, yoki uzidan oldingi formulalardan keltirib chiqarish qoidalari yordamida keltirib chiqarilgan bulganda va faqat shu xolda ning formulalarining natijasi yoki dan keltirib chiqarilgan deyiladi.
n soniga isbot uzunligi deyiladi.
Bu A₁,...,A_n ketma-ketlik A ning dagi isboti deyiladi. Bu xolda ning formulalari gipotezalar deyiladi.
A formula dan kelib chiqadi, deyish urniga ├A yozuvdan foydalanamiz.
Agar chekli bulsa {B₁,...,B_n}├A yozuv urniga B_1,B₂,...,B_n ├A yozuvdan foydalanamiz.
Masalan; A, B, A(BC)├ C yozuv C formulaning L nazariyada {A,B,A(BC)} formulalar tuplamidan keltirib chiqarilishini, shu formulalarning natijasi yoki shu tuplamda isbotga ega ekanini bildiradi. Bu isbotni A, B, A(BC) gipotezalardagi isbot deb aytishimiz mumkin.
MULOXAZALAR XISOBIDA DEDUKSIYA TEOREMASI.