Random Girard stuff

Changes

1 changed files (+182/-0)

• Paradox.lean
  • @@ -30,3 +30,185 @@ theorem false : False :=
    -- 'false' depends on axioms: [Bad, bad] #print axioms _root_.false + + + + + def girard' (α : Type) (bad : (β : Type) × β ↪ α) : False := + and_not_self ⟨fun _ _ hab ↦ eq_of_heq (Sigma.mk.inj (bad.injective hab)).2, (bad ⟨Set α, ·⟩).cantor_injective⟩ + + + lemma blah (p : α → Prop) (x : α) (h : p x) : (Subtype.mk x h).val = x := by + grind + + theorem subtype_eq_implies_predicate_eq {A : Type 1} {P Q : A → Prop} + (h : {a : A // P a} = {a : A // Q a}) : ∀ a, P a ↔ Q a := by + intro a + constructor + · intro hpa + let a' : {x : A // P x} := ⟨a, hpa⟩ + have : a'.val = a := by + grind + rw [h] at a' + have : a = a'.val := by + exact blah P a hpa + exact this ▸ a'.prop + · intro hqa + have a' : {x : A // Q x} := ⟨a, hqa⟩ + have : a = a'.val := by + exact Subtype.mk + rw [← h] at a' + have : a = a'.val := by + sorry + exact this ▸ a'.prop + + + #check Function.surjective_iff_hasRightInverse + + theorem not_surjective_Type (f : Type → Type 1) : ¬f.Surjective := by + intro hf + -- let g := f.surjInv hf + -- have g.Injective := f.injective_surjInv hf + let T : Type 1 := Sigma f + cases hf (Set T) with | intro U hU => + let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩ + have hg : g.Injective := by + intro s t h + suffices cast hU (g s).2 = cast hU (g t).2 by + simp only [g, cast_cast, cast_eq] at this + assumption + · congr + exact g.cantor_injective hg + + + + def girard (f : Type (u + 1) ↪ Type u) : False := by + let g := f.toFun.invFun + have hg : g.Surjective := by + intro a + use f.toFun a + simp [g, Function.invFun] + let T := Sigma g + obtain ⟨U, hU⟩ := hg (Set T) + let k (s : Set T) : T := + ⟨U, cast hU.symm s⟩ + have hk : k.Injective := by + intro s t _ + have : cast hU (k s).2 = cast hU (k t).2 := by congr + simpa [k] + -- Now we have an injective function `k` from `Set α → α` (intuitively this is like a function from the power set to a set) which violates `Function.cantor_injective k` + -- Here's how to manually finish the proof + -- This is like the set of sets that don't contain themselves + let Q := { b : T | ∃ P, k P = b ∧ b ∉ P } + -- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q` + have down (h : k Q ∈ Q) : k Q ∉ Q := by + obtain ⟨P, hP⟩ := h + exact (hk hP.1) ▸ hP.2 + -- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition + have up (h : k Q ∉ Q) : k Q ∈ Q := + ⟨Q, rfl, h⟩ + -- Now use a diagonalization argument (alternatively, we can use the law of excluded middle) + let f := fun h ↦ down h h + exact f (up f) + + + + + + -- let hf := Function.invFun_surjective f.inj' + -- and_not_self ⟨Function.invFun_surjective f.inj', Function.not_surjective_Type.{1, 1} f.toFun.invFun⟩ + -- let T : Type 2 := Sigma bad + -- let k (P : Set T) : T := ⟨Set Type, P⟩ + -- have k_injective : k.Injective := by + -- intro a b hab + -- exact eq_of_heq (Sigma.mk.inj hab).2 + --eq_of_heq (Sigma.mk.inj (bad.injective hab)).2 + + + + -- let k (P : Set Type) : Type := bad P + -- have : k.Injective := by + -- intro a b hab + -- -- have := bad.injective hab + -- -- have : { x // a x } = { x // b x } := bad.injective hab + -- exact Set.ext <| subtype_eq_implies_predicate_eq <| bad.injective hab + -- exact and_not_self ⟨this, k.cantor_injective⟩ + + + + + -- The same proof works for any type in `Type`, not just `Unit` + -- Uncomment this line to prove false + axiom bad : Type 1 ↪ Type + + /-- An injective function from sets of `Unit` to `Unit` (internally, a `Set α` is an `α → Prop` predicate for set membership) -/ + noncomputable def k (P : Set Type) : Type := + bad P + + /-- `k` is injective because the sigma constructor and `bad` are injective -/ + lemma k_injective : k.Injective := + fun a b hab ↦ by + have := bad.injective hab + have blah : {x // x ∈ a} = {x // x ∈ b} := this + have : (fun x ↦ x ∈ a) = (fun x ↦ x ∈ b) := by + ext x + constructor + · intro h + let y : {x // x ∈ a} := ⟨x, h⟩ + have : x = y.val := by grind + let := cast blah y + have : x = this.val := by grind + + + by_cases h : ∃ y : {x // x ∈ a}, y = x + · obtain ⟨y, hy⟩ := h + have := cast blah y + have z : {x // x ∈ b} := ⟨y.val, by + have := y.prop + + ⟩ + · sorry + grind + + /-- This is like the set of sets that don't contain themselves -/ + def Q : Set Type := + { b : Type | ∃ P, k P = b ∧ b ∉ P } + + /-- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q` -/ + lemma down (h : k Q ∈ Q) : k Q ∉ Q := by + obtain ⟨P, hP⟩ := h + exact (k_injective hP.1) ▸ hP.2 + + /-- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition -/ + lemma up (h : k Q ∉ Q) : k Q ∈ Q := + ⟨Q, rfl, h⟩ + + /-- Now use a diagonalization argument (alternatively, we can use the law of excluded middle) -/ + theorem false : False := + let f := fun h ↦ down h h + f (up f) + + + + -- We can't actually assign `Type` a different type, but we can assume there's a bad injective function from a sigma (dependent product) type in `Type 1` to some type in `Type`. Intuitively, this sigma type is "too big" to fit in something in `Type`. (Thanks to Aaron Liu and Paul Reichert on the Lean Zulip for this proof.) + + def girard'' (α : Type) (bad : (β : Type) × β ↪ α) : False := by + -- An injective function from sets of `α` to `α` (internally, a `Set α` is an `α → Prop` predicate for set membership) + let k (P : Set α) : α := bad ⟨Set α, P⟩ + -- `k` is injective because the sigma constructor and `bad` are injective + have k_injective : k.Injective := + fun _ _ hab ↦ eq_of_heq (Sigma.mk.inj (bad.injective hab)).2 + -- Now we have an injective function `k` from `Set α → α` (intuitively this is like a function from the power set to a set) which violates `Function.cantor_injective k` + -- Here's how to manually finish the proof + -- This is like the set of sets that don't contain themselves + let Q := { b : α | ∃ P, k P = b ∧ b ∉ P } + -- If `k Q ∈ Q`, then there exists `P` with `k P = k Q` and `k Q ∉ P`, but `k` is injective so `P = Q` and `k Q ∉ Q` + have down (h : k Q ∈ Q) : k Q ∉ Q := by + obtain ⟨P, hP⟩ := h + exact (k_injective hP.1) ▸ hP.2 + -- If `k Q ∉ Q` then choose `P := Q` so `k Q ∈ Q` holds by definition + have up (h : k Q ∉ Q) : k Q ∈ Q := + ⟨Q, rfl, h⟩ + -- Now use a diagonalization argument (alternatively, we can use the law of excluded middle) + let f := fun h ↦ down h h + exact f (up f)