Theory of Lean with n universes

Stream: Type theory

[Jason Rute]

My question is based on a question on PA.SE. The answer by @François G. Dorais I think isn’t quite right and I wanted to continue the discussion here. The original question by the OP is about whether there is a way to know if a theorem of Lean is true in ZFC. I would like to ask a related question here about what if we restrict the number of universes used in a proof.

[Jason Rute]

I think two simplifying assumptions would help. First, let’s restrict ourselves to statements of first-order arithmetic since that is unambiguous (but still really expressive). If we are doing that then obviously we can’t (easily) know if a theorem is compatible with ZFC by the form of a statement alone, since we can encode statements like Con(ZFC) into arithmetic.

[Jason Rute]

So my second assumption is that I’m talking about restricting universes not in the theorem statements themselves, but in the proofs. I know from another thread (#general > Highest universe in mathlib) that we can count this sort of thing (and no more than something like 4 levels are ever used in Mathlib). Also, I know that Lean’s set-theoretic interpretation (from @Mario Carneiro) is something like each Type u is a Grothendieck universe. So does this mean if we have an arithmetic theorem with a proof that only uses one universe level (which we could measure with a linter or with a command analogous to #print_axioms), then it holds in ZFC plus one inaccessible cardinal?

[Jason Rute]

The tricky bit is formalizing what it means to use one universe level, and I could easily imagine there are a few options. For example, it is not clear how to handle polymorphic types like List: Type u -> Type u when counting universe levels. While List.{0} is in Type 1 it might be that if it is used in a certain syntactic way (like a proper class in set theory), then I wouldn’t necessarily count as a universe bump.

[Jason Rute]

Also, I could imagine an off-by-one error in my estimates where theorems using only one universe level need two inaccessible cardinals or something like that.

[Jason Rute]

But if this does hold, could you formalize what it means to use no universes in a proof? Then would such a theorem hold in ZFC?

[Jason Rute]

Anyway, I’m not sure there are fully worked-out answers here, but is there something to this line of logic, or am I fundamentally confused?

[Mario Carneiro]

I believe you are broadly correct. If a proof is conducted using n universes, then it holds in ZFC with n inaccessible cardinals, up to a bit of fencepost error

[Mario Carneiro]

this is proved in my thesis

[Mario Carneiro]

As you say, there are complications in counting exactly when a universe bump occurs, because when you truncate the theory various type theoretic properties fail to hold like "every type has a type". I believe this is not actually the right way to do the truncation, and I make some intimations in this direction in the thesis: rather than throwing away the higher universes entirely, you use strong limit cardinals instead of inaccessible cardinals for them. These can be proved to exist in ZFC, they just aren't closed under inductive types and Pi types. Lacking Pi types is a bit of a problem though so hopefully there is a better choice of truncation that only lacks inductive types, which I think is quite reasonable to count.

[Kevin Buzzard]

@Mario Carneiro do you remember that code you wrote in Lean 3 which convinced us all that some random statement about the empty set required 5 universes? That discussion convinced me that in practice it might be extremely difficult to convince anyone that a random theorem of mathlib was a theorem of ZFC. I never understood that empty set example.

[Mario Carneiro]

it's linked above

[Mario Carneiro]

Note that that calculation was using a rather naive/obvious definition of universe, which has a drawback that very silly things can bump universes. What i mean by my post just above is that there should be a better way to count universes which gives lower numbers in common cases, ideally 0

[Mario Carneiro]

But it's fair to say that this is in the "open research question" category

[Kevin Buzzard]

Can we get this working in lean 4 so we can get to the bottom of why mathlib needs 5 universes whereas it "clearly all works in ZFC"?

[Mario Carneiro]

I'll put it on my stack of projects :)

[Kevin Buzzard]

I've always wanted to get to the bottom of this!

[François G. Dorais]

The question here is a bit different from the SE question. Still, my argument there is about the impredicativity of Prop and this is relevant here too.

Were there no impredicative Prop, then every Type n would have its own Prop n (as subsingletons, hProps or whatever) and it is true that "provable in ZFC" would amount to "true in Prop 0" (±epsilon). Given a model S of ZFC + there is a 17-correct sequence + there are no 18-correct sequences (n-correctness is defined in Mario's MS thesis, 17 is just to get above Mathlib's experimental limit with room to spare). Using S, I can try to carry out the set-theoretic interpretation from Mario's thesis (ignoring things about Prop but all universes are classical so that doesn't matter). That will get me through to some level, say 8 to leave even more wiggle room, where everything is sound and nice. I can then build a model of Lean with no impredicative Prop using these 8 levels and making all higher universes trivial (i.e. every type is inhabited). This is fine since universes 0-8 are protected from universes 9 and up by a predicativity barrier that prevents things from higher universes to trickle down.

