CSB implies LEM

I couldn’t avoid using an extensionality axiom. Also note, that `N_infty` can’t be replaced by `option nat`, without using more axioms. Namely, the definition of the epsilon function fails, or at least needs some non-trivial change. Based on https://arxiv.org/abs/1904.09193
coq-community · Feb 14, 2022 · ada3881 · ada3881
1 parent 06db8cb
commit ada3881
Show file tree

Hide file tree

Showing 2 changed files with 572 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -62,5 +62,6 @@ theories/ZornsLemma/Powerset_facts.v
 theories/ZornsLemma/Proj1SigInjective.v
 theories/ZornsLemma/Quotients.v
 theories/ZornsLemma/Relation_Definitions_Implicit.v
+theories/ZornsLemma/ReverseCSB.v
 theories/ZornsLemma/WellOrders.v
 theories/ZornsLemma/ZornsLemma.v