> various versions of Martin-Löf’s intuitionistic type theory and finally the calculus of constructions of Coquand and Huet. In every case, they were created with no interpretation in mind. They were justified syntactically, for example via proofs of strong normalisation. Models came later.
Martin-Löf very explicitly discussed the denotational meaning of his theories. See for instance Section 5 of the SEoP entry on intuitionistic type theory.
TFA is correct that type theory is syntax, but it would be wrong to think of set theory as any less syntactic to the mind of an intuitionist. The semantics is the actual mathematical ideas going on within the head of the mathematician. Both type theory and set theory must be connected to these in order to be given meaning.
>The semantics is the actual mathematical ideas going on within the head of the mathematician
I think this intuitionism in the (original) sense of Brouwer.
Martin-Löf argued for something different:
"Martin-Löf’s meaning theory of intuitionistic type theory should be understood directly and “pre-mathematically”, that is, without assuming a meta-language such as set theory."
"This meaning theory follows the Wittgensteinian meaning-as-use tradition."
Doesn't answer the question posed on categories but just has a jab at the fact that some categories are much too large to fit in the usual ZFC meta-theory. It's why most books on category theory will mention universes or classes and then just forget about the issue entirely. Type theory has the same problem, to talk about the type of all types requires introducing a hierarchy of universes to avoid logical inconsistencies, i.e. if U denotes the type of all types then U:U would make the theory inconsistent which is the same as saying the set of all sets is a set. Ultimately, to avoid the issue of circular self-reference you must have some kind of hierarchy of classes or universes or you might accidentally introduce a circular self-reference when quantifying over all sets, types, objects, etc.
The issue is the notion that set theory can be the ultimate foundation of mathematics. ZF set theory is not a good foundation because it says “too much” about sets. For examples, every set in ZF has to have a power set, which means you can never talk about any object that doesn’t have a power set, such as the class of all Rings, or the surreal numbers. As it turns out, quite a lot of objects in mathematics are too large to be sets.
Therefore the ultimate foundation must be something else, such as categories, classes and types. You can still have ZF set theory but not at the very bottom.
> Many people are seriously bothered by definitions such as (x,y)={{x},{x,y}}
I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something? Would love to understand why like, system F isn’t the foundation of math (i should care about)
I've never seen anyone bothered by such a definition. It's a good definition that shows that you can construct ordered tuples in set theory without the need for a new primitive notion, and then you can promptly forget it.
> I am bothered by the fact that most mathematicians aren’t bothered by that! Am I missing something?
Outside of logic and set theory, most mathematicians aren't really working in any particular foundation: they're working directly with the relevant structures. An ordered pair `(x,y)` can be modeled as the set `{{x},{x,y}}`, but that doesn't mean it is that set. What it is, to the extent the question is even coherent, is a thing that has the data ordered pairs are supposed to have: a first element, and a second element.
System F just isn't flexible enough to encode most of mathematics. You need at the minimum dependent type and preferably a more flexible identity type to avoid setoid hell. The closest attempts I know of are HOTT in Coq and Cubical Agda. These systems still have a lot of kinks to be sorted out though, e.g. https://www.youtube.com/watch?v=TpUOweB2kHU
Well, yeah, but {x, y} is also a pair. How is (x, y) different? It's ordered, you say? All right, an ordering is a relation that's antisymmetric and so on, but in this case let's say we have a function that maps x to 0 and y to 1… But what is a function? Okay, a function is a type of relation, so let's define a relation first: a set of ordered pairs… oops.
The real problem with defining (x, y) = {{x}, {x, y}} is that elements of a set must also be elements of some universal set 𝓤, {x, y} ⊂ 𝓤, but as we know, there is infamously not such a thing as a "set of all things". Sets have to be typed. But in a pair, x and y can be of entirely different kinds of entities.
Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).
For the dummies like me, what is it that is meant with carrier and group here below?
So when we say that the carrier of a group is a set, it doesn’t have
to be specifically a ZF set; but if we imagine collecting up all
groups as a single entity, that warning light should flash. It’s
dangerous to take the collection of all sets as a single entity, then
to build on top of that. And yet, that is precisely what is done in
category theory, again and again.
"Carrier" isn't a mathematical term, they're just using that word in place of the word "set" to distinguish it from ZF sets. "Group" refers to a specific kind of mathematical structure[0], but it's just given as an example. The important part is that any object can be part of a group, so if the collection of all groups existed as an object, then it would also be part of a group, indirectly containing itself and leading to paradox.
I don't think you're quite right. "Carrier" is absolutely a mathematical term, referring to the set of elements of a group, as opposed to the group operation. That is, a group is defined as a binary operation satisfying the group axioms, on the elements of a certain carrier set.
For those unfamiliar with groups, one way to comprehend groups (by the Cayley theorem) is to essentially imagine groups to be sets of permutations (and in this case, the Carrier set would be the set of permutations, with the group operation being composition of permutations).
I'm not sure I'm any convinced by your argument of the collection of all groups being a group either, and whether that was what was referred to by the author. In any case, I don't think that follows the usual form of the Russell's paradox or Girard's paradox. I'm fairly certain that the "warning light" that the author mentions in relation to the set of all groups is about the set being too large to be consistently considered a set, rather than anything circularly related to groups.
"Carrier" is much more a minority slang than a well-known mathematical term. "Carrier set" is sometimes mentioned as an alternative, but the common term for that is "underlying set".
I have no idea what TFA tries to say, it seems to argue about aesthetics, I am not really into that. If it is very clear, and the authors enthusiasm about their favourite is sticky then sure, but TFA is unclear to me.
It seems to me that the author is attempting to put together some analysis on the essential meaning, purposes, and distinctions of type theory and set theory. While what on offer may not satisfy you or me, it seems a task worthy of doing.
> As a computer scientist, I don’t find it ridiculous: everything on a computer is encoded as a bit string. Let’s pursue the analogy: if we have a directory full of devotional icons in some image format, and another directory full of hardcore porn clips in some video format, it’s certainly conceivable that the exact same bit string could appear in both directories.
I found this to be careless thinking, conflating representation of thing with the thing itself.
Was that not precisely the authors point? We don't feel queasy representing many things different things incidientally with the same binary sequence, so why feel queasy about the same set theoretical representation?
I understood it as the author emphasizing as I believe you also wish the difference between the representation and the thing itself. Sets can be fun and useful without us resorting to reductionistic arguments about what math "is", I believe the author is saying.
It was all fun and games until The most basic rule of the λ-calculus is β-reduction, which replaces (λx.M)N by M[N/x], which denotes a copy of M in which every free occurrence of x has been replaced by N. Obviously, [...]. You know, obviously.
I wouldn't call β-reduction "The most basic rule", but I'd call it the most important.
> denotes a copy of M in which every free occurrence of x has been replaced by N
...breaking it down...
> a copy of
Weird wording, but if you're used to mutability everywhere, and you want to do an immutable operation, then it makes sense to make a copy. But it's kind of like saying 4+3 'makes a copy of four which is three bigger'.
> every free occurrence
Paraphrasing, this says 'pay attention to variable scope'. If you start replacing every x within a scope, and you come across a new declaration of x inside that scope, you should ignore occurrences of that inner x, because it's a different variable (despite having the same name.)
> (λx.M)N ... M[N/x]
This one adds no clarity for me, despite being throughout the literature. Explaining that (λx.M)N is M[N/x] doesn't help a beginner, because you then immediately have to explain what M[N/x] is.
N.replace(x, M) would probably suit a modern audience.
Why bother with all this nonsense? The power-to-weight ratio. λ-calculus (including β-reduction) gives you all of computing. Compared to its contemporary Turing Machine (which was super important theoretically at the time), you can just bootstrap a new language off the lambda calculus.
> Obviously, λx.M should be seen as a sort of function
The fact that lambdas can be seen as a syntax for describing functions (or function-like things) is kind of obvious to anyone who knows basic programming language theory (and many software engineers who use lambdas when they map over a list, for example).
The sentence before it about β-reduction is describing the rule for how to call a function, which we learned in high school as "plug-and-chug".
I think the confusion here might just be that the syntax is unfamiliar. You have probably seen these concepts before.
Martin-Löf very explicitly discussed the denotational meaning of his theories. See for instance Section 5 of the SEoP entry on intuitionistic type theory.
https://plato.stanford.edu/entries/type-theory-intuitionisti...
TFA is correct that type theory is syntax, but it would be wrong to think of set theory as any less syntactic to the mind of an intuitionist. The semantics is the actual mathematical ideas going on within the head of the mathematician. Both type theory and set theory must be connected to these in order to be given meaning.