Global Choice without Excluded Middle in Dependent Type Theory

• The theory with global choice is consistent with the failures of excluded middle and propositional extensionality.Source: §1 · p. 2
• Propositions that become true at different stages can be equivalent while their identity proposition never holds, so propositional extensionality fails.For propositions 0 and 1, equivalence holds from stage 1, while identity never holds.Source: §1 · p. 2
• The model uses staged sets, with global choice selecting an element that appears first when a type is nonempty.A staged set's elements appear at stages; the choice is made in the classical metatheory and is available when propositional truncation becomes true.Source: §1 · p. 2
• When there is no last stage, excluded middle fails because each proposition becomes true only at its own stage.A proposition p that becomes true has p ∨ ¬p only from stage p onward, while universal excluded middle must hold at every stage.Source: §1 · p. 2
• The model also validates proof irrelevance, inductive families, quotients with soundness, and cumulative universes, covering a large fragment of Lean's type theory.Source: §1 · p. 2

2 Staged sets

• A staged set pairs a set with a birthday for each element, and a staged map sends each element to one available by its birthday.Source: §2 · pp. 2–3
• A staged sum gives each pair the later of the base element's and fiber element's birthdays.Source: §2 · p. 3
• A dependent function belongs to the staged product only if its outputs are available once both the input and function are; unbounded output birthdays can exclude it.For L = N, the function n ↦ n has no birthday and is not in the staged product.Source: §2 · p. 3
• Staged sets are equivalent to presheaves on L^op with injective restriction maps, but the model uses their concrete description.The paper notes that Prop is not the strong subobject classifier in the quasitopos, which would validate excluded middle.Source: §2 · p. 3

2.1 Truth values

• Each subobject of the terminal staged set is a truth value p that holds from stage p onward; smaller values are truer.Source: §2.1 · p. 4

3.1 The extra rules

• The added rules make Prop an impredicative universe included in Type, with identity propositions and a global choice operator.The inclusion preserves decoding, and identity propositions decode to identity types with equality reflection.Source: §3.1 · p. 4

3.2 Category with families

• The category with families takes contexts to staged sets, types to families over them, and terms to sections of those families.Context extension is a staged sum, and substitution acts by composition.Source: §3.2 · pp. 4–5

3.3 Type formers

• Impredicative quantification over propositions satisfies substitution and the β- and η-rules, while identity propositions validate equality reflection.The W-type recursor also commutes with substitution and satisfies its computation rule.Source: §3.3 · pp. 6–7

3.4 Universes classifying types

• The model’s Type universe classifies κ-small types, and Prop classifies propositions through a bijection with their codes.Type is constant in the model, unlike the stage-varying universe in.Source: §3.4 · p. 7
• The standard locally cartesian closed interpretation has only weak classification: every type has a code, but no choice of codes is natural in Γ.A constant Type universe can include the constant Prop universe required for the refutations.Source: §3.4 · p. 7

4 The logic of the model

• Quantification over Prop is a supremum over its truth values, yielding p ∧ q = max(p, q), p ∨ q = min(p, q), and ⊥ = ∞.The corresponding encodings include negation and equivalence.Source: §4 · p. 8

4.1 Propositional extensionality

• When L has at least two elements, the supremum over proposition pairs is ∞, refuting propositional extensionality.Identity of propositions is decided at stage 0, while their equivalence may hold only from a later stage.Source: §4.1 · pp. 8–9

4.2 Excluded middle

• When L has no greatest element, excluded middle has value ∞; when L has a greatest element, it has value max L.If L has one element, that value is 0.Source: §4.2 · p. 9

4.3 Global choice

• Global choice is interpreted by selecting, in the metatheory, an element of least birthday from each nonempty small staged set.The resulting closed term interprets choice and commutes with substitution.Source: §4.3 · p. 9

4.4 Proof of Theorem 1.1

• For L = N, the model is consistent, interprets the type theory and global choice, and has closed terms witnessing the negations of propositional extensionality and excluded middle.Consistency follows because ⊥ = ∞ has no closed term.Source: §4.4 · p. 10

5 Further features and Lean

• With L = N, the model validates further rules while the paper’s earlier countermodel continues to refute excluded middle and propositional extensionality.The further rules include proof irrelevance, inductive families, quotients with soundness, and a cumulative hierarchy of universes.Source: §5 · p. 10

