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:
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.
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?”.
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.