ZFSet and computability

Stream: mathlib4

[Violeta Hernández]

Currently, docs#ZFSet is defined as a quotient of docs#PSet, an inductive type which has an incorrect and wholly non-mathematical form of equality. All of the usual set-theoretic functions are first defined on PSet, then transferred to ZFSet. The advantage of doing this, or so I've been told, is that this makes operations on ZFSet computable.

Over at the game-theory repository, we for the longest time had an analogous situation (games are basically two-sided sets, in a way). We had a type PGame with the wrong equality, and after a bunch of tedious set-up we were able to define the type IGame with the correct equality.

On paper, this meant that we had computability and thus decide at our disposal. In practice? It basically never worked. Since all of our definitions were done through well-founded recursion, decide refused to unfold anything ever. Eventually, we figured out that a custom simp set provided most of the same capabilities, and computability fell to the wayside.

Some time later, @Aaron Liu realized that thanks to the machinery of docs#QPF, the PGame setup was completely unnecessary. We could instead define

def GameFunctor (α : Type (u + 1)) : Type (u + 1) :=
  {s : Bool → Set α // ∀ p, Small.{u} (s p)}

and provide a QPF instance on it. The type of games is then the smallest fixpoint docs#QPF.Fix of this functor. A really nice corollary of this is that we could then define the type of loopy games (where a state can be returned to) as the largest fixpoint docs#QPF.Cofix of the same functor. And thus, PGame was vanquished for good. (See Functor.lean for the full details on this setup).

All of this could be done for ZFSet all the same. In fact, we could easily define

def SmallSetTupleFunctor (α : Type (u + 1)) (β : Type) : Type (u + 1) :=
  {s : β → Set α // ∀ p, Small.{u} (s p)}

which would generalize both the ZFSet and the IGame constructions (setting β to either Unit or Bool). In the case of ZFSet, the co-fixpoint doesn't currently exist in Mathlib, but it's still a mathematically interesting object: it gives us a model for Aczel's anti-foundation axiom.

The catch? Since docs#Shrink is non-computable, the QPF instance is too. Which means we lose out on computable ZFC sets. My question is, do we really want them?

• We currently make no use of ZFSet computability within Mathlib. Though arguably that doesn't mean much, since there's only like 4 files in that folder.
• More importantly, I'd argue that the benefits of computability are quite limited in scope. You have no decidable equality, or membership, or subsets, even in the finite case, since ZFSet bundles no Fintype instances or anything of the sort.
• For finite sets, we already have docs#Lists, which models ZFA minus infinity and whose relations and operations are all decidable/computable.
• ZFSet isn't really lacking in any automation that could be provided by computability. A lot of its theorems are proved by simply passing to Set.

[Robin Arnez]

Violeta Hernández schrieb:

Since docs#Shrink is non-computable

Not anymore

[Violeta Hernández]

Wait, what?

[Violeta Hernández]

...yeah, it's computable alright

[Violeta Hernández]

Does that mean there are no drawbacks to this new design?

[Robin Arnez]

Yeah, I believe so

[Robin Arnez]

or well, I don't know whether there's any other reason to use PSet other than computability

[Violeta Hernández]

I think @Mario Carneiro is the person to ask here

[Mario Carneiro]

I don't think this has anything to do with computability. You can define any inductive using QPFs, that doesn't mean it is a good idea

[Aaron Liu]

the advantage is you don't need PSet

[Dexin Zhang]

Is QPF approach essentially different from existing approach? I feel it's not, QPF.Fix expands to W quotient by equality under the functor, which seems to be the same as PSet quotient by extensional equality.

[Aaron Liu]

the advantage is that PSet is never added to the environment and you never have to write lemmas about it

[Dexin Zhang]

Oh I see

[Dexin Zhang]

But if things in ZFSet can be defined via QPF infrastructure without explicit constructions on W types, I guess we can make the same thing to define ZFSet without explicit constructions on PSet?

[Dexin Zhang]

I mean we can define

noncomputable def ZFSet.ofSet (s : Set ZFSet.{u}) [Small.{u} s] : ZFSet.{u} :=
  Quotient.mk' ⟨Shrink s, Quotient.out ∘ Subtype.val ∘ (equivShrink s).symm⟩

and play with it instead of PSet, which is the same approach if you use QPF

[Dexin Zhang]

Oh, we already have docs#ZFSet.toSet_equiv

[Violeta Hernández]

We could in current Mathlib deprecate the vast majority of the PSet API and just leave the minimum necessary to define ZFSet, but that would still be around 100 lines of code or so. The QPF approach means we can remove PSet entirely.

[Violeta Hernández]

Mario Carneiro said:

I don't think this has anything to do with computability. You can define any inductive using QPFs, that doesn't mean it is a good idea

I do think computability is relevant to this discussion, because some of the API is built to explicitly take it into account. This is most visible in docs#ZFSet.Definable, which defines a definable function on ZFSet as one you can lift from PSet into ZFSet, and uses that to make other operations such as docs#ZFSet.image computable.

[Violeta Hernández]

Actually that's worth pointing out, because removing PSet would also imply removing this.

[Violeta Hernández]

Violeta Hernández said:

...yeah, it's computable alright

We briefly discussed the ramifications of this over at #combinatorial-games > Computability, and to quickly summarize things:

Aaron Liu said:

yeah this does nothing for us

Maybe I was mistaken in the assumption that docs#ZFSet.Definable was made for computability purposes. Is there some other reason behind it? And does that reason require PSet to exist?

[Mario Carneiro]

Violeta Hernández said:

Mario Carneiro said:

I don't think this has anything to do with computability. You can define any inductive using QPFs, that doesn't mean it is a good idea

I do think computability is relevant to this discussion, because some of the API is built to explicitly take it into account. This is most visible in docs#ZFSet.Definable, which defines a definable function on ZFSet as one you can lift from PSet into ZFSet, and uses that to make other operations such as docs#ZFSet.image computable.

As the person who wrote the code, I'm telling you that computability was never a concern; it doesn't even make much sense since ZFC is not a computational theory. Rather, the concern was attempting to avoid the axiom of choice to prove everything except for ZFC choice

[Kevin Buzzard]

Oh wow, good luck with that in Lean 4

[Violeta Hernández]

Ah, so I did misunderstand.

[Violeta Hernández]

I'm curious to look at the code as it exists right now and figure out if that goal was actually achieved

[Violeta Hernández]

Otherwise, things would certainly be made much easier by removing PSet and removing Definable

[Mario Carneiro]

Violeta Hernández said:

I'm curious to look at the code as it exists right now and figure out if that goal was actually achieved

I think that's a bit off; it was achieved, and it has most likely been subsequently unachieved

[Mario Carneiro]

and I'm not sure the best response to this is to regress it even further