Do Lean and Set theory prove the same arithmetic facts?

Stream: Type theory

[Jason Rute]

We know Lean (with the 3 axioms) is equiconsistent with ZFC + {there are n inaccessibles | n < ω} by Mario's thesis (and Sebastian's dissertation on Lean 4). But what do we know about the stronger claim that they have the same provable theorems of arithmetic? For now, let's talk about first order theorems in the language of Peano Arithmetic, but if those are the same, we can address higher order $\Pi^k_n$ theorems. Does Mario's set theoretic interpretation say anything obvious about this? (I've sort of took it for granted that this is true, and said it at least one place online, but now I'm second guessing myself, and despite being trained as a logician and having a proof theorist as an advisor, I'm sort of bad at this stuff.)

[Jason Rute]

Wait, does the proof go like this? Take a formula phi provable in ZFC plus n innaccessibles. Then in Lean make a model of it where Nat in the model is isomorphic to Nat in Lean. So we have a proof in Lean that phi holds of Nat. conversely, do the same constructing models of Lean + n universes in ZFC plus n+1 (or more) innaccessibles. This works right?

[Mirek Olšák]

This is true because the equiconsistency goes via modeling one inside the other, and these models keep isomorphic natural numbers. (I am not imagining building a model of $\phi$) For example, we have a class-size model of Lean inside ZFC+inaccessibles. The natural numbers inside (let's call them ℕ) are isomorphic to the standard $\omega$ in ZFC. So every $\phi$ about ℕ which is provable in Lean must be true in the model by a proof in ZFC (these class-sized models translate provability), and by isomorphism provable about $\omega$ in ZFC.

[Jason Rute]

I think we are in agreement. I hadn’t considered class models. That simplifies things a bit. Otherwise you just need a model big enough to model enough axioms (or deduction rule instances) to prove phi (and make it so that the isomorphism holds). I assume you are also implying we need to run your argument both ways, i.e. building a model of ZFC plus inaccessibles in Lean. I don’t know what the Lean analogue of a class model would be? (A universe polymorphic model like ZFSet.{u}?) But regardless, if needed we again can use a slightly smaller model which is large enough to prove phi.)

And this approach seems really general in that it works for any sufficiently strong “set theory” or “set-like” type theory. I think this also works for any level of the hyper-arithmetic hierarchy, i.e. a Pi^k_n sentence, but maybe I am missing something subtle.

[James E Hanson]

Jason Rute said:

I don’t know what the Lean analogue of a class model would be?

You don't really need a Lean analog of a class model because you don't need to build a model of ZFC + {"there are n inaccessible cardinals" : n < ω} all at once. Any given arithmetic consequence of that theory is provable from ZFC + "there are n inaccessible cardinals" for some n (depending on the statement). For each n, you can build an arithmetically standard 'small' model of this theory in Lean, so any arithmetic consequence of the full theory is provable in Lean.

[James E Hanson]

Jason Rute said:

I think this also works for any level of the hyper-arithmetic hierarchy, i.e. a Pi^k_n sentence, but maybe I am missing something subtle.

You should actually be able to prove a lot more than this. Given any first-order language $\mathcal{L}$ and any $\mathcal{L}$-structure $M$ that is definable in $\mathsf{ZFC}$ and provably unique up to unique isomorphism, Lean and the relevant version of $\mathsf{ZFC}$ will prove the same statements about $M$ in "$\alpha$ th-order logic" for any definable ordinal $\alpha$.

[James E Hanson]

Note though that this is specifically not including theorems whose statements include Classical.choice (even if the proof might).

[Mirek Olšák]

James E Hanson said:

You should actually be able to prove a lot more than this. Given any first-order language $\mathcal{L}$ and any $\mathcal{L}$-structure $M$ that is definable in $\mathsf{ZFC}$ and provably unique up to unique isomorphism, Lean and the relevant version of $\mathsf{ZFC}$ will prove the same statements about $M$ in "$\alpha$ th-order logic" for any definable ordinal $\alpha$.

I would try to phrase it as an isomorphism between a specific Lean structure (the Lean structure is a bit missing in that statement), and ZFC-structure. For example, Lean has Real defined in some way, we can define it also in ZFC in another way (say through dedekind cuts), but because the pure-ZFC construction will be isomorphic with the Lean-model construction in ZFC, and vice versa the ZFC construction in a Lean model of ZFC will be isomorphic through Lean with Real.

[Mirek Olšák]

James E Hanson said:

Note though that this is specifically not including theorems whose statements include Classical.choice (even if the proof might).

This can be a bit more subtle. Excluding all uses of choice is a bit too harsh because unique choice should be allowed, and Lean currently doesn't care about the distinction of unique choice & choice at all. We were discussing) that there could be perhaps a keyword arbitrary in the future denoting that an arbitrary choice was made in the definition but it is still a little tricky:

• Arbitrary choice doesn't matter if it hidden in a proof
• There is no way to make Ordinal.ToType or Cardinal.outnon-arbitrary in Lean due to universe constraints (although it doesn't feel like making arbitrary choices).
• choice is sometimes used for dummy values (for example in limUnder) which is unfortunate. If Lean starts caring about arbitrary definitions at some point, it should perhaps reconsider such cases

[Mirek Olšák]

I decided to open a dedicated thread about arbitrary definitions. It is a complex topic on its own.

[James E Hanson]

Mirek Olšák said:

This can be a bit more subtle.

Okay then I think the best approach would be to think of Classical.choice as a parameter on the ZFC side.