https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html

[utterances-bot]

Machine Logic

https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html

[phlegmaticprogrammer]

In my opinion, in the end you just need some sort of collections. The requirements vary, depending on what you want to do with them. Both type theory and set theory should just be viewed as mathematical theories that are applicable in many situations where you need collections. For example, general set theory might often be enough. The use of types is often confused with the issue of binding. But these issues are really separate, as Abstraction Logic shows. So types should NOT be viewed as syntactic; if you do, all you are doing is freeze some mathematical theory of collections and make a logic out of your mathematical theory. I don't think much is gained by doing so: You just lose flexibility (you are now stuck with that particular theory) and clarity (what exactly is the semantics of your logic now?). Used like this, types are just refrigerated sets.

[lawrencecpaulson]

Where your notation has an obvious interpretation, it's fine to identify the two. We identify "3" with the real number 3 and this is also sensible for set-theoretic notations. It doesn't work in systems like System F or AUTOMATH, which lack set-theoretic models. It doesn't work in the untyped lambda-calculus because it's hard to argue that the models capture Church's intentions.

[lobotomization]

I wanted to comment with my thoughts on your last paragraph, specifically this point: "you risk inconsistency if you assume collections that are too big".

My takeaway from the natural inconsistencies that arise in set theory when you try to form "the set of all sets" is not that it's fundamentally impossible, but that when you form a "collection" (for lack of a better term) of objects which satisfy a particular property (i.e. the property of being a set) that collection cannot also satisfy that property, at least if we're discussing well-founded theories.

Given any set S consisting of objects satisfying a property P, we cannot also have S have the property P, or else we hit inconsistencies.

This means "the set of all sets" cannot be a set, it must be something else. We have a natural hierarchy which must emerge, along the lines of n-category theory. The category of all categories cannot be a category, it must be a higher order object. You could, for instance, have a stratification of set theory where you can form the set of all order 0 sets into a set with order 1, all order 1 sets into a set of order 2, etc., but you cannot be unqualified in your collections and attempt to put everything together into a single mass without overshooting the entire theory itself.

To me this is an interesting viewpoint. The further we go up the hierarchy of collections of objects the fewer properties we can necessarily ascribe to them. Each larger collection must throw away properties that lower order collections can satisfy, until we are ultimately left with nothing, an indescribably large collection.

[lawrencecpaulson]

You seem to be referring to predicativity (the vicious-circle principle). You are right that by continually moving to a higher level you have a good chance of avoiding paradoxes. I suspect that some people would rather not be bothered with the details of doing it carefully. A saving grace is that if you "prove" something by exploiting a paradox, you are likely to notice. Once we go formal, however, our problem is that the computer will not notice.

[typeterrorist]

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.

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.

[phlegmaticprogrammer]

Just this morning I woke up, wondering how exactly to explain the difference between Isabelle/Pure and abstraction logic (AL). This of course boils down to explaining the difference between intuitionistic type theory (ITT) and AL. Then I saw the above comment in my mail, and went to this page again. It seems this blog post contains all the answers for my question!

I would like to explain the difference between Pure and AL as follows (and actually said so to a friend yesterday, discussing the book about AL I am writing; I have this wild idea that if I just explain AL properly, I'll get through to people): Pure has no semantics, and AL has one. Therefore if you develop a theory on top of Pure, you are on your own in coming up with a semantics for your theory, while if you develop a theory on top of AL, you can use the one inherited from AL.

But of course, as such, this statement is wrong. ITT has a semantics, and ChatGPT can tell me what it is: you can take your pick between "realizability semantics" and "topos theory".

To be honest, the only thing I know about "realizability" is that it probably has something to do with constructive mathematics, and about "topos" that it is some sort of category-theoretic generalisation of the notion of set. Of course, that's my ignorance, and I would like to rid myself soon of this ignorance by formalising toposes in AL. But let's be clear here. Mathematics is supposed to clarify things and make things simpler, so if you have to use complicated concepts such as realizability and/or topos to explain what logic is, supposedly the simplest layer of mathematics on which to build everything else, then something is wrong.

As this blog post states, ITT was NOT invented with a semantics in mind. It was invented to encode a certain way of doing mathematics WITHOUT any semantics. And it is the same way with Pure.

So while my above explanation of the difference between Pure and AL is not factually correct, I think it is still correct in spirit. To make it factually correct, I can rephrase the difference as follows:

Pure has no simple semantics, and AL has one.

How simple is AL's semantics? Well, it is so simple I can describe it right here: There are mathematical objects (also just called values), forming the/a mathematical universe. Then there are operations, which are functions mapping a finite number of input values to an output value. And then there are operators, which are functions mapping a finite number of operations to a value, such that at each input position the arity of the operation at this position is fixed. Values are special cases of operations, and operations are special cases of operators. An abstraction is simply a name for an operator.

That's it. And yes, that is objectively much simpler than "realizability" or "topos". You could try to argue about that, but I would just think you are being a troll. Even ChatGPT agrees now with me.

Of course, if you want to prove technical results such as completeness, you have to add a little bit more in the form of valuation spaces, but this is straightforward. If you don't want completeness, you don't even have to think about valuation spaces.

AL's semantics has something very algebraic about it, in fact I call a collection of abstractions an abstraction algebra, which is a generalisation of an abstract algebra. This is interesting with respect to Neel Krishnaswami's comment that he feels that the syntactic rules of type theory are giving a presentation of an algebraic theory. Yes, this is indeed the case. Just formalise ITT in AL, and you get a truly simple semantics for it: an AL one. In fact, it would be good to actually do such a formalisation in AL, and prove that it preserves ITT's "semantics". Either this works, and would confirm my high opinion of AL, or it doesn't, and then this is definitely something I need to think about.

[lawrencecpaulson]

I wonder why you say that Isabelle/Pure has no semantics. It is just a fragment of higher-order logic. Because it lacks the excluded middle, it admits intuitionistic models but also the usual classical ones.

[phlegmaticprogrammer]

As far as I understand, Isabelle/Pure is essentially intuitionistic higher-order logic (IHL). And as far as I know, IHL has no simple semantics in terms of models. I cannot say, ∀ means that, and ⟹ means that, without using heavy tools like toposes. Sure, IHL also has simple classical models, but just looking at the classical models does not give a full picture of the meaning of IHL. Happy (well, maybe not happy, but ready) to be corrected about that!

[keithleit]

"It’s dangerous to take the collection of all sets as a single entity, then to build on top of that." There's nothing dangerous about the class of all sets.
"Their very starting point, Set, is the category of all Zermelo–Frankel sets. What on Earth do they need all of them for? No one has ever told me." It's the same thing as foundations for ordinary math, how you formalize it isn't usually relevant. Categories for Working Mathematicians gives alternative definitions of categories that avoids using sets of objects + sets of homs. And if you do want to use sets, Russell's paradox is avoided by defining "Large categories" which have classes of objects rather than sets of objects, etc.

"And category theorists are happy to tell you how much they despise ZF set theory, although they have gobbled it up whole." This seems like a straw man argument. It's also missing nuance/context. Despise is a strong word. Perhaps someone who claims to despise ZF set theory, really only despises certain aspects of its usage, and avoid that in their own usage.