5.1 Universes

• Each Typeᵢ classifies κᵢ-small types, and the construction supplies a global choice operator at every universe level.The hierarchy includes Prop in Type₀.Source: §5.1 · p. 10, §5 · p. 10

5.2 Inductive families

• Inductive families use W-types, while subsingleton elimination lets certain inductive propositions eliminate into types.The relevant propositions have at most one constructor, with arguments that are propositions or result indices; global choice derives this elimination rule.Source: §5.2 · pp. 10–11

5.3 Quotients

• The quotient construction provides a quotient type with lifting, induction, and soundness, but not exactness.With global choice, exactness would imply excluded middle.Source: §5.3 · p. 11

5.4 Lean

• Together, the rules of Sections 1 and 5 cover the type theory specified in Carneiro’s thesis except propositional extensionality.The paper notes that most mutual and nested inductive types are expected to be derivable as well.Source: §5.4 · p. 11

6 Related work

• Earlier derivations of excluded middle from choice rely on extensionality, including extensionality of propositions or quotients [Bel93, §3] [Roc25a, Lea26] [Uni13, Theorem 10.1.14].Bell’s first-order result uses an ε-operator that assigns the same witness to formulas with the same extension [Bel93, §3].Source: §6 · p. 12
• Earlier ε-operator countermodels address first-order or higher-order logic, but not dependent types; a related higher-order model has no ε-operators [Bel93, §7] [MPR17, Example 5.14, Theorem 6.6].The latter uses truth values from a well-order with a greatest element.Source: §6 · p. 12
• The Section 3 model interprets dependent type theory with global choice, using the guarded form of the ε-operator; its types and propositions are staged sets, and each proposition has at most one element.The inclusion of Prop into the universes is the identity on staged sets.Source: §6 · p. 12

• Claude Opus 5.5 was used to develop the model and formalize it in Rocq.Source: Software use · p. 12

A Proof obligations

• Rocq checks that the staged-set CwF satisfies the type theory’s rules together with proof irrelevance and quotients.The formalization defines the CwF and model structures and instantiates the model for well-orders without a greatest element, including L = N.Source: A Proof obligations · p. 15
• The specification verifies that type and term operations commute with substitution, including the dependent function-space and lambda operations.The appendix explains that equations such as the beta rule are verified for defined operations.Source: A Proof obligations · p. 16
• Substitution laws for ∀ and refl, and the beta and eta rules for ∀, are derived from proof irrelevance.Source: A Proof obligations · p. 16
• The eliminator J and function extensionality follow from equality reflection, but these derivations, the universe hierarchy, and inductive families were not formalized.Source: A Proof obligations · p. 16

• Substitution is associative and preserves identities for types and terms, with reindexing along composed context morphisms matching successive substitutions.Source: Category with families · p. 16
• Comprehension pairs a context morphism with a term, recovers both through projection and variable, and makes the empty context terminal.Source: Category with families · p. 16

• The universe specification provides U, its decoding El, and substitution operations for both codes and decoded types.Source: Universe · p. 16

Propositions

• Propositions form a type whose elements decode to types; the section also specifies proof irrelevance, impredicative quantification, Π-types, and Σ-types.Source: Propositions · pp. 16–17

Finite types

• The finite types include an empty type, a singleton unit type, and booleans, with their eliminators and computation or uniqueness rules.Source: Finite types · p. 17

Identity propositions

• Identity propositions contain reflexivity proofs, and reflection identifies terms whenever the corresponding identity proposition has a proof.Source: Identity propositions · p. 17

W-types

• The W-type specification describes its branching family and includes a constructor and recursive operation.Source: W-types · p. 18

Quotients

• Quotients provide representatives, lifting, and induction, with the specification also including a quotient soundness operation.Source: Quotients · p. 18

Codes

• The universe codes Π, Σ, finite types, W-types, and quotients, with decoding equations connecting codes to their type formers.Source: Codes · pp. 18–19

Choice, excluded middle and propositional extensionality

• The model specifications include global choice and refutations of excluded middle and propositional extensionality.Source: Choice, excluded middle and… · p. 19

Consistency

• The consistency result states that no closed term inhabits the empty proposition.Source: Consistency · p. 19