That doesn't work with an impredicative Prop since that forces all universe levels to have the same propositions: if one universe level is trivial then they are all trivial. That is why I answered No on SE. The question posed here is more precise. If you have a proof of an arithmetical statement that doesn't use universes above 8, can that be translated in to a proof in ZFC + there is a 17-correct sequence? Yes, most likely, this is exactly what my hand wavy construction above proves modulo all the nontrivial stuff I swept under the rug. (Note that the construction can be fitted with a Prop which is impredicative up to level 8, which helps with the nontrivial stuff.)

Can Lean actually be used this way? Maybe Mario knows better but I don't think so. I think the kernel has some uses of impredicativity that can't be effectively measured.

[Jason Rute]

@François G. Dorais I have to admit I don’t understand your argument about impredictivity, or even what you are arguing. Are you suggesting that Lean with say 8 universes can prove Con…Con(ZFC) for any number of Con? (I don’t understand n-correctness but I assume it is similar.) If so that seems to violate what @Mario Carneiro said above. Are you saying that impredictivity can somehow be used to do hidden universe jumping which is not easily measured by the kernel.

Or am I still totally misunderstanding you? Honestly I can’t even tell if you disagree with the statement that if one measures at most n universe jumps used in a Lean proof (of say an arithmetic theorem) then that theorem holds in ZFC plus n + k inaccessible cardinals for some constant k. That seems to be what Mario is suggesting.

(I’m also a bit confused by your statements about universes having the same propositions. Prop only has two elements. But that is probably just confusion on my part.)

[Jason Rute]

Our are you saying there is something special about small numbers of universe levels (which show that the constant k has to be greater than 0), so we can’t get exactly ZFC + 0 innaccessibles?

[François G. Dorais]

I think there is some fundamental misunderstanding, I'm not sure how to pinpoint it. In my predicative universes example, universes 9 and up have only one truth value while universes 0-8 have two. This is how inconsistency manifests itself in type theories. Having an impredicative Prop forces all universes to have the same propositions.

[Jason Rute]

Why do you need to consider models where there are trivial universes? They are not models of the fragment of Lean I’m talking about. I’m talking about the fragment of Lean with only n universes (not n nontrivial universes)? I agree having higher universes changes which props are true (just like adding inaccessible cardinals to ZFC changes which theorems of arithmetic are true).

[Jason Rute]

I get the impression that at least in the original question, you were focusing on if there was a way to tell if a theorem was provable in ZFC from the statement of the theorem, and I interpreted the question that you can look at the proof too.

[François G. Dorais]

I agree, if you look at a proof then you can see if it is formalizable in ZFC. This is regularly done with paper proofs, for example. But Lean's type theory has two features: proof irrelevance and impredicative propositions. The first prevents you to equate theorems and proofs, which is fine if you're looking at a specific proof rather than the existence of a proof. The second erases type levels when it comes to propositions: this is significant since the kernel might use a thousand universe levels without telling you about it.

[Jason Rute]

Ok, so you are saying that type checking may hide universe levels, so possibly Mario’s approach to measuring universe levels misses universe bumps which happen during type checking. That is interesting and I am curious if Mario agrees.

[Jason Rute]

(I think we now understand each other more or less.)

[François G. Dorais]

I'm also curious about that. I suspect nothing bad happens out of the box but I'm not sure once you throw in user stuff into the mix.

[François G. Dorais]

The problem with truncating to n universes with an axe is that some terms go untyped. That's why I extended my model with trivial universes. These are fictional type theories anyway so there is no point arguing about fine details. I think my version is basically the same as yours.

[François G. Dorais]

