BuraliFortiParadox.agda

{-# OPTIONS --type-in-type #-}

-- Burali-Forti's paradox in MLTT-ish without W-types

-- I was following Coquand's paper "An Analysis of Girard's Paradox"
-- and Hurkens's paper "A Simplification of Girard's Paradox".
-- Code is released under CC0.

-- Σ-types
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ
infixr 4 _,_

-- Non-dependent version
_×_ : Set → Set → Set
A × B = Σ A λ _ → B

-- Empty type
data ⊥ : Set where

-- Composition
_∘_ : ∀ {A : Set} {B : A → Set} {C : (a : A) → (B a → Set)}
  → (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → (C a (f a))
g ∘ f = λ x → g (f x)

-- Identity
id : ∀ {A : Set} → A → A
id x = x

------------------------------------------------------------------------------

-- Binary relation
rel : Set → Set
rel A = A → A → Set

-- Is it transitive?
is-trans : (A : Set) → rel A → Set
is-trans A ordA = ∀ c b a → ordA c b → ordA b a → ordA c a

-- Does the induction principle hold?
--
-- Note: [has-rec] is the official definition of "well-founded", but I decide to
-- consider only _transitive_ relations in [is-well-founded] for convenience.
-- One can always consider the transitive closure of a well-founded relation.
has-rec : (A : Set) → rel A → Set
has-rec A ordA = (P : A → Set) → (∀ a → (∀ b → ordA b a → P b) → P a) → ∀ a → P a

-- Is it a well-founded type?
-- That is, a type with a transitive, well-founded relation.
-- (This is DIFFERENT from "well-founded sets".)
is-well-founded : (A : Set) → rel A → Set
is-well-founded A ordA = is-trans A ordA × has-rec A ordA

-- The type of all well-founded types.
well-founded : Set
well-founded = Σ Set λ A → Σ (rel A) (is-well-founded A)

-- Convenient projection.
#set : well-founded → Set
#set = fst
#ord : ∀ A → rel (#set A)
#ord A = fst (snd A)
#trans : ∀ A → is-trans (#set A) (#ord A)
#trans A = fst (snd (snd A))
#rec : ∀ A → has-rec (#set A) (#ord A)
#rec A = snd (snd (snd A))

-- The induction principle rejects reflexivity.
rec-irr : ∀ A → ∀ a → #ord A a a → ⊥
rec-irr A = #rec A (λ a → #ord A a a → ⊥) (λ a ih refl → ih a refl refl)

-- [embed-up-to A B b] means that [A] can be embedded into [B]
-- with the strict upper bound [b].
embed-up-to : well-founded → (B : well-founded) → #set B → Set
embed-up-to A B b =
  Σ (#set A → #set B) λ f -- the function
  → (∀ a → #ord B (f a) b) -- the proof that it's a upper bound
  × (∀ {a₁ a₂} → #ord A a₁ a₂ → #ord B (f a₁) (f a₂)) -- the proof that it preserves orders

-- [embed A B] means [A] can be embedded into [B] with some upper bound
embed : well-founded → well-founded → Set
embed A B = Σ (#set B) (embed-up-to A B)

-- [embed] is a transitive relation on [well-founded].
embed-trans : is-trans well-founded embed
embed-trans _ _ _ (b↑ , g , g-bound , g-mono) (_ , f , _ , f-mono)
  = f b↑ , f ∘ g , f-mono ∘ g-bound , f-mono ∘ g-mono

-- [embed] admits an induction principle too!
embed-rec : has-rec well-founded embed
embed-rec P ind A = ind A lemma
  where
    lemma : ∀ B → embed B A → P B
    lemma B (a↑ , embed-up-to-a↑) = #rec A P′ lemmaA a↑ B embed-up-to-a↑
      where
        P′ : #set A → Set
        P′ a↑ = ∀ B → embed-up-to B A a↑ → P B

        lemmaA : ∀ a↑ → (∀ a↑′ → #ord A a↑′ a↑ → P′ a↑′) → P′ a↑
        lemmaA a↑ ih B (f , f-bound , f-mono) = ind B lemmaCB
          where
            lemmaCB : ∀ C → embed C B → P C
            lemmaCB C (b↑ , g , g-bound , g-mono) =
              ih (f b↑) (f-bound b↑) C (f ∘ g , f-mono ∘ g-bound , f-mono ∘ g-mono)

-- As a result, [embed] is a well-founded!
embed-is-well-founded : is-well-founded well-founded embed
embed-is-well-founded = embed-trans , embed-rec

-- So all the well-founded types form a well-founded
well-founded-well-founded : well-founded
well-founded-well-founded = well-founded , embed , embed-is-well-founded

-- Initial segment.
init : ∀ A → #set A → Set
init A a = Σ (#set A) λ b → #ord A b a

-- Induced order.
init-order : ∀ A a → rel (init A a)
init-order A a a+₁ a+₂ = #ord A (fst a+₁) (fst a+₂)

-- Induced order is still a well-founded.
init-is-well-founded : ∀ A a → is-well-founded (init A a) (init-order A a)
init-is-well-founded (A , ordA , transA , recA) a = (λ _ _ _ → transA _ _ _) , λ P indA+ b+ →
  recA (λ b → ∀ b<a → P (b , b<a)) (λ b ih b<a → indA+ (b , b<a) (λ c+ c<b → ih (fst c+) c<b (snd c+))) (fst b+) (snd b+)

-- Therefore the initial segment of a well-founded type is a well-founded type.
init-well-founded : (A : well-founded) → #set A → well-founded
init-well-founded A a = init A a , init-order A a , init-is-well-founded A a

-- Every initial segment can be embedded back to the original well-founded type.
embed-init-self : ∀ A a → embed (init-well-founded A a) A
embed-init-self A a = a , fst , snd , λ < → <

-- And smaller initial segments can be embedded into the larger ones.
embed-init-mono : ∀ A {b a} → #ord A b a → embed (init-well-founded A b) (init-well-founded A a)
embed-init-mono A {b} {a} b<a =
  (b , b<a) ,
  (λ b+ → fst b+ , #trans A _ _ _ (snd b+) b<a) ,
  snd ,
  id

-- Therefore, every well-founded type can be embedded into the type of all well-founded types,
-- where the upper bound is the well-founded type in question.
well-founded-is-max : ∀ A → embed A well-founded-well-founded
well-founded-is-max A = A , init-well-founded A , embed-init-self A , embed-init-mono A

-- It means that we can embed well-founded into well-founded itself.
absurd : ⊥
absurd = rec-irr well-founded-well-founded well-founded-well-founded (well-founded-is-max well-founded-well-founded)

This is really great! Defining well ordering from an induction principle is really elegant. I didn't see that in any of the papers you cited, did you come up with it?

Hello, I like it a lot too!

This development is very similar to Martin-Löf's presentation of Girard Paradox in his 1972 presentation of MLTT. However, he used nat-indexed sequences to define well-founded orderings.

I just translated this development to Dedukti and I remarked that the lemma init-is-tree-order uses twice the eta rule for sigma-types implicitely: the term ih (fst c+) c<b (snd c+) proves P (fst c+ , snd c+) instead of P c+ and similarly, the whole recA term proves P (fst b+ , snd b+) instead of P b+. Dedukti has no eta rule by default so I inserted the propositional eta rule ∀ (A : Set) (B : A → Set) (P : Σ A B → Set) (a : Σ A B) → P (fst a , snd a) → P a.