Documentation

A Simplification of Girard's Paradox by Hurkens (TLCA '95)

Hurkens' version fails in HOL, there are no (△,□,□)-rule:

>>> runSilent $ spec_ HOLStar >> hurkensScript
λ» :define ⊥ : ⋆ = ∀ x → x
λ» :define ¬ : ⋆ → ⋆ = λ P → P → ⊥
λ» :define U : □ = ∏ (X : □) → (((X → ⋆)..
error:
• No PTS Rule (△,□,-)
• when checking expression
  ∏ (X : □) → (((X → ⋆) → ⋆) → X) → (X → ⋆) → ⋆

It fails even sooner in predicative systems, because we cannot define ⊥ purely; to begin with:

>>> runSilent $ spec_ (MartinLof 0) >> hurkensScript
λ» :define ⊥ : 𝓤 = ∀ x → x
error:
• Couldn't match expected type 𝓤 with actual type 𝓤₁
• In the expression: ∀ x → x

...or if we try to define U, it will be in the wrong universe:

>>> runSilent $ spec_ (MartinLof 0) >> defineU
λ» :define U : 𝓤₁ = ∏ (X : 𝓤₁) → (((X → 𝓤)..
error:
• Couldn't match expected type 𝓤₁ with actual type 𝓤₂
• In the expression: ∏ (X : 𝓤₁) → (((X → 𝓤) → 𝓤) → X) → (X → 𝓤) → 𝓤

However in System U, the script goes through:

>>> runSilent $ spec_ SysUStar >> hurkensScript
λ» :define ⊥ : ⋆ = ∀ x → x
λ» :define ¬ : ⋆ → ⋆ = λ P → P → ⊥
λ» :define U : □ = ∏ (X : □) → (((X → ⋆)..
λ» :define Δ : U → ⋆ = λ y → ¬ (∏ (p : (U →..
λ» :define Ω : U = λ X f p → (λ p₁ → ∏ (x..
λ» :define Θ : ⋆ = ∏ (p : (U → ⋆)) → (∏..
λ» :define D : ⋆ = ∏ (p : (U → ⋆)) → Ω U..
λ» :define lemma : Θ = λ p t₁ → t₁ Ω (λ x →..
λ» :define H : D = λ p → lemma (λ y → p..
λ» :define negH : ¬ D = lemma Δ (λ x H₂ H₃ →..
λ» :define ¡Ay, caramba! : ⊥ = negH H
∎