Конструктивное Исчисление Высказывании

Логическое исчисление, описывающее способы вывода высказываний, истинных с точки зрения конструктивной математики. Обычно этот термин рассматривается как синоним термина интуиционистское исчисление высказываний. Однако, при нек-рых специальных интерпретациях конструктивизма интуиционистское исчисление высказываний оказывается неполным. Напр., известная формула Роуза: где A -формула a p, q- пропозициональные переменные, не выводится в интуиционистском исчислении высказываний и в то же время тождественно истинна в интерпретации рекурсивной реализуемости К лини, по крайней мере, если признавать конструктивного подбора принцип. Актуальной задачей является исследование полноты К. п. в. для различных вариантов семантики конструктивной математики. Лит.:[1] Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; [2] Rоse G. F., "Trans. Amer. Math. Soc", 1953, v. 75, p. 1 — 19. А. Г. Драгалин.