Girard's Paradox

Definition

Girard’s Paradox is a proof that an extension of System $F_{\omega }$ with a type of all types $Type:Type$, is inconsistent. It demonstrates that assuming a universe contains itself leads to a logical contradiction analogous to Russell’s Paradox in set theory.

Formal Mechanism

The paradox exploits the fact that if $Type:Type$, one can construct a type representing the collection of all well-founded relations. By defining a specific ordering on these relations, one can construct a relation that is well-founded if and only if it is not well-founded.

In the presence of Impredicative and a self-containing universe, we can define:

1. A type of all ordinals.
2. An ordering on these ordinals.
3. The Burali-Forti-style contradiction where the set of all ordinals would itself be an ordinal greater than any element in the set.

Impact on Type Theory

The discovery of this paradox by Jean-Yves Girard in 1972 necessitated the use of predicative hierarchies in Martin-Löf Type Theory. To maintain consistency, universes must be indexed by levels $l$, ensuring ${\mathcal{U}}_l:{\mathcal{U}}_{l+1}$ and prohibiting $\mathcal{U}:\mathcal{U}$.

Relation to Coq and Agda

• Agda: Strictly adheres to a predicative hierarchy of Set n.
• Coq: Utilizes an impredicative universe Prop and a predicative hierarchy Type n. Girard’s Paradox is avoided by ensuring only Prop is impredicative and does not contain itself.

References

• girard1972-cuts-higher-order-arithmetic
• coquand1986-girard-paradox
• nederpelt2014-type-theory