Another thing:

(I’m also a bit confused by your statements about universes having the same propositions. Prop only has two elements. But that is probably just confusion on my part.)

The fact that Prop has only two elements is itself a proposition. There is in fact no such restriction! So long as Prop is a Boolean algebra this is valid. There are plenty of Boolean algebras with more than two elements. Logically this is a non-issue, so long as you have a flexible mindset to allow Boolean valued models or if you believe in ultrafilters.

[Mario Carneiro]

I think the easiest way to conceptualize what it means to truncate the type theory is to say that the kernel will throw an error when it ever sees or attempts to construct Sort n where n > 18. In fact, lean's kernel actually does this (for a larger limit, I think around 2^21), because it's implemented in a computer and there are a finite number of representable universes. Under this constraint, if the kernel typechecks the theorem and proof, then the proof was performed "using only 18 universes", and it will be provable in ZFC with 18 inaccessible cardinals.

[Mario Carneiro]

Whether the statement is arithmetic or not makes no difference here. There are no "multiple Props" in the model I describe; there is one Prop and it has two elements. This is necessary to model impredicative Prop correctly, and even with only 18 universes lean is still impredicative. You can't prove Con(ZFC+20 inaccessibles) in lean with 18 universes, but you can state it.

[Mario Carneiro]

François G. Dorais said:

Another thing:

(I’m also a bit confused by your statements about universes having the same propositions. Prop only has two elements. But that is probably just confusion on my part.)

The fact that Prop has only two elements is itself a proposition. There is in fact no such restriction! So long as Prop is a Boolean algebra this is valid. There are plenty of Boolean algebras with more than two elements. Logically this is a non-issue, so long as you have a flexible mindset to allow Boolean valued models or if you believe in ultrafilters.

No, you can prove in lean that Prop has exactly two elements, so in order to have a more general boolean algebra for Prop you would need equality to mean something other than ZFC equality, and if you do that then defining substitution becomes harder. It may be possible but it significantly changes the character of the theory, to something more like a HoTT model.

[Mario Carneiro]

I've never really given much thought to "predicative Lean" or what properties it has, because the model theory of predicative type theories is quite different and weaker, we probably wouldn't be talking ZFC at all (even with the universes) but rather a subsystem of second order logic.

[François G. Dorais]

Mario Carneiro said:

François G. Dorais said:

Another thing:

(I’m also a bit confused by your statements about universes having the same propositions. Prop only has two elements. But that is probably just confusion on my part.)

The fact that Prop has only two elements is itself a proposition. There is in fact no such restriction! So long as Prop is a Boolean algebra this is valid. There are plenty of Boolean algebras with more than two elements. Logically this is a non-issue, so long as you have a flexible mindset to allow Boolean valued models or if you believe in ultrafilters.

No, you can prove in lean that Prop has exactly two elements, so in order to have a more general boolean algebra for Prop you would need equality to mean something other than ZFC equality, and if you do that then defining substitution becomes harder. It may be possible but it significantly changes the character of the theory, to something more like a HoTT model.

Exactly! Which equality is actual equality in the model. There are several notions of equality in Lean. Syntactic equality is one but it's not part of the internal language. Propositional equality is in the language. Actual equality is not in the language and not expressible in it. So long as I have a model where ∀ (p : Prop), p = True ∨ p = False is True then everything is fine. For example, Lean^2 where two classical Leans are working independently and in parallel from each other is a perfectly fine model of Lean. However, there are actually four truth values in this Boolean valued model.

[Mario Carneiro]

Jason Rute said:

Are you suggesting that Lean with say 8 universes can prove Con…Con(ZFC) for any number of Con? (I don’t understand n-correctness but I assume it is similar.)

n-correctness is just saying that if we have 8 inaccessibles we can put them in a line and then fill in the rest of the line with weak universes which still have the same basic structural properties but aren't full universes closed under all the operation they should be. Existence of an n-correct sequence is equivalent to existence of n inaccessible cardinals over ZFC.

