> Не, в виде чего угодно плохо, само доказательство должно быть конструкцией. Собранной по правилам нашего конструктора - всяких introduction/elimination правил и связанных с ними definitional equalities.

Да кто же вам это сказал? :)

Вы путаете два совершенно разных понятия - идею, которая у математика в голове, и запись этой идеи. Вот идея (которая вне любых формальных систем, это то, как, и о чем математик рассуждает, собственно, это и есть математика, доказательство, сидящее в голове до того, как его переложили на бумагу), она может быть конструктивной или нет. А как записываете (в какой формальной системе) - это не важно. Конструктивная идея будет иметь конструктивный вид, на каком языке не напиши. И наоборот. Другое дело, что есть некоторые языки, в которых вы просто не сможете выразить неконструктивные идеи. Но какие-то конструктивные идеи вы на нем тоже выразить не сможете.

Напомню, что конструктивизм и интуитивизм вообще появились из-за отказа от формальных систем, убеждения математиков в их ненужности. Единственный критерий конструктивности - мнение математика. Если математик видит алгоритм в вашем доказательстве - оно конструктивное. Других критериев не придумали.

Что до A | -A - формально говоря, это утверждение вовсе нельзя сформулировать в рамках констурктивизма, т.к. тут не говорится ни о существовании объектов ни об их свойствах.