Are there non-diagonal proofs for Cantor's continuum and Godel's incompletness theorems?

Question

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?

Answer 1

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:

Does Lawvere's fixed point theorem continue to hold for closed monoidal categories?

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.

Answer 2

Here is an answer to Qiaochu's question

Does Lawvere's fixed point theorem continue to hold for closed monoidal categories?

As expected, the answer is "no".

Define a graded set to be a set $X$ with a map $\mathrm{deg}: X \to \mathbb{Z}_{\geq 0}$. For $X$ and $Y$ graded sets, and $d \in \mathbb{Z}_{\geq 0}$, define a map $f: X \to Y$ to have degree $d$ if, for all $x \in X$, we have $\deg(f(x)) = \deg(x) + d$. Define $\mathcal{C}$ to be the category whose obects are graded sets and where $$\mathrm{Hom}_{\mathcal{C}}(X,Y) = \{ (f,d):\ f: X \to Y,\ f\ \mbox{of degree}\ d \}.$$ $$(f,d) \circ (g,e) = (f \circ g, d + e).$$ Let me emphasize that $\mathrm{Hom}_{\mathcal{C}}(\emptyset,Y)$ is $\mathbb{Z}_{\geq 0}$; we do not identify the degree $d$ map from $\emptyset \to Y$ with the degree $e$ map, for $d \neq e$.

Put a monoidal structure on $\mathcal{C}$ where: $$X \otimes Y := X \times Y \quad \mathrm{deg}(x \times y) = \mathrm{deg}(x) + \mathrm{deg}(y)$$ $$1_{\mathcal{C}} = \{ \mathrm{pt} \} \quad \mathrm{deg}(\mathrm{pt}) =0.$$ $$(f,d) \otimes (g,e) = (f \times g, d+e).$$ If I am not confused, this structure is closed, with $Y^X = \mathrm{Hom}_{\mathcal{C}}(X,Y)$ and with $\mathrm{deg}$ taking a map to its degree.

Then take $X = Y = \mathbb{Z}_{\geq 0}$ with $\mathrm{deg}(i) = i$. Note that $Y^X \cong X$, but $Y$ has an automorphism $i \mapsto i+1$ with no fixed points.

Answer 3

About 2 (2nd Gödel) see http://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf, quoted in What are some proofs of Godel's Theorem which are *essentially different* from the original proof? (the zoo of Gödel's proofs).

Answer 4

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.