6
$\begingroup$

It seems well known that Lean's type theory is equiconsistent with ZFC + the existence of $n$ inaccessible cardinals for every $n>0$.

Suppose I want to ensure that my lean proofs depend only on ZFC, and do not use additional large cardinal axioms. How can this be done?

(This is a repost of this unanswered M.SE question.)

$\endgroup$
8
  • $\begingroup$ By “well known”, you mean it follows from Mario Carneiro’s master thesis. For that I understand that it is consistent that each universe corresponds to one one inaccessible cardinal. We also known (formalized in Lean), that each Type u can be used to construct a model of ZFC. So it might be that if you only use types in Type 0, then you are ZFC compatible, but I don’t know the subtleties enough to give a full answer. (If this or similar was true, you could probably write a Lean linter to check that you aren’t using large types.) $\endgroup$
    – Jason Rute
    Feb 10 at 11:56
  • $\begingroup$ Another option would be to use Lean’s formulation of ZFC to formally show a fact holds in ZFC. This is likely not too hard for results about sets, functions, etc. I imagine you could transfer the Lean results easily to ZFC using the existing formalization tools. But I don’t know how you would do it for other mathematical objects without it requiring reimplementing all the definitions in a ZFC specific way. $\endgroup$
    – Jason Rute
    Feb 10 at 12:01
  • 1
    $\begingroup$ Also, while this is an interesting question, I think it is worth mentioning that I think mathematics is going to embrace inaccessible cardinals (a.k.a. universes) at some point. Our exact foundations is flexible and is as much social as scientific. With tools such as Coq and Lean having this baked in, with reflection techniques being well understood, and with some areas of math already using universes freely, it might be that mathematics changes its notion of what it means to be a theorem (without asterisks). (But again, this is speculative and shouldn’t detract from your good question.) $\endgroup$
    – Jason Rute
    Feb 10 at 12:07
  • $\begingroup$ @JasonRute Thank you for your comments. The linked question suggests that checking that Type u isn't used for u>0 is not enough. I'm not exactly sure why this is, or if this statement is even true, but it suggests there is some subtlety here. $\endgroup$
    – Potato
    Feb 10 at 14:34
  • 1
    $\begingroup$ The correct statement is that the consistency of Lean's Type Theory with Choice is equivalent to $\forall n\,\mathrm{Con}(ZFC + \text{there are $n$ inaccessibles})$ (in PA, say). "ZFC + the existence of $n$ inaccessible cardinals for every $n > 0$" is logically equivalent to "ZFC + there are infinitely many inaccessible cardinals", which is strictly stronger in consistency strength. . $\endgroup$ Feb 12 at 11:56

2 Answers 2

4
$\begingroup$

Your question probably needs some clarification.

Which theorems make sense in both ZFC and Lean

It isn't 100% non-ambiguous what it means for a Lean theorem to "hold in ZFC". Sometimes it comes down to just how stuff is defined. For a silly example, in ZFC with the usual encoding, $\mathbb{Z} \neq \mathbb{N}$, but in Lean it is well-known that this is independent. Of course in both ZFC or Lean, one could have defined $\mathbb{Z} := \mathbb{N}$ and then we have $\mathbb{Z} = \mathbb{N}$.

For a normal mathematical theorem, there is no ambiguity and it doesn't come down to definitions. In practice, a mathematician has a good sense of what a "normal mathematical theorem" means. However, just to be pedantic, for the rest of this answer I'll just talk about theorems of higher-order arithmetic (which is a common approach in logic to deal with these sorts of issues). This eliminates the ambiguity, and surprisingly you can encode a huge amount of mathematics into arithmetic.

Not enough to look at the theorem statement itself

As François G. Dorais's answer suggests, you can't just look at the statement of the theorem itself. We can encode theorems like $\text{Con}(\mathsf{ZFC} + \text{$n$ inaccesibles})$ into arithmetic and they are provable in Lean for any given $n$, but they are not provable in ZFC.