Lean with 8 universes can indeed prove Con...Con(ZFC) but that's because it can construct a model of ZFC. This is true even with only 1 universe, or in ZFC + 1 inaccessible. Iterating Con is a very weak way of growing the consistency strength, adding an inaccessible goes past all of them. But maybe what you wanted to ask, can lean with 8 universes prove Con(ZFC + n inaccessibles) for n > 8? In which case the answer is no, because ZFC with 8 inaccessibles can prove the consistency of lean with 8 universes.

[Mario Carneiro]

@François G. Dorais Yes, you can paste independent models together but then there isn't any equality that corresponds to actual equality in the model. You can also make some elements be doubled in a way that no set picks out. I don't think these are particularly interesting changes to the model though. I think this is a bit different from "there are no restrictions other than Prop being a boolean algebra", because you had to clone all of the rest of the model in parallel to what you did to Prop.

[Mario Carneiro]

Also, for boolean algebras other than 2^A I don't know what you would do to the rest of the model to ensure only the representable elements appear as elements of Prop

[François G. Dorais]

As I said earlier: Logically this is a non-issue, so long as you have a flexible mindset to allow Boolean valued models or if you believe in ultrafilters.

[Mario Carneiro]

I don't believe you, Lean is a type theory not a FOL so you can't just reduce everything to propositions with boolean values. Maybe you can do it but it's not at all obvious and there will be many subtleties

[Mario Carneiro]

The model in my thesis takes as a "simplifying assumption" that equality in ZFC, equality in lean, and defeq in lean are all made equivalent. This model validates the equality reflection rule as a result

[Mario Carneiro]

But my thesis is not really a model theory paper, I did not consider the full spectrum of possible models, only a few models that have useful properties (in particular existence). If you would like to write one I'll be interested to read it

[François G. Dorais]

There is nothing wrong with your thesis! It's a wonderful work! I'm pointing out that the "simplifying assumptions" (your words, I don't think they simplify much!) can be relaxed to reveal more models with interesting properties.

That said, my original comment explores a theoretical version of Lean with no impredicative Prop. I never had any intent to make that version real. Lean is perfectly fine with an impredicative Prop and that is fully compatible with the usual two-valued Prop model that everyone loves.

[Mario Carneiro]

I'm pointing out that the "simplifying assumptions" (your words, I don't think they simplify much!) can be relaxed to reveal more models with interesting properties.

I'm aware of this, I'm saying that this would be another paper entirely and without going to the effort I'm not going to make claims in this area because I'm not sure it's as simple as just replacing 2 by B and getting a BVM out

[François G. Dorais]

I agree. I don't think anyone was pressing you to do this. If anyone appeared to do that, I'm sure it was a misunderstanding or an error of some kind.

[Mario Carneiro]

I'm not saying that either. Until someone (including possibly me) writes that paper and I read it I don't believe blanket claims that you can BVM-ize the model straightforwardly. I do believe it in the case where you just construct Lean^A in the manner you described, this is a weaker statement though

[François G. Dorais]

Sorry, what does BVM-ize mean?

[Mario Carneiro]

make a boolean valued model from a classical model construction

[François G. Dorais]

Ah! That's not what I tried to say. I pointed out that Lean naturally allows some Boolean valued models, not the other way around.

[François G. Dorais]

I have no idea what the spectrum of Lean models actually is.

[Mario Carneiro]

me neither, hence the skepticism

[François G. Dorais]

I think we're in agreement. Sorry for the confusion.

[Mario Carneiro]

but maybe this is getting off topic of Jason's original question. I would be interested to know your answers to Jason's questions to you above, to the extent they apply to (impredicative) Lean

[François G. Dorais]

Which questions specifically? It's getting a bit late and I'm losing track of this long thread. I'm always happy to clarify and answer questions.

[Mario Carneiro]

François G. Dorais said:

The question posed here is more precise. If you have a proof of an arithmetical statement that doesn't use universes above 8, can that be translated in to a proof in ZFC + there is a 17-correct sequence? Yes, most likely, this is exactly what my hand wavy construction above proves modulo all the nontrivial stuff I swept under the rug. (Note that the construction can be fitted with a Prop which is impredicative up to level 8, which helps with the nontrivial stuff.)

Can Lean actually be used this way? Maybe Mario knows better but I don't think so. I think the kernel has some uses of impredicativity that can't be effectively measured.

