There is a formal definition for the notion of a formal proof.
Question 1. Is there any formal definition for the notion of a diagonal formal proof?
Consider the following theorems both proved by diagonal proofs.
Theorem 1. (Cantor) $2^{\aleph_{0}}>\aleph_{0}$
Theorem 2. (Godel) $ZFC\nvdash Con(ZFC)$
Question 2. Are there any known non-diagonal proofs for these theorems?
There are proofs for non-existence of formal proofs for some mathematical statements. Now Assuming an affirmative answer for the question 1,
Question 3. Are there proofs for non-existence of non-diagonal formal proofs for some mathematical statements? Are Cantor and Godel's theorems in this category?
Best Answer
This isn't an answer but a proposal for a precise form of the question. First, here is an abstract form of Cantor's theorem (which morally gives Godel's theorem as well) in which the role of the diagonal can be clarified.
Lawvere's fixed point theorem: Let $X, Y$ be objects in a cartesian closed category. Suppose $f : X \times X \to Y$ is a map such that $\text{curry}(f): X \to Y^X$ is surjective on points in the sense that the induced map $\text{Hom}(1, X) \to \text{Hom}(1, Y^X) \cong \text{Hom}(X, Y)$ is surjective. Then $Y$ has the fixed point property: every map $g : Y \to Y$ has a fixed point in the sense that if $g$ is such a map then we can find a map $y : 1 \to Y$ such that $g \circ y = y$.
Proof. Write down the composition $h = g \circ f \circ \Delta_X : X \to Y$, where $\Delta_X : X \to X \times X$ is the diagonal map. By hypothesis, there exists a point $x : 1 \to X$ such that $h = f \circ (x \times \text{id}_X)$. But then
$$h \circ x = f \circ (x \times x) = f \circ \Delta_X \circ x$$
so $g \circ h \circ x = g \circ f \circ \Delta_X \circ x = h \circ x$, and it follows that $h \circ x : 1 \to Y$ is the desired fixed point. $\Box$
(We get back Cantor's theorem by taking the contrapositive and noting that if $Y = 2$ is the $2$-element set in $\text{Set}$, then it fails to have the fixed point property. But there are interesting special cases where we don't take the contrapositive but actually conclude that something has the fixed point property. See, for example, Yanofsky.)
We can try to remove the diagonal map from this proof by working in a closed monoidal category, which retains all of the other structure we use above. So here is a precise form of the question:
I would be very surprised if the answer was yes. Unfortunately, off the top of my head, the examples I'm familiar with of non-cartesian closed monoidal categories (for example, $\text{Vect}$) have zero objects, and every object in a category with zero objects trivially has the fixed point property because the zero morphism is always a fixed point.