Mulohazalar xisobi

mulohazalar hisobi Reja: mulohazalar hisobi va uning aksiomalari mulohazalar hisobida deduksiya teoremasi. mulohazalar hisobining tulaligi. mulohazalar hisobining ziddiyatsizligi mulohazalar hisobi aksiomalarining erkliligi. mulohazalar hisobi uchun formal aksiomatik L nazariyani quyidagicha kiritamiz: -L nazariyaning simvollari ,, (,) va Ai xarflardan iborat, bunda i natural son bo'lib , biz , larni primitiv bog'lovchilar, Ai larni esa propozitsional xarflar deb yuritamiz. - L nazariyada formula tushunchasini quyidagicha aniqlanadi: (a) Har bir propozitsional xarf formuladir. (b) Agar A va B lar formulalar bulsalar, u holda (A), (AB) lar formulalardir. (Keyingi urinlarda tashqi qavslarni tashlab yozishga kelishiladi). (v) Ifoda, agar u (a) va (b) punktlar yordamida hosil qilingan bulsa va faqat shu holda formuladir. - A, B, C lar qanday formulalar bo'lishlaridan qatiy-nazar, quyidagi formulalar L ning aksiomalaridir . (A1) A(BA). (A2) (A(BC))((AB)(AC)). (A3) (BA)((BA)B). - L da yagona keltirib chiqarish qoidasi modus ponens (MP) dan iborat bo'lib, u quyidagicha ifodalanadi : B formula A va AB formulalarning bevosita natijasidir. Biz kuramizki, cheksiz ko'p aksiomalar sistemasi, bor yug'i uchta aksiomalar sxemasi bilan berilmoqda va xar qanday formulaning aksioma yoki aksioma emasligini aniqlash xech qanday qiyinchilik tug'dirmaydi, bu kabi aksiomalashtirilgan nazariyalar effektiv aksiomalashtirilgan nazariyalar deyiladi. Formulalarni qisqaroq yozish maqsadida yana , , bog'lovchilarni quyidagi ta'riflar bilan beramiz; (D1) (AB) ifoda (AB) ni bildiradi. (D2) (AB) ifoda AB ni bildiradi. (D3) AB ifoda (AB)(BA) ni bildiradi. L nazariyaning formulalari uchun isbot tushunchasini quyidagi ta'rif yordamida kiritamiz. ta'rif: L nazariyaning A formulasi agar L ning formulalaridan tuzilgan shunday A1,,An ketma-ketlik mavjud bo'lib, bunda xar-bir Ai, i1,,n, yoki aksioma, yoki uzidan oldingi formulalarning MP xulosa qilish qoidasi bo'yicha natijasidan iborat bulsa va An formula A formulaning uzidan iborat bulsa L nazariyada keltirib chiqariluvchi yoki isbotga ega deyiladi, A1,,An formulalar ketma-ketligi esa A formulaning L dagi isboti deyiladi. Isbotga ega bo'lgan formula teorema deyiladi. n soniga isbot uzunligi deyiladi. Agar A formula L ning teoremasi bulsa, biz bu holatni├A kabi yozamiz. Masalan: ├((AB)A)B yozuv ((AB)A)B formulaning mulohazalar hisobida isbotga ega ekanligini, yani teorema ekanligini bildiradi. 1-misol: AA formulaning mulohazalar hisobida isbotga ega ekanligin kursating. Bunda A mulohazalar hisobining ixtiyoriy formulasi. Yechilishi: Isbot ketma-ketligini quramiz: (1) (A ((B A)A))((A(BA))(AA)). (A2 aksioma). (2) (A ((B A)A). (A1 aksioma). (3) (A(BA))(AA). ((1), (2) dan MP bo'yicha). (4) (A(BA)). (A1 aksioma). (5) AA. ((3), (4) dan MP bo'yicha). Shunday qilib biz AA formula uchun ta'rifda aytilgan isbot ketma-ketligini qura oldik. Bu ketma-ketlik (1), (2), (3), (4), (5) formulalar ketma-ketligidan iborat. Bu yerda isbot uzunligi ...