Can ZFC model restricted Lean?

Stream: Type theory

[Mirek Olšák]

I thought this could be well-known among type theorists. I have two restrictions in mind

1. No inductive types & no choice (not even unique choice)
2. The same as (1) but we allow the inductive type Nat (and recursion on it).
   The question is whether Lean's type theory restricted in such way can be modeled inside ZFC (without inaccessibles).

Intuitively, well-founded recursion and unique choice are the constructs that allow building crazily large objects, so I wonder if without them we cannot get too high, and actually don't need inaccessibles, or if more levels of the universe hierarchy can somehow compensate for the restrictions.

To my knowledge, @Mario Carneiro formalized ZFC in Lean without much inductives but choice was fundamental there, right?

[Mario Carneiro]

This sounds like MLTT, which is known to be interpretable inside second order arithmetic. See: #maths > Consistency strength bounds from Lean proofs @ 💬

[Mario Carneiro]

actually you may need to ban Prop as well (i.e. impredicativity) to get the usual MLTT

[Mirek Olšák]

MLTT sounds like a good start but I was imagining if there was some way to model it with "bounded" functions (where I don't know how to define boundedness well). Intuitively, it should be fine to add almost all the classical features such as impredicativity, excluded middle, decidability, quotients, perhaps even a Quotient.choice. Only I don't want to allow functions to grow too fast. Of course, unique choice must be forbidden for that reason (because it can find something extremely large only because it exists).

[Mario Carneiro]

I don't think lean allows you to build fast growing functions through unique choice

[Mario Carneiro]

the only functions you can prove exist this way you can already construct directly AFAIK

[Mirek Olšák]

Unique choice with Quotient allows you to build ordinals, no?

[Mirek Olšák]

I agree that without Quotient, you cannot select the specific big type.

[Aaron Liu]

without inductive types I don't think you can build very big ordinals

[Mario Carneiro]

quotients don't let you do anything new either, you just work with setoids instead

[Mirek Olšák]

I can define well founded recursion using unique choice without inductives.

[Mirek Olšák]

that is the standard ZFC way

[Mario Carneiro]

in a world without prop, well founded recursion is tautological

[Mario Carneiro]

since recursion is what it means for a type to be inductive

[Mario Carneiro]

Mirek Olšák said:

I can define well founded recursion using unique choice without inductives.

that's how it's done in my ZFC without inductives thing

[Mario Carneiro]

I think you might be right, you basically don't have any kind of induction so you can bound type sizes as one does in HOL

[Mario Carneiro]

and even if you have Nat you can still bound type sizes under $\aleph_1$ iterations

[Mirek Olšák]

Yes, that is my intuition but I am not sure how to prove it.

[Mario Carneiro]

if you don't have well founded recursion you don't get to turn a large universe into a tall ordinal hierarchy, so it just becomes a matter of bounding ranks and determining what $V_\lambda$ we are looking at

[Mario Carneiro]

One universe bounding argument which is similar to HOL's but deals with dependent types is the one for PVS

[Mirek Olšák]

do you have a link?

[Mario Carneiro]

https://pvs.csl.sri.com/doc/semantics.pdf

[Mario Carneiro]

the relevant stuff is on page 34-37

[James E Hanson]

Mario Carneiro said:

that's how it's done in my ZFC without inductives thing

Where is this, by the way?

[Mirek Olšák]

Mario Carneiro said:

https://pvs.csl.sri.com/doc/semantics.pdf

It seems to me that PVS doesn't have universes, without them, it is relatively straightforward. I mostly struggle to define what functions in a higher universes to allow. For example, I cannot allow Type -> Type to contain all mathematical functions because then I could use that to define a cofinal sequence Nat -> Type...

[Mario Carneiro]

James E Hanson said:

Mario Carneiro said:

that's how it's done in my ZFC without inductives thing

Where is this, by the way?

https://github.com/leanprover-community/mathlib4/blob/zfc_without_inductives/Counterexamples/ZFCWithoutInductives.lean

[Mario Carneiro]

Mirek Olšák said:

Mario Carneiro said:

https://pvs.csl.sri.com/doc/semantics.pdf

It seems to me that PVS doesn't have universes, without them, it is relatively straightforward. I mostly struggle to define what functions in a higher universes to allow. For example, I cannot allow Type -> Type to contain all mathematical functions because then I could use that to define a cofinal sequence Nat -> Type...

Not sure I follow this. The basic pattern is that these types consist of large sets of small rank, like the low levels of the beth hierarchy. The point is that it doesn't matter if you can construct cofinal sequences because there is no union-like operator, everything you construct is uniformly bounded

[Mario Carneiro]

The easy solution for Type is to just say that universe-making is an operator which bumps the cofinality and don't worry too much about it. So you get something like $V_\omega$ or $V_{\omega_1}$ for everything except universes and then you just get a cardinal $\mathrm{cf}(\lambda)=|V_{\omega_1}|$ as a bound on the rank of the next layer building up to Type 1 (and then you stack another $\omega_\lambda$ layers of pis and such on top on your way to Type 2), and so on.

[Mario Carneiro]

that's probably overkill and you can get away with less if you have Type -> Type functions be some kind of uniformly bounded function type

[Bas Spitters]

There's this work by Bruno Barras: https://jfr.unibo.it/article/download/1695/1316
I recall follow-up work, but I currently cannot find it.

[Mirek Olšák]

Mario Carneiro said:

Not sure I follow this. The basic pattern is that these types consist of large sets of small rank, like the low levels of the beth hierarchy. The point is that it doesn't matter if you can construct cofinal sequences because there is no union-like operator, everything you construct is uniformly bounded

I just think it is not that simple (and was arguing about it with chatbots for a while). Even if we model Type with $V_{\omega_1}$, there is a set $X$ of cardinality at least $\omega_1$ there. So in case my model has a function $f : X \to V_{\omega_1}$ covering all the $V_\alpha$ for $\alpha < \omega_1$, I have a problem, because I should at least allow a forall type ∀ x : X, f x, which I cannot model.

Sure, so this $f$ cannot be in the model of X → Type, we have a boundedness condition that we only allow the functions X → Type which are set-theoretically inside $V_{\omega_1}$. But which objects of Type 1 should we allow? In particular, consider the following set-theoretical function $g : V_{\omega_1} \to V_{\omega_1}$, take $x \in V_{\omega_1}$, if $x \in X$, return $f(x)$, otherwise return $x$. If we allow $g$ to be in my model of functions g : Type → Type : Type 1, I have a problem, because I can have a function emb : X → Type which is modeled just by a set-theoretical inclusion, and should be safely inside the model, and can obtain back the problematic f := g ∘ emb : X → Type. Sure, the function $g$ is a bit crazy, and should not be allowed but I don't see a good general rule for constructing Pi objects of Type 1.

[Mirek Olšák]

For example, for functions Type → Type it is still doable, there I consider only such functions $f$, so that there exists a function $\varphi : \omega_1 \to \omega_1$ such that for every $\alpha\in\omega_1$, and $x \in V_{\omega_1}$, if ${\rm rank}(x) < \alpha$, then ${\rm rank}f(x) < \varphi(\alpha)$. I have some ideas how to continue but it is unclear if it can generally work.

[Mario Carneiro]

I'm currently reading Luo's thesis on ECC and I think chapter 7 has what you want

[Mario Carneiro]

Oh, never mind, chapter 7 uses inaccessible cardinals in the end and the extra realizers are just used to provide a computational interpretation. I think the reason it is cited in Barras (referenced by Bas above) is because of chapter 6, which is a fully syntactic proof of consistency based on strong normalization. You can use that to construct a model but it won't have "the obvious" semantics for function types

[Mirek Olšák]

Actually, I think you are right that just some HOL-like hierarchy can do this, so without recursion, it could fit inside $V_{\omage\cdot\omega}$. Only the higher universe I take, the more complex information I need to keep it all bounded. The type that could store how an element on universe level u at the l-th level of building HOL-functions can be bounded could be Limit u l defined by

def Limit : Nat → Nat → Type
| 0, 0 => Nat
| u, l+1 => Limit u l × (Limit u l → Limit u l)
| u+1, 0 => Limit u 0 × (Σ l, Limit u l)

[Mirek Olšák]

Which is interestingly almost the same as defining the STT hierarchy on its own, just shifted by one universe...

[Mirek Olšák]

Perhaps something along those lines. I imagine building a model out of all the Bounded Hierarchys.

def Hierarchy (u : Nat) (l : Nat) : Type := match u with
| 0 => Unit
| u+1 => aux (Σ l, Hierarchy u l) l
  where aux (start : Type) : Nat → Type
  | 0 => start
  | l+1 => aux start l → aux start l

def Hierarchy.toFun {u l : Nat} (x : Hierarchy (u+1) (l+1)) : Hierarchy (u+1) l → Hierarchy (u+1) l := x
def Hierarchy.ofFun {u l : Nat} (f : Hierarchy (u+1) l → Hierarchy (u+1) l) : Hierarchy (u+1) (l+1) := f

def Hierarchy.liftLev1 {u l : Nat} (x : Hierarchy (u+1) l) : Hierarchy (u+1) (l+1) := fun _ ↦ x
def Hierarchy.liftLevel {u l1 l2 : Nat} (x : Hierarchy (u+1) l1) (h : l1 ≤ l2) : Hierarchy (u+1) l2 :=
  if eq : l1 = l2 then eq ▸ x
  else
    match l2 with
    | 0 => False.elim (by omega)
    | l2+1 => (x.liftLevel (l2 := l2) (by omega)).liftLev1

def Hierarchy.bounds {u l : Nat} (bound : Hierarchy u l) (f : Hierarchy (u+1) l) : Prop
  := match u, l with
  | 0, _ => True
  | u+1, l+1 =>
    ∀ (xb : Hierarchy (u+1) l) (xf : Hierarchy (u+2) l),
      xb.bounds xf → (bound.toFun xb).bounds (f.toFun xf)
  | u+1, 0 =>
    ∃ (h : f.1 ≤ bound.1), bound.2.bounds (f.2.liftLevel h)

def Hierarchy.Bounded {u l : Nat} (x : Hierarchy u l) := match u with
| 0 => True
| u+1 => ∃ bound : Hierarchy u l, bound.bounds x ∧
          bound.Bounded -- not sure if condition is necessary...

[Mario Carneiro]

I think the base of your hierarchy needs to be something other than Unit or else the whole hierarchy is unit types

[Mario Carneiro]

but I'm not sure how you are solving the dependent types problem

[Mirek Olšák]

The base should not matter too much, I insert natural numbers with the Sigma type.

[Mario Carneiro]

is the idea that each type is a subset of one of the hierarchy types?

[Mario Carneiro]

the base of the hierarchy needs to cover all of your constant types, as well as Prop

[Mario Carneiro]

I think the hierarchy step function needs to be A + (A -> A) rather than just A -> A

[Mirek Olšák]

Well yeah, it could be more convenient to use later, I just wanted to define something simple to start with.

[Mirek Olšák]

My original idea was also to use the A + (A -> A) but then I realized I can do this lift using constant functions.

[Mirek Olšák]

the lift A -> (A -> A)

[Mirek Olšák]

The universe Type u could correspond to {x : Hierarchy (u+2) 0 // x.Bounded}

[Mario Carneiro]

What is the point of Bounded?

[Mirek Olšák]

To restrict the possible functions in higher universes, so that I cannot build a cofinal sequence.

[Mario Carneiro]

do you have an example in mind?

[Mario Carneiro]

I'm trying to unpack the definition

[Mirek Olšák]

The issue I was explaining here: #Type theory > Can ZFC model restricted Lean? @ 💬

[Mario Carneiro]

this seems more syntactic than that

[Mirek Olšák]

The idea is: I don't want to allow all functions Type -> Type.

[Mirek Olšák]

so for every function f : Type -> Type, I need a function bound : Nat -> Nat

[Mario Carneiro]

but bound isn't a Nat -> Nat, it's a Type u-1 -> Type u-1 IIUC

[Mirek Olšák]

well yes, it gets more complicated in higher universes :sweat_smile:

[Mario Carneiro]

okay so your case is for u=0?

[Mirek Olšák]

Otherwise, this hierarchy starts with Unit, Nat, and then something rich.

[Mario Carneiro]

Oh no, for u=0 Bounded is trivial

[Mario Carneiro]

so you allow Type -> Type to contain everything

[Mario Carneiro]

but only restrict it when used as an element of Type 1?

[Mirek Olšák]

The start is a bit random, I imagine Type to be Hierarchy 2 0

[Mirek Olšák]

Hierarchy 0 0 is just dummy Unit, Hierarchy 1 0 is Nat

[Mario Carneiro]

okay so you want x : Hierarchy 2 0 which is bounded by some bound : (Hierarchy 1 0 := Nat)

[Mario Carneiro]

Unraveling the definition of bounds I don't see why it's not just trivially true in this case

[Mario Carneiro]

maybe it is?

[Mirek Olšák]

Every x : Hierarchy 2 0 is still trivially Bounded by something but the bound is not constant.

[Mirek Olšák]

So not every function f : Hierarchy 2 1 is Bounded.

[Mirek Olšák]

I will write you an example of unbounded function

[Mario Carneiro]

so this is a function Hierarchy 2 0 -> Hierarchy 2 0, the identity function is presumably not bounded

[Mirek Olšák]

Identity should be bounded by identity

[Mario Carneiro]

oh because the bound is Hierarchy 1 1

[Mario Carneiro]

why is the bound not Hierarchy 1 0?

[Mirek Olšák]

The idea is that it must be bounded by an "approximation" Nat -> Nat

[Mirek Olšák]

Because the identity function should exist in my type system

[Mirek Olšák]

This should be an unbounded example

-- not a relevant definition, just something of that type
def something {l : Nat} : Hierarchy 1 l := (id ⟨0, ()⟩ : Hierarchy 1 0).liftLevel (Nat.zero_le l)

def unboundedExample : Hierarchy 2 1 := .ofFun fun x =>
  let ⟨l, x1⟩ := x
  match l with
  | 0 => ⟨x1.1, something⟩
  | _+1 => x

But it is true that I haven't thought much yet how to represent sets...

[Mirek Olšák]

The idea is that it takes the bottom level of Hierarchy 2 0, and maps it to a sequence spanning all the levels.

[Mario Carneiro]

theorem unbounded (bound : Hierarchy 1 1) : ¬ bound.bounds unboundedExample := by
  open Hierarchy in
  intro H
  unfold bounds at H
  replace H n := H ⟨0, ()⟩ ⟨0, n, ()⟩ <| by simp [bounds]
  simp [unboundedExample, bounds, Hierarchy.ofFun, Hierarchy.toFun] at H
  exact Nat.not_succ_le_self _ (H ((bound ⟨0, ()⟩).1 + 1))

[Mirek Olšák]

I am now more mathematically hopeful that the answer is positive, and it is possible to limit growth rate of the functions. I think it is possible within ZFC to model Lean with predicativity, Quotient.choice, Classical.em but without unique choice, and with limiting recursors with a particular fixed cardinality.

But I would like to be sure by implementing it in Lean.

What approach would you suggest? Implementing full Lean seems a little too complicated (let, projections, various reductions). Is there some simpler axiom list that I could implement of equal strength as Lean?

[James E Hanson]

Mirek Olšák said:

Is there some simpler axiom list that I could implement of equal strength as Lean?

Section 5 of Mario's thesis talks about a reduction of Lean 3 to a simpler type theory. Essentially the same ideas should work for Lean 4.

[Jason Rute]

@Mirek Olšák I think this is an open question, see https://proofassistants.stackexchange.com/questions/4532/does-cic%cf%89-prove-conzf and the other questions it links to (although I think one has to read the details to get to your question). Also see this tweet of @Elliot Glazer, which I think is directly the exact question you are asking about.

[Jason Rute]

Reading the relevant papers, it looks like the expectation is ZF should be able to consistency and strong normalizability of CIC (even with universes), by some sort of generalization of the strong normalization proof for CC_{\omega}, but there’s a lot of technical hurdles.

[Jason Rute]

(I also didn't read all the above. I might just be repeating what you already know.) (Edit: I think my answer is just noise. Sorry!)

[Mirek Olšák]

Jason Rute said:

Mirek Olšák I think this is an open question, see https://proofassistants.stackexchange.com/questions/4532/does-cic%cf%89-prove-conzf and the other questions it links to (although I think one has to read the details to get to your question). Also see this tweet of Elliot Glazer, which I think is directly the exact question you are asking about.

Thanks, something similar was indeed discussed but I don't think it is exactly my question. I would like to have a model closer to classical logic -- impredicativity (I am not sure what exactly it is), excluded middle, even Quotient.choice. My idea to avoid inaccessibles was to limit the growth rate of available functions.

[Elliot Glazer]

@Mirek Olšák So to be clear, "restricted Lean" doesn't just mean "Lean without the 3 standard axioms" but some more thoroughly adjusted entity?

[Mirek Olšák]

Well, Lean does not have "unique choice" as an axiom, so you cannot remove it directly. The way you could do that is by separating it from Quotient.choice (instead of both Quotient.choice & "unique choice" being a consequence of Classical.choice).

[Mirek Olšák]

And I would indeed like to preserve some degree of structure manipulation, such as a non-recursive match. I am aware that forbidding any recursion breaks many basic things such as equality, etc. That's why I suggested keeping recursion on natural numbers in my second point.

[Mirek Olšák]

In short. I am indeed not asking about Lean's type theory without Quot.sound, propext & Classical.choice

[Mirek Olšák]

On the other hand, I am starting to suspect it is an original question by how far it is from the mainstream study...

Type theorists are like: "Why do you want to include so many (from type-theory perspective) weird axioms, and break something as basic as structural recursion? Should it still be called type theory?"

Set theorists are like: "What do you mean by not having unique choice? It holds trivially from the definition of a function..."

[James E Hanson]

Mirek Olšák said:

Set theorists are like: "What do you mean by not having unique choice? It holds trivially from the definition of a function..."

I feel like this opinion is not unique to set theorists.

[Cody Roux]

It's also not not unique to set theorists. ;)

[James E Hanson]

I didn't really mean this comment as a joke. I've talked to mathematicians about unique choice before and they tend to find the idea of not being able to specify a function by proving that its output value is uniquely defined by some property extremely strange.

[Cody Roux]

Mathematicians think not having choice is weird as well, tbh

[James E Hanson]

Sure, but I think it's reasonable to say that they find this strange in an even more fundamental way.

[James E Hanson]

And outside of the context of type theory the idea of unique choice being a 'choice principle' seems extremely strange too.

[Mario Carneiro]

I'm not entirely sure about that. Back in Euler's day the concept of a function was more like the type theory notion, it was Dedekind who popularized the ZFC style definition

[James E Hanson]

We aren't currently in Euler's day.

[Mario Carneiro]

but I think that gives evidence that this is ultimately a set theory derived intuition

[James E Hanson]

Even if it is, that doesn't actually contradict my point.

[James E Hanson]

The opinion is not unique to set theorists, even if it might come from set theory in some sense.

[Mario Carneiro]

you can of course have both kinds of function in type theory, it just makes the distinction

[James E Hanson]

Sure, but I'm saying that this distinction is something that a typical modern mathematician would find very strange.

[Mario Carneiro]

I'm pretty convinced that this is a learned intuition

[Mario Carneiro]

but sure, modern mathematics is built on something foundationally resembling ZFC

[James E Hanson]

Again, that doesn't contradict what I'm saying. Nothing about mathematical intuition being learned or cultural contradicts the fact that this is the way that it commonly is right now.

[Mario Carneiro]

I don't think anyone disputes that

[James E Hanson]

This is a minor point, but the kind of distinction between 'first-class functions' and 'merely definable' functions also exists in certain set theories with restricted comprehension, like $\mathsf{KP}$, so I wouldn't even say it's a uniquely set-theoretic intuition.

[Jason Rute]

I’ve always found it sort of amazing that unique choice holds in cubical type theory without breaking computability.

[François G. Dorais]

This may have come up, I didn't have time to read the full thread. @Robin Arnez has achieved an interpretation of Z in Lean with zero axioms! This combines PER models with Gödel-Gentzen style negative interpretation. It's actually done in the opposite way I would expect but it seems to work really well! They claim they can get to ZF with no axioms. I personally don't think this is possible but I would also be very happy to be proven wrong.

https://github.com/Rob23oba/lean4-no-axioms

[Cody Roux]

I remember Alexandre Miquel building a realizability model for ZF (with some work) so I wouldn't be shocked.

[James E Hanson]

Jason Rute said:

I’ve always found it sort of amazing that unique choice holds in cubical type theory without breaking computability.

I don't really find this that surprising given that it was already known unique choice can be given a computational interpretation in things like $\mathsf{CZF}$.

[Elliot Glazer]

François G. Dorais said:

This may have come up, I didn't have time to read the full thread. Robin Arnez has achieved an interpretation of Z in Lean with zero axioms! This combines PER models with Gödel-Gentzen style negative interpretation. It's actually done in the opposite way I would expect but it seems to work really well! They claim they can get to ZF with no axioms. I personally don't think this is possible but I would also be very happy to be proven wrong.

https://github.com/Rob23oba/lean4-no-axioms

I would find this a bit surprising. In Bruno Barras' habilitation thesis, page 135, he bounds the consistency strength of CIC below IZF_R + universes, which is conjectured to be below ZF in consistency strength (note this has been open since the 70s). He achieves an interpretation of ZF in CIC + TTColl, a type theoretic collection axiom he formulated. @Robin Arnez does Lean have a feature which behaves analogously to TTColl?

[Robin Arnez]

To be honest, I originally thought you could model ZF with no axioms but then I realized the axiom of replacement existed. So the construction I was working with does definitely require another axiom, some form of choice or something like TTRepl or TTColl without which you only have "weak" replacement in the form of an image with a function ZFSet → ZFSet (or to be precise ZFSet ~> ZFSet as the type of congruent functions, since I can't use quotients).

[Mario Carneiro]

A while ago I convinced myself that every ZFC definable function is the image of a ZFSet -> ZFSet function and you can prove this by induction on the formula. That's the origin of docs#ZFSet.Definable