Cantor-Bernstein implies Excluded Middle
| Autor: | Pradic, Pierre, Brown, Chad |
|---|---|
| Přispěvatelé: | Faculty of Mathematics, Informatics, and Mechanics [Warsaw] (MIMUW), University of Warsaw (UW), École normale supérieure - Lyon (ENS Lyon), Laboratoire de l'Informatique du Parallélisme (LIP), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Preuves et Langages (PLUME), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Czech Technical University in Prague (CTU), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Pradic, Pierre |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Mathematics::Logic
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO] [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory [MATH.MATH-LO] Mathematics [math]/Logic [math.LO] Mathematics::General Topology [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
| Popis: | Update: fixed an error on the applicability of thm 1, added some acks and a ref; We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Martín Escardó stating that quantification over a particular subset of the Cantor space ℕ → 2, the so-called one-point compactification of ℕ, preserves decidable predicates. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|