МАТЕМАТИ́ЧНА ЛО́ГІКА — наука про математичні методи побудови й аналізу міркувань. Ін. назви: символ. логіка, формал. логіка. Включає як матем. під­ходи до міркувань взагалі, так і способи формалізації самих матем. теорій. Становле­н­ня М. л. роз­почалося у серед. 19 ст., коли англ. математик Дж. Буль та шотланд. математик А. Морґан описали формал. алгебраїчну систему (нині ві­дома як булева алгебра) та вказали, що логіка висловлювань може бути формально описана засобами такої системи. Цей під­хід роз­вивав класичне аристотелів. уявле­н­ня про логіку та до­зволив роз­глядати її також і як матем. теорію, описувати та досліджувати алгебраїч. методами. Пізніше алгебру логіки почали за­стосовувати під час проектува­н­ня та роз­робле­н­ня електрон. обчислюв. при­строїв. У теорії складності обчислень використовують низку задач алгебри логіки, зокрема задачі про виконливість булевих схем і формул. Роз­виток метаматематики (під­ґрунтя) у 2-й пол. 19 ст. у ви­гляді аксіоматич. під­ходу до осн. на той час її роз­ділів призвів до інтенсив. викори­ста­н­ня логіч. апарату. Водночас виникне­н­ня логіч. парадоксів зумовило необхідність формалізувати не лише самі матем. теорії, а й способи їх побудови та вираже­н­ня. Формал. теорія містить такі компоненти, як алфавіт, тобто набір символів, що в ній використовують, правильно побудовані формули над цим алфавітом, тобто ті слова над алфавітом, що роз­глядають в теорії, аксіоми теорії та правила виводу. Математики ввели поня­т­тя «формал. виводу» та сукупність формул, що формально виводять з аксіом. Найбільш важливими формал. теоріями є числе­н­ня висловлювань, числе­н­ня предикатів, теорії першого порядку та теорії першого порядку з рівністю. Ключові властивості формал. теорій: аксіоматичність, роз­вʼязність, несуперечливість і повнота. Найістотніший роз­виток М. л. від­бувався у 1-й третині 20 ст. Тоді створ. формал. теорію множин, доведено повноту теорій першого порядку й алгоритмічну неро-звʼязність низки задач, введено формал. поня­т­тя «алгоритм». Одним з найбільш знач. результатів того періоду є теорема Ґьоделя про неповноту, що встановила певні межі за­стосовності формально-логіч. під­ходу в математиці. Осн. роз­діли М. л.: теорія множин, теорія моделей, теорія обчислюваності (теорія рекурсії) та теорія доведень. У теорії множин роз­глядають формалізації (аксіоматизації), що до­зволяють строго ви­вчати множини, дії над ними та повʼязані з ними поня­т­тя, зокрема й «потужності». Найві­домішою з них є аксіоматизація Цермело–Френкеля. Часто досліджуваною та вживаною є аксіома вибору. Доведено її незалежність від ін. аксіом. Також тривалий час на роз­виток теорії множин значно впливала континуум-гіпотеза, включена 1901 нім. математиком Д. Гільбертом до пере­ліку 23-х найважливіших нерозвʼязаних матем. задач. Нім. математик К. Ґьодель показав, що ця гіпотеза не може бути спростована в існуючій аксіоматизації, а амер. математик П.-Дж. Коен об­ґрунтував, що довести її справедливість неможливо. Теорія моделей роз­глядає семантичні властивості формал. синтаксич. систем. Важливим напрямом дослідж. є побудова й аналіз не­стандарт. теорій (напр., не­стандарт. аналізу). В теорії обчислюваності ви­вчають як конкретні формалізації поня­т­тя «алгоритм», так і нерозвʼязні алгоритмічно задачі. Остан­ні поділяють за т. зв. ступ. нерозвʼязності. Теорія нерозвʼяз. алгоритмічно про­блем базується на діагонал. методі Кантора, поня­т­тях ефектив. нумерації, рекурсив. злічен­ності та поліноміал. звідності; містить такі приклади, як про­блема зупинки машин Тьюрінґа та функція продуктивності Радо. Класичні під­ходи до формалізації поня­т­тя «алгоритм» містять машини Тьюрінґа, лямбда-числе­н­ня, рекурсивні функції, системи пере­писува­н­ня Поста та нормал. алгоритми Маркова. Клас алгоритмів, ви­значений кожним з цих під­ходів, є одним і тим же. Згідно з тезою амер. математика А. Чьорча, він містить усі можливі алгоритми у нестрогому, інтуїтив. сенсі. Тьюрінґово повним називають сукупність алгоритмів, що містить усі алгоритми, формалізовані одним із вказаних методів. Теорія обчислюваності — основа як роз­робленої амер. математиком Дж. фон Но­йманом архітектури сучас. електрон. обчислюв. при­строїв, так і мов про­грамува­н­ня, що поділяють на імперативні та функціональні. Теорія доведень роз­глядає формал. виводи теорем у формал. теоріях. Самі правила побудови виводів, їхні типи та властивості є основою різних методологій отрима­н­ня теорем у формал. теоріях. М. л. за­стосовують у філософії, праві, екон. теорії, психології, інформатиці, про­грам. і компʼютер. інженерії.