Predikatlar hisobining keltirib chiqariluvchi formulalari
Mulohazalar hisobining barcha aksiomalari va keltirib chiqarish qoidalari predikatlar hisobiga to‘liqligicha kirganligi sababli mulohazalar hisobining hamma keltirib chiqariluvchi formulalari predikatlar hisobining ham keltirib chiqariluvchi formulalari bo‘lad Bundan tashqari mulohazalar hisobining keltirib chiqariluvchi formulalariga predikatlar hisobining o`rniga qo‘yish va boshqa qoidalari ni =o`llab, yana keltirib chiqariluvchi formulalar hosil qilishimiz mumkin.
+uyida predikatlar hisobining ba’zi keltirib chiqariluvchi formulalarini ko`rib chiqamiz. Mulohazalar hisobidagidek ℑ keltirib chiqariluvchi formula bo‘lsa, uni qisqacha ⊢ ℑ ko‘rinishda belgilaymiz.
6.1 – teorema. ⊢ / ( x ) Þ / ( x ) Ú "u G ( y ).
Isbot. Mulohazalar hisobida ⊢ A Þ A Ú V bo‘lganligi uchun A ni / ( x ), ℬ ni "x G ( y ) bilan almashtirsak, u holda ⊢ / ( x ) Þ / ( x ) Ú "u G ( y ) hosil bo‘lad
quyidagi teoremalarning isboti mulohazalar hisobining keltirib chiqariluvchi formulalarida o`rniga qo‘yish qoidalari ni qo‘llash natijasida hosil bo‘lad
6.2 – teorema. ⊢ / ( x ) Ú ù / ( x ).
6.3 – teorema. ⊢ A Þ ( $x / ( x ) Ù "u N ( u ) Þ
Mulohazalar hisobida isbot qilingan hosilaviy keltirib chiqarish qoidalari predikatlar hisobi uchun ham hosilaviy keltirib chiqarish qoidalari bo‘lishi ravshan. Undan tashqari, predikatlar hisobi uchun mulohazalar hisobida bo‘lmagan quyidagi keltirib chiqarish qoidasini kiritamiz.
6.4 – teorema.( Umumiylik kvantori bilan bog‘lash qoidasi). Agar ℑ( x ) predikatlar hisobining x erkin o‘zgaruvchi predmet qatnashgan keltirib chiqariluvchi formulasi bo‘lsa, u holda "x ℑ ( x ) ham predikatlar hisobining keltirib chiqariluvchi formulasi bo‘lad
Isbot. Bu qoidaning isboti quyidagi tizimdan iborat :
⊢ A Þ Â ( Â - mulohazalar hisobining keltirib chiqariluvchi formulasi).
⊢ A Þ ℑ ( x ).
⊢ A Þ "x ℑ ( x ).
⊢ Â Þ "x ℑ ( x ).
"x ℑ ( x ).
Bu qoidani qisqacha ℑ ( x )
"x ℑ ( x ) ko‘rinishda yozish mumkin.
6.5 – teorema. ⊢ "x / ( x ) Þ $x / ( x ).
Isbot. V1, V2 aksiomalarga asosan ⊢ "x / ( x ) Þ / ( u ) va ⊢ / ( u ) Þ $x / ( x ). Bu formulalarga sillogizm qoidasini =o`llasak ⊢ "x / ( x ) Þ $x / ( x ) hosil bo‘lad
O`=uvchilar mustaqil isbot qilishlari uchun predikatlar hisobining yana bir nechta keltirib chiqariluvchi formulalarini keltiramiz .
6.6 – teorema.
⊢ "x "u / ( x, u ) ~ "u "x / ( x, u ).
⊢ $x "u / ( x, u ) Þ "u $x / ( x, u ).
⊢ "x ( / ( x ) Þ G ( x )) Þ ( "x F ( x ) Þ "x G ( x )).
⊢ "x ( F ( x ) Þ G ( x )) Þ $x F ( x ) Þ $x G ( x )).
⊢ "x ( F ( x ) Þ G ( x )) Þ ( "x F ( x ) Þ "x G ( x )).
⊢ "x ( F ( x ) ~ G ( x )) Þ ( "x F ( x ) ~ "x G ( x )).
⊢ $x F ( x ) ~ ù ( "x ù F ( x )).
⊢ $x ù F ( x ) ~ ù ( "x F ( x )).
⊢ ù ( $x F ( x )) ~ "x ù F ( x ).
⊢ $x ù F ( x ) ~ "x F ( x ).
⊢ ( A Þ "x F ( x )) ~ "x ( A Þ F ( x )).
K. Gyodel teoremasiga asosan predikatlar algebrasining har qanday aynan rost formulasi predikatlar hisobining keltirib chiqariluvchi formulasi ekanligidan foydalanib ham YUqoridagi formulalarning keltirib chiqariluvchi formulalar ekanligini isbot qilish mumkin.
Masalan, ⊢ ( A Þ "x / ( x )) ~ "x ( A Þ / ( x )) ning
aynan rost formula bo‘lishini isbot qilaylik.
A Þ "x / ( x ) = 1 bo‘lsin. U holda A = 0 bo‘lsa,
A Þ / ( x ) har qanday / ( x ) uchun, demak, har qanday x uchun rost bo‘lad U holda "x ( A Þ / ( x )) = 1 bo‘lad
A = 1 bo‘lsa, A Þ "x / ( x ) = 1 bo‘lganligidan
"x / ( x ) = 1 , ya’ni, har qanday x uchun / ( x ) = 1 demak,
"x ( A Þ / ( x )) = 1 bo‘lad
Shuddi shunday, A Þ "x / ( x ) = 0 bo‘lsa, "x ( A Þ
Þ / ( x )) = 0 bo‘lishi ko`rsatilad
Do'stlaringiz bilan baham: |