Consistency of choice + fun ext + prop ext axioms

Stream: lean4

[Son Ho]

I'm using the excluded middle and the epsilon operator in some of my proofs in Lean, which from my understanding derive from the axioms of choice, functional extensionality and propositional extensionality (https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html). Does someone know of papers/work which study whether it is consistent to use those axioms in combination in a logic like the one implemented by Lean? (I really want to be able to argue that it is ok to use those axioms if someone asks me the question).

[Alex J. Best]

I think the best reference is still @Mario Carneiro's masters thesis which says that the type theory of lean is equiconsistent with ZFC + countably many inaccessible cardinals https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf (corollary 6.8 for example)

[Son Ho]

Alex J. Best said:

I think the best reference is still Mario Carneiro's masters thesis which says that the type theory of lean is equiconsistent with ZFC + countably many inaccessible cardinals https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf (corollary 6.8 for example)

Thanks! This looks like what I was looking for.

[Jason Rute]

It is really only the axiom of choice you have to be concerned about, since the others can all be derived from choice as shown in that chapter you linked to.

[Jason Rute]

(And again, you don't have to be concerned about choice thanks to Mario.)

[Son Ho]

Jason Rute said:

It is really only the axiom of choice you have to be concerned about, since the others can all be derived from choice as shown in that chapter you linked to.

Just checking: can we really derive the others from the axiom of choice? It seems not to be the case according to this sentence: "Using a clever trick (known as Diaconescu's theorem), one can use propositional extensionality, function extensionality, and choice to derive the law of the excluded middle."

[Henrik Böving]

propext and choice are axioms in the theory, funext is derived using quotient types and em using the mentioned trick

[Jason Rute]

Sorry, I apparently misremembered the details.