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))