WikiDer > Umumjahon umumlashtirish

Yilda mantiq, umumlashtirish (shuningdek universal umumlashtirish yoki universal kirish,^[1][2][3] GEN) a yaroqli xulosa qilish qoidasi. Unda aytilganidek ${ displaystyle vdash ! P (x)}$ olingan, keyin ${ displaystyle vdash ! forall x , P (x)}$ olinishi mumkin.

Gipotezalar bilan umumlashtirish

To'liq umumlashtirish qoidasi gipotezani chap tomonda bo'lishiga imkon beradi turniket, lekin cheklovlar bilan. Faraz qiling ${ displaystyle Gamma}$ bu formulalar to'plami, ${ displaystyle varphi}$ formula va ${ displaystyle Gamma vdash varphi (y)}$ olingan. Umumlashtirish qoidasida ta'kidlangan ${ displaystyle Gamma vdash forall x , varphi (x)}$ agar olinishi mumkin ${ displaystyle y}$ da tilga olinmagan ${ displaystyle Gamma}$ va ${ displaystyle x}$ ichida bo'lmaydi ${ displaystyle varphi}$.

Ushbu cheklovlar mustahkamlik uchun zarurdir. Birinchi cheklovsiz xulosa qilish mumkin ${ displaystyle forall xP (x)}$ gipotezadan ${ displaystyle P (y)}$. Ikkinchi cheklovsiz, quyidagi chegirmalarni amalga oshirish mumkin:

1. ${ displaystyle mavjud z , mavjud w , (z not = w)}$ (Gipoteza)
2. ${ displaystyle mavjud w , (y not = w)}$ (Mavjud ibrat)
3. ${ displaystyle y not = x}$ (Mavjud ibrat)
4. ${ displaystyle forall x , (x not = x)}$ (Noto'g'ri universal umumlashtirish)

Bu shuni ko'rsatmoqchi ${ displaystyle mavjud z , mavjud w , (z not = w) vdash forall x , (x not = x),}$ bu asossiz chegirma. Yozib oling ${ displaystyle Gamma vdash forall y , varphi (y)}$agar joiz bo'lsa ${ displaystyle y}$ da tilga olinmagan ${ displaystyle Gamma}$ (ikkinchi cheklov, ning semantik tuzilishi kabi qo'llanilishi shart emas) ${ displaystyle varphi (y)}$har qanday o'zgaruvchini almashtirish bilan o'zgartirilmaydi).

Isbotning misoli

Isbotlang: ${ displaystyle forall x , (P (x) rightarrow Q (x)) rightarrow ( forall x , P (x) rightarrow forall x , Q (x))}}$ dan olingan ${ displaystyle forall x , (P (x) rightarrow Q (x))}$ va ${ displaystyle forall x , P (x)}$.

Isbot:

Raqam	Formula	Asoslash
1	${ displaystyle forall x , (P (x) rightarrow Q (x))}$	Gipoteza
2	${ displaystyle forall x , P (x)}$	Gipoteza
3	${ displaystyle ( forall x , (P (x) rightarrow Q (x))) rightarrow (P (y) rightarrow Q (y)))}$	Umumjahon instantiatsiya
4	${ displaystyle P (y) rightarrow Q (y)}$	(1) va (3) dan Modus ponenslari
5	${ displaystyle ( forall x , P (x)) rightarrow P (y)}$	Umumjahon instantiatsiya
6	${ displaystyle P (y) }$	(2) va (5) dan Modus ponenslari
7	${ displaystyle Q (y) }$	(6) va (4) dan Modus ponenslari
8	${ displaystyle forall x , Q (x)}$	Umumlashtirish bo'yicha (7) dan
9	${ displaystyle forall x , (P (x) rightarrow Q (x)), forall x , P (x) vdash forall x , Q (x)}$	Xulosa (1) dan (8) gacha
10	${ displaystyle forall x , (P (x) rightarrow Q (x)) vdash forall x , P (x) rightarrow forall x , Q (x)}$	(9) dan Chegirma teoremasi
11	${ displaystyle vdash forall x , (P (x) rightarrow Q (x)) rightarrow ( forall x , P (x) rightarrow forall x , Q (x))}}$	(10) dan Chegirma teoremasi

Ushbu dalilda 8-bosqichda universal umumlashtirish ishlatilgan chegirma teoremasi 10 va 11 bosqichlarida qo'llanilishi mumkin edi, chunki ko'chirilayotgan formulalar erkin o'zgaruvchiga ega emas.

Shuningdek qarang

• Birinchi darajali mantiq
• Shoshilinch umumlashtirish
• Umumjahon instantiatsiya

Adabiyotlar