What aspect of this are you unsure about? We are not "measuring impredicativity" in any sense, and the stuff about predicative universes (edited out since it is mostly irrelevant to impredicative lean) doesn't clarify this point.

François G. Dorais said:

I agree, if you look at a proof then you can see if it is formalizable in ZFC. This is regularly done with paper proofs, for example. But Lean's type theory has two features: proof irrelevance and impredicative propositions. The first prevents you to equate theorems and proofs, which is fine if you're looking at a specific proof rather than the existence of a proof. The second erases type levels when it comes to propositions: this is significant since the kernel might use a thousand universe levels without telling you about it.

How might "the kernel might use a thousand universe levels without telling you about it"?

[Mario Carneiro]

To be clear, when I talk about a "proof" in lean (in this context, at least) I don't mean the inhabitant of a proposition, I mean the full typing derivation that the expression has the stated type. This is mostly just a copy of the input expression, but it differs when defeq conversion is triggered. Use of higher universes anywhere in a typing derivation "counts" against it being a proof in Lean with n universes.

[François G. Dorais]

The "to be clear" part really clarifies the discrepancy.

I'm not thinking syntactically. It's pretty clear that (but not at all easy how) one could translate a Lean proof into a ZFC proof, or fail and perhaps explain why.

I'm thinking semantically. There is no internal way to distinguish whether a statement requires level 1000 or not. For example, Con(ZFC) is provable in Lean. This is an arithmetical statement which doesn't require more than Type 0 to state. Because Type 1 exists and there is a model of ZFC in Type 1, that arithmetical statement is true. Because Prop is impredicative, this statement is true at all levels of the hierarchy. Impredicativity of Prop not only requires that all levels have the same Prop but also that the interpretations match. So Con(ZFC) is necessarily true in Type 0 and there must therefore be a model of ZFC in Type 0 (not the same one as in Type 1, probably one constructed using the Henkin method). That this model exists in Type 0 entails Con(ZFC). There is no connection with this model to Type 1, it just works inType 0!

[Mario Carneiro]

Provability is a syntactic notion, not a semantic one. Truth in a model is a semantic notion but you can cook up models which satisfy only the consistency statements you want by tweaking the metatheory

[Mario Carneiro]

For example, Con(ZFC) is provable in Lean. This is an arithmetical statement which doesn't require more than Type 0 to state. Because Type 1 exists and there is a model of ZFC in Type 1, that arithmetical statement is true.

That is to say, any proof of Con(ZFC) in lean is going to go through a lemma which is "Type 1 exists", so syntactically I can see this in the proof, and semantically if I have a truncated model which fails this then it will also fail when trying to access Type 1 because Type 1 doesn't exist in the model (or exists and doesn't have all the properties of a universe)

[François G. Dorais]

If you don't believe in completeness and soundness, then I'm afraid we have nothing else to talk about in this thread.

[Mario Carneiro]

I'm not sure how you gathered that from what I said

[Mario Carneiro]

but note that Lean is not complete for the model in my thesis

[François G. Dorais]

The first sentence?

[Mario Carneiro]

That's just a fact. Proof is syntactic, truth in a model is semantic. Soundness and completeness are two ways to connect between these two notions

[François G. Dorais]

What do you think completeness means?

[Mario Carneiro]

that everything which is true in a model or class of models is provable in the theory

[François G. Dorais]

Exactly.

[Mario Carneiro]

Completeness is a property that may or may not hold when you vary the theory and the class of models

[François G. Dorais]

Model theoretic reasoning is sound, so long as you consider all models.

[Mario Carneiro]

for the case of lean and the standard model of lean, it doesn't hold

[François G. Dorais]

I am not just considering the standard model. I am reasoning inside any model.

[Mario Carneiro]

there might be some class of lean models for which completeness holds but it would have to include some quite exotic models to falsify all the things which are independent in lean. This is starting to get back to that point of "we don't have a model theory paper on lean"

[Mario Carneiro]

and in any case it's irrelevant to the point

[François G. Dorais]

Do you disagree that in any model of Lean (the whole thing) the arithmetic statement "Con(ZFC)" is true?

[Mario Carneiro]

yes I do not disagree with that

[François G. Dorais]

