Интуиционистская Логика

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

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

Л. Развитие интуиционистской теории видов позволяет в рамках интуиционизма точно формулировать многие семантич. Проблемы. Так, К. Гёдель (К. Godel) показал, что полнота интуиционистского исчисления предикатов относительно интуиционистской теории видов влечет принцип конструктивного подбора Маркова для примитивно-рекурсивных предикатов, что является аргументом в пользу неполноты исчисления предикатов с точки зрения такой семантики. С другой стороны, были найдены интуиционистски приемлемые доказательства полноты И. Л. Относительно алгебраич. Семантик типа моделей Бета или моделей Крипке. Лит.:[1] Гейтинг А., Интуиционизм, пер. С англ., М., 1965. [2] К л и н и С. К., Введение в метаматематику, пер. С англ., М., 1957. А. Г. Драгалин..