ЛОГИКО-МАТЕМАТИЧЕСКОЕ ИСЧИСЛЕНИЕ

— формализация математической (или логической) аксиоматической теории. Л.-м. и. задают языком логико-математическим, списком постулатов (аксиом и правил вывода) и в большинстве случаев снабжают семантикой. Существенными чертами, которыми Л.-м. и. отличаются от аксиоматических теорий традиционной математики, являются: переход от разговорного языка к точному формализованному языку и выявление используемых теорией логич. средств с помощью полного перечисления всех аксиом и всех правил, позволяющих выводить одно утверждение из другого. Язык Л.-м. и. и перечень его постулатов образуют синтаксис. Осн. единица языка Л.-м. и.- формула, которая интерпретируется как высказывание или как высказывательная ф-ция (если формула содержит свободные переменные). Осн. понятие теории Л.-м. и.- понятие вывода (из гипотез). Формула А (или секвенция — для секвенциальных исчислений, см. Генцена формальные системы), не являющаяся аксиомой, есть вывод ф-лы А из списка гипотез А. Аксиома есть свой собственный вывод из пустого списка гипотез. Если выводы из списков и В получается из по одному из правил рассматриваемого Л.-м. и., то есть вывод А из списка

. Ф-ла выводима, если имеется ее вывод из пустого списка допущений. По языку Л.-м. и. классифицируются на исчисления первого и более высоких порядков; исчисления первого порядка в свою очередь делят кванторные и бескванторные. Самое крупнее подразделение Л.-м. и. по семантическому признаку — это деление на классический и неклассические исчисления. Классически исчисления содержат (в той или иной форме) постулат, выражающий в интерпретации, чего любое высказывание либо истинно, либо ожно. В большинстве случаев таким постулатом является исключенного третьего закон p. V А или правило разбора случаев: из вывести В. Часто неклассическими считаются также логики, содержащие нетрадиционные логические связки [напр., модальные исчисления со связками (необходимо) (возможно)], даже если в них постулирован закон исключенного третьего.

Два Л.-м. и. наз. равнообъемными (эквивалентными), если мн-ва выводимых в них объектов совпадают. Иногда равнообъемность понимается более широко: достаточно, чтобы совпадали мн-ва выводимых объектов спец. вида. Так, при сравнении исчислений предикатов иногда ограничиваются рассмотрением чистых которые никакая переменная не входит и свободно, и связанно), а при сравнении генценовских исчислений — рассмотрением секвенций только вида А (т. е., по существу, формул). Часто рассматривают мн-во не только выводимых ф-л, но и выводимых (производных) правил: правило систем называемых применениями этого правила; посылки; В — заключение] производно в Л.-м. и., если заключение каждого его применения выводимо из его посылок. От производных следует отличать допустимые правила, присоединение которых не изменяет объема выводимых правило подстановки вместо пропозициональной переменной допустимо в классическом исчислении высказываний (сформулированном с использованием схем аксиом), но не производно в нем. Л.-м. и. делятся на логические и собственно логико-математические (прикладные).

Логические исчисления основаны на логич. языках; понятие ф-лы, выводимой в логич. исчислении, служит уточнением и формализацией понятия утверждения, истинного в силу своей логической формы, независимо от истолкования входящих в него символов понятий и отношений. Примеры: классическое исчисление высказываний, исчисление предикатов и др.

