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

Математичка логика е поле во математиката. Се дели на теорија на моделите, доказна теорија, теорија на множествата и теорија на рекурзијата. Истражувањата во математичката логика имаат придонесено кон, и се мотивирани од, изучувањето на основите на математиката, но во математичката логика спаѓаат и области од чистата математика кои не се директно поврзани со основни прашања.

Заедничка тема во математичката логика е изучувањето на експресивната моќ на формалната логика и формалните доказни системи. Оваа моќ се мери по тоа што овие формални системи можат да докажат и по тоа што можат да дефинираат.

Претходно математичката логика се нарекувала симболичка логика (наспроти филозофска логика) и метаматематика. Првонаведениот термин сѐ уште се користи (како кај Здружението за симболичка логика), а второнаведениот термин се користи за извесни аспекти од доказната теорија.

Историја

Називот математичка логика го измислил Џузепе Пеано, кој и го дал на симболичката логика. Во нејзината класична верзија, основните концепти личат на оние на Аристотел, но напишани со симболичка нотација наместо природен јазик. Некои од пофилозофските математичари како Лајбниц и Ламберт направиле обиди за третирање на операциите во формалната логика на симболички или алгебарски начин; но нивните трудови биле малку познати и изолирани. Кон средината на XIX век Џорџ Бул и потоа Огастес Де Морган претставиле систематички математички начин на гледање на логиката. Традиционалната Аристотелова логичка доктрина била реформирана и довршена; и од неа произлегол адекватниот инструмент за истрага во фундаменталните концепти на математиката. Би било збунувачки да се каже дека основните полемики во периодот 1900–1925 се решиле сите до една; но филозофијата на математиката била мошне разјаснета со оваа „нова“ логика.

Додека грчкиот развој во логиката (видете список на теми во логиката) остро ги нагласувал формите на аргументи, ставот на моменталната математичка логика може накратко да се опише како комбинаторичко изучување на содржина. Тука спаѓаат како синтаксичките (на пример праќање на низа формален јазик на компилаторска програма да го напише како секвенца инструкции за машината), така и семантичките (конструирање на конкретни модели или цели множества од нив, во теоријата на моделите). Ова изучување на математиката однадвор се нарекува метаматематика.

Некои дела од клучно значење се „Поимно писмо“ од Готлоб Фреге, „Логички студии“ од Чарлс Парс, „Принципија Математика“ од Бертранд Расел и Алфред Норт Вајтхед и „За формално нерешителните тврдења во „Принципија Математика“ и сродните системи“ од Курт Гедел.

Формална логика

Во нејзината с'рж, математичката логика се занимава со математички концепти изразени по пат на формални логички системи. Системот на логиката од прв ред е најшироко изучуваниот заради неговата применливост во основите на математиката и заради неговите пожелни својства. Се изучуваат и посилните класични логики како логиката од втор ред или бесконечносната логика, заедно со некласичните логики како интуиционистичката логика.

Полиња на математичката логика

Книгата „Прирачник за математичката логика“ (Handbook of Mathematical Logic) (1977) ја дели математичката логика на четири дела:

Теорија на множествата е изучувањето на множествата, кои се апстрактни збирови на предмети.

Основните концепти на теоријата на множествата како подмножеството и релативно дополнение често се нарекуваат наивна теорија на множествата. Современото истражување се одвива во областа на аксиоматската теорија на множествата, која користи логички методи за изучување на тоа кои тврдења се докажливи во разни формални теории како Цермело-Френкеловата теорија на множествата или Новите основи.

Доказна теорија е изучувањето на формалните докази на разните логички дедукциони системи.

Овие докази се претставени како формални математички предмети, упростувајќи ја нивната анализа со математички техники. Фреге работел на математички докази и го формализирал поимот „доказ“.

Теорија на моделите е изучувањето на моделите на разни формални теории.

Множеството од сите модели на дадена теорија се нарекува елементарна класа; класичната теорија на моделите се стреми кон одредување на својствата на моделите на дадена елементарна класа, или да одреди дали извесни класи на структури сочинуваат елементарни класи. Со цел да се покаже дека моделите на дадени теории неможат да бидат премногу комплицирани се користи методата на елиминација на квантификатори.

Теорија на рекурзијата, наречена и теорија на пресметливоста, е изучувањето на својствата на пресметливите функции и Тјуринговите степени, кои ги делат непресметливите функции во множества кои имаат исто ниво на непресметливост.

