Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
We have several entries that used to mention Lawvere’s fixed point theorem without linking to it. I have now created a brief entry with citations and linked to it from relevant entries.
I added a proof and some remarks.
Thanks!
The hypothesis of point-surjectivity seems insufficiently general to me. Can the internal Cantor’s theorem in an elementary topos be deduced from this version?
So, let’s see if this is what you want: we want to prove there is no epi in a topos. For any epi , we have that the counit is an equality, so that is a retract of . We thus deduce that for , that is a retract of . But a retraction is automatically point-surjective.
I’d be interested though in potential improvements of the lemma; I’m not aware of any.
Yes, that seems to work. I think I was thinking more along the lines of running the existing proof in the internal logic of the topos.
My feeling is that the internal version of point-surjectivity of is the existence of a section of , which sort of brings us back around to the proof of #5. :-)
I think the internal version of point-surjectivity is being an epimorphism.
I added (in a section “History”) that quote from Lawvere:
In ‘Diagonal arguments and Cartesian closed categories’ we demystified the incompleteness theorem of Gödel and the truth-definition theory of Tarski by showing that both are consequences of some very simple algebra in the Cartesian-closed setting. It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a “paradox” by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science. Now, one hundred years after Gödel’s birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.
At the end of that passage, Lawvere darkly hints at a movement with an agenda to substitute belief for science. Anyone know what he is alluding to? The Templeton Foundation might be what he has in mind; see here for some criticisms that have been mounted.
The article Lawvere’s fixed-point theorem was looking a little thin, so I added one more remark and some related pages (and fixed some small inaccuracies).
I’m puzzled by the earlier sentences in that passage too:
It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a “paradox” by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science.
Is there any evidence of this? I’ve never heard of it before.
I think the part I’d agree with is that the philosophical significance of diagonal arguments, as in Russell’s paradox and incompleteness phenomena, has often been overblown. I’ve not read The Emperor’s New Mind, but just from what I’ve heard, Roger Penrose in his philosophical ruminations might be an example. Probably straight googling would turn up other examples of hyperbole.
Was it Manin who said that the incompleteness of arithmetic is just like a case of finding that some algebra is not finitely generated?
Yes, in Cantor and his heritage:
Baffling discoveries such as Gödel’s incompleteness of arithmetics lose some of their mystery once one comes to understand their content as a statement that a certain algebraic structure simply is not finitely generated with respect to the allowed composition laws.
Direct link for #15. The quote appears on page 7.
That’s right, thanks. Manin goes on to higher categories in a page:
there is no equality of mathematical objects, only equivalences. And since an equivalence is also a mathematical object, there is no equality between them, only the next order equivalence etc., ad infinitim.
Could you add this quote and reference to the entry? Thanks!
That Manin article is a gem. With lots of good quotes, and insights (as one would expect).
Re #18, I added them at incompleteness theorem as it seemed to make more sense there, as not obviously about the fixed-point theorem. But then, in what sense do (in)finite generation and Lawvere’s theorem have something to say to each other?
Thanks!
it seemed to make more sense there
True. Accordingly, I have also copied over that quote by Lawvere to incompleteness theorem. And then I moved both these quotes and the paragraph that precedes them from the beginning of the technical section to the end of the Idea-section, where they clearly belong.
Now if we could un-gray those two links “equational theory” and “primitive recursive arithmetic”, that would be good for the appearance of this entry.
I might be able to work up a stub for primitive recursive arithmetic. Some time back I ran up a flagpole the idea that PRA could be nPOViewed as the walking parametrized NNO, meaning initial among Lawvere theories for which the object (generating objects under products) is a parametrized NNO. A while back I seemed to have found confirmation of this in work of Leopoldo Roman.
I’d have to look again at the article to check why “equational theory” couldn’t simply link to something like Lawvere theory or algebraic theory.
For what it’s worth, I don’t entirely agree with Manin’s comment. Describing the theory of as a “certain algebraic structure” that is not finitely generated by the axioms of Peano arithmetic seems to presuppose a Platonic point of view that there is a “real” “theory of ” about which we can make statements like “it is not finitely generated”, which I find rather dubious.
Yes, I was wondering how the non-finite generation story worked in #20. Is there any way to interpret “a certain algebraic structure” as something other than the theory of ?
An alternative way to prove Cantor’s theorem from Lawvere’s fixed point theorem is the following.
First start exactly like in the proof given in this nlab page, to conclude that there is a proposition which is equivalent to its own negation. But then change the second step to apply Lawvere’s fixed point theorem again, instead, using the fact that this equivalence gives a surjection, and then conclude, in particular, that the map from the initial object 0 to itself has a fixed point, so that the topos is degenerate, because negation is given by implication into 0.
I have written this in univalent mathematics, where in addition to this Cantor theorem for the subtype classifier, we get a Cantor theorem for the universe (= map classifier), again using Lawvere’s fixed point theorem twice.
https://www.cs.bham.ac.uk/~mhe/agda-new/LawvereFPT.html
This doesn’t shorten the proof in length, but somehow seems a more natural or “conceptual” proof, and it is amusing to use LFPT twice. In the case of the universe U, this is even more interesting, because first we get fixed points of endomaps of U, and then, by a second application of the LFTP, fixed points of endomaps of types in U.
Cute!
This does, I think, “-reduce” to the other proof: if you trace through the proof of LFPT, we have (in notation of the nlab page) and and , then the map is the proof of given by “assuming , we have , hence , hence ”. Then from this proof of we lift along to get a proof of , and apply the former to the latter (this is the diagonalization) to get . This is just a longer way to write the proof “Then , whence ” as given.
Would it be okay if someone adds a link to your code to the page?
Thanks, yes, it is okay to add a link.
Regarding the beta reduction, if you first define the maps between p and its negation, and use ctrl-c-ctrl-a (auto) in Agda with them as hints, then you get a proof automatically, which is the beta-unfolding of (the second use of) LFPT.
In return, I have added a circular reference back to the nlab page.
Has anyone tried to make this work for monoidal closed categories?
I haven’t as of yet understood why typed lambda calculus doesn’t model monoidal closed categories just as well as cartesian closed categories. Perhaps someone can inform me on that.
Making this work for monoidal categories would entail replacing product with the monoidal operation, and with the monoidal identity. Point surjective would mean that maps from the monoidal identity lift. Eval comes from the counit of the adjunction. I wonder about this diagonal map … but is the diagonal map really essential here?
It might seem pretty silly, since the other major class of categories this generalization would include is the monoidal linear categories (linear = coproduct isomoprhic to product) (commmonly the monoid distributes over coproduct or product), and there we can say that any map fixes , as there is a unique map from the terminal object.
But there are still some other interesting examples which could lead to fixed point theorems:
1) The category of affine spaces over a ring. If this ring is nonzero then the shift map , has no fixed point. The theorem would say that any map is not surjective. This gives a version of Cantor’s diagonal argument for affine spaces.
2) The category of convex spaces with internal hom being the space of convex maps.
Hmm…maybe these examples are not so important after all.
-Dean edeany@umich.edu
(1) above shows that for all vector spaces :) (1 dimension for the choice of where to send ;
dimension adds in exact sequences and there is an exact sequence of -modules
Now take dimensions to get .
Recall the generalization above would show is that cannot surject onto , so that the dimension of the first is strictly smaller. For infinite cardinals, does nothing. So altogether this would show that for infinite cardinals. :)
typically proofs of this are longer…
Sorry, I I messed up the short exact sequence. It should read
and the unknown characters are < signs.
Suppose you take the category whose objects are Banach spaces and whose morphisms are continuous affine maps between them. This should carry an closed affine monoidal structure. But there should also be surjections , say for a separable infinite-dimensional Hilbert space, and the chosen ground field (real or complex numbers).
I believe it’s no coincidence that it’s called a diagonal argument and that the basic construction uses diagonal maps.
@Todd Trimble
Oh, I see. In hindsight it was a bit of a blunt mistake to suggest that the diagonal argument would not require a diagonal map. Sorry for the time that must have taken from you.
It does suggest the question of whether the proof applies in relevance monoidal categories or monoidal categories with diagonals.
And also the reason that typed lambda calculus models cartesian closed categories rather than monoidal closed categories is that you can use variables any number of times, including 0 (which semantically is modeled by using the “discard” map ) and 2 or more (which semantically is modeled using the diagonal map ). If you restrict to always using every variable exactly once, you get linear logic, which models monoidal categories.
I wrote a short note showing that one only needs a pointed magmatic category with diagonals (none of the coherence conditions of a monoidal cat with diags are needed), to get the diagonal argument to work, but while it works in this generality, I couldn’t think of any decent applications. I’m also not happy with the state of the notes, but can point to them if people really want to see them.
David, I wouldn’t mind having a look at your note.
OK, I will email you, including comments on my current thoughts on it.
The page is about the result of Lawvere 1969 and the quote reflects what its author thinks about the meaning and significance of this result:
we demystified the incompleteness theorem of Gödel and the truth-definition theory of Tarski
1 to 43 of 43