(Also, this comes down to Lean's Prop being impredicative. If it was not, then each universe would have its own Prop level, and it would likely be true that (arithmetic) theorems in Prop 0 also hold for ZFC, and likely weaker from my limited understanding.)

What if we restrict the universes used in a proof?

The picture changes if we can also look at the proof. In Lean, to prove $\text{Con}(\mathsf{ZFC} + \text{$n$ inaccesibles})$ it takes roughly $n+1$ universe levels, Type 0, Type 1, ..., Type n. Mario Carneiro's thesis roughly proves that if a theorem (of arithmetic) is provable in Lean with $n$ universe levels, then it is provable in ZFC plus $n$ inaccessible cardinals "up to a fence post error" as Mario says in a Zulip discussion inspired by this PA.SE question.

And it probably shouldn't be that hard to get an upper bound on how many universes go into a proof. Indeed, a few years ago, Mario Carneiro wrote a script to measure this and determined that Mathlib used only four universe levels. I could even imagine having a command analogous to #print_axioms that counts how many universe levels are needed for a theorem.

But this doesn't fully answer your question. The "fence-post error" above hasn't been sufficiently worked out, so knowing something uses 0 universes doesn't alone necessarily guarantee it holds in ZFC.

Also, Lean doesn't record every step of the proof. Some parts are computed on the fly through type checking, and as François G. Dorais pointed out in that Zulip discussion above, it might be possible that hidden universe bumps may happen there which are hard to measure. (There is more discussion on that Zulip thread about this.)

Also, if one does Mario Carneiro's naive method to compute an upper bound on the universe levels, a lot of things would bump the level up unnecessarily. I think just using List Nat would already bump the universe level since List.{0} has type Type 0 -> Type 0 which lives in Type 1. (Note, the analog to List in ZFC is not a set, but a proper class because it is too big.) But that universe bump is a bit silly if we never use more than List Nat in the proof, since that lives in Type 0. Mario discussed (again in that Zulip thread) better ways to bound the universe levels to try to truly capture if something is provable in ZFC.

Practically speaking

Given the practical concerns I mention above, I doubt (at least right now) you could easily figure out if a theorem in Lean holds in exactly ZFC. I think without doing a lot of meta-logic and meta-programming work, the easy upper bounds that would pop out would likely include at least one universe level for most theorems in Lean's Mathlib.

If you care about this sort of thing, I think it would be better right now to use HOL-Light or Isabelle/HOL whose logic is (I believe) strictly weaker than ZFC. (Isabelle's AFP is a very large theorem library.)

Also, this concern is not new to math. Lean's users have embraced universes and use them freely, just like most mathematicians have embraced the axiom of choice and the law of excluded middle. This may still be odd in some circles of math. I remember once someone telling me Fermat's last theorem wasn't currently a "theorem" since it used universes in its proof. (This has since been worked out.) But what counts as a "real theorem" is a social norm that may change over time. For example, some categorical fields of math have already widely embraced universes.

Still one can also of course ask what the minimal axioms needed to prove a theorem are. There are entire fields of logic devoted to these sorts of questions. But that investigation becomes harder and harder as you restrict the logic more and more. (One of the most extreme examples I've seen is Harvey Friedman's conjecture that all theorems in Annuals which can be stated in first-order arithmetic, including Fermat's Last Theorem, hold in elementary finite arithmetic, which is an exceedingly weak theory. I doubt this will be proven any time soon.)

$\endgroup$
1
  • $\begingroup$ This is a wonderful and comprehensive summary. Thank you very much for taking the time to write this! $\endgroup$ Feb 20 at 5:29
3
$\begingroup$

This is not possible because Lean's Prop is impredicative. Restricting to Type 0 is close but not exactly the same as working in ZFC.

For example, Con(ZFC) (formalized in a typical Gödelian manner) is an arithmetical proposition that only talks about Nat, which lives in Type 0. So this is within the scope of "restricting to Type 0".

It so happens that there is a model of ZFC that lives in Type 1. This means that Con(ZFC) must be true in Lean: there is no model of Lean where Con(ZFC) is false. But there is no way to tell that the truth of Con(ZFC) depends on the existence of some Type 1 object because Prop is impredicative.

As far as I can tell, Lean's type theory (with Choice) is conservative over ZFC ∪ {Con(ZFC + there are at least n inaccessibles) : n = 0,1,2,...} for arithmetical statements.

$\endgroup$
9
  • 1
    $\begingroup$ Choice shouldn't actually be relevant for arithmetical statements, unless it's how you're deriving LEM. $\endgroup$ Feb 12 at 17:01
  • $\begingroup$ I’m confused by this answer. The OP didn’t necessary propose a particular method so I don’t know what the “This” in “This is not possible” means. Is it impossible to find a nice syntactic subset of Lean code that is ZFC compatible? If you just mean restricting to Type 0 is not good enough, what do you mean by “restricting to Type 0”? I can think of three interpretations: (1) Only considering propositions which reference objects in Type 0. (Your answer clearly explains why that is not sufficient.) … $\endgroup$
    – Jason Rute
    Feb 12 at 18:42
  • $\begingroup$ … (2) Only ever using one universe, Type 0. (I guess one can still use that universe to build a model of ZFC proving Con(ZFC).) (3) Only using one universe and only using it in certain syntactic positions. (For example, you shouldn’t be allowed to construct objects with Type 0. But I think Andre’s point is by doing that we loose dependent types and basically have higher order logic, which is known to be weaker than ZFC.) Also, maybe your point is that if we use option (2) then we get a theory which is about the same as ZFC plus one inaccessible? $\endgroup$
    – Jason Rute
    Feb 12 at 18:43
  • 1
    $\begingroup$ @JamesHanson Yes that is how Lean derives LEM. $\endgroup$
    – Jason Rute
    Feb 12 at 20:04
  • 1
    $\begingroup$ Another way to think about it: Con(ZFC) is a statement about Nat, which lives in Type 0, and this statement is true in every model of Lean. So if "using only Type 0" (whatever that means) can't prove this statement, then it is not a complete proof system for Type 0. $\endgroup$ Feb 13 at 14:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.