Исчисления высказываний — это логич. исчисления, в которых заданы правила оперирования с пропозициональными логическими связками (см. Логические операции), но не предусмотрены правила оперирования с кванторами (V, 3) и предметными переменными, хотя такого рода символы могут быть в языке исчисления. Постулаты чаще всего делятся на группы, соответствующие оперированию со связкой: ее введению (доказательству ф-л, содержащих связку) и удалению (использованию уже доказанных ф-л, содержащих связку). Примеры: правило , аксиома правила . Аксиомы (S - удаления получаются из правил заменой на 3.

Среди неклассических исчислений чаще всего упоминаются многозначные логики и конструктивное (интуиционистское) исчисление высказываний (см. Логика конструктивная), аксиоматика которого получается удалением схемы из аксиоматики классического исчисления высказываний.

Важным методом исследования структуры исчислений высказываний является использование матриц — конечных таблиц для связок исчисления, аналогичных обычным таблицам для булевых функций, но имеющих, возможно, несколько выделенных значений (соответствующих значению «истина»). Формула общезначима на матрице, если при любой комбинации значений пропозициональных переменных она принимает одно из выделенных значений; формула опровержима, если она не общезначима. Матрица М корректна для исчисления, если все выводимые формулы общезначимы на М. Исчисление наз. финитно аппроксимируемым, если имеется последовательность матриц, корректных для этого исчисления и таких, что любая невыводимая формула опровержима на одной из матриц этой последовательности. Для финитно аппроксимируемого исчисления разрешима проблема распознавания выводимых формул: чтобы узнать, выводима ли формула А, следует развернуть процесс порождения формул из аксиом по правилам вывода и процесс поиска опровержения А на матрицах из последовательности Один из этих процессов оборвется через конечное число шагов и даст искомый ответ. Матрица М адекватна для некоторого исчисления, если для любой формулы общезначимость на М эквивалентна ее выводимости. Обычная булева матрица адекватна для классического исчисления высказываний; аналогично этому многозначные матрицы адекватны для многозначных исчислений высказываний. Для остальных исчислений высказываний адекватные матрицы обычно невозможны.

Исчисление предикатов (узкое) получается обычно из соответствующего исчисления высказываний путем расширения языка и добавления аксиом где t — терм, свободный для а также добавления правил (-удаление), где не входит свободно в С (или соответствующих правил для генценовского

варианта). В неклассических исчислениях иногда добавляются отдельные аксиомы, связывающие пропозициональные связки и кванторы. В случае, если имеются исчисления с несколькими сортами переменных в аксиомах -удаления и Введения требуется, чтобы t был термом того же сорта, что и переменная

Исчисление предикатовс равенством — результат добавления к соответствующему исчислению предикатов символа аксиомами:

для любой формулы А.

Прикладные исчисления обычно представляют собой формализацию теории некоторых ф-ций и предикатов. Специфические (т. е. нелогические) аксиомы выражают свойства этих ф-ций и предикатов, а логич. аппарат (за исключением бескванторного случая) — соответствующее исчисление предикатов (с равенством, если оно входит в язык рассматриваемой системы). Бескванторные прикладные исчисления либо снабжаются логическим аппаратом исчисления высказываний (чаще всего классического, т. к. основные предикаты оказываются разрешимыми; см. Алгоритмов теория), либо (если единственным предикатом является равенство) оформляются в виде исчисления равенств. Аксиомами тогда считают определяющие равенства рассматриваемых ф-ций , а правила вывода формализуют: 1) осн. свойства равенства (рефлексивность, симметричность, транзитивность, возможность замены одного из равных объектов другим); 2) рассуждения методом матем. индукции (чаще всего по образцу: можно вывести правило отождествления ф-ций, определяемых одной и той же примитивной рекурсией); 3) рассуждения, соответствующие -удалению: «из можно вывести (правило подстановки вместо свободной предметной переменной). Прикладными исчислениями являются, напр., примитивно рекурсивная арифметика (бескванторное прикладное исчисление), арифметика формальная, аксиоматические множеств теории, элементарная групп теория, аксиоматическая проективная геометрия, арифметика 2-го порядка с одноместными предикатами и несколькими ф-циями следования (прикладное исчисление 2-го порядка).

Семантика Л.-м. и. задает интерпретацию переменных матем. символов (символов предикатов и ф-ций) и логических операций. Тем самым определяются модели Л.-м. и. Важным свойством, которым обладают не все Л.-м. и., является семантическая полнота: формула, истинная на всех моделях, выводима. Семантически полными оказываются классическое исчисление высказываний, классическое исчисление предикатов узкое и др. Дедуктивная полнота означает, что каждая формула А без свободных переменных выводима, или опровержима (т. е. выводима ). Из дедуктивной полноты Л. -м. и. следует разрешимость проблемы выводимости — существование алгоритма, позволяющего по каждой формуле узнать, выводима она или нет. Важнейшим дедуктивно полным Л. -м. и. является теория вещественно замкнутых полей (система, Тарского). Согласно Гёделя теореме о неполноте дедуктивно полные теории редки; всякое Л.-м. и., содержащее некоторый весьма узкий фрагмент арифметики, дедуктивно (и семантически) неполно. Для еще более широкого класса Л.-м. и. (включающего исчисление предикатов, формализованную арифметику и др.) проблема выводимости неразрешима (теорема Чёрча).

Вопросы внутр. структуры Л.-м. и. — непротиворечивость, независимость отдельных постулатов, существование отделенных аксиоматик (т. е. таких, что всякая выводимая формула А имеет вывод, использующий постулаты лишь для символов, входящих в А, и, быть может, для импликации), существование интерпретаций одних Л.-м. и. в других и т. д. — исследуются в доказательств теории.

Лит.: Новиков П. С. Элементы математической логики. М., 1973; Клини С. К. Математическая логика. Пер. с англ. М., 1973 [библиогр. с. 451—465]; Чёрч А. Введение в математическую логику. Пер. с англ., т. 1. М., 1960; Карри X. Б. Основания математической логики. Пер. с англ. М., 1969 [библиогр. с. 518—547]. Г. Е. Минц.