Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
1  
The Baire Category Theorem implies $2^\omega > \omega$. I wouldn't say it is a diagonal argument. –  Monroe Eskew Feb 27 at 5:38
1  
@Monroe: that's news to me! Can you sketch the proof or give a reference? –  Qiaochu Yuan Feb 27 at 5:56
5  
Sure. BCT says that the intersection of any countable collection of open and dense subsets of the real line is dense. For any $x \in \mathbb{R}$, $\mathbb{R} \setminus \{ x \}$ is open and dense. Thus, for any countable collection of reals $\{ x_n : n \in \mathbb{N} \}$, BCT implies that there is a real in $\bigcap_{n} \mathbb{R} \setminus \{ x_n \}$. Hence $\mathbb{R}$ is not countable. –  Monroe Eskew Feb 27 at 6:05
3  
@MonroeEskew, the comments in Andres' link seem to conclude that the Baire Category Theorem can be cast as a diagonalization argument. –  usul Feb 27 at 6:57
2  
There are some other questions here and/or math.se ... things like "Proofs of uncountability of the reals" or "undecidable statements not using self-reference" –  Gerald Edgar Feb 27 at 14:19
show 8 more comments

4 Answers

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.

share|improve this answer
    
Okay, the category of combinatorial games appears to be a non-cartesian closed monoidal category without a zero object, but I don't understand this category well enough to immediately write down a counterexample in it. –  Qiaochu Yuan Feb 27 at 6:02
    
Another candidate: the category of commutative semigroups. It has a tensor product with the usual universal property but a priori it seems tricky to compute. –  Qiaochu Yuan Feb 27 at 6:15
    
by "morally" do you mean "normally"? (I'm a philosopher not a mathematician) –  ArtB Feb 27 at 18:46
    
@ArtB: I mean "morally" roughly in the sense of cheng.staff.shef.ac.uk/morality/morality.pdf. I can't name a category such that applying Lawvere's FPT in that category reproduces Godel's theorem, and IIRC when I looked into this there were some obstacles to getting this to work directly and you needed to do something tricky, but if the universe were more just this would be the case. –  Qiaochu Yuan Feb 27 at 20:23
1  
Qiaochu: a while back I wrote something about Goedel's incompleteness theorem on the nLab that incorporates Lawvere's FPT; see theorem 1 here: ncatlab.org/nlab/show/incompleteness+theorem –  Todd Trimble Feb 27 at 21:05
add comment

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.

share|improve this answer
1  
On further reflection, we could work with sets graded by any abelian monoid $M$, as long as there is some $m \in M$ so that translation by $m$ is fixed point free. For example, you could take $M = \mathbb{Z}/2$ and work with "super sets". –  David Speyer Feb 27 at 14:03
1  
Nice! It had just occurred to me to try graded sets when I went to bed last night. Just to verify more directly that this monoidal structure is not cartesian, the cartesian product in this category is the fiber product over $\mathbb{Z}_{\ge 0}$; if one thinks of graded sets as analogous to power series, then the cartesian product is like the Hadamard product of power series whereas the monoidal structure above is like the Cauchy product. –  Qiaochu Yuan Feb 27 at 17:08
add comment

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).

share|improve this answer
    
That version has a serious typo, by the way (my fault, not Hugh's). I thought I had uploaded an update. As noted by Robert Solovay, rather than simply requiring that $P$ is a hereditary property of models, we must require that $\mathsf{ZFC}$ proves this. –  Andres Caicedo Feb 28 at 14:53
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.