{"id":"arxiv:2610.37498","kind":"preprint","title":"Global Choice without Excluded Middle in Dependent Type Theory","authors":["Sewon Park"],"author_count":1,"year":2026,"published":"2026-10-27","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2610.37498","nct_id":null,"source_url":"https://arxiv.org/abs/2610.37498","archive_url":"https://space-kitty.com/papers/arxiv:2610.37498","updated":"2026-10-27","pmid":null,"pmcid":null,"openalex_id":"W7224121726","pdf_url":"https://arxiv.org/pdf/2610.37498","abstract":"Diaconescu's theorem derives excluded middle from the axiom of choice, using propositional extensionality. We show that in dependent type theory without propositional extensionality, global choice alone does not imply excluded middle. We consider extensional Martin-Löf type theory with an impredicative universe of propositions included in the universe of types, extended with a global choice operator. We construct a consistent model of this type theory and show that the model refutes excluded middle and propositional extensionality. The model is built from staged sets, sets whose elements appear at stages of a well-order. It further validates proof irrelevance, inductive families, quotients with soundness, and a cumulative hierarchy of universes, which together cover a large fragment of the type theory of the proof assistant Lean. Even together with these features, global choice does not imply excluded middle.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}