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

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

]]>More shameless advertising of my recent preprint

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

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

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

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

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

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

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

$0 \rightarrow \text{LinearMaps}(V, R) \rightarrow \text{AffineMaps}(V, R) \rightarrow R \rightarrow 0$and the unknown characters are < signs.

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

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

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

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

typically proofs of this are longer…

]]>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 $A \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 $X \rightarrow X$ fixes $I \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 $R$ is nonzero then the shift map $R \rightarrow R$, $a \mapsto a +1$ has no fixed point. The theorem would say that any map $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

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

]]>add reference to Escardo’s version

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

]]>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=p$ and $B=0$ and $f=id_0$, then the map $q : 1 \to B^A$ is the proof of $\neg p$ given by “assuming $p$, we have $p \wedge p$, hence $\neg p \wedge p$, hence $0$”. Then from this proof of $\neg p$ we lift along $p=\neg p$ to get a proof of $p$, and apply the former to the latter (this is the diagonalization) to get $0$. This is just a longer way to write the proof “Then $0 = p \wedge \neg p = p \wedge p = p$, whence $\neg 0 = 0$” as given.

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

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

]]>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}$?

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

]]>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 $1$ (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.

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

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

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?

]]>