Дәріс 4. Формальды жүйелер

Формальды жүйелер анықталған, егер:

1. Соңғы алфавит берілген

2. Формула құру процедурасы анықталған

3. Аксиома деп аталатын формулалар белгіленген

4.  Соңғы шығару ережелер жиыны берілген, ол бір формулалар жиыннан басқа формулалар жиынын алуға мүмкіндік береді. Бұл ережелер мына түрде берілген:

Ui және Wi - формалды жүйе формуласы, -> «следует» Формалды жүйені аксиоматика немесе  формальды теория деп атайды. Және бұларда ауыспалы және операторлы константалар анықталады. Ереже қойылымы барлық формалды жүйелерде жарамды болып саналады.  Ереже нәтижесін формалды жүйеге жататын қандай да болмасын М формуласына қою үшін, Q ережесінің сол элементін М формуласымен біріктіру керек. Бұл Q элементін қою немесе М элементін қою көмегімен анықталады.Қойылым формалды жүйеден формулаларды ауыстырумен бекітіледі.

Формалды жүйе берілімінде бірінші сұрақ инверсия туралы, яғни қандай да болмасын қалыпты жүйе формуласын қарастыра отырып, оның дәлелдеме бола ма, жоқ па соны анықтау. Басқаша айтқанда берілген формула теорема бола ма, жоқ па және оны қалай дәлелдеу керек екенін анықтау.

  Математикада формалды жүйе тапсырмалары соңында берілген сұраққа жауап табатын, жақсы анықталған тәсіл беріледі. Бұл тәсіл, егер ол бар болса, процедура шешімі деп аталады, сәйкес формалды жүйесі шешілген деп аталады. Негізінен, мұндай процедура жиі кездесе бермейді, тіпті қарапайым теоремаларда да. Оның себебі келесілерден тұрады. Тіпті сөз жасау ережесін (формула құрастыру ережесі, нәтиже ережесі) қалыпты жүйенің барлық объектісіне қарастырсақ, онда қалыпты жүйе ауытқымалы мүмкіндікте де (тіпті бітпейтін сандарда да) қарапайым теорияда да орындала бермейді. Комбинаторлық әдіспен де бұл мәселені шешу мүмкін емес, қарастырылып отырған формуланың сұрағына жауап алмасақ, онда оның себебін де түсіндіру мүмкін емес: онда қарастырылып отырған формула теорема емес, не қалыпты жүйенің шешімі жоқ. Бұндай тәсіл, процедура шешімі деп аталады.       

Формалды жүйе жай ғана “ми ойыны” болып келмейді, шындық моделін сипаттайды (нақты немесе математикалық). Интерпретация қалыпты жүйенің жай күйін көрсетеді. Интерпретация қалыпты жүйенің барлық символына түсініктеме береді және объектілерге де. Қалыпты жүйенің теоремалары интерпретаталы, қарапайым сөз түсінігінде расталған, және бұл жағдайда ақиқат немесе жалған нәтиже шығару. Интерпретация формалды жүйенің шындық өмірін сипаттайды.

     Интерпретация формалды жүйенің әрбір символына анықтама береді, символдар мен объектілер арасындағы сәйкестікті береді. Математик бірінші формалды жүйе туралы оқып, содан кейін теореманы дәлелдейді. Осы нәтиженің арқасында бірдей формалды жүйелер көпсанды нақты моделдерге қызмет етеді. Интерпретация теориясына формализация нәтижесінде алған нәтижені қайтарады.

Нақты формалды жүйе қызықты болып келеді. Бір формалды дәлелдеме нақты нәтиже көрсетеді. Жаңа математикада формалды жүйе категория теориясында және модель теориясында үлкен роль атқарады.

Дәлелдеме және шындық. Концепция дәлелдемесі мен шындық арасында айырмашылық бар. Бұл түсініктемелер екі облысқа жатады. Шындық пен дәлелдеме арасында төрт нұсқалы айырмашылық бар. Формула бір жағынан теорема болуы мүмкін, екінші жағынан оның интерпретациясы шындық (К)  немесе жалған (F) болуы мүмкін.