Some rough thoughts (not a complete or formal answer!).

I don't think I've seen this written down anywhere in as many words, but as someone who studies algorithms, let me propose an answer to question 1:

Let *diagonal proof* mean an algorithm taking a map $f: \mathbb{N} \to \mathcal{Y}$ and producing some $y^*$ such that $f^{-1}(y^*) = \emptyset$.

(Of course we did not really need to restrict the domain to the naturals.) In the case of Cantor we take an enumeration of reals and produce a real number not in its range. In the case of Godel's first incompleteness, I think we could for instance take an enumeration of all provable or disprovable statements and produce a statement that is not in the enumeration, *i.e.* neither provable nor disprovable.

Now here is an algorithmic sort of philosophy towards refining question 3: *A non-diagonal proof should be completely non-constructive.* If it constructs an explicit counterexample, then it essentially fits our definition above.

Formalizing this could be quite tricky. Here's one avenue. Suppose we can determine the *computational complexity* of this particular problem, $T$ (i.e. $T$ is the minimum running time of an algorithm, formalized as with e.g. Turing Machines, that given $f$ produces $y^*$). Then suppose we have a proof of a theorem in some theorem-proving language; this is equivalent to a program that produces an instance of a particular type. Then let's consider the proof "nonconstructive" if, for any algorithm "$A$" running in time $o(T)$, invoking that algorithm $A$ on the output of the proof program does not guarantee to produce a counterexample $y^*$.

If you aren't familiar with complexity, the above seems to guarantee that the proof is essentially nonconstructive: $A$ cannot compute a counterexample on its own because $A$ runs in time $o(T)$ and time $T$ is required to compute a counterexample. So all that $A$ has "to work with" is the output of the previous proof. If this output somehow embeds a counterexample, then (presumably) (one might hope) $A$ can uncover and output this counterexample; but if the previous proof is entirely nonconstructive, then there is no hope for $A$ to find a counterexample.

The problem with this complexity approach is that we might be interested in theorems that require Turing Degree higher than zero, or require a type II sort of TM that deals with real numbers, or so on, so complexity isn't necessarily well-defined or well-studied. But hey, it's a really hard problem to say what sort of proof argument is "necessary" for a theorem. It seems clear to me that this is the sort of approach we'll need to formalize it, but I don't know if this has been studied much....

P.S. You can probably also come at this from the direction of Lawvere, something like: Let a fixed-point proof mean an algorithm taking in some $t: Y \to Y$ and a surjective $f: A \to (A \to Y)$ and producing a $y^*$ such that $t(y^*) = y^*$. Then a non-fixed-point proof should be totally nonconstructive, *i.e.* should not provide any means of actually finding a fixed point.

8more comments