Статья 349

Классическая логика вкладывается в интуиционистскую с помощью, например, вставки двух отрицаний перед каждой элементарной подформулой и каждой подформулой вида. Если доказуемо, то доказуемо либо, либо. Если доказуемо, то доказуемо Последние два свойства называются свойством дизъюнкции и свойством существования. Они выполнены лишь для выводимости без допущений, в частности, они могут быть невыполнены в конкретной аксиоматической теории. Поэтому они могут рассматриваться.
В самом деле, классическую логику можно рассматривать как интуиционистскую прикладную теорию, если к ней добавить схему аксиом как необходимый признак конструктивности интуиционистской теории.
Важную роль в конструктивном истолковании интуиционистской теории играют позитивные подформулы, которые не входят ни в одну посылку импликации и ни в одну подформулу типа.