The consistency of NF

Stream: maths

[Timothy Chow]

I have recently been having a discussion with Randall Holmes (Boise State University) about his amazing proof of the consistency of Quine's New Foundations (NF) system for axiomatic set theory. This proof resolves a major question in logic that has been open since the 1930s. There is a little problem, however. Holmes's proof is so intricate that it has run into the same problem that Hales (and Ferguson) encountered with the (pre-Flyspeck) proof of the Kepler conjecture. Namely, the experts have taken a serious look, and believe that it is probably correct, but have not been able to understand the proof thoroughly enough to vouch for its correctness. Holmes has responded by trying to rewrite the proof in a simpler and more understandable manner, but his multiple rewrites have generated a new problem: Experts don't want to invest a lot of time studying a proof that is not stable and that might change from under their feet at any time. Even though Holmes announced the proof back in 2010, it has not yet been accepted for publication. I believe that the main obstacle is the difficulty of finding a referee who is willing to sign off on the paper.

Holmes is proficient with proof assistants, so it might seem that the doubts about the correctness of his argument could be circumvented with a formal proof. A few years ago, I asked him exactly this question, and he said that he was seriously considering a formalization, but that the practical difficulties were formidable. We left it at that. In the meantime, of course, proof assistant technology has been steadily improving, and the community of users has been steadily growing. Recently, I raised the question with Holmes again, and suggested that Lean might be a good choice. Coincidentally, he had been thinking exactly the same thing. I have encouraged him to join this forum and share his thoughts in more detail.

