Possible refactor from Type* to Type?

Stream: Equational

[Terence Tao]

@Daniel Weber is reporting some issues with converting between laws and equations at equational#147 due to the inability to define G ⊨ law if G is Type* rather than Type. I had thought that equational#186 would fix the issue, but apparently this is insufficient. (Edit: and now @Cody Roux has thrown in the towel on equational#186, so maybe unrestricted universes are not the way to go here.)

I am not well versed in the finer subtleties of Lean's type theory, so I am not sure how serious this issue is. One possible way out is to refactor the entire project to only consider Magmas in Type rather than in Type*. This could potentially lead to a slight loss of expressivity in our results, but perhaps some version of equational#168 is still possible that would recover that. But now that we have a large amount of both human-generated and computer-generated Lean code, this could be a non-trivial refactor.

I am not sure how to proceed here. Any thoughts would be appreciated.

[Cody Roux]

I can give it another shot, my tentative feeling is that either everything should be Type* + Prop or everything should be Type; the "half and half" seems to require some subtle casts which I do not know how to express (I know nothing of polymorphism in Lean).

I can try to do the former.

[Daniel Weber]

I also agree with the former, except for non implications, which I think should be exists (G : Type) [Magma G], ... (or potentially allowing for a fixed universe for G)

[Shreyas Srinivas]

@loogle ULift

[loogle]

:search: ULift, ULift.down, and 576 more

[Cody Roux]

Thanks!

[Eric Wieser]

Daniel Weber said:

except for non implications, which I think should be exists (G : Type) [Magma G], ... (or potentially allowing for a fixed universe for G)

In counterexamples I guess the question is whether you want to exhibit a counterexample in every universe, or in any universe.

[Cody Roux]

The latter, typically

[Kevin Buzzard]

I don't really see what universes are buying this project; I read the claim that it could in theory be the case that some random large category could be a counterexample but I'll believe it when I see it! If they're causing trouble then why not just retreat to Type? This is where mathematicians typically work.

[Mario Carneiro]

I'm pretty sure it's possible to prove that every counterexample is at most countable and therefore no smallest counterexample can live in a larger universe

[Terence Tao]

Yes, the problem here is more technical and Lean-specific than mathematical... we're having some problems actually formalizing in Lean a proof of this assertion, even though it should just be a consequence of standard logical theorems such as the completeness or compactness theorem (or the Lowenheim-Skolem theorem).

[Mario Carneiro]

if you want to construct a counterexample to A -> B, you can construct a free magma quotient by A and if it satisfies B also then A -> B is true in every magma, and if it doesn't then it's a countable counterexample

[Terence Tao]

Though there may be some subtleties about what "countable" means in different universes

[Mario Carneiro]

no, countability is absolute I think?

[Mario Carneiro]

certainly in lean they are provably equivalent

[Terence Tao]

Yeah I do feel that these assertions are provable in Lean, but it needs someone who really understands Lean's universe type system to actually work out the details.

[Mario Carneiro]

Is there a general definition of what the class of equational theories in question is?

[Mario Carneiro]

you should be able to formalize everything I just said above in lean if you have that

[Mario Carneiro]

in any case, if you construct proofs and counterexamples in Type for every entry in your table, then you've sort of answered this question too without needing to address it explicitly

[Mario Carneiro]

I would be interested to know if there are any cases of A -> B failing where the smallest counterexample is infinite

[Mario Carneiro]

are there any infinite counterexamples being used in the project currently?

[Zoltan A. Kocsis (Z.A.K.)]

I would be interested to know if there are any cases of A -> B failing where the smallest counterexample is infinite

Yes, there are already proofs about the unavoidability of such examples for certain pairs of eqns. I think proved by @Daniel Weber ?

[Terence Tao]

