Математик логиканың төп мәсьәләләреннән берсе — фикер йөртүләрнең математик исбатлануын өйрәнү. Шул ук вакытта башлангыч, исбатлауларсыз кабул ителгән нигезләмәләр дә (аксиомалар) бар, алардан билгеле бер фикерләү принциплары ярдәмендә нәтиҗәләр чыгарыла. Нәтиҗәнең дөреслеге башлангыч нигезләмәләргә һәм исбатлау барышында кулланылган фикерләү принципларына бәйле. Шул рәвешле үстерелгән матем. теорияләр аксиоматик дип аталалар. Математик логиканың аксиомалар бәйсезлегенә һәм теорияләрнең капма-каршы булмаучанлыгына караган мөһим бүлекләре шулар белән бәйләнгән.

Математик логиканың аксиоматик теориясенә нигез салучы — Россия математигы, Казан университеты профессоры Н.И.Лобачевский. Бу теориянең классик үрнәге булып Евклидның берничә постулатына, шул исәптән турыларның параллельлеге турындагы 5 нче постулатка нигезләнеп төзелгән Евклид геометриясе тора. 5 нче постулатны бу геометриянең башка постулатларыннан чыгарып булмасына инану Лобачевскийны бу постулат Евклид геометриясенең башка аксиомаларына бәйле түгел дигән фикергә китерә. Ул 1826 елда соңыннан Лобачевский геометриясе дип йөртелүче яңа геометрияне төзи һәм анда әлеге постулат капма-каршысы белән алыштырыла. Аннан соң итальян математигы Е.Бельтрами Лобачевский аксиомалары үтәлә торган геометриянең моделен төзи (1868), немец математигы Ф.Клейн Лобачевский геометриясенең капма-каршы булмаганлыгын катгый исбатлый (1872). Шулай итеп, 5 нче постулатның Евклид геометриясенең башка аксиомаларына бәйле түгеллеге дәлилләнә.

ХХ йөздә күплекләр теориясендә математик логиканың мөһим нәтиҗәләре алына: Австрия математигы К.Гедель континуум сайлау һәм аның проблемасы аксиомасының күплекләр теориясе аксиомалары белән капма-каршы булмавын исбатлый (1934), Америка математигы П.Коэн аларның күплекләр теориясе аксиомаларына бәйле түгеллеген билгели (1963).

Математик логикада тикшеренүләр үткәргәндә карала торган математик теория белән билгеле дәрәҗәдә бәйләнгән формаль системалар төзелә. Бу алымның авторы — немец математигы Д.Гильберт. Аңа кадәр бу өлкәдә инглиз мантыйкчысы Дж.Буль, немец математиклары Э.Шредер һәм Г.Фреге, итальян математигы Дж. Пеано, Казан университеты профессоры, астроном П.С.Порецкий хезмәтләрендә логика алгебрасы эшкәртмәләре урын ала. Порецкийның «Логик нигезләмәләрне чишү юллары һәм математик логиканың кире ысулы турында» («О способах решения логических равенств и об обратном способе математической логики», 1884) дигән хезмәте логика алгебрасы үсешендә зур роль уйный. Галим Россиядә беренче тапкыр Казан университетында үзенең әлеге хезмәте нигезендә математик логика курсыннан лекцияләр укый (1887).

Формаль системаларның логика өлеше үз эченә формальләштерелгән аксиомаларны һәм формаль чыгару кагыйдәләрен ала; аларны ничек сайлап алуга һәм фикерләүләр мәгънәсен дөреслек ягыннан ничек кабул итүгә карап, интуицион, конструктив, күп мәгънәле, модаль һ.б. логикаларны аерып өйрәнәләр.

Казан университеты профессоры Н.А.Васильев хезмәтләрендә урын алган идеяләр күп мәгънәле, шулай ук интуицион һәм конструктив логикаларның төп нигезләмәләре чагылышы буларак бәяләнә.

1960 еллардан башлап Казан университетында Н.К.Замов җитәкчелегендә исбатлаулар теориясе, гамәли математик логика, ясалма интеллект теориясе, программалар синтезы һәм программалаштыруны укыту методикасы өлкәләрендә тикшеренүләр алып барыла. Резолюцияләр алымында терминнарны тәртипкә салу стратегиясе эшләнә, һәм ул предикатлар исәпләүнең бик күп формулалары өчен хәлиткеч процедура булып тора. Шул ук алым нигезендә теоремаларны исбатлау программасы төзелә, аның ярдәмендә модаль логикалар һәм күплекләр теориясенең күпчелек теоремаларын автоматик режимга исбатларга мөмкин (В.Ю.Базылев, В.Ю.Михайлов).

Математик логика алгоритмнар теориясе белән принципиаль бәйләнгән. XX йөзнең урталарында инглиз математигы А.Тьюринг һәм Америка математигы А.Черч хезмәтләрендә алгоритмик чишелүчән функция төшенчәсе аныклана, ә бу элегрәк чишелеш алгоритмы табылмый килгән күп кенә математик проблемаларның алгоритмик чишелмәүчәнлеген исбатларга мөмкинлек бирә. 1970 елларда Казан университеты галимнәре М.М.Арсланов җитәкчелегендә алгоритмик чишелмәүчән теорияләрне чишелмәүчәнлек дәрәҗәләре буенча классификациялиләр; матем. проблемаларның әлеге класслар иерархиясендәге конкрет баскычка керүе критерийларын табалар, чишелмәүчәнлек дәрәҗәләрен төп җыелучанлыклары буенча тәртипкә салуның алгебраик структурасын төзүгә зур өлеш кертәләр.

Әдәбият       

Клини С.К. Математическая логика. М., 1973;

Арсланов М.М. Рекурсивное перечисление множества и степени неразрешимости. К., 1986;

Resolution methods for the decision problem. B.–N.Y., 1993.                      Автор — М.М.Арсланов