Tom Leinster’s Rethinking set theory is quite a nice paper showing how category bigots do set theory—but skipping the category theory. The paper serves as a gentle introduction to category theory—perhaps a lead up to:

HoTT

or “Homotopy Type Theory: Univalent Foundations of Mathematics”. Actually this seems to have nothing to do with topology except for the fact that topologists invented some terms for topological purposes that were intuitive and serve as candidates for foundational mathematical concepts. Category theory enthusiasts have pioneered this way of introducing mathematical concepts. The several introductions to category theory that I have looked at all seem directed to the professional mathematician with an implication that these ideas are obviously so simple that they can be taught to high school students. We must not lose sight of the fact that most practicing mathematicians have never bothered to examine any foundation for mathematics; and they do just fine. I worry about foundations perhaps out of a morbid philosophical fascination. Perhaps, however, it relates to the biological question of how creatures, such as humans, manage to make a living in a universe such as ours. It may thus bear on creating AIs.

I was steeped in ZFC axiom foundations for math and am not yet ready to give up that hand-hold on understanding for a new one. Over the course of my college math I came to believe that ZFC was an adequate formal theory to express my mathematical ideas, albeit only in principle. The main departure here is to include functions as a primitive concept, in place of sets; ZFC systems derive functions from sets.

Page 2, in the introduction, mentions the ‘intuitionistic’, roots of this work. I have been under the impression that intuitionist mathematics had not made much progress in the 20th century. In particular it had not been able to provide the fruits of Lebesgue measure theory which illuminates Hilbert space which many engineers need. Perhaps this is an end-run, perhaps this work aspires to provide an alternate platform for such useful math. Do we need the Tarski-Banach ‘paradox’ which seems to be the pornography of measure theory? It is great fun.

I shall be surprised and pleased with homotopical axioms even nearly as simple as those for sets. I consider constructing homology, via point set topology, via sets, an elegant accomplishment of the 20th century.

I concur with the author’s remarks about type theory and the real practice of programming computers. Even programmers who have never heard of type theory use it informally as they design and understand programs.

I find the paragraph following the heading “Constructivity” (Page 8) well worth reading very carefully. There they describe a bridge between two ways of looking at the same math that goes back to the Curry−Howard correspondence which has hitherto escaped me. I find it necessary to elaborate their example even further to glean the ramifications.

If functions are to be taken as a primitive I wonder if their domain and range are to be taken as sets which are characterized by their elements or as some more primitive notion. Benson Mates who read Greek mathematics in Greek told me that the Greek’s notion of an area was in no way like a set of points, which is the modern notion. The Greeks knew well the area of an ellipse which I would compute and justify as an affine transformation of a circle whose area was already known. After Pappus the Greeks would have divided the area into smaller and smaller areas but that is not the same as considering the area as a set of points. There is thus perhaps a notion of a function that does not depend on the members of the domain of the function.

In short do type people ever write something like y = f(x) where f is one of their functions? If so what meaning do they ascribe to x or y?

The book is discursive and exploratory. It approaches the subject from different vantage points. If you come across something that you do not understand, skip a chapter. I would like to see a stab at a bottom up development; perhaps that is premature. Set theory preceded ZFC.

Connect to: xx xx

These ideas bear on a question that has bothered me for 60 years: “How did we get smart enough on the savannah to be able to do mathematics?”.

The set theory primitive ∊ depicts membership in a set. “x∊y” means that x is an element of the set y. In set theory ⊆ is a defined concept and “x⊆y” means that every element of x is an element of y. Democritus believed that things were made of atoms which were of some other sort than the bulk material—different in that they could not be subdivided without losing the nature of the material. (I think that Democritus believed that they could not be divided.) Usually the sets that mathematicians suppose are some different sorts of things than the things of which the set is composed. In particular the ∊ relationship is definitely not transitive while the ⊆ relationship is.

In category theory relationships between things (arrows) are taken as most primitive and sometimes the ‘things’ are also included as equally primitive. Mathematics has examples of structures with a structure like ⊆ with members but no atoms—everything is divisible into yet smaller things. (Boolean algebras are the first instance of this that I learned. The set of unions of half open intervals is such a boolean algebra.) Proper inclusion (⊂) might be a more intuitive primitive and I think that this is mainly an aesthetic issue.

The paragraph with text “objects are classified using a primitive notion” We learn that this new math style treats individual variables as strongly typed computer languages do. You can tell what sort (‘type’) of thing is denoted by an expression with a fast finite algorithm that scans the text—something a compiler does. In set theory, as in dynamically typed languages, the type emerges only as the theory is elaborated, and theorems are proved or the program runs.