We have a MagmaLaw object which encodes a syntactic assertion LawX (it's a pair of elements from FreeMagma Nat). We also have an operation G ⊧ E for when a (G: Type) [Magma G] obeys E: MagmaLaw, with a completeness theorem for this operation, but we don't currently have the same operation for (G: Type*) [Magma G], with the corresponding completeness theorem in an unspecified universe. Perhaps if we had both completeness theorems linking completeness to an absolute syntactic assertion then we would not have any issue.

[Shreyas Srinivas]

@Mario Carneiro I'll give you a quick file overview

[Shreyas Srinivas]

1. Starting point: We define a free magma here
2. Magma Equations are defined here: https://github.com/teorth/equational_theories/blob/main/equational_theories/MagmaLaw.lean
   (Side note: I'll remove that toplevel hygiene option in a PR quickly now)
   This contains our derivation rules

[Shreyas Srinivas]

3. The magma operation is given semantics here: https://github.com/teorth/equational_theories/blob/main/equational_theories/MagmaOp.lean

[Mario Carneiro]

Terence Tao said:

We have a MagmaLaw object which encodes a syntactic assertion LawX (it's a pair of elements from FreeMagma Nat). We also have an operation G ⊧ E for when a (G: Type) [Magma G] obeys E: MagmaLaw, with a completeness theorem for this operation, but we don't currently have the same operation for (G: Type*) [Magma G], with the corresponding completeness theorem in an unspecified universe. Perhaps if we had both completeness theorems linking completeness to an absolute syntactic assertion then we would not have any issue.

Yes, that sounds about right. You should be able to prove the exact same completeness theorem in an arbitrary universe, and because the conclusion is something in Type 0 this tells you that they all have the same implication graph

[Shreyas Srinivas]

Then we have soundness and completeness proofs here: https://github.com/teorth/equational_theories/blob/main/equational_theories/Completeness.lean

[Shreyas Srinivas]

The current version of compactness is here: https://github.com/teorth/equational_theories/blob/main/equational_theories/Compactness.lean

[Terence Tao]

I agree it does sound doable, the main issue is technical (and not getting trapped in some weird "universe hell").

[Mario Carneiro]

that does exist, but you are not likely to encounter it in this project

[Mario Carneiro]

I don't have any spare time to allocate, but if I get the chance I will see if I can audit the project and make sure the universes aren't an issue

[Cody Roux]

Basically the idea is that one may define satisfaction "generically" over a universe:

def satisfies {α : Type*} (G : Type*) [Magma G] (E : MagmaLaw α) := ∀ (φ : α → G), satisfiesPhi φ E

This is the "natural" notion: we have no idea where such a G might live! So one can "just" prove that this is equivalent to

def satisfies {α : Type*} (G : Type) [Magma G] (E : MagmaLaw α) := ∀ (φ : α → G), satisfiesPhi φ E

But this is both hard to state and to prove, I think.

Here's a branch, where Preorder.lean fails. Happy to know how to fix it. https://github.com/codyroux/equational_theories/tree/universes

[Mario Carneiro]

I think you want to universally quantify over G there

[Mario Carneiro]

otherwise the two satisfies relations can only be compared over the same G and at that point it's obviously true

[Cody Roux]

That's the next definition in MagmaLaw.lean

[Cody Roux]

fair

[Cody Roux]

at some point one has to cast explicitly, I'm sure

[Terence Tao]

If one can prove soundness in arbitrary universes, completeness in the Type 0 universe, and can cast the satisfies relation from Type 0 to arbitrary Types, this should show everything is equivalent, I think...

[Cody Roux]

Then using the compactness theorem shouldn't be _too_ tough, it just involves collecting all the finite variables and mapping them injectively to, say ℕ, but it's also a bit tedious.

[Cody Roux]

Amusingly there's a proof of cut-elimination that works like this: prove soundness of the system with cut and completeness for the system without cut.

Computational content of the proof left as exercise.

[Mario Carneiro]

I think what you want is something like:

def implies {α : Type*} (E1 E2 : MagmaLaw α) := ∀ (G : Type) [Magma G], E1 |= G -> E2 |= G

and then the theorem is

theorem implies_def {α : Type*} (E1 E2 : MagmaLaw α) :
  implies E1 E2 <-> ∀ (G : Type u) [Magma G], E1 |= G -> E2 |= G

[Cody Roux]

I think I tried something similar and struggled to prove it, but I can give it another whirl tomorrow, unless someone else wants to give it a shot

[Cody Roux]

I wonder if Lowenheim-Skolem is stated inter-universe in Mathlib (I assume it is)

[Mario Carneiro]

The fact that alpha is also universe parametric here complicates things, but you can use compactness to show that it suffices to take alpha = Nat

[Mario Carneiro]

(that is, E1 and E2 have finite support so you can map them to a finite set of generators)

[Terence Tao]

It's amusing to see model theory having to come in for a project as concrete as proving (22 million times) that one algebraic identity implies or does not imply another. (I mean, we could finish the project without this, but then we would not be able to do things like automatically invoke duality on implications within Lean, but instead have to do some awful metaprogramming to dualize proofs or something.)

[Shreyas Srinivas]

It is usually simpler to prove a theorem and apply it than generate a proof wholesale from tactics.

[Cody Roux]

It still disturbs me that we spend so little time as humans thinking about this but a lot in ITP. I had hoped that a "sufficiently polymorphic" type theory would save us, but no dice.

[Shreyas Srinivas]

I wonder how Coq's cumulative universes would affect this question.

[Cody Roux]

Meta-theoretically it should be the same (maybe avoid a cast somewhere) I would guess. I've already used choice in the proof of completeness though.

[Terence Tao]

It's surprising to me that choice is needed. Shouldn't there be a canonical model - a free magma quotiented out by syntactic equivalence or something?

[Cody Roux]

Yes, I don't think it's needed, but at some point in the proof I needed to turn an instantiation into the canonical model into a substitution by "lifting". And this is only possible with choice in general.

I didn't think much harder.

[Mario Carneiro]

Cody Roux said:

It still disturbs me that we spend so little time as humans thinking about this but a lot in ITP. I had hoped that a "sufficiently polymorphic" type theory would save us, but no dice.

No, I actually think it is the opposite, allowing universe levels was the original sin, we should have just stuck to ZFC

[Cody Roux]

The "F" is already universes, in a way :)

[Mario Carneiro]

FWIW this stuff never came up when I was working in metamath

[Mario Carneiro]

heck, this whole project can be done in PA with a bit of finagling

[Cody Roux]

It's fair it's fair, but someone, someday is going to want the "magma of Types with products"...

[Mario Carneiro]

but in ZFC you handle that by reinterpreting what Type is instead of reinterpreting the whole rest of the theory to stick astro sets on top

[Terence Tao]

I imagine that once the project is completed, some external tool could deconstruct the Lean proofs and give extremely low-level proofs using essentially no axioms, which could also be exported to other languages than Lean. In particular, any invocation of duality could be replaced by some ad hoc code to dualize the low level proof instead.

[Mario Carneiro]

e.g. you just say "oh and by the way there is an inaccessible cardinal" and you haven't made all of the previous theorems no longer completely general

[Mario Carneiro]

Terence Tao said:

I imagine that once the project is completed, some external tool could deconstruct the Lean proofs and give extremely low-level proofs using essentially no axioms, which could also be exported to other languages than Lean. In particular, any invocation of duality could be replaced by some ad hoc code to dualize the low level proof instead.

I will absolutely attempt to do this at some point

[Mario Carneiro]

I already want to do this for FLT, but this project will be way easier to do reverse mathematics on

[Terence Tao]

I wonder whether FLT will encounter this issue. There was a famous debate some decades ago as to whether Wiles's proof really used Grothendieck's axiom of universes or whether it could be avoided "in principle". Tangential to the current discussion, but I would be curious as to @Kevin Buzzard 's opinion on this.

[Mario Carneiro]

We've had discussions about this. Ideally Kevin won't have to do anything untoward with the proof, this should be a completely automatic affair. In practice it requires solving some tricky theoretical problems in addition to building a tool (the tool already exists, it just doesn't give answers I like)

[Mario Carneiro]

FLT will certainly engage with universes in some ways, but not really in interesting ways that would cause universe hell issues. For that you need to be doing set theory or category theory I think

[Terence Tao]

That sounds plausible to me.

[Mario Carneiro]

My hope is to prove that while it refers to Type as a thing, that thing doesn't actually need to be a full ZFC universe, only an approximation thereof, and ZFC proves the existence of an abundance of approximate universes so you can use that to construct a model to conduct the proof in

[Mario Carneiro]

i.e. it's sort of automating the technique of sticking $\kappa$-small in front of everything

[Terence Tao]

Yeah that roughly tracks with how ultrafilters / choice tends to come up in analysis. In practice there's always some finitary approximate version that's good enough, but the exact quantification of "approximate" depends on how complicated your proof is so it's far more convenient to assume a strong axiom and just use the transfinite object or whatever instead.

[Mario Carneiro]

right, which is why it's a prime target for ITP proofs since you can automate the derivation of what "good enough" means for your proof

[Cody Roux]

Ok, so what should we do pragmatically? I can just search-replace Type* to Type, honestly that might just work, or I can give another shot at making the other direction prove.

[Terence Tao]

It might temporarily disrupt some of the automated proof code to do this refactor to retreat from Type* to Type, but I assume this would all get sorted out relatively quickly. I guess one could always pursue the model theoretic question of establishing soundness in arbitrary universes at a later date. In principle there is a scenario in which the most natural counterexample for an implication turns out to live in a higher universe than Type 0, but I think this is really, really unlikely. (Unless our example somehow relies on FLT :joy: .)

[Mario Carneiro]

reminder that FLT is a statement about natural numbers :wink:

[Terence Tao]

In particular if we do retreat from Type* to Type it's not quite enough to search-and-replace all the human-generated and computer-generated Lean code; we also have to go into some of the scripts that generate the latter and do appropriate search-and-replaces there too, otherwise they will autogenerate back results in the wrong format. But I assume that should be doable, just tedious. I can't imagine that any code will actually break with this edit.

[Mario Carneiro]

My recommendation is to not do that, just keep proofs in Type* and counterexamples inType

[Terence Tao]

But then we can't use duality without a soundness theorem in Type* and a completeness theorem in Type and we only have the latter currently

[Mario Carneiro]

all of the universe handling will focus on a few theorems like completeness, and it will provide an interface most convenient for everything else

[Mario Carneiro]

so just sorry the theorem if you need it for something and set it as an objective for the people who work on this kind of thing

[Terence Tao]

I mean I agree this is the right format for proofs and counterexamples, it's just that we still need a metatheorem that we don't currently have (soundness in Type*).

[Mario Carneiro]

I'm quite sure the theorem is true as long as you can state it in a way that typechecks

[Mario Carneiro]

but I need to sleep now (or rather 4 hours ago), I am sure others can continue this

[Terence Tao]

Maybe @Cody Roux you have another run at this problem but bring any issues you discover to this thread and we can try to problem solve any universe issues that arise?

[Terence Tao]

Some of our counterexample code I think is in Type* instead of Type (e.g., https://github.com/teorth/equational_theories/blob/main/equational_theories/FactsSyntax.lean ). Regardless of what we do, I guess we have to do some refactoring to make this consistent.

I created equational#344 to deal with this refactor (which is separate from the soundness issue, and I think can be handled independently.)

[Cody Roux]

Soundness in Type* is done, no problem, it's the second bit we need.

[Cody Roux]

I'll try to sort it all out tomorrow and advise.

[Daniel Weber]

I was asleep so I couldn't participate in the discussion, but I'm not sure I was clear enough what the problem was:
Suppose we have an implication theorem Equation2_implies_Equation3 (G: Type*) [Magma G] (h: Equation2 G) : Equation3 G. Suppose you then invoke equation_to_law - the natural goal for it to produce is G ⊧ Lf 0 ≃ Lf 0 ⋆ Lf 0. However, this isn't type correct, because satisfies is defined as def satisfies {α : Type} (G : Type) [Magma G] (E : MagmaLaw α)

[Terence Tao]

Is it type correct to also define def satisfies' {α : Type*} (G : Type*) [Magma G] (E : MagmaLaw α) and G ⊧' Lf 0 ≃ Lf 0 ⋆ Lf 0 in the obvious fashion? Then have some soundness theorem that shows that the latter is implied by G ⊧' Lf 0 ≃ Lf 1 and (Lf 0 ≃ Lf 1) ≤ (Lf 0 ≃ Lf 0 * Lf 0)?

[Daniel Weber]

It is, but I think it makes more sense to just modify the existing satisfies - would that cause a problem anywhere?

[Terence Tao]

Well we want our counterexamples to live in Type rather than Type*

[Daniel Weber]

That shouldn't affect it - Type* is a superset of Type, you could still write G ⊧ Lf 0 ≃ Lf 0 ⋆ Lf 0 for G : Type

[Cody Roux]

Note also that the "syntactic model" is also bounded by the universe of the argument to FreeMagma, though I don't think anyone's complained about that one.

[Terence Tao]

Yeah fair enough

[Terence Tao]

I thought we were using FreeMagma Nat for the syntactic model, so always Type 0

[Cody Roux]

@Daniel Weber (modulo some cast, I think)

[Cody Roux]

No it's all parametrized over alpha.

[Terence Tao]

oh but maybe we could force alpha to be Type 0? I see no scenario in which we would need a higher universe of variable symbols

[Daniel Weber]

Terence Tao said:

I thought we were using FreeMagma Nat for the syntactic model, so always Type 0

For equation_to_law, yes, but for law_to_equation it can accept any free magma

[Terence Tao]

In fact it's already rare that we need more than six variables

[Cody Roux]

Sure, of course one may add many many variables if one likes, e.g. to build non-standard models, but all this is theoretical.

[Mario Carneiro]

As I mentioned earlier, given 2 or 4 elements of FreeMagma A representing the equations you want to relate, they can altogether mention only finitely many elements of A, so you can map the question onto Fin n for some n

[Cody Roux]

Yes, I was intending to do that yesterday but ran into universe issues.

[Mario Carneiro]

so you can prove that having a large A gives you no extra power

[Terence Tao]

Well we would need the alphabet in Type if we want a completeness theorem in Type. I hardly think this is a great loss though.

[Cody Roux]

Agreed, will try that as well

[Kevin Buzzard]

The Wiles/Taylor--Wiles proof of FLT can be proved in ZFC, but in practice the most convenient way to prove it is to use a universe and then just ask the logicians to please shoehorn it back into ZFC. For example here is Johan de Jong making some very artificial definitions to demonstrate that in the stacks project whenever he is arguing in a large category (schemes) he could in fact be arguing in a small one (schemes of "size" at some some cardinal whose existence can be proven in ZFC). Similarly here, section 4, is Peter Scholze showing that his work on applications of perfectoid spaces to the Langlands program can all be stuffed into ZFC by using techniques which logicians have figured out over the decades. The trick is always the same -- instead of using a universe just observe that something weaker will do because in practice (eg $V_\kappa$ for $\kappa$ a strong limit cardinal), although the details are tedious (but also well-understood). Of course Grothendieck never did any such thing, he just used universes. My personal interpretation of these results is that ZFC is in some sense unsuitable/inconvenient as a foundation for algebraic geometry if it's forcing people like this to take time explaining how in theory ZFC can be used but in practice they're not going to use it.

[Mario Carneiro]

This is exactly the argument I've used for why we should all just use Type : Type and let "the logicians" figure out how to pick out an actual proof from a proof constructed in these more convenient foundations (because obviously we won't be using those assumptions to prove a contradiction, because that would be rude)

[Mario Carneiro]

Type : Type is obviously the right foundations for category theory

[Mario Carneiro]

and when "mathematicians" go to some effort to avoid using it because it's inconsistent, this is a violation of division of labor since that's "the logician's" job

[Daniel Weber]

After trying for a bit to change it to Type*, I mostly agree. However, perhaps the most basic definitions, e.g. satisfies, should still be universe-general? It's quite annoying to be unable to write G ⊧ Lf 0 ≃ Lf 0 for G : Type*. Although perhaps that just pushes the problem a bit further, as given G ⊧ law1 and implies law1 law2 you couldn't conclude G ⊧ law2 without equational#186 (and implies is ∀ {G : Type} [Magma G], satisfies G l₁ → satisfies G l₂, which can't be made universe general as that requires quantifying over universes)

[Mario Carneiro]

So my claim above is that if you define implies like that (not universe-general), then you can prove that it is equivalent to the same definition over Type u, and you use that equivalence to apply it to general magmas

[Daniel Weber]

I know, that's equational#186

[Mario Carneiro]

can someone point me to the relevant code and/or previous attempts at this?

[Daniel Weber]

I think @Cody Roux attempted something, they might have relevant code

[Cody Roux]

Yep you were already in the conversation @Mario Carneiro :) https://github.com/codyroux/equational_theories/tree/universes

[Cody Roux]

do please ping me if you have a PR that fixes/works towards this.

[Cody Roux]

Nope, stuck again, models is annoyingly non-variant: G appears on the lhs and the rhs of an implies.

[Mario Carneiro]

I'm about 90% of the way through a proof, I worked on this on a plane so I didn't see your post but it looks like my stuff subsumes that

[Mario Carneiro]

in particular, I was able to fairly easily get the completeness theorem to generalize to

theorem Completeness'_0 {α : Type*} {β : Type} (Γ : Ctx α) (E : MagmaLaw β) (h : Γ ⊧ E) : Nonempty (Γ ⊢' E) :=
  FreeMagmaWithLaws.isDerives _ _ (h _ (FreeMagmaWithLaws.isModel _))

and the rest of the work is to generalize beta to higher universes (for which you need the compactness argument I sketched)

[Terence Tao]

I can see that our final paper is going to have a section on universe issues. Hopefully we find some standard solutions that future projects of this type can adopt without having to trek through universe hell.