Originally, I was hoping that some people in the Lean community might be willing to help Holmes with his formalization efforts. After all, it seems that this is precisely the sort of difficulty that proof assistants ought to be able to help with, so a success story would presumably be good press for formal theorem proving in general. (I can already picture the Quanta magazine article in my mind's eye.) However, I have been cautioned that there aren't many people in the Lean community with an interest in logic. More generally, mathematical logic seems to be a "low status" area of mathematics, and the consistency of NF might seem totally uninteresting to the average "mathematician in the street." So maybe there will be no takers. However, I figured that it couldn't hurt to ask, so that is why I am here. As I said, I am hoping that Holmes himself will chime in soon with further thoughts.

[Johan Commelin]

@Timothy Chow I understand that the proofs are long and complicated, but can you say a bit more about how long? Is there a PDF somewhere?

[Ruben Van de Velde]

I found https://randall-holmes.github.io/Nfproof/newattempt.pdf , which is... 45 pages?

[Yaël Dillies]

Just looking at the length of the paper, I would guess it could be formalized in about 6 months. However, are there any prerequisites?

[Kevin Buzzard]

Yael are you in any position to make this estimate? If I gave you the Taylor-Wiles paper which proved Fermat's Last Theorem that's just some stupid lemma in algebra and it's about 30 pages. How long do you think that would take?

[Yaël Dillies]

Yeah, that's why I said "Just looking at the length of the paper" :stuck_out_tongue:

[Kevin Buzzard]

And the other question is where are you going to find the person/people to do it?

[Kevin Buzzard]

I think that right now that's a big part of the problem unless some logicians come out of the woodwork. Patrick. Johan and I spent a year of our lives doing perfectoid and it attracted perfectoid people, but I suspect that starting will be the hard part. Of course the best possible solution is that Holmes works on it themselves -- that's what Hales did to get himself out of the mess he found himself in.

[Kevin Buzzard]

Holmes will find plenty of support from the community here, but big formalision projects like LTE need leaders.

[Shing Tak Lam]

btw I found this when looking for potential summer project supervisors.

There is a plan to get some money together for a Ph.D. studentship to do a formal verification of Holmes' proof of Con(NF). It's only at the design stage as yet, but if you are suitably qualified it would do you no harm to tell me about yourself.

https://www.dpmms.cam.ac.uk/~tf/

[Timothy Chow]

The leader would have to be Holmes himself. I don't think he knows Lean but he has experience with other proof assistants, and I think he's willing to put in the effort. As for Shing Tak Lam's comment, yes, I have been in touch with Thomas Forster, and while he is not going to participate in the formalization himself, he has said that he is eager to help in other ways. For example, he is organizing an NF meeting in Cambridge some time in May/June (exact date TBD), and he said, "If there is a head of steam behind these Lean ideas (``The Lean Green Mean Machine proves Con(NF)!!'') then we can have part of the meeting devoted to it. The programme is entirely up for grabs at this stage." (By the way, Kevin, Thomas says hi.)

[Timothy Chow]

In terms of prerequisites, the good news is that (from a human point of view at least) there doesn't seem to be a huge amount of background material being relied on. However, if there isn't much support in Lean for logic and set theory, then what seems to a human to be modest prerequisites could of course be a tremendous amount of work. The primary difficulty for a human seems to be the intricacy of the new constructions, and the fact that there were some bugs in the earlier versions.

[Johan Commelin]

Independence of CH was done in Lean. So I guess that will cover some prerequisites. But this is very far from my home turf, so I really can't estimate the effort that is needed.

[Patrick Massot]

Ruben Van de Velde said:

I found https://randall-holmes.github.io/Nfproof/newattempt.pdf , which is... 45 pages?

Reading the version notes and introduction make it very clear why nobody would trust this. So formalizing the proof would be a really really nice and useful achievement (assuming there are people who are interested in this result, but I trust Timothy here).

[Patrick Massot]

Johan, I think the issue is that independence of CH never went to mathlib, so presumably the code is not super easy to reuse.

[Johan Commelin]

@Timothy Chow Is there any way a lay person like me can get a feeling for what the impact of Con(NF) is for the "working mathematician" who is doing geometry or PDE's or number theory?

[Johan Commelin]

If NF disproves choice, I guess NF and ZF aren't really on speaking terms, are they?

[Kevin Buzzard]

Experience shows that it's extremely difficult to make accurate estimates about how long a formalision effort will take until a blueprint is written. The blueprint is a fully fleshed out explanation of the proof with no external references and everything brought down to stuff mathlib has already. A random throwaway comment in a paper which is unnoticed by a quick read-through can lead to a big rabbit hole or road block. An example is an application of Gordan's Lemma in the Scholze project. It's applied in the paper with the remark that it's a "standard fact". It's just some dumb assertion about monoids -- how hard can it be? The two proofs we found -- one used graded rings and one used results about convexity. I thought I'd try knocking off the graded ring proof but we didn't have graded rings at the time and it was hard to get these things right; a month later I still had no proof (and we might have even still been working on the definition). Bhavik Mehta then tried the convexity proof which turned out to be feasible given what we had already. This process ended up taking about two months, and it was one line in the paper.

[Patrick Massot]

Johan, we don't really need any impact for the working mathematician for this to be an interesting formalization challenge. We only need it to be interesting to a non-trivial amount of specialists in logic and set theory.

[Johan Commelin]

Agreed, but I'm just curious

[Patrick Massot]

If NF disproves choice then you already have your answer.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Experience shows that it's extremely difficult to make accurate estimates about how long a formalision effort will take until a blueprint is written. The blueprint is a fully fleshed out explanation of the proof with no external references and everything brought down to stuff mathlib has already. A random throwaway comment in a paper which is unnoticed by a quick read-through can lead to a big rabbit hole or road block. An example is an application of Gordan's Lemma in the Scholze project. It's applied in the paper with the remark that it's a "standard fact". It's just some dumb assertion about monoids -- how hard can it be? The two proofs we found -- one used graded rings and one used results about convexity. I thought I'd try knocking off the graded ring proof but we didn't have graded rings at the time and it was hard to get these things right; a month later I still had no proof (and we might have even still been working on the definition). Bhavik Mehta then tried the convexity proof which turned out to be feasible given what we had already. This process ended up taking about two months, and it was one line in the paper.

I remember this process quite well :sweat:

[Kevin Buzzard]

The fact that the CH stuff didn't make it into mathlib is another serious issue. My MSc project student Joseph Hua needed some results on model theory for his thesis but already the stuff in the CH repo had rotted quite badly, and when Joseph tried to use an old version of mathlib in order to be able to use it there was then of course a bunch of stuff in mathlib master which he couldn't get to (in particular Chris Hughes' work on the classification of algebraically closed fields, which was also crucial for Joseph). This presented us with a genuine problem until @Yakov Pechersky out of the blue bumped the model theory part of the CH repo to compile with mathlib master thus enabling Joseph's project to get off the ground and saving the project. Yakov I am still extremely grateful for this!

[Patrick Massot]

Kevin and Johan, remember you still have homework to do to put perfectoid spaces into mathlib. Almost all the topology parts went in.

[Kevin Buzzard]

When I've finished my course at the end of March I will be completely free and will have 100% of my time available for this job Patrick

[Kevin Buzzard]

More seriously the topology parts were essential for Maria, who is now beginning to PR her work to mathlib

[Yaël Dillies]

Bringing stuff to mathlib is the kind of dirty work I could do. What's the current status of bringing Flyspeck to mathlib? I saw model_theory got quite a lot of new files recently.

[Kevin Buzzard]

There are plenty of projects out there with to_mathlib folders :-) (perfectoid, CH, FLT-regular, Scholze)

[Yaël Dillies]

Still waiting to know from @Floris van Doorn what's happening with nnrat.

[Timothy Chow]

The consistency of NF would have zero practical impact on the mathematician doing PDEs or number theory, just as the consistency (or inconsistency, for that matter!) of ZF would have zero practical impact. A major motivation for NF was to take a different approach (from ZF) to avoiding the classical paradoxes. The underlying philosophy behind ZF is that the fundamental cause of the paradoxes is the lack of well-foundedness, and that if you just build the cumulative hierarchy from the ground up, then all will be well. NF, which was introduced by Quine, instead takes its cue from (Quine's) type theory. Impredicativity, or self-reference if you will, is avoided by restricting statements to "talking about" entities of lower type. The trouble with this brand of type theory is that all those subscripts are unworkable in practice for doing mathematics. To circumvent that, Quine introduced the concept of "stratification." This is a rather technical concept and I won't go into it here; the Stanford Encyclopedia of Philosophy article on NF provides a good introduction if you want to delve further. In any case, the point is that the motivation for NF is primarily philosophical rather than practical. In fact, some (including Holmes) would argue that any philosophical concerns that would be addressed by a consistency proof of NF have already been addressed by the (known) consistency proof of the variant of NF known as NFU. (But there are important differences between NF and NFU; for example, the standard proofs that NF implies the axiom of infinity and refutes the full axiom of choice don't carry over to NFU.) So arguably the main interest of Con(NF) is really that it is a natural problem that has defied solution for a long time, indicating that we don't understand some basic concepts (sets, types) as well as one might think.

As for the axiom of choice, the fact that NF disproves full AC doesn't mean that "NF and ZF aren't on speaking terms." I believe that NF is not known to disprove weaker forms of AC such as DC (the axiom of dependent choice), which covers most uses of choice that you need in practice.

[Johan Commelin]

Thank you very much for that explanation!

[Aaron Anderson]

Yaël Dillies said:

Bringing stuff to mathlib is the kind of dirty work I could do. What's the current status of bringing Flyspeck to mathlib? I saw model_theory got quite a lot of new files recently.

I've been putting those files in model_theory- there's quite a bit of stuff now, but nowhere near all of Flypitch (and a decent amount is kind of orthogonal to what they did in Flypitch). I know very, very little about NF, and less about this proof, but I think we could have the general model-theoretic foundations required within a few months if there was actual interest.

[Aaron Anderson]

However, I imagine that that's not really the hard part, as the hard part is probably more to do with the underlying set theory/infinite combinatorics, and/or totally unique things to this proof.

[Timothy Chow]

I asked Thomas Forster if he had anything to add to what I said about NF. He says that when people ask if NF and ZF are in conflict, he points out that NF has a concept of a well-founded set, and there is nothing to suggest that NF proves anything about well-founded sets that contradicts anything in ZF. Quote: "It is a long-standing conjecture in NF studies that every model of ZF (Zermelo, or KP even) has an end-extension with the same well-founded sets that is a model of NFD."

[Mario Carneiro]

I read this paper when it came out and was very excited to finally see the resolution of the NF consistency question, and I think that lean would be a great setting to formalize this proof. I could be missing something like Kevin's example of the throwaway comment in LTE, but this kind of logic is fairly self contained and it looks significantly easier than LTE. I would estimate closer to 1 month if you have at least one experienced formalizer and one person who knows the mathematics and can elaborate on skipped steps.

[Mario Carneiro]

I would volunteer myself but I definitely don't have the time to take on a project of this size right now. But I'm happy to help on the edges

[Thomas Forster]

Holmes' proof is a gigantic Fraenkel-Mostowski construction. It could be that a good start (a dry run) would be for someone to do a Lean proof of a simple FM proof. For example the original one that shows that the class of sets hereditarily of finite support does not obey AC for pairs. I am guessing that this would be comparatively straightforward. Any difficulties that do in fact show up would certainly show themselves in the Lean execution of Holmes' proof. So i would expect the exercise to be either easy or reassuring, or possibly both. With any luck i might persuade two of our local Leanies in Cambridge to tackle it for a summer project.

[Kevin Buzzard]

Hello Tom! Yeah there's a lean club in Cambridge, it meets on Wednesdays. @Bhavik Mehta will know the details

[Timothy Chow]

For those who know about the existing model theory code in Lean, do you think that any of it will help with the Fraenkel-Mostowski construction that Thomas Forster is suggesting? F-M constructions per se don't show up in the proof of the independence of CH, but there could still be something useful in flypitch. What about really basic stuff such as support for cardinals and ordinals?

[Randall Holmes]

Please note that I am here. I am not proficient in Lean: but I do write proof assistants myself, and I have experience using my own, and I think I can learn Lean. I have looked over it in the past. My proof is large, badly written (I have on good authority) and requires prerequisites in model theory (standard stuff) and set theory. It is an FM construction and does not involve forcing.

The proof comes in a number of different versions. It presents serious difficulties of exposition. There is no need to think about stratification: the formalization need not handle NF directly at all, but merely construct a model of an auxiliary theory called "tangled type theory". No one doubts that consistency of tangled type theory, or alternatively the existence of something called a "tangled web of cardinals" in ZF or probably even Mac Lane set theory without choice, implies Con(NF). That can be written in a few pages, and everyone able to read it believes it: it is a variation on Jensen's proof of Con(NFU). What is monstrous is the FM construction of these tangled things.

[Thomas Forster]

The NF meeting at which these matters might be discussed will take place in Cambridge some time after Randall Holmes arrives in Cambridge soon after 15/v and before i leave at the start of July. Recruitment will be word-of-mouth

[Timothy Chow]

Welcome, Randall! I wonder if some of the more experienced folks around here can suggest what first steps he should take?

[Randall Holmes]

Not that it would be at all a bad idea to prove Con(NFU) following Jensen, which would give a model to do the entire proof of Con(NF).

[Randall Holmes]

I have a good formal idea of what formal steps to take, but local conditions of course I do not know.

1. I need to target exactly what to prove. This might for example be Con(TTT) rather than Con(NF). this then conditions:

2. Determine what the prerequisites are and what might already exist. Certainly work on FM methods is needed.

I am leaving out

0. Learn basics of Lean. I can do this ;-)

[Timothy Chow]

I suspect that a good preliminary step would be to spell out the "standard stuff" from model theory and set theory that is going to be needed. Kevin's cautionary LTE tale about the one-line throwaway comment (regarding a standard fact that took two months to prove) strongly suggests that it is important to be explicit about these "standard" prerequisites, especially since it sounds like they might not already be in Lean.

[Randall Holmes]

It is worth remarking that my proof (assuming validity) settles that the mathematics of familiar structures is the same in NF as in ZF (mod the fact that ZF contains much stronger assumptions about large cardinals); certainly DC is consistent with NF, and so is well orderability of the continuum, or any familiar small mathematical structure. It is NOT evident from previous work that NF is consistent with DC or the continuum being well ordered; though certainly most NFistes believe that.

[Randall Holmes]

On a side note, the posted versions on my web page may not be up to date at the moment. I have spent the last few months working on two different new drafts in parallel, trying to deal with the problems in the exposition.

[Randall Holmes]

The part linking Con(NF) to existence of a tangled web of cardinals or to tangled type theory is absolutely solid and indeed doesnt strictly need to be formalized (though it would be no bad thing to do so). It is a retread of Jensen's proof of Con(NFU). But the construction of models of either of those things is hard, and hard to follow because what is being done is complicated and unfamiliar.

[Randall Holmes]

and for those without experience with this branch of mathematics, verifying Jensen's proof of Con(NFU) and adapting it to show that the consistency of tangled type theory or the existence of a tangled web of cardinals implies Con(NF) would

a. be a substantial amount of work and

b. have no bearing on and provide no assistance with the really needed consistency proof of tangled type theory or a tangled web of cardinals, which would be conducted in ordinary set theory of some flavor (and yes, with choice in the background, though it would be factored out by an FM construction), oh and

c. be a Very Good Thing in itself.

[Kevin Buzzard]

@Mario Carneiro are you able to state in lean the main theorems in this paper (the tangled type theory assertion and the consistency of NF)? Or at least sketch what you would envisage the assertion looking like (the "shape")? One could imagine starting a new lean project called con-nf or con_nf or whatever, and put a file in src/ containing a statement of the main theorem. This would be a way to begin to understand what the actual job will entail. By the way lean does have a theory of cardinals and ordinals (thanks to Mario), and @Violeta Hernández has been proving theorems about them, there's occasionally discussions of her work on the Discord.

[Mario Carneiro]

I will say that it is much easier to formulate the goal as "prove the existence of a tangled web of cardinals" or even "construct a model of NF" rather than "prove Con(NF)", because this last statement involves a bunch of proof theory that is only marginally involved since we want to immediately defer to the model theoretic perspective by constructing a model, after which point we don't need formal syntax anymore

[Mario Carneiro]

From what Randall says it sounds like that last step is not questionable, so it would be suitable to be deferred after the main part of the proof (like we did for LTE)

[Randall Holmes]

Replying to Kevin, I have to learn Lean first ;-) I know what kind of thing it is, but I don't know the details. Mod that, I should probably be able to state what has to proved, in the course of which I would have to describe intermediate concepts which have to be developed if they do not exist.

There are steps. My guess is that formulating the statement "There is a model of tangled type theory" would be relatively easy (and reveal requirements). This definition will involve some formal syntax, unfortunately.

Formulating the description of the structure which I claim is a model of tangled type theory would be harder and longer, and probably reveal more requirements.

Formulating the proof that the structure described in part 2 really is a witness to the statement in part 1 will be horrible.

[Randall Holmes]

Replying to Mario, Constructing a model of NF would not be easier. I precisely do not directly construct or describe a model of NF, though one can tell from the proof various things about what one would be like. The relative consistency proof Con(TTT) -> Con(NF) handles all of that.

[Randall Holmes]

I do very concretely describe and verify a model of Con(TTT) in that version of the proof.

[Mario Carneiro]

@Randall Holmes How do the statements "There is a model of tangled type theory" and "there is a tangled web of cardinals" compare?

[Randall Holmes]

They are closely related. One is an assertion about cardinal arithmetic in ZF (or Zermelo or Mac Lane set theory) which is inconsistent with choice. One is the assertion of a model of a certain very strange type theory. Both involve the ability to say that a sentence is true in a structure, unfortunately: formal syntax will be involved. The model of type theory in the TTT approach is described as a structure in an ambient ordinary set theory (with choice); the proof of existence of a tangled web is carried out by FM methods starting in a model of ordinary set theory with choice. The difference between the two approaches is a style difference: the tangled web approach is the one I took initially and is friendlier to state; but I think the technicalities may be easier in the TTT approach. Both approaches were evidently possible from the time of my 1995 paper. FM methods are also implicit in the TTT approach.
I dont recommend reading my 1995 paper; read the preamble to the current paper.

One of my Tasks if we are to do this is to prune the stuff presented on my web page at the moment, and just give two papers, one for each approach.

[Mario Carneiro]

One is an assertion about cardinal arithmetic in ZF (or Zermelo or Mac Lane set theory) which is inconsistent with choice.

Hm, that's too bad, if you mean the tangled web here. I was hoping this one could be written directly in lean without further embedding

[Randall Holmes]

Ill be concrete: one has to be able to talk about what sentences are satisfied in the natural model of the simple typed theory of sets with the base type of a given cardinality.

[Mario Carneiro]

Is "the natural model of the simple typed theory of sets" defined explicitly in the paper?

[Mario Carneiro]

that sounds like a good place to start

[Randall Holmes]

Yes. That is easy: it is the natural model whose types are the base type and its iterated power sets, with the membership and equality of the ambient set theory inherited. One has to deal in one of a couple of ways with the fact that the iterated power sets might overlap, but that is an imagined horror. And of course that is the power set of an FM model.

[Mario Carneiro]

how many times iterated? I guess we have axiom of replacement here so that any set has cardinality less than the ordinals?

[Randall Holmes]

a finite number of times in each instance, actually.

[Randall Holmes]

But one needs to be able to handle any finite number of types, so being able to talk about the model of omega types might be useful.

[Mario Carneiro]

hm, I could use a precise description then since I can't quite picture it

[Mario Carneiro]

If you just take all the finite powersets of the base type you will get a model in which the ordinals are omega, right?

[Randall Holmes]

The von Neumann definition of ordinals is wrong in this context. Think of Scott ordinals.

[Randall Holmes]

If you want to talk about what ordinals can be represented, in V_omega*2 the ordinals certainly dont stop at omega. But the von Neumann definition is not the right one.

[Randall Holmes]

But you can use von Neumann ordinals in your metatheory to your heart's content, I hasten to add.

[Mario Carneiro]

well I'm mostly just looking for a precise description that can be leanified. Is it something like this:

• $M_0=A$
• $M_{n+1}=\mathcal{P}(M_n)$
• $M=\bigcup_{n<\omega}M_n$

[Randall Holmes]

Im getting to that. Its roughly like that but with technical refinements. M_0 is a set of atoms. (we might as well use ZFA since we are doing FM constructions anyway) of the cardinal kappa of interest

M_n+1 is the power set of M_n, with the empty set replaced by an atom emptyset_n+1, these being different with different indices

The modifications ensure that the types do not overlap, which avoids technical issues

Then it is straightforward that the first order theory of the model is entirely determined by the cardinality of the base set

[Randall Holmes]

and then part of the description of the tangled web of cardinals involves facts about sentences satisfied by this model for cardinals in the web

[Mario Carneiro]

types not overlapping is actually the easy case in type theory

[Randall Holmes]

Of course, and that is why I want to get to it

[Mario Carneiro]

So you want something like this:

• $M_0=A$
• $M_{n+1}=\mathcal{P}(M_n)$
• $M=\Sigma_{n<\omega}M_n$

[Randall Holmes]

Notice that is really M_kappa,n -- the model has a parameter kappa, the cardinality of the base type. Which is not an ordinal, it is a Scott cardinal, in a context where choice wont hold.

[Mario Carneiro]

Yes, $A$ is a parameter to the construction, it's your type of atoms

[Mario Carneiro]

and its cardinality is presumably important here

[Randall Holmes]

M_n+1 = P(M_n) - {emptyset) + {emptyset_n+1}

[Randall Holmes]

it isnt a type of atoms, its a set of atoms in a background untyped theory

[Randall Holmes]

and |A| is the real parameter of interest

[Mario Carneiro]

You don't need to swap out empty sets with the construction I just mentioned, because they are disjointified by the construction of $M$

[Mario Carneiro]

the sigma there means disjoint union

[Randall Holmes]

That is all in the tangled web approach

[Randall Holmes]

or one way of doing it

[Randall Holmes]

Oh I see, of course. But Im working in an ambient untyped theory in that approach. I would have to think about what things would look like in a typed metatheory.

[Randall Holmes]

It might be perfectly adaptable to that environment, but I havent thought of it that way.

[Mario Carneiro]

Right, that's going to be part of the formalization since you're working in lean. It usually isn't a huge difference, but sometimes you can avoid some awkwardness of ZF style constructions

[Mario Carneiro]

in particular, disjoint union is more natural than union in type theory

[Mario Carneiro]

so I would avoid plain union unless it's required by the construction

[Randall Holmes]

I know this very well. I just havent thought of what the proof would look like in that metatheory.

[Randall Holmes]

It might be very nice.

[Randall Holmes]

Still horrible, but it might be managed just fine in that framework.

[Mario Carneiro]

You mention that the metatheory needs a set of atoms (you have ZFA as the metatheory). This seems odd to me - don't you need to constrain the atoms in some way? Otherwise you could just say at the end of the construction that $A$ was empty after all and it was really a construction in ZF

[Mario Carneiro]

In lean, I think that will probably just be a type parameter to the entire construction

[Randall Holmes]

No, the set of atoms has to be large. This is specified. Then one applies permutations to it.

[Mario Carneiro]

are there any constraints other than cardinality? You used named empty-set atoms in the construction

[Randall Holmes]

It has structure, probably many types of atoms in a formalization in that metatheory. Types of atoms indexed by finite sets of ordinals taken from a limit ordinal lambda

[Randall Holmes]

The named empty sets were just a gadget to make the types disjoint

[Mario Carneiro]

gotcha

[Mario Carneiro]

How do you access the structure on the atoms in the construction? I.e. how do you use this "finite sets of ordinals taken from a limit ordinal"

[Randall Holmes]

The types of atoms are all in the metatheory of the same size, a strong limit cardinal mu. They would be indexed by nonempty finite subsets of a limit ordinal lambda. The construction absolutely would not work if the sets of atoms were empty.

[Mario Carneiro]

I'm wondering if some other indexing mechanism is viable, for example list V where V is a type with cardinality mu

[Randall Holmes]

That is complicated. It is described in the paper, of course. And I must stop this fascinating conversation for the present and write some class notes for an undergraduate class :-( You have put a bee in my bonnet.

[Mario Carneiro]

Can you point me to where in the paper this is addressed? You don't have to cover it here of course, I'm looking for pointers

[Randall Holmes]

Before you can talk about how the structure could be modified, you have to know what is going to be done with it. That is...tangled
The indexing by finite subsets of a limit ordinal is natural to the application.

[Mario Carneiro]

that's fair. It's also possible to use finite sets for indexing here, but there might be some trivial optimizations possible in the new metatheory

[Randall Holmes]

Look at the definition of a tangled web of cardinals. and the proof that if there is one, NF is consistent. But I also want to point you to the right version of the paper. Let's continue this later. In the interim, I might purge the various drafts there and put up the exact ones I would want participants in this conversation to look at.

[Randall Holmes]

That definition and proof are stable in any version of the paper, though.

[Randall Holmes]

and solid. They are unfamiliar to most people, but anyone who knows Jensen's proof has accepted this after a few questions.

[Mario Carneiro]

I'll be looking at https://randall-holmes.github.io/Nfproof/newattempt.pdf until you suggest otherwise

[Mario Carneiro]

Question: what is the powerset of an atom in ZFA? It seems like a naive reading of {x | x ⊆ S} and x ⊆ y ↔ ∀ z, z ∈ x → z ∈ y would have every atom being a subset of every other atom, and therefore every powerset contains every atom, but this seems bad. Should ${\mathcal P}(a) = \{a\}$? ${\mathcal P}(a) = \{\emptyset, a\}$? ${\mathcal P}(a) = \{\emptyset\}$?

[Timothy Chow]

Certainly an atom should not be a subset of an atom because an atom is not a set. The standard approach is to make axioms empty, so P(a) = {{}}. https://ncatlab.org/nlab/show/ZFA

By the way, I might be jumping the gun a bit, but I propose naming this project "Conifer." Like "Flyspeck," it's a quasi-acronym (for Con(NF)).

[Mario Carneiro]

@Timothy Chow My point is that since atoms are empty, they are subsets of the empty set: they satisfy ∀ z, z ∈ a → z ∈ ∅ vacuously. So either the definition of the powerset or the definition of subset has to be modified somehow if we want to not accidentally pick up all the atoms in every powerset.

[Mario Carneiro]

Here's a first shot at the main definitions of the paper: https://gist.github.com/digama0/1e3cf75427b0caffdac566d01a2e2bcb

• ZFA, normal filters, (hereditarily) symmetric, symmetric powerset
• Parameters of the construction
• Extended type indexes
• clans, atoms, litters, near litters, local cardinality
• strict dominance
• support order
• the groups $G$ and $G_S$
• The normal filter used in the construction
• The $\tau(A)$ function
• The properties of a tangled web

The paper seems to be written in a very nonlinear style. In the last few parts we incur a dependency on the $\Pi_A$ function, which seems not to be defined until somewhere in the depths of the paper; there appears to be a giant recursion on $A$ involved, but the lack of explicit theorem statements makes it difficult to follow what is actually being proved in some parts. So the definition of $\tau$ I think currently has a spurious dependency on $\Pi$.

[Timothy Chow]

I have no experience with Lean so I'm probably talking nonsense here, but ZFA, like the systems in Simpson's book, is two-sorted. Atoms and sets are two different sorts of things. I'm not even sure why you need to define P(a) where a is an atom; I figured it was out of convenience, like it's convenient to define 0/0 = 0.

[Timothy Chow]

If there's a formula in the paper that seems to be picking up atoms when it shouldn't, there's presumably an implicit restriction to sets somewhere.

[Thomas Forster]

One thing you can do is expand the language with a name for the empty set.

[Mario Carneiro]

@Randall Holmes Could you explain what's going on in the definition of a strong support order? I'm having trouble type checking it.

2. If $S_β$ is a near-litter belonging to $clan[B]$ with $B$ strictly downward
   extending $A$, then either the parent of $S_β$ is an atom and either equal
   to $S_γ$ for some $γ < β$ or not an element of $S$ at all, or there is a subset
   $T$ of $β$ such that the restriction of $<_S$ to $T$ is a $B$-strong support for
   the parent of $S_β$.

In the second part of the clause, we know that the parent of $S_\beta$ is in the second case, that is, a subset of ${\mathcal P}^*(clan[B\cup\{\alpha\}])$ for some $\alpha$ with $B\cup\{\alpha\}\ll B$. We also know $\beta$ is some ordinal less than the order type of $<_S$, so $T$ is a subset of an ordinal. So it seems strange to be restricting $<_S$ to $T$, given that the domain of $<_S$ is a collection of atoms and near-litters, not ordinals.

Also, this definition seems to involve a recursion, since there is a reference to $B$-strong supports in the definition of $A$-strong supports. What is the well founded relation we are recursing along (I'm guessing $\ll$), and how much of the definition actually needs this recursion? Is this definition monotonic w.r.t extension or subsetting the domain?

[Mario Carneiro]

Here is a version that works without any direct reference to ZFA. This also includes the complete recursive definition of the parent_map, so I think the final theorem is now the correct statement. I'm hoping someone like @Randall Holmes or @Thomas Forster can learn enough lean to pick this up and do the proofs, though; I'm not in a position to spend a month on this.

import set_theory.cofinality
import order.symm_diff
import group_theory.group_action.basic

noncomputable theory
open_locale cardinal classical

universes u v

local attribute [instance]
def mul_action.set {G} [group G] {α} [mul_action G α] : mul_action G (set α) :=
{ smul := λ π S, (λ x, π • x) '' S, one_smul := sorry, mul_smul := sorry }

section
variables (A : Type*) {X : Type*} [group X] [mul_action X A] (G : subgroup X)
structure normal_filter :=
(Γ : set (subgroup X))
(is_perm : ∀ (K ∈ Γ), K ≤ G)
(atoms : ∀ a : A, mul_action.stabilizer X a ∈ Γ)
(upward : ∀ H K, H ∈ Γ → H ≤ K → K ∈ Γ)
(inter : ∀ H K, H ∈ Γ → K ∈ Γ → H ⊓ K ∈ Γ)
(conj : ∀ (π ∈ G) (h ∈ Γ), (h:subgroup _).map (mul_aut.conj π).to_monoid_hom ∈ Γ)

variables {A G} (F : normal_filter A G)

def normal_filter.symm {α} [mul_action X α] (x : α) : Prop :=
mul_action.stabilizer X x ∈ F.Γ

def normal_filter.set (α) [mul_action X α] : Type* := { s : set α // F.symm s }

instance (α) [mul_action X α] : mul_action X (F.set α) :=
{ smul := λ x S, ⟨x • S.1, sorry⟩,
  one_smul := sorry,
  mul_smul := sorry }
end

namespace con_nf

class params :=
(Λ : Type u) (Λr : Λ → Λ → Prop) [Λwf : is_well_order Λ Λr]
(hΛ : (ordinal.type Λr).is_limit)
(κ : Type u) (hκ : (#κ).is_regular)
(μ : Type u) (μr : μ → μ → Prop) [μwf : is_well_order μ μr]
(μ_ord : ordinal.type μr = (#μ).ord)
(μ_limit : (#μ).is_strong_limit)
(μ_cof : max (#Λ) (#κ) < (#μ).ord.cof)
(δ : Λ)
(hδ : (ordinal.typein Λr δ).is_limit)

open params

variable [params.{u}]

def small {α} (x : set α) := #x < #κ

instance : is_well_order Λ Λr := Λwf
instance : linear_order Λ := linear_order_of_STO' Λr

-- extended type index
def xti : Type* := {s : finset Λ // s.nonempty}

def xti.min (s : xti) : Λ := s.1.min' s.2
def xti.max (s : xti) : Λ := s.1.max' s.2

def xti.drop (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.min, h⟩ else none
def xti.drop_max (s : xti) : option xti := if h : _ then some ⟨s.1.erase s.max, h⟩ else none

instance : has_singleton Λ xti := ⟨λ x, ⟨{x}, finset.singleton_nonempty _⟩⟩
instance : has_insert Λ xti := ⟨λ x s, ⟨insert x s.1, finset.insert_nonempty _ _⟩⟩

noncomputable def xti.dropn (s : xti) : ℕ → option xti
| 0 := some s
| (n+1) := xti.dropn n >>= xti.drop

def sdom : xti → xti → Prop
| A := λ B, A.max < B.max ∨ A.max = B.max ∧
  ∃ A' ∈ A.drop_max, ∀ B' ∈ B.drop_max,
    have (A':xti).1.card < A.1.card, from sorry,
    sdom A' B'
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ A, A.1.card)⟩]}

instance : has_lt xti := ⟨sdom⟩
instance xti.is_well_order : is_well_order xti (<) := sorry
instance : has_well_founded xti := ⟨_, xti.is_well_order.wf⟩
instance : has_le xti := ⟨λ A B, A < B ∨ A = B⟩

def clan (A : xti) := μ × κ
def atoms := Σ A, clan A

def litter (A) (x : μ) : set (clan A) := {p | p.1 = x}

def litter.is_near {A} (N : set (clan A)) (x : μ) := small (N Δ litter A x)

def local_cards (A : xti) : Type u := μ

structure clan_perm (A : xti) : Type u :=
(ρ : equiv.perm (local_cards A))
(π : equiv.perm (clan A))
(near (x) : litter.is_near (π '' litter A x) (ρ x))

instance (A) : group (clan_perm A) := sorry

instance (A) : mul_action (clan_perm A) (local_cards A) :=
{ smul := λ π, π.ρ, one_smul := sorry, mul_smul := sorry }

instance (A) : mul_action (clan_perm A) (clan A) :=
{ smul := λ π, π.π, one_smul := sorry, mul_smul := sorry }

def near_litter (A) := Σ' (N : set (clan A)) x, litter.is_near N x

def near_litter.is_litter {A} (N : near_litter A) := N.1 = litter A N.2.1

instance (A) : mul_action (clan_perm A) (near_litter A) :=
{ smul := λ π N, ⟨π • N.1, π.ρ N.2.1, sorry⟩, one_smul := sorry, mul_smul := sorry }

def clans_perm := Π A, clan_perm A
instance : group clans_perm := pi.group

instance (A α) [mul_action (clan_perm A) α] : mul_action clans_perm α :=
{ smul := λ π a, π A • a,
  one_smul := λ a, one_smul _ a,
  mul_smul := λ π ρ c, mul_smul (π A) (ρ A) c }

instance (α β) [mul_action clans_perm α] [mul_action clans_perm β] :
  mul_action clans_perm (α ≃ β) :=
{ smul := λ π e, ⟨λ a, π • e (π⁻¹ • a), λ b, π⁻¹ • e.symm (π • b), sorry, sorry⟩,
  one_smul := sorry,
  mul_smul := sorry }

instance : mul_action clans_perm atoms :=
{ smul := λ π a, ⟨a.1, π a.1 • a.2⟩,
  one_smul := sorry,
  mul_smul := sorry }

def local_card {A} (N : near_litter A) : local_cards A := N.2.1

def parent_set (A : xti) :=
(Σ' A' (h : A.drop = some A'), clan A') ⊕
(Σ' a (h : insert a A < A), set (set (clan (insert a A))))

instance (A) : mul_action clans_perm (parent_set A) :=
{ smul := λ π x, match x with
  | sum.inl ⟨A', h, c⟩ := sum.inl ⟨A', h, π • c⟩
  | sum.inr ⟨a, h, s⟩ := sum.inr ⟨a, h, π • s⟩
  end,
  one_smul := sorry,
  mul_smul := sorry }

def support_el (Q : xti → Prop) := Σ A, Σ' _ : Q A, clan A ⊕ near_litter A
def support_el.inl (Q : xti → Prop) {A}
  (h : Q A) (c : clan A) : support_el Q := ⟨A, h, sum.inl c⟩
def support_el.inr (Q : xti → Prop) {A}
  (h : Q A) (N : near_litter A) : support_el Q := ⟨A, h, sum.inr N⟩

def support_el.below {Q A} (x : local_cards A) : support_el Q → Prop
| ⟨A, h, sum.inl c⟩ := μr c.1 x
| ⟨A, h, sum.inr N⟩ := N.is_litter ∧ μr N.2.1 x

instance {Q : xti → Prop} : mul_action clans_perm (support_el Q) :=
{ smul := λ π x, match x with
  | ⟨A, h, sum.inl c⟩ := support_el.inl _ h (π • c)
  | ⟨A, h, sum.inr N⟩ := support_el.inr _ h (π • N)
  end,
  one_smul := sorry,
  mul_smul := sorry }

structure support_order (Q : xti → Prop) :=
(S : set (support_el Q))
(small : small S)
(disj (A h M N) :
  @support_el.inr _ Q A h M ∈ S → support_el.inr _ h N ∈ S → M ≠ N → disjoint M.1 N.1)
(r : S → S → Prop)
(wo : is_well_order S r)

variables {P : xti → Prop} (PI : ∀ B, P B → local_cards B → parent_set B)

def allowable' : subgroup clans_perm :=
{ carrier := { π | ∀ B h x, PI B h (π • x) = π • PI B h x },
  one_mem' := sorry,
  mul_mem' := sorry,
  inv_mem' := sorry }

def supported' {Q} (S : support_order Q) : subgroup clans_perm :=
allowable' PI ⊓ ⨅ a ∈ S.S, mul_action.stabilizer _ a

def has_support' {Q} (S : support_order Q) {α} [mul_action clans_perm α] (x : α) : Prop :=
supported' PI S ≤ mul_action.stabilizer clans_perm x

def support_filter' (Q) : normal_filter atoms (allowable' PI) :=
{ Γ := {K | ∃ S : support_order Q, supported' PI S ≤ K},
  is_perm := sorry,
  atoms := sorry,
  upward := sorry,
  inter := sorry,
  conj := sorry }

def parent_set.symm' (Q) {A} : parent_set A → Prop
| (sum.inl ⟨A', _, c⟩) := (support_filter' PI Q).symm c
| (sum.inr ⟨a, _, x⟩) := (support_filter' PI Q).symm x ∧ ∀ s ∈ x, (support_filter' PI Q).symm s

def parent_range' (Q A) := {x : parent_set A | x.symm' PI Q}

theorem parent_range'_card (Q A) : #(parent_range' PI Q A) = #μ := sorry

structure good_bij' (Q : xti → Prop) {A} (f : local_cards A → parent_set A) : Prop :=
(inj : function.injective f)
(range : set.range f = parent_range' PI Q A)
(below (x : local_cards A) :
  ∃ S : support_order Q, has_support' PI S (f x) ∧
    ∀ c : support_el Q, c ∈ S.S → c.below x)

theorem exists_bij' (Q A) : ∃ f : local_cards A → parent_set A, good_bij' PI Q f := sorry

def the_bij (Q A) := classical.some (exists_bij' PI Q A)

noncomputable def parent_map : ∀ (A : xti), local_cards A → parent_set A
| A := @the_bij _ (λ B, B < A) (λ B hB, parent_map B) (λ B, B ≤ A) A
using_well_founded {dec_tac := `[assumption]}

def allowable : subgroup clans_perm := allowable' (λ B (_ : true), parent_map B)

def support_filter : normal_filter atoms allowable :=
support_filter' (λ B (_ : true), parent_map B) (λ _, true)

def parent_set.symm {A} (s : parent_set A) := s.symm' (λ B (_ : true), parent_map B) (λ _, true)
def parent_range := parent_range' (λ B (_ : true), parent_map B) (λ _, true)
theorem parent_range_card (A) : #(parent_range A) = #μ := parent_range'_card _ _ _

def symm {α} [mul_action clans_perm α] (x : α) := support_filter.symm x

def sset (α) [mul_action clans_perm α] := support_filter.set α
instance (α) [mul_action clans_perm α] : mul_action clans_perm (sset α) :=
by unfold sset; apply_instance

def sset_n : ℕ → ∀ (α) [mul_action clans_perm α], Type*
| 0 α h := α
| (n+1) α h := sset_n n (by exactI sset α)

noncomputable instance mul_action.sset_n :
  ∀ n α [mul_action clans_perm α], by exactI mul_action clans_perm (sset_n n α)
| 0 α h := h
| (n+1) α h := mul_action.sset_n n _

def xti_below := {A : xti // A < {δ}}
def τ (A : xti_below) := sset_n 2 (clan (insert δ A.1))
instance (A) : mul_action clans_perm (τ A) := by unfold τ; apply_instance

theorem τ_power (A A' : xti_below) (h : A.1.drop = some A'.1) :
  ∃ f : τ A ≃ sset (τ A'), symm f := sorry

theorem τ_elementary (A A' B B' : xti_below) (n)
  (hA : A.1.dropn n = some A'.1) (hB : B.1.dropn n = some B'.1)
  (H : A.1.1 \ A'.1.1 = B.1.1 \ B'.1.1) :
  sset_n (n+2) (τ A') ≃ sset_n (n+2) (τ B') := sorry

end con_nf

[Thomas Forster]

Wow!

[Yaël Dillies]

A power unbeknowst to us mortals...

[Kevin Buzzard]

@Thomas Forster if you like the computer puzzle game analogy, Mario has now "made the level" (this sort of stuff needs a lot of expertise) and then the next step is to "solve the level", which can be attempted by someone whose lean expertise is far lower -- for example a maths PhD student in this area with no prior lean experience can learn enough about the basics of lean to try and fill in some of those sorries with tactic proofs. Once they're all filled in, you're done. Some of them will no doubt be straightforward.

[Thomas Forster]

That makes it sound as if i cld make myself useful. Randall is going to be here from mid-may for a good long while (a month or so) so perhaps we could confer with the local Leanies? The major drawback with that is that this is smack in the middle of the time when they should be steeling themselves for exams...

[Timothy Chow]

Hope I used :working_on_it: correctly. I was searching for what :octopus: meant and found this:
https://leanprover-community.github.io/archive/stream/113488-general/topic/octopus.20emoji.html

[Randall Holmes]

I can only answer briefly right now. All of these are comments for Mario.

There is a notion of set and there is only one empty set. A is a subset of B means, A is a set and B is a set and every element of A is an element of B. (Anything with an element is a set, and there is only one empty set).

So atoms have no subsets. The power set of an object is the collection of its subsets, so if one must ask what the power set of an atom is,
the answer is, either it is undefined or it is the empty set. The question should not come up.

I cant evaluate definitions until I understand the Lean formalism, and at the moment I am buried in teaching and administration. Ill try to get to it soon!

The paper is written in a highly nonlinear style because there is a really horrible recursion involved. The dependence of tau on Pi is certainly not spurious.

[Randall Holmes]

Mario, did you figure out the definition of strong support order?

I will add, there is another generation of versions of the paper. I think this one is going to be pretty impenetrable.

One comment which is useful is that Pi_A isn't defined: these maps are chosen at each step of the construction based on cardinality facts which have to be verified (that various sets which are constructed as one recurses along << are in fact all of the same size mu).

I will try to (1) post newer versions soonish (within weeks) if I think they are ready to be presented as targets. (2) Try to read this version itself again and see if I can give explicit answers to questions Mario raises. (3) try to read what Mario has done and see if I agree! For all of these, the time target is within weeks: I am taking time away from getting to the university to print out exams I am giving today which I will be marking over the weekend, I am behind on writing my own contribution to my annual personnel evaluation and I have bunches of other things I should have done a month ago.

Sorry that my writing here is unlovely; I dont understand the bells and whistles of this medium.

[Randall Holmes]

Ill try to look in here again soonish. Mario, feel free to email me questions if you have more.

[Randall Holmes]

I have just posted a more recent document, a construction of a model of tangled type theory, on my web page. A more recent document taking the same approach as the one Mario is using (and I think meeting his requirements better) will appear, but isn't accessible to me as I tyoe; it is on my old laptop and I don't seem to have copied if over.

The document just posted has a considerably more linear style. But what it describes is awful.

[Thomas Forster]

I need some guidance from this community. I have the possibility of the university funding one or possibly two students over the summer to do some preparatory work on this project. But of course i have to prepare a proposal! I have no idea what do say, having no experience in these matters. I would be very glad of some advice on what to put in such a proposal. Specifically the funders say that if they are to fund two students for a collaboration the proposal has to have a Good Story about what form the collaboration would take. HELP!!

[Jeremy Avigad]

Hi, Thomas! I think it is safe to say that if you have good students that are willing to learn to use Lean and work on the project, they will have plenty of support from this community. You have already seen that they can get answers on Zulip around the clock. Students are always welcome here in Pittsburgh. There's a workshop at ICERM this summer: https://icerm.brown.edu/topical_workshops/tw-22-lean/. And Kevin Buzzard and all our friends in London are just a stone's throw away.

[Thomas Forster]

So i just put them in a room with comfy chairs and a supply of coffee/tea, plus access to LEAN support and Randall and just let them get on with it? The fact that i, Thomas Forster, have no idea how to set about it doesn't really matter...? I'm not sure that my students can get funding to come to your workshop, nice tho' that would be.

[Kevin Buzzard]

This kind of approach can work. They will have two kinds of questions -- maths ones and lean ones, and the community here can help with the lean ones and you can help with the maths ones. To give a related example, Scholze challenged the community to prove a theorem of himself and Clausen, and then stayed around to help us with maths questions and the community just translated the work

[Thomas Forster]

Thanks, Kevin. I've got some funding for this project so i'll just go ahead, trusting them to Do The Right Thing. Randall is coming to Cambridge for a month or so from mid-may and it will be wonderful to have him here. Sadly, the timing is not ideal, given that my students have exams during that time, but we'll manage. I suspect there will be very little for me to do, since there are people who understand LEAN better than i do, and Randall understands his proof better than i do! But at least i know how to make a decent pot of tea, so i won't be completely useless.

[Timothy Chow]

Thomas, maybe what you need for a proposal are "deliverables"? The fact that the Lean community recognizes the importance of building up libraries should be helpful to you. At minimum, your students should be able to improve the general library support in Lean for model theory and set theory. This should be a lasting contribution even in the worst case that Randall's argument turns out to be wrong. (I'm not sure what story to tell about Lean 3 versus Lean 4 libraries; maybe someone who knows what they're talking about can chime in here.) Also, since Mario Carneiro has "made the game" so to speak, there are measurable milestones; your students can flesh out the sorrys one by one.

[Mario Carneiro]

I wouldn't worry too much about the library building being in lean 3 (I do recommend sticking to lean 3 for this project) even though lean 4 is on the horizon. Everything will get mostly-automatically ported in the end, so a new lean 3 library development will definitely contribute to an eventual corresponding lean 4 library, and even if we weren't trying to port everything, "second system" formalizations are always a lot easier than the first one, even if we're talking about a fully manual port from something significantly different like Coq/Mizar/Metamath, because at least half of the work is spent on trying to say something in a fully precise way and the other half is expressing that precision in a specific formal language.

[Thomas Forster]

I'm thinking that it could be good to verify a basic Fraenkel-Mostowski construction. I'm guessing that that hasn't been done in LEAN? It would be a useful stage 0 rehearsal for Randall's proof (which is the mother of all F-M constructions) and might be a good idea on its own account..(?)

[Mario Carneiro]

Note that in the proof sketch I give above, most of the F-M stuff has been boiled away. Instead we just have normal_filter and a bunch of stuff about group actions, both of which are not particularly specific to the proof

[Mario Carneiro]

I thought there would be an actual F-M construction because it is stated like that in the original proof, and v1 actually does have a permutation model and an action on the universe, but it is more natural in type theory to have actions on each of the sets (reinterpreted as types) rather than encoding everything in set theory first, and once you make this shift then the statement becomes much simpler

[David Michael Roberts]

One thing that has struck me ever since I tried reading the proof is that it feels very much like the Cole–Mitchell–Osius–(Hayashi?) construction of something like a model of BZA from a category of equivariant sheaves on a Boolean algebra. The complexity in describing a ZFA forcing model looks to my eyes like it arises from a factorisation of the process ZF(A) ~> its category of sets ~> category of sheaves ~> model of ZFA.

@Randall Holmes have you talked to any category or topos theory people? @Thomas Forster I do wonder what Peter Johnstone might make of the construction...

[Thomas Forster]

This is all news to me, and i would like to chase it up. Can you tell me more? I could ask PTJ about it but i am in contact with the other senior categorist at Cambridge, namely Martin Hyland - who is definitely following developments re Holmes' proof. He hasn't mentioned this stuff to me. I shall show him your message...

[Thomas Forster]

It seems that the parallel with Cole-Mitchell-Osius is not helpful.

[David Michael Roberts]

OK, good to know. It just seemed rather reminiscent, and there's still a rather 'structural' feel to the construction that seems foreign from the point of view of more traditional set theory (i.e. ZF(C)/ZFA)