1903-yilda bo`lgan jahon matematiklarining kongressida D.Gilbert o`sha davrgacha yechilmagan va Gilbertning fikricha katta ahamiyatga ega bo`lgan 23 ta problemani taklif etdi. Ana shu problemalardan biri – matematikani asoslash problemasi edi. Bu problema ushbu ko`rinishda qo`yilishi mumkin: “Matematika ziddiyatsiz ekanligi isbotlansin yoki rad etilsin”.
1903-yilda bo`lgan jahon matematiklarining kongressida D.Gilbert o`sha davrgacha yechilmagan va Gilbertning fikricha katta ahamiyatga ega bo`lgan 23 ta problemani taklif etdi. Ana shu problemalardan biri – matematikani asoslash problemasi edi. Bu problema ushbu ko`rinishda qo`yilishi mumkin: “Matematika ziddiyatsiz ekanligi isbotlansin yoki rad etilsin”.
Bu ulkan problemani yechishda bir necha yo`nalish paydo bo`ldi.Har bir yo`nalish namoyondalari o`z dasturlari bilan chiqib, mazkur problemani yechishga harakat qila boshladilar. “Formalizm” , “Intuisiolizm” , “logizm”, “konstruktibizm” shu oqimlar jumlasidandir. “Formalistlar” deb ataluvchi D.Gilbert boshchiligidagi nemis matematiklari quyidagi dastur (Gilbert dasturi) ni ilgari surishdi:
1. Matematika yoki uning katta bir fragmenti (bo`lagi) (masalan, arifmetika, analiz va to`plamlar nazariyasi) formallashtirilishi kerak, ya`ni matematikani (yoki bo`lagini) biror formal sistema (formalizm) ko`rinishiga keltirish kerak.
2. Hosil bo`lgan formal sistema aksiomalaridan aniqlangan (va berilgan) qoidalar (to`plami) yordamida hech bo`lmaganda matematikaning asosini tashkil etuvchi jumlalarni (formulalarni) keltirib chiqarish kerak.
3. Keltirib chiqarish qoidalarini formal sistema aksiomalariga qo`llanilganda hech qachon (formal) ziddiyat hosil bo`lmasligini ko`rsatish kerak.
Formal (nazariya) sistema formallashtirilgan nazariya tushunchasining xususiy holi bo`lib , formal nazariya o`zining isbotlanuvchi (keltirib chiqariluvchi) formulalari sinfi bilan aniqlansa, formallashtirilgan nazariya o`zining rost (umumrost, umumqiymatli) formulalari sinfi bilan aniqlanadi. Bu sinf, odatda, keltirib chiqarishga nisbatan yopiq bo`lishi kerak, ya`ni rost formulalardan keltirib chiqariluvchi har bir formula rost bo`lishi kerak. Tabiiy , bunda formallashtirilgan nazariyaning aksiomalari ham rost formulalar bo`lishi kerak.
Formal (nazariya) sistema formallashtirilgan nazariya tushunchasining xususiy holi bo`lib , formal nazariya o`zining isbotlanuvchi (keltirib chiqariluvchi) formulalari sinfi bilan aniqlansa, formallashtirilgan nazariya o`zining rost (umumrost, umumqiymatli) formulalari sinfi bilan aniqlanadi. Bu sinf, odatda, keltirib chiqarishga nisbatan yopiq bo`lishi kerak, ya`ni rost formulalardan keltirib chiqariluvchi har bir formula rost bo`lishi kerak. Tabiiy , bunda formallashtirilgan nazariyaning aksiomalari ham rost formulalar bo`lishi kerak.
Formallashtirilgan nazariyani ma`lum bir mazmunda unga ekvivalent bo`lgan formal sistema bilan ifodalash mumkin, ya`ni bu nazariyaning barcha rost formulalari sinfini biror aksiomalar sistemasidan keltirib chiqarish qoidalari yordamida hosil qilinadigan formulalar sinfi sifatida hosil qilish mumkinmi – degan masala, odatda, muhim masaladir. Bu masalani yana quyidagicha qo`yish mumkin: formallashtirilgan nazariyani aksiomalashtirish mumkunmi, ya`ni uni biror aksiomatik qurilgan formal sistema ekvivalent deyish mumkinmi ?
“Formalizm” yo’nalishining namoyondalari bugun matematika aksiomalashtiriluvchi nazariya deb hisoblashgan edilar. Ammo aslida ko`pgina matematik nazariyalar, jumladan, natural sonlar arifmetikasi aksiomalashtiriluvchi nazariya emasligi aniq bo`ldi.
1931-yili avstraliyalik K.Gyodel o`zining mashxur ikkita teoremasini e`lon qildi. Bu teoremalardan birinchisining mazmuni shundan iboratki, (formal) arifmetikaning yoki (formal) arifmetikani o`z ichiga olgan har qanday formal sistemaning zidsizligini shu nazariyaning o`z vositalari yordamida isbotlab bo`lmaydi ya`ni formal sistemaning zidsizligini isbotlash uchun unga kirmaydigan kuchliroq vositalar ishlatilishi kerak.
Gyodel teoremasining ikkinchisi ushbu mazmunga egadir:
Formal arifmetikada shunday formula topiladiki , u rost formula bo`lib, o`zi ham, inkori ham formal arifmetikada keltirib chiqariluvchi formulalar emasdur.
Mazkur teorema Gyodelning arifmetikaning to`liq emasligi haqidagi teoremasi deyiladi. Gyodel teoremalari , birinchidan , arufmetika aksiomalashtiriluvchi nazariya emasligini ko`rsatgan bo`lsa ikkinchidan Gilbert dasturi bajarilmasligini namoyish qiladi.
