A constructive Cantor–Schröder–Bernstein theorem #1206
Conversation
|
Some of the work I need to do to continue this PR depends on #1188. Could we merge that PR soon? |
Thanks for the heads up! I'll make it a priority. |
|
Turns out the approach I had in mind for this PR doesn't quite work and needs to be rethought a little. Since this PR still covers some additions not covered by other PRs I'll leave it open, but ultimately this PR should be closed until a correct approach is found. |
Some logic formalizations extracted from #1206. ### Summary - Create `logic` namespace - Double negation elimination - Double negation stable propositions - Maps with double negation elimination and closure properties - Double negation stable embeddings and closure properties - De Morgan's law - De Morgan types and De Morgan propositions - De Morgan maps and closure properties - De Morgan embeddings and closure properties - Markov's principle and a strong version for finite types - Some additional closure properties for decidable maps, decidable embeddings, decidable propositions... - Diaconescu's theorem - The suspension of a proposition is a set Initial work for #1069
fredrik-bakke
changed the title
|
Whelp, I finally pieced together an incredibly crude formalization of the theorem! Turns out WLPO + decidable embeddings is enough. I'll clean up the code one of the coming days so it can be reviewed. The relevant code is in |
|
Alright, I'm opening this PR up for review now. Sorry if parts of it appear less polished. I've sort of lost track of the contents of this PR. |
|
Never mind. I'd like to let this stew for a little while longer first. |
Formalizes a fine-grained analysis of the construction used for the Cantor-Schröder-Bernstein-Escardó theorem, and uses this deconstruction to give a series of generalizations of the theorem. Perhaps most importantly, although not most general,
AandBmutually embed by decidable embeddings, and WLPO is true, thenAandBare equivalent.