Во теоријата на рекурзијата исто така спаѓа и изучувањето на генерализирана пресметливост и дефинитивност.

Границите помеѓу овие полиња, како и помеѓу математичката логика и другите полиња на математиката, не секогаш се рески; на пример, Геделовата теорема за непотполноста не е само клучна во теоријата на рекурзијата, и во доказната теорија, туку исто така довела до Лебовата теорема, која е важна во модалната логика. Математичкото поле на теоријата на категориите користи многу формални анксиоматски методи слични на оние користени кај математичката логика, но теоријата на категориите обично не се смета за поле на математичката логика.

Поврзаност со информатиката

Постојат многу врски помеѓу математичката логика и информатиката. Многу од раните пионери на информатиката како Алан Тјуринг, биле исто така математичари и логичари.

Изучувањето на теоријата на пресметливоста во информатиката е во блиско сродство со изучувањето на пресметливоста во математичката логика. Меѓутоа постои и разлика на нагласок. Информатичарите често се концентрираат на конкретни програмски јазици и изведлива пресметливост, додека истражувачите на математичката логика се концентрираат на пресметливоста како теоретски концепт и на непресметливоста.

Изучувањето на семантиката на програмскиот јазик е сродно со теоријата на моделите, како што е програмска верификација (поконкретно проверка на модели). Кари-Хавардовиот изоморфизам помеѓу доказите и програмите е сроден на доказната теорија; интуиционистичката логика и линеарната логика тука играат важна улога. Пресметките како Ламбда-сметањето и комбинаторичката логика денес се изучуваат главно како идеализирани програмски јазици.

Информатиката исто така придонесува кон математиката со развој на техники за автоматска проверка, па дури и изнаоѓање на докази како автоматското докажување на теореми и логичкото програмирање.

Пионерски подвизи

Левенхајм–Сколемовата теорема (1919) покажала дека ако множество реченици во избројлив јазик од прв ред има бесконечен модел, тогаш има најмалку еден модел од секоја бесконечна кардиналност.
Геделовата теорема на потполноста (1929) ја воспоставила еквиваленцијата помеѓу семантичките и синтаксните дефиниции на логичката последователност во логиката од прв ред.
Геделовата теорема за непотполноста (1931) покажала дека ниеден достатно силен формален систем не може да ја докаже сопствената доследност.
Алогаритмичката нерешливост на проблемот на одлучувањето, основан независно од Алан Тјуринг и Алонзо Черч во 1936, покажала дека ниеден компјутерски програм не може да се користи за точно одлучување дали произволните математички искази се вистинити.
Независноста од континуумската хипотеза од Цермело-Френкеловата теорија на множествата (ЦФТМ) покажала дека елементарниот доказ или побивање на оваа хипотеза е невозможно.

Фактот што континуумската хипотеза е доследна на ЦФТМ (ако самата ЦФТМ е доследна) е докажан од Курт Гедел во 1940. Фактот што негацијата на континуумската хипотеза е доследна со ЦФТМ (ако ЦФТМ е доследна) бил докажан од Пол Коен во 1963.

Алогаритмичката нерешливост на Десеттиот Хилбертов проблем, основан од Јуриј Матијасевич во 1970, покажала дека е невозможно било кој компјутерски програм точно да реши дали повеќеваријантните полиноми со коефициенти од цел број воопшто имаат корени од цел број.

Поврзано

Наводи

Andrews, Peter B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof^{[мртва врска]}, Второ изд. Kluwer Academic Publishers.
Barwise, Jon, Едиц. (1977) Handbook of Mathematical Logic, Amsterdam: North-Holland.
George Boolos, John Burgess, и Richard Jeffrey (2002) Computability and Logic, Четврто изд. Cambridge University Press. ISBN 0-521-00758-5.
Enderton, Herbert (2002) A mathematical introduction to logic, Второ изд. Academic Press.
Hamilton, A. G. (1988) Logic for Mathematicians Cambridge University Press.
Wilfrid Hodges, 1997. A Shorter Model Theory. Cambridge University Press.
Mendelson, Elliott (1997) Introduction to Mathematical Logic, Четврто изд. Chapman & Hall.
A. S. Troelstra & H. Schwichtenberg (2000) Basic Proof Theory, Второ изд. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1.