Re: Monadicity questions

[Patrik Eklund <peklund@cs.umu.se>]

[-- Attachment #1: Type: text/plain, Size: 8665 bytes --]

These may provide some added ingredients:

https://www.sciencedirect.com/science/article/pii/S0165011413000997<https://protect-au.mimecast.com/s/cgOJC91W8rCBJj6zsoLXJl?domain=sciencedirect.com>

https://www.sciencedirect.com/science/article/pii/S0165011415003152?via%3Dihub<https://protect-au.mimecast.com/s/82rDC0YKgRs3nz9kUDO3U2?domain=sciencedirect.com>

https://link.springer.com/book/10.1007/978-3-319-78948-4<https://protect-au.mimecast.com/s/5DzKCgZ05Jf2vJjqt2lXs4?domain=link.springer.com>

The focus here is on (multi-sorted) term constructions and more generally over monoidal closed categories. Other papers we've written build upon these where term constructions are used in sentence (formula) constructions.

Not clear to me what David precisely means by "no new", but in our case we have been used to say "logic must be lative" in the sense that "first terms, then sentences from terms" and no new terms from that, and "then entailment constructions from sentences" so that no new sentences are constructed from entailment. Here is where logic mixes "true" and "provable", and this is the very spot which allows Gödel to "prove" incompleteness using the Liar and Richard's technique.

Respecting this principle of lativity, Gödel's 1931 results are basically non-sense. Grundlagen II §4-5 tries to deal with it, with some success, but not fully as GdM amd other work at that time, not just in Göttingen, never properly dealt with the underlying multi-sortedness with subsequent term and sentence constructions. Maybe it's Russell's fault? Principia said Peano had suggested that logic must be freed from algebra. Peano never said that, but Principia did it, so "formula constructions" remained as a, as Peano said,  "putting symbols one by one in sequence". That's not a monadic approach to forming terms and sentences, is it?

My point is this: Category could have been around already before 1917, as the set theory used in category theory basically is the set theory that was available before Hilbert invited Bernays to Göttingen. Had they used categories for foundations, Gödel's 1931 paper would probably never have been written. I have always wondered what Gödel means by "isomorphic image" (in his footnote 9) in his 1931 paper.

Patrik


On 2024-02-05 06:21, Jonas Frey wrote:

Dear David,

Yes, models of single-sorted algebraic theories are always monadic over Set, and such theories correspond precisely to finitary, ie omega-filtered-colimit-preserving monads on Set. If we take the correspondence between single-sorted algebraic theories and Lawvere theories for granted, this is stated eg in Hyland--Power [1], with further references there. More generally, monads preserving alpha-filtered colimits for a higher regular cardinal alpha correspond to algebraic theories with alpha-ary operations; unbounded monads (such as the powerset monad) can be viewed as corresponding to "large theories" with no bound on their arities. The theory corresponding to the powerset monad, eg, is the theory of sup-lattices, ie posets with arbitrary small joins, which is not expressible with operations of bounded arities. Regarding references on these generalizations, I would also be curious.

Concerning your questions on extensions of theories, and more general kinds of theories and base categories, there recently was a long thread on the category theory zulip server [2], which I'll try to summarize: extensions of single-sorted theories by new operations and/or equations are always monadic (regardless of arities); this follows from the fact that monadic functors have the left cancellation property (Proposition 3.3 in [3]). Extensions by new sorts are typically not monadic, eg Set x Set is not monadic over Set. The models of many-sorted theories are monadic over powers of Set, and extensions of many-sorted theories by operations and axioms are also monadic, again by cancellation. Things become more complicated in the generalized/essential algebraic case, since (in the generalized algebraic, ie dependently typed case), adding new operations can create new sorts by substitution, which can lead to successive monadic extensions which are not composable, as Tom Hirschowitz, James Deikun, and possibly others pointed out. In general there's a lot of ongoing work on the dependently typed, ie generalized algebraic case, such as eg Chaitanya Leena Subramaniam's recent PhD thesis representing dependent algebraic theories by finitary monads on presheaf categories over direct categories [4].

[1] https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf<https://protect-au.mimecast.com/s/2fosCjZ12Rfqz0wYf7hoKP?domain=dpmms.cam.ac.uk>
[2] https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/distributive.20laws.20and.20monadic.20functors<https://protect-au.mimecast.com/s/ITObCk815RCQDvRkUJn1iR?domain=categorytheory.zulipchat.com>
[3] https://ncatlab.org/nlab/show/monadic+functor<https://protect-au.mimecast.com/s/jscqClx1OYUZWl31UYnCqB?domain=ncatlab.org>
[4] https://arxiv.org/abs/2110.02804<https://protect-au.mimecast.com/s/reH-CmO5wZsnVq7pcNV9nj?domain=arxiv.org>

On Sun, 4 Feb 2024 at 21:00, David Yetter <dyetter@ksu.edu<mailto:dyetter@ksu.edu>> wrote:
We are all, of course, familiar with Beck's Theorem.  I'm rather hoping that there are results in the literature that will save me from having to prove that the underlying functor U creates coequalizers for U-split pairs in the context of two quite different projects I'm working on.  Thus, I have two questions for the community:


  1.
It seems obvious to me that for the same reason categories of models of finitary algebraic (equational) theories are monadic over Set, if one has (I think I'm using the term correctly here) a conservative extension of an equational theory (by which I mean, add operations and equations in such a way that no new equations are imposed on the operations of the original theory), then the category of models of the extension is monadic over the category of models of the original theory.  Surely this is either explicitly stated and proved somewhere, or follows easily from some result I simply have not encountered.   Citations?

  2.   What is the most general sort of theory whose models are monadic over Set? Or if that is not known, what sorts of theories have monadic categories of models over Set?   Are there multisorted generalizations of any results of that sort, ideally not just to Set^\alpha, where \alpha is the cardinality of a set of sorts, but to things like Graph?  Again some citations would be much appreciated.


Best Thoughts,
David Yetter
University Distinguished Professor
Department of Mathematics
Kansas State University

(That is the first and last time I'll use that signature block in writing to the list, but I thought I'd do it once since I thought the community would be gratified that a categorist was so honored.  After this it's back to David Y. or D.Y.)



You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://protect-au.mimecast.com/s/DjW7Cnx1Z5Uo4V1XU0vZbV?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/p4NeCoV1Y2SzAm1DT2pY3j?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/PwlyCp81gYC8gZJ9fvYLu0?domain=aka.ms>



You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://protect-au.mimecast.com/s/Grb4Cvl1g2S6JZPESYBcVr?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/o8pvCwV1jpS15n4vS3ocoE?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/PwlyCp81gYC8gZJ9fvYLu0?domain=aka.ms>



You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 19008 bytes --]