Do you believe the Henkin construction can be formalized in Lean using only Type 0?

[Mario Carneiro]

I don't know what you mean by that. It's not directly applicable

[Mario Carneiro]

again, because Lean isn't a FOL

[François G. Dorais]

ZFC is a FOL.

[Mario Carneiro]

do you mean the Henkin construction of FOL being formalized in lean?

[Mario Carneiro]

Sure I guess, not sure why you want to do metatheory in lean now though

[François G. Dorais]

So you believe there is a model of ZFC in Type 0?

[Mario Carneiro]

I don't think the question is well formed

[Mario Carneiro]

If you mean in (full) lean, then yes

[Mario Carneiro]

but in the truncated model of lean, or the truncated type theory of lean to 0 universes, no

[François G. Dorais]

So, using only objects in Type 0, I can establish Con(ZFC)?

[Mario Carneiro]

Depends on what you mean by "using", but probably no

[François G. Dorais]

(In full Lean.)

[Mario Carneiro]

still depends on what you mean by "using"

[François G. Dorais]

How can you tell whether that model came from higher reasoning or not? It's in Type 0.

[Mario Carneiro]

you are going to be hard-pressed to come up with a proof that does not involve constructing Type 0 in the course of the proof

[François G. Dorais]

Yes, I'm not thinking about proofs. I'm working in _any_ model of Lean.

[Mario Carneiro]

François G. Dorais said:

How can you tell whether that model came from higher reasoning or not? It's in Type 0.

The proof that it satisfies the axioms of ZFC will make use of properties of inductive types inside Type 0 and quantifications that are not valid in the truncated model

[François G. Dorais]

So, in _any_ model of Lean, I claim there exists an object in Type 0 which is a model of ZFC. I think we've established that.

[François G. Dorais]

So, by completeness...

[Mario Carneiro]

the exact details of this relate to how the truncation is performed, but for example we might have that Type 0 does not have all inductive types, and in particular does not have the pSet inductive type; or maybe it's proper-class like and doesn't admit higher order quantification above a certain level

[François G. Dorais]

I'm not talking about the proof. We already discussed that point.

[Mario Carneiro]

You keep talking about full lean, but the point here is that the semantic analogue of the syntactic proof theory of "lean with n universes" is "the truncated model with n universes", that is, an n-correct model instead of an omega-correct model

[François G. Dorais]

Sure, if you restrict the type theory, then I won't be able to prove some things.

[Mario Carneiro]

and in this model various parts of the proof you are trying to conduct will be false

[Mario Carneiro]

in particular the final theorem, but also many of the statements leading up to it

[François G. Dorais]

Which theorems? The Henkin construction is really basic, so is the soundness theorem.

[François G. Dorais]

I'm just using the fact that Con(ZFC) is true.

[François G. Dorais]

That's an arithmetic statement.

[Mario Carneiro]

Is it okay if I add n inaccessibles to that statement? Things are a bit clearer with some wiggle room

[Mario Carneiro]

Con(ZFC + 18 inaccessibles) is not true in a metatheory of ZFC with no inaccessibles

[François G. Dorais]

That would be weird. Not sure why you would want to do that. What are you getting at?

[Mario Carneiro]

and if I have a construction of a 0-correct lean model in that metatheory, Con(ZFC + 18 inaccessibles) will still not be true

[Mario Carneiro]

(having an n to play with there makes it really obvious which statements are weak and which are strong)

[François G. Dorais]

Why are you insisting on building Lean models? I don't get it.

[Mario Carneiro]

Didn't you want to go the semantic route?

[Mario Carneiro]

I'm saying that there exists a (truncated) lean model in which Con(ZFC + n inaccessibles) is false

[François G. Dorais]

That doesn't mean building models. What model do you want to build and why?

[Mario Carneiro]

even though it's an arithmetic statement which can be stated only using objects in Type 0

[François G. Dorais]

What is a truncated lean model? (There is no lean model where Con(ZFC + n inaccessibles) is false).)

[Mario Carneiro]

An n-correct model

[François G. Dorais]

That's a notion in ZFC. I don't know what you mean.

[Mario Carneiro]

This is defined in my paper, which in fact never works with omega-correct models, the main theorem is actually about n-correct models

