@Zanna It occurred to me that, during the course of making notes, you likely had thoughts or questions about, or noticed errors in, things I've said. I had meant to ask you if there was anything along those lines that you wanted to share... but I don't think I did ever ask you that.

@Zanna I think that the reason "type" does not seem like a helpful name is due to a deficiency limitation in my presentation of this topic. I am not actually conversant in any system of second or higher-order logic.

I know a very small about such systems, which enables me to have an idea of why first-order logic is first order, and I don't know of any effective ways to communicate why first-order logic is first order, which is why I've talked about second and higher order logics from very early on.

But even when giving examples of what one can say with them, I have used a notation that is deliberately adapted from first-order logic, since my actual goal has been to show what sort of things first-order logic does and does not permit.

Regarding type theory, that is not my only reason for talking about it--you asked what happened, historically, after Russell's paradox was discovered and published, and I figured this is interesting and important enough for me to try to answer it honestly, even though my knowledge of the history of logic is really not altogether up to the task.

My main goal, in concord with your having asked originally about set theory, not about higher-order logics or even about logic at all, is to present modern set theory in general--and ZFC in particular--and the manner in which mathematics can be done with it. But that did not come until later--it was not the immediately apparent solution to problems like Russell's paradox--and so it is not the answer to your historical question about what happened next.

I have a small amount of familiarity with type theory, from having read parts of Principia Mathematica. But most of that was years ago. Furthermore and perhaps more importantly, I have made no effort to write in a way that captures how one expresses things in type theory, and I have overly simplified types by identifying them with integers.

In actuality, the types are richer than that. A very brief exploration of how that is so may clarify some of what I have said, and also make it intuitive why the syntactically discernible information about how a well-formed assemblage of symbols is permitted to be used is called a "type" in type theory.

@EliahKagan I meant to say, I don't know of any other ways to effectively communicate why first-order logic is first-order, than by comparing it to other more powerful logics.

@EliahKagan I mean to say, I know a very small amount about such systems.

@EliahKagan I will certainly mention anything like that. I was confused about some things at the start of making notes, but writing always helps me a lot

today was an exceptionally frustrating day at the bureaucracy grindstone

making another attempt on it tomorrow

@Zanna I'd also be interested in the details of what made more sense upon reflection and notetaking--if you feel like talking about that.

@Zanna I'm sorry to hear that!

I take it that there are you referring to interacting with the bureaucracy and there you are referring to logic and set theory?

@EliahKagan sure, I am super sleepy but I will try to talk about that next time I am here

@EliahKagan yes, correct!

@Zanna Thanks! There is of course no hurry!

:) :) thank you

@Zanna In that case, I feel less concerned that I suggested I was about to give clarifying information about type theory and then disappeared for hours and still haven't given it. :)