Re: Signing off

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

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

Dear all,

Thank you for mailing, throughout decades, as it has helped create new 
things and invite younger researchers, at the same time it preserves 
community and maintains a forum.

I've learned a lot, and I am grateful for that.

---

Yes, looking back, we have good memories, and we know we did the right 
things. Many things we wouldn't have done differently.

Are we looking forward? What's in for CT in 50-100 years to come?

I'm less than epsilon in the universe on CT knowledge but allow me to 
write this.

---

I wrote recently to Michael Barr privately as I had found a mail 
exchange from 2015.

On 2015-01-29 02:59, Michael Barr wrote:
I wonder what kind of science outside of string theory would find CT 
useful.

I wrote some, and related to what I have posted sometimes at CT (and 
FoM) on the need to use CT in understanding syntax within the 
foundations of logic.

---
---
---

Here's what I (somewhat shortened) wrote to Michael:

I have come back to that "outside of string theory". For decades I was 
flabbergasted about Gödel's fame given his 1931 paper. He is basically 
very shallow on formalising what formulas and provable formulas actually 
are. Once he has sets for these, no matter what they are, he sees 
formulas in there as sequences of symbols, and proofs as sequences of 
sequences of symbols. In his footnote 9 he says he works with an 
"isomorphic image" of Principia Mathematica. It could and should be an 
adjunction if he would have tried something out.

Anyway, in Gödel's use of the power type, he essentially works with 
terms over sets rather than sets of terms, i.e.. he leans on the TP 
composition rather than the PT composition. So basically he doesn't 
realize that his substitutions cannot compose. His efforts on 
substitution is in his steps 30 and 31 in his 1-46 steps before he 
"proves" his incompleteness results.

So basically Gödel proves incompleteness of systems that actually do not 
exist anywhere. Saying that whatever system P we have, formulas must be 
nothing but sequences of symbols (Peano 1889), and proofs are sequences 
of such sequences, is absurd.

---

On 2015-01-29 02:59, Michael Barr wrote: I wonder what kind of science 
outside of string theory would find CT useful.

Today I write: I wonder why CT never looked into being useful more 
generally within fuondations, and not just marginally curious about its 
own foundations.

Gödel's meta language is "logical arithmetic" where his "numbers" and 
recursion reside, and he uses that to drag sequences of sequences of 
symbols into the mud. So I wonder why CT never looked into using 
categorical arithmetic as meta to enrich Hilbert's program. Gödel's 1931 
paper is seen as having crashed everything about Hilbert's program, and 
he did it by dragging sequences of sequences of symbols into the mud.

---

The Foundations of Mathematics side never seriously looked into CT, and 
CT never seriously looked into FoM.

I always wondered why.

---
---
---

That was indeed my mail to Michael a few days ago.

To repeat: Are we looking forward? What's in for CT in 50-100 years to 
come?

Some 50 years ago Bernays and Gödel exchanged letters on category 
theory. They had heard something about someone being in Poland, but that 
was basically it.

Today, is there any exchange at all between CT and FoM (not the mailing 
lists!)?

---

Thank you Bob Rosebrugh for everything you've done, and thank you JS 
Lemay in advance for everything you will do.

Best,

Patrik



On 2023-10-26 17:14, Bob Rosebrugh wrote:
> Dear Colleagues,
> 
> From March 1990 until recently it was my privilege to moderate the
> categories mailing list. For a couple of years it has been my
> intention to pass the list to a new moderator, but I was too slow to
> act. Changes to IT service at my former employer, Mount Allison
> University, abruptly made it impossible for me to continue running the
> list.
> 
> Those changes were unexpected for me, but I have been away from the
> campus for over three years and was not aware. The IT staff at Mount
> Allison have always been very supportive of the list and I thank them
> for their more than three decades of generous assistance.
> 
> It is a reassuring pleasure to know that the list is now in the
> capable hands of JS Lemay who kindly accepted the invitation to revive
> it. I am very grateful. Moreover, there is no one better suited to the
> role and our community is fortunate to have him moderating. I am also
> very happy that the new home of the list is Macquarie.
> 
> Best wishes to everyone. I am hoping to see many of you in the not
> distant future,
> Bob Rosebrugh
> 
> 
> 
> ----------
> 
> You're receiving this message because you're a member of the
> Categories mailing list group from Macquarie University.
> 
> Leave group:
> https://protect-au.mimecast.com/s/F_r_C4QO8xSPgRRASOwJwn?domain=outlook.office365.com

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