Global choice in type theory does not imply excluded middle principle
Global Choice without Excluded Middle in Dependent Type Theory
Logic in Computer Science
Summary
In some areas of logic used for computer programming and math, there are two principles called "global choice" and the "excluded middle." Usually, having global choice means you can assume the excluded middle. But this paper shows that in certain advanced logical systems used for programming proof software, global choice does NOT force you to accept excluded middle. The authors built a mathematical model proving this is consistent and explained how the model works. This helps clarify what assumptions are needed for certain logic principles in these systems.
What this means in practice
- •For proof assistant developers: Design type theories in proof assistants that include global choice without forcing excluded middle, enabling flexible logic foundations.
- •For programming language designers: Develop dependently typed languages that support global choice operators while preserving constructive logic principles.
A theory result. No direct application yet.
Authors
Sewon Park
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.