|
Predikatlar hisobining to‘liqligi
Predikatlar hisobi tor ma’noda to‘liq emas. YA’ni uning aksiomalar sistemasiga predikatlar hisobida keltirib chiqarilmaydigan $x / ( x ) Þ "x / ( x ) formulani qo‘shsak, hosil bo‘lgan aksiomalar sistemasi zidsizligicha qolad CHunki, oldingi paragrafdagi isbot qilish sxemasini hosil qilingan aksiomalar sistemasiga qo‘llasak, / Þ / ko‘rinishdagi aynan rost mulohaza hosil bo‘lad YA’ni, hosil bo‘lgan aksiomalar sistemasi zidsizdir.
Bundan tashqari, predikatlar hisobi uchun keng ma’nodagi to‘liqlik masalasi qaralad
Biz YUqoridagi paragraflarda predikatlar hisobining keltirib chiqariluvchi formulasi predikatlar algebrasining formulasi sifatida qaralsa. Aynan rost formula bo‘lishini ko`rgan edik. Predikatlar algebrasining aynan rost formulasi predikatlar hisobining formulasi sifatida qaralsa, keltirib chiqariluvchi bo‘ladimi – degan savol tu\ilishi tabydir. YA’ni, predikatlar hisobi predikatlar algebrasini ifodalash uchun to‘liqmi- degan savol tug‘ilad
Bu savolga K.Gyodelning quyidagi teoremasi javob berad
5.1 – teorema. Predikatlar algebrasining har qanday aynan rost formulasi, predikatlar hisobida keltirib chiqariluvchi formula bo‘lad
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
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: |
