Анализ теорем арифметики показывает, что в математике употребляются различные варианты отрицания. Нас далее будут интересовать два таких варианта, различие между которыми особенно наглядно проявляется при рассмотрении отрицания всеобщности некоторого суждения.
Обозначим, например, через F некоторое свойство натуральных чисел и рассмотрим следующее высказывание: ..неверно, что всякое число обладает свойством F". Доказательство такого высказывания может быть двояким. С одной стороны, можно под его доказательством понимать приведение к противоречию предположения о том, что всякое число обладает свойством F. С другой стороны, под этим доказательством можно понимать построение некоторого примера, опровергающего, что всякое натуральное число обладает свойством F, т . е. указание такого натурального числа, для которого свойство F не имеет места.
Классическая постановка вопроса не отдает предпочтения доказательству существования опровергающей конструкции перед доказательством путем приведения к противоречию. С конструктивной же точки зрения эти два доказательства равноценными не являются. Построение опро­вергающей конструкции доказывает, очевидно, более сильное утверждение и содержит больше информации.
Это дало основание Нельсону [1] построить логическое исчисление, в котором употребляется вторая форма отрицания, основанная на пост­роении опровергающей конструкции.
Как было показано А. А. Марковым [2] , из правил истолкования с конструктивной точки зрения основных логических связей вытекает, что опровержение путем приведения к противоречию можно в известном смысле выразить через опровержение путем построения опровергающей конструкции.
Тем не менее ограничиваться только второй концепцией отрицания нецелесообразно. Приведение к противоречию является весьма употребительным в математике приемом доказательства , так что в тех моделях
математического мышления, какими являются различные логические ис­числения, свойства соответствующего отрицания должны быть отражены. В обычной конструктивной арифметике (а потому и в обычном конструктивном исчислении высказываний) именно эта форма отрицания и приме­няется.