Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 4th 2019
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexHere's something that I was thinking about recently: what is the most general setting of Lawvere's version of the diagonal argument. I wrote [some brief notes](https://github.com/DavidMichaelRoberts/Sandbox/blob/master/Diagonal.pdf). I tweeted the relevant definitions and proof (3 tweets!), but this is a better format. I end with some comments that will probably be expanded over time. I don't yet have nontrivial examples of the categories to which this applies, so would be interested to know if people think of any.

   Here’s something that I was thinking about recently: what is the most general setting of Lawvere’s version of the diagonal argument. I wrote some brief notes. I tweeted the relevant definitions and proof (3 tweets!), but this is a better format. I end with some comments that will probably be expanded over time. I don’t yet have nontrivial examples of the categories to which this applies, so would be interested to know if people think of any.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 4th 2019
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexInteresting! I'll think about this some. I noticed one type in the proof: the term on the right side of the first equation should be $\sigma \circ F \circ \delta \circ a$.

   Interesting! I’ll think about this some. I noticed one type in the proof: the term on the right side of the first equation should be $\sigma \circ F \circ \delta \circ a$.

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 4th 2019
   • (edited May 4th 2019)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThanks, fixed that. Also there was another typo in the definition ($f$ instead of $F$). Was in too much of a hurry when typing this up. I have an article I want to read, _What is wrong with Cantor's diagonal argument?_ ([Logique et Analyse](http://virthost.vub.ac.be/lnaweb/ojs/index.php/LogiqueEtAnalyse/article/view/1709/0)), where the authors are apparently dedicated relevant logicists. This is _actually published_ in a philosophy journal. Added: One of them also wrote [this](https://ojs.victoria.ac.nz/ajl/article/download/4863/4317), where in section 4 it is claim LEM is used in the diagonal argument. Again, published in a philosophy journal, though this time it's more of a retrospective/tribute article. I might talk to the local paraconsistent/inconsistent philosophers and see what they think about this.

   Thanks, fixed that. Also there was another typo in the definition ($f$ instead of $F$). Was in too much of a hurry when typing this up.

   I have an article I want to read, What is wrong with Cantor’s diagonal argument? (Logique et Analyse), where the authors are apparently dedicated relevant logicists. This is actually published in a philosophy journal.

   Added: One of them also wrote this, where in section 4 it is claim LEM is used in the diagonal argument. Again, published in a philosophy journal, though this time it’s more of a retrospective/tribute article.

   I might talk to the local paraconsistent/inconsistent philosophers and see what they think about this.

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 5th 2019
   • (edited May 5th 2019)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI rephrased a key motivational phrase. As it was, it implied one fixed a map $B\to C$ and then allowed the family $A\#B\to C$ to vary when looking for it, whereas of course we want the family to be fixed.

   I rephrased a key motivational phrase. As it was, it implied one fixed a map $B\to C$ and then allowed the family $A\#B\to C$ to vary when looking for it, whereas of course we want the family to be fixed.

5. • CommentRowNumber5.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 5th 2019
   • (edited May 8th 2019)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI guess I should thrash out why it's worth thinking of $F\colon A\#B\to C$ as being a family of morphisms $B\to C$. Given any $a\colon X\to A$, hence supposedly picking out one such morphism, then for any $p\colon Y\to X \in \mathcal{C}/X$ and $b\colon Y\to B$ we get $$ Y\xrightarrow{\delta} Y\# Y \xrightarrow{p\# id_Y} X\# Y \xrightarrow{a\# b} A \# B \xrightarrow{F} C\qquad (1) $$ So, if we think of $a$ as being an element of $A$ at stage $X$, then for any later stage $Y$ (via $p$), we have an assignment of elements $b\mapsto F(p^*a,b)$. I want to think of this, for fixed $a$, as some kind of map of presheaves with codomain the representable given by $C$, but I'd have to think exactly how. Thinking out loud, I have two presheaves $(\mathcal{C}/X)^{op} \to \mathcal{C}^{op} \to Set$, namely $X^*y(B)\colon (Y\to X) \mapsto \mathcal{C}(Y,B)$ and $X^*y(C)\colon (Y\to X) \mapsto \mathcal{C}(Y,C)$. If I've done my calculation correct, $(1)$ above seems like it gives a natural transformation $F_a\colon X^*y(B) \Rightarrow X^*y(C) \colon (\mathcal{C}/X)^{op} \to Set$ with component $(Y\to X) \mapsto \big( (Y\to B) \mapsto (1) \big)$. So the intuition that $F$ is a family of maps $B\to C$ seems to hold up, at some level.

   I guess I should thrash out why it’s worth thinking of $F\colon A\#B\to C$ as being a family of morphisms $B\to C$. Given any $a\colon X\to A$, hence supposedly picking out one such morphism, then for any $p\colon Y\to X \in \mathcal{C}/X$ and $b\colon Y\to B$ we get

   $$Y\xrightarrow{\delta} Y\# Y \xrightarrow{p\# id_Y} X\# Y \xrightarrow{a\# b} A \# B \xrightarrow{F} C\qquad (1)$$

   So, if we think of $a$ as being an element of $A$ at stage $X$, then for any later stage $Y$ (via $p$), we have an assignment of elements $b\mapsto F(p^*a,b)$.

   I want to think of this, for fixed $a$, as some kind of map of presheaves with codomain the representable given by $C$, but I’d have to think exactly how. Thinking out loud, I have two presheaves $(\mathcal{C}/X)^{op} \to \mathcal{C}^{op} \to Set$, namely $X^*y(B)\colon (Y\to X) \mapsto \mathcal{C}(Y,B)$ and $X^*y(C)\colon (Y\to X) \mapsto \mathcal{C}(Y,C)$. If I’ve done my calculation correct, $(1)$ above seems like it gives a natural transformation $F_a\colon X^*y(B) \Rightarrow X^*y(C) \colon (\mathcal{C}/X)^{op} \to Set$ with component $(Y\to X) \mapsto \big( (Y\to B) \mapsto (1) \big)$. So the intuition that $F$ is a family of maps $B\to C$ seems to hold up, at some level.

6. • CommentRowNumber6.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 6th 2019
   • (edited May 6th 2019)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex[The notes](https://github.com/DavidMichaelRoberts/Sandbox/blob/master/Diagonal.pdf) are somewhat expanded now, including the material from #5. Since Lawvere arrives at the diagonal argument as the contrapositive of his fixed-point theorem, it's worth thinking about whether what I have in my notes arises as the contrapositive of some sensible fixed-point theorem. One thing that is a little odd in my notes is that the notion of incomplete parametrisation $A\#B\to C$ deals with external maps $B\to C$, rather than general $X\#B\to C$, which in the cartesian closed setting would correspond to the rather natural generalised points $X\to C^B$. On the other hand, asking whether all external maps are captured by an internal parametrisation seems reasonably natural. We can then try to define a _complete parametrisation_ $A\#B \to C$, as follows > for every $B\to C$ there is a $X\xrightarrow{a} A$ such that for all $Y\xrightarrow{p} X$ and $Y\xrightarrow{b} B$ we have $f\circ b = F\circ ((p^*a)\#b) \circ \delta\colon Y\to C$. Then we can prove, following Lawvere, that if $A\#A\to C$ is a complete parametrisation, every $\sigma\colon C\to C$ has a fixed point, in the sense that there is a $Y\xrightarrow{c} C$ with $\sigma\circ c = c$. We take $c$ to be $X\xrightarrow{a} A \xrightarrow{\delta} A\# A \xrightarrow{F} C\xrightarrow{\sigma} C$, where we take $a$ as in the above definition (and $p=id_X$). This seems to be the result whose contrapositive is then the diagonal argument I give, though if I'm trying to convince people who love substructural logics, the direct proof I give of the diagonal argument is better. However, I'm not 100% satisfied with the definition of complete parametrisation, since in principle, the statement after the existential quantifier could be satisfied by taking $Y$ to be an initial object, assuming one exists. What is missing is the notion of 'display maps' or covers: in a topos, the epimorphisms $Y\to 1$. It's not clear how one should interpret this. Clearly, in the proof of the fixed-point theorem, if one constructs a 'fixed point' $0\to C$ with $0$ initial, then that's not so exciting! As in the explanation in #5, one would hope that examining what is happening with the slice categories and presheaves, it might shed some illumination. Other than that, I guess I need to knuckle down and find an interesting application/example, to see what's going on. Harley Eades III had [a proposal](https://www.cs.ox.ac.uk/conferences/fscd2017/preproceedings_unprotected/TLLA_Eades.pdf) to look at magmoidal categories as underlying various substructural logics and interactions with dependent type theory, along the lines of how linear and dependent types can be made to interact, so it's possible he has some ideas in this space.

   The notes are somewhat expanded now, including the material from #5.

   Since Lawvere arrives at the diagonal argument as the contrapositive of his fixed-point theorem, it’s worth thinking about whether what I have in my notes arises as the contrapositive of some sensible fixed-point theorem. One thing that is a little odd in my notes is that the notion of incomplete parametrisation $A\#B\to C$ deals with external maps $B\to C$, rather than general $X\#B\to C$, which in the cartesian closed setting would correspond to the rather natural generalised points $X\to C^B$. On the other hand, asking whether all external maps are captured by an internal parametrisation seems reasonably natural.

   We can then try to define a complete parametrisation $A\#B \to C$, as follows

   for every $B\to C$ there is a $X\xrightarrow{a} A$ such that for all $Y\xrightarrow{p} X$ and $Y\xrightarrow{b} B$ we have $f\circ b = F\circ ((p^*a)\#b) \circ \delta\colon Y\to C$.

   Then we can prove, following Lawvere, that if $A\#A\to C$ is a complete parametrisation, every $\sigma\colon C\to C$ has a fixed point, in the sense that there is a $Y\xrightarrow{c} C$ with $\sigma\circ c = c$. We take $c$ to be $X\xrightarrow{a} A \xrightarrow{\delta} A\# A \xrightarrow{F} C\xrightarrow{\sigma} C$, where we take $a$ as in the above definition (and $p=id_X$). This seems to be the result whose contrapositive is then the diagonal argument I give, though if I’m trying to convince people who love substructural logics, the direct proof I give of the diagonal argument is better.

   However, I’m not 100% satisfied with the definition of complete parametrisation, since in principle, the statement after the existential quantifier could be satisfied by taking $Y$ to be an initial object, assuming one exists. What is missing is the notion of ’display maps’ or covers: in a topos, the epimorphisms $Y\to 1$. It’s not clear how one should interpret this. Clearly, in the proof of the fixed-point theorem, if one constructs a ’fixed point’ $0\to C$ with $0$ initial, then that’s not so exciting! As in the explanation in #5, one would hope that examining what is happening with the slice categories and presheaves, it might shed some illumination. Other than that, I guess I need to knuckle down and find an interesting application/example, to see what’s going on. Harley Eades III had a proposal to look at magmoidal categories as underlying various substructural logics and interactions with dependent type theory, along the lines of how linear and dependent types can be made to interact, so it’s possible he has some ideas in this space.

7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeMay 8th 2019
   • (edited May 8th 2019)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexTaking the presheaf view as in #5, an incomplete parametrisation is a map $F\colon A\#B\to C$ such that there exists $f\colon B\to C$ such that for no $a\colon X\to A$ is $X^*f = F_a$. But $F$ is complete parametrisation if for every $f\colon B\to C$ there is $a\colon X\to A$ with $X^*f = F_a$. Notice that there is a subtlety in that the first quantifier is _external_: it quantifies over the hom-set of the category, but the following ones are essentially in the internal logic, such that it is. Moreover, the ("internal") existential quantifier in the definition of complete parametrisation doesn't have much to work with, as opposed to in a regular category, where existentials work fine, one has regular epimorphisms alpenty. More generally, one could ask that one has a regular epi to interpret $\exists$, but in this case we are starting from the empty context; if there is a terminal object we could ask for $X\to 1$ to be regular epi, but I haven't assumed that. It may be that to get a sensible, contentful statement of Lawvere's fixed-point theorem I should assume more than what I have...

   Taking the presheaf view as in #5, an incomplete parametrisation is a map $F\colon A\#B\to C$ such that there exists $f\colon B\to C$ such that for no $a\colon X\to A$ is $X^*f = F_a$. But $F$ is complete parametrisation if for every $f\colon B\to C$ there is $a\colon X\to A$ with $X^*f = F_a$.

   Notice that there is a subtlety in that the first quantifier is external: it quantifies over the hom-set of the category, but the following ones are essentially in the internal logic, such that it is. Moreover, the (“internal”) existential quantifier in the definition of complete parametrisation doesn’t have much to work with, as opposed to in a regular category, where existentials work fine, one has regular epimorphisms alpenty. More generally, one could ask that one has a regular epi to interpret $\exists$, but in this case we are starting from the empty context; if there is a terminal object we could ask for $X\to 1$ to be regular epi, but I haven’t assumed that. It may be that to get a sensible, contentful statement of Lawvere’s fixed-point theorem I should assume more than what I have…