Высказываний исчисление

ВЫСКАЗЫВАНИЙ ИСЧИСЛЕНИЕ (пропозициональное исчисление), общее название аксиоматических систем (смотри Аксиоматический метод), предназначенных для доказательства утверждений (формул), составленных из простейших (не анализируемых в рамках данной системы) утверждений при помощи логических связок, таких как «не», «или», «если... то...» и др.

С синтаксической точки зрения различают несколько видов высказываний исчисления: так называемый гильбертовские, секвенциальные (генценовские), системы натурального вывода и др. Важнейшим примером высказываний исчисления является классическое высказываний исчисление, где используются традиционные логического связки: «или» (v), «и» (&), «если..., то...» (→), «не» (-). При этом утверждения интерпретируются как булевы функции, принимающие два значения: «истина» (1) и «ложь» (0); связки соответствуют стандартным операциям на множестве {0,1}: v - взятию максимума, & - взятию минимума, и т. д. В гильбертовской формулировке используются схемы аксиом (такие как А → (В → А); А&В→А; В→AvB; Av-A и др.) и единственное правило вывода modus ponens (правило отделения), позволяющее из формул А и А → В получить В. Теоремами этого исчисления являются в точности все тавтологии - формулы, отвечающие тождественно истинным булевым функциям. Отсюда следует алгоритмическая разрешимость, т. е. существование алгоритма, распознающего теоремы данного исчисления (смотри Алгоритмическая проблема).

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

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

Лит.: Клини С. К. Математическая логика. М., 1973; Gabbay D., Guenthner F. Handbook of philosophical logic. 2nd ed. Dordrecht; Boston, 2001-2005. Vol. 1-13.