Saul Shanabrook

Wow, I just watched the second lecture by Vladimir Voevodsky called "The story of set theory (so far)".

It's amazing in that it builds a narrative around all of these concepts I have been bumping into... predicate logic, ZFC, godel's incompleteness theorem, type theory, category theory, etc.

And more directly, it as close to a modern theology as I can muster. God doesn't come up really in the second lecture, as much as it does in the first, mainly because Math after the 1800s in Europe explicitly chose to distance itself from theology. But meta-mathematics, to me, is so close there, because it is all about defining how we talk about truth, what languages we create, what they are useful for, and how they relate to one another. And this fundamental sense of "in general, by a 'manifold' or 'set' I understand every multiplicity which can be thought as one" (Cantor 1883) is the fundamental concept, which is type theory, which is fundamentally a concept of abstraction. Abstraction, built on the dichotomy of True and False, i.e. the movement from first order logic to second order logic, these are all ways of saying "we have many things and we must move up one level to understand them as one thing" But then when you move up one level, you now have a new thing, and you can consider many of those... etc to get the infinite category theory work. But this is a concept that is really concrete in type theory, especially in dependent type systems like Lean where you have multiple "universes".

And god is where the limit of language sits to talk about these things, it's the infinite rising of abstraction that is outside of our ability to reason about, and yet we keep trying with these metamathemtical concepts.

Anyways, I meant was meaning to say something about how we get confused that Computer Science is "mathematical" people always say "But I was bad at math! That means programming will be hard for me?" But the math we are learning comes from Foundations 1, which is about the tower of theories, learning basic things that then can be leveraged to prove more advanced things, building up this structure of mathematical knowledge. And programming is where the reality of Foundations 2 comes in, which is about the substrate in which we talk about math, the meta-math. Because building a website is not done with predicate logic, Django is it's own language, so programming is fundamentally about this building of forms that are useful to come to from our own human thought.

It's a task of Foundations 2.