12

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?

user47544
  • 141
  • 4
    The Baire Category Theorem implies $2^\omega > \omega$. I wouldn't say it is a diagonal argument. – Monroe Eskew Feb 27 '14 at 05:38
  • 1
    @Monroe: that's news to me! Can you sketch the proof or give a reference? – Qiaochu Yuan Feb 27 '14 at 05:56
  • 6
    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 '14 at 06:05
  • 1
    @Monroe: cool. But it's a little distressing that BCT is independent of ZF, isn't it? The standard proof works under much, much weaker set-theoretic hypotheses (given below). – Qiaochu Yuan Feb 27 '14 at 06:09
  • Good point. I don't know of a non-diagonal proof of the uncountability of $\mathbb{R}$ that works in ZF. But dependent choice so obviously true... But now I wonder, is the BCT proof actually non-diagonal in some rigorous sense? – Monroe Eskew Feb 27 '14 at 06:23
  • 1
    For Cantor's theorem, see here. – Andrés E. Caicedo Feb 27 '14 at 06:26
  • @MonroeEskew The proof I linked to in my previous comment works in $\mathsf{ZF}$. – Andrés E. Caicedo Feb 27 '14 at 06:41
  • 4
    @MonroeEskew, the comments in Andres' link seem to conclude that the Baire Category Theorem can be cast as a diagonalization argument. – usul Feb 27 '14 at 06:57
  • 1
    @Qiaochu: For separable completely metrizable spaces BY is provable without any additional choice. See Herrlich, The Axiom of Choice, Theorem 4.102 – Asaf Karagila Feb 27 '14 at 07:06
  • By the way, I believe it was von Neumann who proves that $\sf ZFC$ doesn't prove its own consistency. Goedel did prove the general theorem, though. – Asaf Karagila Feb 27 '14 at 07:58
  • 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 '14 at 14:19
  • Proofs of the uncountability of the reals is definitely related: http://mathoverflow.net/questions/46970/proofs-of-the-uncountability-of-the-reals – Timothy Chow Feb 27 '14 at 22:46
  • The usual proof of the Baire Category Theorem is certainly by diagonalization; we need to meet a sequence of requirements (open sets, in this case) and we meet requirement $i$ on stage $i$. @Monroe Eskew – Carl Mummert Mar 05 '14 at 12:06

4 Answers4

20

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.

Qiaochu Yuan
  • 114,941
  • 1
    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 '14 at 06: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 '14 at 06:15
  • by "morally" do you mean "normally"? (I'm a philosopher not a mathematician) – Sled Feb 27 '14 at 18:46
  • 1
    @ArtB: I mean "morally" roughly in the sense of http://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 '14 at 20:23
  • 2
    Qiaochu: a while back I wrote something about Goedel's incompleteness theorem on the nLab that incorporates Lawvere's FPT; see theorem 1 here: http://ncatlab.org/nlab/show/incompleteness+theorem – Todd Trimble Feb 27 '14 at 21:05
15

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.

David E Speyer
  • 150,821
  • 2
    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 E Speyer Feb 27 '14 at 14:03
  • 2
    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 '14 at 17:08
4

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

Community
  • 1
Martín-Blas Pérez Pinilla
  • 631
  • 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. – Andrés E. Caicedo Feb 28 '14 at 14:53
1

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.

usul
  • 4,429