Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 4th 2014

    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.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2014

    I added a proof and some remarks.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 6th 2014

    Thanks!

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2014

    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?

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2014

    So, let’s see if this is what you want: we want to prove there is no epi e:X[X,Ω]e: X \to [X, \Omega] in a topos. For any epi f:XYf: X \to Y, we have that the counit f[f,Ω]1 [Y,Ω]\exists_f \circ [f, \Omega] \leq 1_{[Y, \Omega]} is an equality, so that [Y,Ω][Y, \Omega] is a retract of [X,Ω][X, \Omega]. We thus deduce that for Y=[X,Ω]Y = [X, \Omega], that [Y,Ω][Y, \Omega] is a retract of YY. But a retraction r:Y[Y,Ω]r: Y \to [Y, \Omega] is automatically point-surjective.

    I’d be interested though in potential improvements of the lemma; I’m not aware of any.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2014

    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.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2014

    My feeling is that the internal version of point-surjectivity of f:XYf: X \to Y is the existence of a section of ff, which sort of brings us back around to the proof of #5. :-)

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMar 7th 2014

    I think the internal version of point-surjectivity is being an epimorphism.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2016

    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.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 16th 2016

    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.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 16th 2016

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

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeApr 16th 2016

    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.

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 16th 2016

    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.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 18th 2016

    Was it Manin who said that the incompleteness of arithmetic is just like a case of finding that some algebra is not finitely generated?

    • CommentRowNumber15.
    • CommentAuthorMatt Earnshaw
    • CommentTimeApr 24th 2016

    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.

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 24th 2016
    • (edited Apr 24th 2016)

    Direct link for #15. The quote appears on page 7.

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 24th 2016

    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.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2016

    Could you add this quote and reference to the entry? Thanks!

    • CommentRowNumber19.
    • CommentAuthorTim_Porter
    • CommentTimeApr 25th 2016

    That Manin article is a gem. With lots of good quotes, and insights (as one would expect).

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 25th 2016

    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?

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2016

    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.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2016

    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.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 25th 2016

    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 11 (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.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeApr 25th 2016

    For what it’s worth, I don’t entirely agree with Manin’s comment. Describing the theory of \mathbb{N} 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 \mathbb{N}” about which we can make statements like “it is not finitely generated”, which I find rather dubious.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 26th 2016

    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 \mathbb{N}?

    • CommentRowNumber26.
    • CommentAuthormartinescardo
    • CommentTimeSep 5th 2018
    • (edited Sep 6th 2018)

    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.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2018

    Cute!

    This does, I think, “β\beta-reduce” to the other proof: if you trace through the proof of LFPT, we have (in notation of the nlab page) A=pA=p and B=0B=0 and f=id 0f=id_0, then the map q:1B Aq : 1 \to B^A is the proof of ¬p\neg p given by “assuming pp, we have ppp \wedge p, hence ¬pp\neg p \wedge p, hence 00”. Then from this proof of ¬p\neg p we lift along p=¬pp=\neg p to get a proof of pp, and apply the former to the latter (this is the diagonalization) to get 00. This is just a longer way to write the proof “Then 0=p¬p=pp=p0 = p \wedge \neg p = p \wedge p = p, whence ¬0=0\neg 0 = 0” as given.

    Would it be okay if someone adds a link to your code to the page?

    • CommentRowNumber28.
    • CommentAuthormartinescardo
    • CommentTimeSep 6th 2018
    • (edited Sep 6th 2018)

    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.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2018

    add reference to Escardo’s version

    diff, v9, current

    • CommentRowNumber30.
    • CommentAuthormartinescardo
    • CommentTimeSep 6th 2018

    In return, I have added a circular reference back to the nlab page.

    • CommentRowNumber31.
    • CommentAuthorGuest
    • CommentTimeMar 4th 2020

    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 AAAA \rightarrow A \prod A… 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 XXX \rightarrow X fixes I0XI \rightarrow 0 \rightarrow X, 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 RR is nonzero then the shift map RRR \rightarrow R, aa+1a \mapsto a +1 has no fixed point. The theorem would say that any map A[A,R]A \rightarrow [A, R] 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

    • CommentRowNumber32.
    • CommentAuthorGuest
    • CommentTimeMar 5th 2020

    (1) above shows that dim(V)Unknown characterdim(V *)+1\text{dim}(V) < \text{dim}(V^*) + 1 for all vector spaces :) (1 dimension for the choice of where to send 00;

    dimension adds in exact sequences and there is an exact sequence of RR-modules

    0LinearMaps(V,R)AffineMaps(V,R)eval 0RR0 \rightarrow \text{LinearMaps}( V, R) \rightarrow \text{AffineMaps}(V, R) \stackrel{eval_0}{\rightarrow} R \rightarrow R

    Now take dimensions to get dim(LinearMaps(V,R))+1=dim(AffineMaps(V,R))\text{dim}(\text{LinearMaps}( V, R) ) + 1 = \text{dim}( \text{AffineMaps}(V, R) ).

    Recall the generalization above would show is that VV cannot surject onto AffineMaps(V,R)\text{AffineMaps}(V, R), so that the dimension of the first is strictly smaller. For infinite cardinals, +1+1 does nothing. So altogether this would show that dim(V)Unknown characterdim(V *)\text{dim}(V) < \text{dim}(V^*) for infinite cardinals. :)

    typically proofs of this are longer…

    • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeMar 5th 2020

    Sorry, I I messed up the short exact sequence. It should read

    0LinearMaps(V,R)AffineMaps(V,R)R0 0 \rightarrow \text{LinearMaps}(V, R) \rightarrow \text{AffineMaps}(V, R) \rightarrow R \rightarrow 0

    and the unknown characters are < signs.

    • CommentRowNumber34.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 5th 2020
    • (edited Mar 5th 2020)

    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 A[A,R]A \to [A, R], say for AA a separable infinite-dimensional Hilbert space, and RR 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.

    • CommentRowNumber35.
    • CommentAuthorDean
    • CommentTimeMar 6th 2020
    • (edited Mar 6th 2020)

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

    • CommentRowNumber36.
    • CommentAuthormaxsnew
    • CommentTimeMar 6th 2020

    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 A1A \to 1) and 2 or more (which semantically is modeled using the diagonal map AA×AA \to A \times A). If you restrict to always using every variable exactly once, you get linear logic, which models monoidal categories.

    • CommentRowNumber37.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 7th 2020

    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.

    • CommentRowNumber38.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 7th 2020

    David, I wouldn’t mind having a look at your note.

    • CommentRowNumber39.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 10th 2020

    OK, I will email you, including comments on my current thoughts on it.

    • CommentRowNumber40.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 5th 2021

    More shameless advertising of my recent preprint

    diff, v11, current

    • CommentRowNumber41.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 5th 2021

    Fixed grammar to the new citation, based on Urs’ prompting here

    diff, v12, current

    • CommentRowNumber42.
    • CommentAuthorGuest
    • CommentTimeJan 9th 2023
    It's not clear to me what the meaning, relevance, or significance of quote under "History" is.
    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2023
    • (edited Jan 9th 2023)

    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