Математическая энциклопедия - интуиционистская логика

совокупность приемлемых с точки зрения интуиционизма методов доказательства утверждений. В более узком смысле под И. л. понимается интуиционистское исчисление предикатов, сформулированное А. Рейтингом (A. Heyting) в 1930. Это исчисление формулируется обычно в стандартном языке предикатов исчисления, содержит все схемы аксиом и правила вывода интуиционистского исчисления высказываний (но для языка исчисления предикатов) и, кроме того, следующие кванторные аксиомы и правила вывода. Аксиомы:

Два правила вывода:

где хпеременная, tтерм языка, формула Сне содержит хв качестве параметра.

Полнота интуиционистского исчисления предикатов зависит от семантич. принципов, к-рые лежат в основе рассматриваемой интуиционистской теории. Так, принцип конструктивного подбора Маркова (см. Конструктивного подбора принцип )в форме

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

являющийся истинным в нек-рых интуиционистских интерпретациях и в то же время несовместный с принципом конструктивного подбора в рамках арифметич. теории с Чёрча тезисом. Приведенные примеры показывают, что не существует единого полного интуиционистского исчисления предикатов, к-рое могло бы служить логич. базисом всех прикладных интуиционистских теорий. В зависимости от применяемых семантич. соглашений возможны существенно различные варианты И. л. Развитие интуиционистской теории видов позволяет в рамках интуиционизма точно формулировать многие семантич. проблемы. Так, К. Гёдель (К. Godel) показал, что полнота интуиционистского исчисления предикатов относительно интуиционистской теории видов влечет принцип конструктивного подбора Маркова для примитивно-рекурсивных предикатов, что является аргументом в пользу неполноты исчисления предикатов с точки зрения такой семантики. С другой стороны, были найдены интуиционистски приемлемые доказательства полноты И. л. относительно алгебраич. семантик типа моделей Бета или моделей Крипке.

Лит.:[1] Гейтинг А., Интуиционизм, пер. с англ., М., 1965; [2] К л и н и С. К., Введение в метаматематику, пер. с англ., М., 1957.

А. Г. Драгалин.

Математическая энциклопедия. — М.: Советская энциклопедия

И. М. Виноградов

1977—1985