Логико-математические исчисления

прикладные исчисления,- формализации математич. теорий. Л.-м. и. задается своим языком и перечнем постулатов (эти элементы образуют синтаксис).и в большинстве случаев снабжается семантикой. Существенными чертами, отличающими Л.-м. и. от аксиоматич. теорий традиционной математики, являются: 1) выявление используемых теорий логич. средств путем формулирования всех аксиом и вывода правил, позволяющих выводить одно суждение из другого; 2) переход от разговорного языка к точному формальному языку. Обычно Л.-м. и. строится на базе нек-рого логического исчисления (базисного логического исчисления). Язык Л.-м. и. получается из языка этого логич. исчисления добавлением символов специальных функций и предикатов (и, быть может, удалением предикатных переменных и переменных для функций). Перечень постулатов Л.-м. и. получается путем добавления к перечню постулатов базисного логич. исчисления (понимаемых применительно к новому языку) нек-рых постулатов, описывающих свойства добавленных функций и предикатов. Напр., язык элементарной теории групп получается по этой схеме из языка классич. исчисления предикатов с равенством: добавляются символы (умножение), inv (обращение) и е(единица), а выбрасываются все предикатные символы, кроме равенства. Дополнительный постулат [img: http://localhost:8080/file/031325-15.jpg] утверждает, что е - групповая единица, inv (x) - элемент, обратный к x, и умножение ассоциативно. Л.-м. Простейшими по своей структуре являются бескванторные Л.-м. и. Они употребляются чаще всего для описания свойств различных классов вычислимых функций. Язык бескванторного Л.-м. и. строится на основе языка исчисления высказываний с равенством или даже состоит из одних равенств. В первом случае логич. аппаратом Л.-м. и. служит классич. исчисление высказываний, во втором случае Л.-м. и. оформляется в виде исчисления равенств. Постулатами в обоих случаях считаются: 1) определяющие равенства рассматриваемых функций (напр., [img: http://localhost:8080/file/031325-16.jpg]), 2) основные свойства равенства, 3) рассуждения методом матемвтич. индукции (чаще всего по образцу "из [img: http://localhost:8080/file/031325-17.jpg] [img: http://localhost:8080/file/031325-18.jpg]) можно вывести f(x) = g(x)"), 4) рассуждение, соответствующее [img: http://localhost:8080/file/031325-19.jpg] удалению: "из (х).вывести A(t)"(правило подстановки вместо свободной предметной переменной). Пример - система ПРА (примитивно рекурсивная арифметика). Предметные переменные ПРА (а),(аа), (ааа),...;функциональные переменные (f). (ff), (fff),...; натуральные числа 0, 0', 0",... Функциональные символы (функторы) строятся из исходных - ("следующий за"), Z (тождественный 0), [J, п, т](т - местная функция, значение к-рой равно n-му аргументу), где n, т - натуральные числа, [img: http://localhost:8080/file/031325-20.jpg] с помощью подстановки,9 и примитивной рекурсии R:если j есть га-местный функтор, [img: http://localhost:8080/file/031325-21.jpg] суть m-местные функторы, то [img: http://localhost:8080/file/031325-22.jpg] [img: http://localhost:8080/file/031325-23.jpg] (результат подстановки [img: http://localhost:8080/file/031325-24.jpg]) есть m-местный функтор; если j есть re-местный функтор, [img: http://localhost:8080/file/031325-25.jpg] есть (n+2) -местный функтор, то [img: http://localhost:8080/file/031325-26.jpg] есть (n+1) местнын функтор [примитивная рекурсия: [img: http://localhost:8080/file/031325-27.jpg] Термы ПРА: 0, предметные переменные и выражения вида [img: http://localhost:8080/file/031325-28.jpg] где s, s1..., sn - термы, j - функтор. Формулы ПРА: r=s, где r, s - термы. Допустимые значения предметных переменных - натуральные числа, допустимые значения функциональных переменных - примитивно рекурсивные функции (иногда более широкие классы вычислимых функций). При описании частичных (не всюду определенных) функций, кроме предиката равенства, появляется предикат [img: http://localhost:8080/file/031325-29.jpg] или ! ("определено"); r=s интерпретируется в этом случае как [img: http://localhost:8080/file/031325-30.jpg] и из !r следует, что значение r равно значению s". Добавляются также средства для изображения функции, универсальной для рассматриваемого класса: либо символ для этой функции, либо правило: если t - терм, то <t> - функтор (номер к-рого в нек-рой заранее фиксированной нумерации рассматриваемого класса равен t). Постулаты [img: http://localhost:8080/file/031325-31.jpg] -удаления и [img: http://localhost:8080/file/031325-32.jpg] -введения модифицируются: [img: http://localhost:8080/file/031325-33.jpg] Добавляется аксиома !t, где t - предметная переменная или константа, а также аксиомы вида [img: http://localhost:8080/file/031325-34.jpg] Употребляются также Л.-м. и. для описания вычислимых функционалов различных типов: 0 есть тип (объекты типа 0 - натуральные числа); если s и t - типы, то [img: http://localhost:8080/file/031325-35.jpg] есть тип (операций, перерабатывающих объекты типа ав объекты типа t). Это - конечные типы (см. Типов теория). Рассматриваются также трансфинитные типы. Для каждого типа указываются переменные и константы этого типа, в их число обычно входит символ операции, все значения к-рой равны О, а также объект ' типа [img: http://localhost:8080/file/031325-36.jpg] Для каждого sв число констант типа [img: http://localhost:8080/file/031325-37.jpg] часто включают оператор примитивной рекурсии. Термами типа s наз. переменные и константы типа а, выражения вида r(s), где r - терм типа [img: http://localhost:8080/file/031325-38.jpg] s - терм типа t, а также выражение вида [img: http://localhost:8080/file/031325-39.jpg] к-рое интерпретируется как обозначение функционала, перерабатывающего хв r(х), где rтипа b, хтипа a и [img: http://localhost:8080/file/031325-40.jpg] Бескванторные Л.-м. и. для функционалов конечных типов используются для математич. изучения кванторных Л.-м. и. В частности, с помощью бескванторной системы примитивно рекурсивных функционалов удается доказать непротиворечивость формальной арифметики; добавление оператора т. н. бар-рекурсии позволяет доказать непротиворечивость формализованного анализа. Важное свойство Л.-м. и. - дедуктивная полнота: она означает, что каждая формула без свободных переменных выводима или опровержима. Из дедуктивной полноты Л.-м. и. следует разрешимость проблемы выводимости - существование алгоритма, позволяющего по каждой формуле узнать, выводима она или нет. Примером дедуктивно полного Л.-м. и. является теория алгебраически замкнутых полей (система Тарского). Согласно Гёделя теореме о неполноте дедуктивно полные теории редки: всякое Л.-м. и., содержащее нек-рый весьма узкий фрагмент арифметики, дедуктивно неполно. Для еще более широкого класса Л.-м. и. проблема выводимости алгоритмически неразрешима. Важная характеристика Л.-м. и.- его выразительная способность. Часто удается ввести выразительные средства, не фигурирующие явно в языке рассматриваемого Л.-м. и. Так, в бескванторных языках удается ввести логич. связки и ограниченные кванторы: [img: http://localhost:8080/file/031325-41.jpg] В языке формальной арифметики можно говорить о конечных множествах, частично рекурсивных функциях и т. д. Одни логич. связки выражаются через другие; так, в исчислениях 2-го порядка (в том числе основанных на интуиционистской логике) все связки выражаются через [img: http://localhost:8080/file/031325-42.jpg] напр. [img: http://localhost:8080/file/031325-43.jpg] эквивалентно [img: http://localhost:8080/file/031325-44.jpg] [img: http://localhost:8080/file/031325-45.jpg] Принципиальные ограничения выразительной способности языка дает теорема Тарского: при естественной нумерации формул языка, содержащего нек-рый минимум арифметики, невозможно указать формулу Т(х).этого языка такую, что Т(п).истинно тогда и только тогда, когда п - номер истинной формулы. Для Л.-м. и., основанных на конструктивной (интуиционистской) логике, часто имеет место теорема о "расщеплении" дизъюнкций: из выводимости замкнутой формулы [img: http://localhost:8080/file/031325-46.jpg] следует выводимость одной из формул А, В. Для исследования структуры таких Л.-м. и. применяются различные аналоги понятия реализуемости. Вопросы непротиворечивости Л.-м. и., независимости отдельных постулатов, существования отделенных аксиоматик (т. е. таких, что каждая выводимая формула Аимеет вывод, использующий постулаты лишь для импликации и символов, входящих в А), существование интерпретаций одних Л.-м. и. в других исследуются в доказательств теории.