[François G. Dorais]

What is a n-correct model of Lean?

[Mario Carneiro]

You do the same construction as in the standard model but you use a sequence of cardinals that ceases to be inaccessible above n

[Mario Carneiro]

as a result, the higher universes are not closed under some operations

[Mario Carneiro]

this is a model of "lean with n universes" because if you never use the higher universes then you never notice that they are kinda broken

[François G. Dorais]

That's sort of what I described above, no? That requires no impredicative Prop since the whole theory would collapse.

[Mario Carneiro]

everything is impredicative here

[Mario Carneiro]

the theory does not collapse, but maybe you mean something more specific

[François G. Dorais]

Why do you have universes then?

[Mario Carneiro]

?

[Mario Carneiro]

Type is predicative, of course, because Type : Type is inconsistent. But Prop is impredicative and I don't want to be sidetracked by discussing predicative Prop

[Mario Carneiro]

François G. Dorais said:

That's sort of what I described above, no? That requires no impredicative Prop since the whole theory would collapse.

You described a sequence of Prop n types, some of which have one element and others which have two. I am not describing anything like that, there is one Prop and it has two elements in all truncated models

[François G. Dorais]

So, in Type n+1 (or whatever) you can prove False is inhabited, so False is inhabited by impredicativity and this a fact at all levels.

[Mario Carneiro]

Is that a claim about the model or the proof theory?

[François G. Dorais]

The proof theory.

[Mario Carneiro]

In the proof theory, when you write down Type n+1 the kernel says ERROR OVERFLOW

[Mario Carneiro]

In the model Type n+1 exists but is weird and doesn't act like the other universes. False is still sitting there at the bottom and uninhabited though

[François G. Dorais]

I have no idea what the kernel would say, but lean would be inconsistent so I wouldn't care much what it says.

[Mario Carneiro]

No, ERROR OVERFLOW means the proof doesn't typecheck, so you didn't prove false

[Mario Carneiro]

less dramatically, the proof is simply not well typed

[François G. Dorais]

So you're working in that "type theory" where typeworthy terms don't have types? I'm not sure what to do with that.

[Mario Carneiro]

that's right

[Mario Carneiro]

There exist type theories with only a finite number of universes. Just think that we are working in one of those

[Mario Carneiro]

usually you will have a Gamma |- A type judgment separate from Gamma |- A : U for typing the things at the top that have no type

[Mario Carneiro]

or maybe Gamma |- A : * where * isn't a term

[François G. Dorais]

That's not what I was thinking about. I would rather have trivial higher universes and restricted impredicativity, but whatever.

[François G. Dorais]

I can play along so long as you're clear.

[Mario Carneiro]

In this case, we are rather rudely just chopping off the top of the lean type system, so we just have the one judgment and there are types that don't have types near the top

[François G. Dorais]

That's what I called "axe chopping" earlier. It's kind of sketchy.

[Mario Carneiro]

This is part of what I meant earlier about finessing this truncation process so that we don't lose "every type has a type" and instead lose less structurally important properties like "every universe has inductive types"

[François G. Dorais]

Yes, that's essentially equivalent to the predicative model I described before. I just don't think "axe chopping" as finesse :joking:

[Mario Carneiro]

well no, the axe chopping is without the finesse

[Mario Carneiro]

with the finesse you would be allowed to have Type n for every n in the proof theory, and every type would have a type

[Mario Carneiro]

they still wouldn't actually be modeled as inaccessible cardinals though

[Mario Carneiro]

the part of the ZFC construction that would fail is the construction of the docs#PSet type

[Mario Carneiro]

I don't think it's the same as the predicative model, there would still only be one Prop and indeed it would be not very obviously different from the usual lean

[François G. Dorais]

Yeah, i don't think we disagree here, these are hypothetical type theories. I'm not super interested in working out the details of what "Lean_n" ought to mean.

I'm reaching the end of my useful hours here. Should we continue tomorrow?

[Mario Carneiro]

I think there may eventually be something useful to come out of a "typechecker for Lean_n" to practically address the issue of how to know whether your proof has been conducted in ZFC when it feels like it should have been

[Mario Carneiro]

the finesse is important for this though, especially for n = 0