Monadicity questions

Monadicity questions

[David Yetter]

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

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://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: 7409 bytes --]

Re: Monadicity questions

[Jonas Frey]

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

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/N3UtCnx1Z5Uo4jqxC9_Zed?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/3Qc9CoV1Y2SzAZL8szZkKB?domain=categorytheory.zulipchat.com>
[3] https://ncatlab.org/nlab/show/monadic+functor<https://protect-au.mimecast.com/s/aZA7Cp81gYC8gKNyCY-403?domain=ncatlab.org>
[4] https://arxiv.org/abs/2110.02804<https://protect-au.mimecast.com/s/SmU3Cq71jxf5glPRtEKwVz?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/i9PHCr810kCvyo06cjH4Tf?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/yniJCvl1g2S6JKj4S5SHXc?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/UDbXCwV1jpS159zPtxmrj9?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: 13044 bytes --]

Re: Monadicity questions

[Patrik Eklund]

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

Re: Monadicity questions

[Paul Levy]

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

Dear Jonas,
Regarding powerset and other unranked monads, I don’t know if this is quite what you’re seeking, but you might look at our paper on monad tensorability:
https://lmcs.episciences.org/740<https://protect-au.mimecast.com/s/ZJnCC4QO8xS1k4wEiOHa6g?domain=lmcs.episciences.org>
Section 2 explains the relationship between large theories and monads, and in particular makes the following point.  When considering large theories, we need to distinguish between the property of having small free algebras and the weaker property of having free small algebras.   This leads to two distinct notions of presentation of a monad on Set, which we call  “genuine” and “spurious”.
Best,
Paul


From: Jonas Frey <jonas743@gmail.com>
Date: Monday, 5 February 2024 at 04:30
To: David Yetter <dyetter@ksu.edu>
Cc: categories@mq.edu.au <categories@mq.edu.au>
Subject: Re: Monadicity questions
CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

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/bE-CC5QP8ySGNkr3tOeX8X?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/9CwpC6XQ68fKwL47fmA10s?domain=categorytheory.zulipchat.com>
[3] https://ncatlab.org/nlab/show/monadic+functor<https://protect-au.mimecast.com/s/0qt_C71R63Ck7GB2SNvs3g?domain=ncatlab.org>
[4] https://arxiv.org/abs/2110.02804<https://protect-au.mimecast.com/s/FvgeC81Vq2CR4NyWco3f8C?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?


  1.   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/Y4mxC91W8rCB74wAU1KYq7?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/o_EnC0YKgRs3PNAQHLqK4s?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/BcryCgZ05Jf2QEzKsK_Fpg?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/tRkaCjZ12RfqNoxDSM4Hvd?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/7v1YCk815RCQG2JAfDRxBj?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/BcryCgZ05Jf2QEzKsK_Fpg?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: 18666 bytes --]

Re: Monadicity questions

[Patrik Eklund]

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

Hi Vaughan,

I hesitate to say anything specifically about Goldbach's conjecture, but let me comment at least on "proof ... exists".

The very basic, simple and first idea of "lativity" is that it was never good that symbolic logic was ``freed from its undue obsession with the forms of ordinary algebra'', like Principia writes in its PREFACE, referring to Peano having said that, but Peano never did say that. Peano did say "We shall generally write signs on a single line" (Lat. Signa plerumque in eadem linea scribemus), but he didn't say "For a monadic term and formula construction, just go with a magma; don't care about multi-sortedness and universal algebra, they won't do any good". I don't know who to blame, Russell or Whitehead, for fake reference to Peano, but I tend to choose Russell. He had struggled with substitution, and PM continued to struggle with substitution. Everybody else did, over decades to come, until GdM II is printed and beyond.

If we say "a conjecture is true", what do we mean? Do we mean that the formula (sentence formed categorically from underlying terms, again formed categorically, and based on signatures, whether denoted a la Benabou or not) is true, where that 'true' is the boolean constant in the underlying signature? Or do we mean that it is "true" that we can find a proof for that conjecture, i.e. "proof ... exists" is "true". Lativity would say that the latter "true" is not the "true" we have as sorted in the signature.

I've often commented that "P is true" and "|-P is true" cannot use the same "true". PM struggled with this, GdM struggled with this. P is a formula, |-P is not. There may be a proof for P, but it makes no sense saying there may or may not be a proof for |-P. John Stuart Mill was very smart. He said “nothing but a Proposition can be an object of proof”. Gödel thinks differently, as Bw and Bew are of the same type, kind of.

It's good if formalization proceeds latively, from signature to term to sentence to entailment to proof rules to proofs ...", and even better if always "closing the door behind you" so that nobody comes up with viewing a proof sequence as a constant operator in the starting point signature. I feel uncomfortable to speak of a "lative axiomatization", unless by "axiomatization" we mean "from signature to term to sentence to entailment to proof rules to proofs", because then, by definition of lativity, axiomatization is lative.

So, within syntax, we should keep things apart, and also, as far as borderlines are concerned, between object and meta. We shouldn't shift things in meta sometimes to be used objectively or vice versa. Numbers and numerals are on different sides of that borderline. GdM writes about Nummern and Ziffern, but does not really make that borderline explicit. And indeed, I'm sad to say, GdM never tried out rigour concerning types. Neither did Grundzüge. And Gödel 1931 is extremely illative in these respect along the whole progression of "from signature to term to sentence to entailment to proof rules to proofs".

On GdM, already at its starting point, in GdM I §1, GdM "departs even further from such rigour by making a dubious statement basically saying that a boolean predicate symbol complies with its arity but need not be bound to respect any specific typing of its domain, as long as satisfiability of a formula is invariant under a one-to-one mapping of one typing to another". I put that in quotation marks because I quote directly from drafting I presently have on what I have called a "dialogue" between GdM II §§4-5 and Gödel 1931. I'm trying to use categorical terms constructions and "categorically lative axiomatization" to explain why and where things go wrong.

So, to your question "Would you then call the conjecture undecidable?", I am unable to provide an answer until I understand latively what is meant by "conjecture" as related to formula or entailment or something else, and what is understood as "decidable" as related to a more lative definition of "proof sequence" including all its ingredients. I don't think PM's, GdM's and Gödel's notions of "decidability" are mutually isomorphic.

Putting symbols one by one in sequence is "no good", not good at all. Russell made a fake reference to Peano, and even if Russell would have said being freed from the burden of algebra is something good without referring to Peano, I would say Russell's approach is "no good".

Foundations must be revisited. Foundations need category theory more than category theory needs foundations. I would invite everybody to think about the way foundations might be revisited using categorical constructions, and thereby making logical constructions much more "lative" than they are in traditional foundations of logic (and computing for that matter), and in particular for the reason to finally get rid of self-referentiality and malicious use of antinomies. Doing so will make discussions on answers to your question, Vaughan, really interesting.

That's my credo. Has been for a long time.

Best,

Patrik


On 2024-02-08 08:20, Vaughan Pratt wrote:

On Sun, Feb 4, 2024 at 11:30 PM Patrik Eklund <peklund@cs.umu.se<mailto:peklund@cs.umu.se>> wrote:

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


Patrik, how does "lative" bear on Goldbach's conjecture in the event that it is true, and furthermore provably so in some consistent non-lative recursively enumerable axiomatization of arithmetic, but for which it can be shown that no proof of the conjecture exists in any lative axiomatization?

Would you then call the conjecture undecidable?

Vaughan Pratt







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: 11262 bytes --]