Математична логіка

Визначення і загальна характеристика

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

Завантажити статтю