Kripke.Completeness

import Logic.Syntax
import Kripke.Frame
import Mathlib.Order.Zorn



namespace Kripke



open Classical


open Set


open Syntax



namespace Canonical



abbrev Theory := Set Tm



def ProvableFrom (T : Theory) (φ : Tm) : Prop :=
  ∃ Γ : Ctxt, (∀ ψ ∈ Γ, ψ ∈ T) ∧ Pf Γ φ



def Closed (T : Theory) : Prop :=
  ∀ ⦃φ : Tm⦄, ProvableFrom T φ → φ ∈ T



def Consistent (T : Theory) : Prop :=
  Tm.ff ∉ T



def Prime (T : Theory) : Prop :=
  ∀ ⦃φ ψ : Tm⦄, (φ ∨ ψ) ∈ T → φ ∈ T ∨ ψ ∈ T



def closure (T : Theory) : Theory := {φ | ProvableFrom T φ}



structure Admissible (S : Theory) (A : Tm) (T : Theory) : Prop where
  base : S ⊆ T
  closed : Closed T
  consistent : Consistent T
  avoids : A ∉ T



lemma subset_closure {T : Theory} : T ⊆ closure T := byT : Theory
⊢ T ⊆ closure T
  intro φ φ_in_TT : Theory
φ : Tm
φ_in_T : φ ∈ T
⊢ φ ∈ closure T
  refine ⟨[φ], ?_, ?_⟩refine_1T : Theory
φ : Tm
φ_in_T : φ ∈ T
⊢ ∀ ψ ∈ [φ], ψ ∈ T
refine_2T : Theory
φ : Tm
φ_in_T : φ ∈ T
⊢ Pf [φ] φ
  ·refine_1T : Theory
φ : Tm
φ_in_T : φ ∈ T
⊢ ∀ ψ ∈ [φ], ψ ∈ T intro ψ ψ_in_lsrefine_1T : Theory
φ : Tm
φ_in_T : φ ∈ T
ψ : Tm
ψ_in_ls : ψ ∈ [φ]
⊢ ψ ∈ T
    have : ψ = φ := byT : Theory
⊢ T ⊆ closure T
      simpa using ψ_in_ls
    simpa [this] using φ_in_T
  ·refine_2T : Theory
φ : Tm
φ_in_T : φ ∈ T
⊢ Pf [φ] φ exact Pf.assume



lemma closure_mono {S T : Theory} (S_in_T : S ⊆ T) : closure S ⊆ closure T := byS : Theory
T : Theory
S_in_T : S ⊆ T
⊢ closure S ⊆ closure T
  intro φ φ_in_clSS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
φ_in_clS : φ ∈ closure S
⊢ φ ∈ closure T
  rcases φ_in_clS with ⟨Γ, Γ_in_S, pf_φ⟩S : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ φ ∈ closure T
  exists ΓS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ (∀ ψ ∈ Γ, ψ ∈ T) ∧ Pf Γ φ
  constructorleftS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ ∀ ψ ∈ Γ, ψ ∈ T
rightS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ Pf Γ φ
  ·leftS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ ∀ ψ ∈ Γ, ψ ∈ T intro ψ ψ_in_ΓleftS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
ψ : Tm
ψ_in_Γ : ψ ∈ Γ
⊢ ψ ∈ T
    apply S_in_Tleft.aS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
ψ : Tm
ψ_in_Γ : ψ ∈ Γ
⊢ ψ ∈ S
    apply Γ_in_S ψ ψ_in_Γ
  ·rightS : Theory
T : Theory
S_in_T : S ⊆ T
φ : Tm
Γ : Ctxt
Γ_in_S : ∀ ψ ∈ Γ, ψ ∈ S
pf_φ : Pf Γ φ
⊢ Pf Γ φ exact pf_φ



lemma provable_merge {T : Theory} :
    ∀ Γ : Ctxt, (∀ ψ ∈ Γ, ProvableFrom T ψ) →
      ∃ Δ : Ctxt, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ ∈ Γ, Pf Δ ψ
  | [], _ =>T : Theory
x✝ : ∀ ψ ∈ [], ProvableFrom T ψ
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ ∈ [], Pf Δ ψ byT : Theory
x✝ : ∀ ψ ∈ [], ProvableFrom T ψ
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ ∈ [], Pf Δ ψ
    exists []T : Theory
x✝ : ∀ ψ ∈ [], ProvableFrom T ψ
⊢ (∀ ξ ∈ [], ξ ∈ T) ∧ ∀ ψ ∈ [], Pf [] ψ
    aesop
  | ψ :: Γ, Γ_from_T =>T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ_1 ∈ ψ :: Γ, Pf Δ ψ_1 byT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ_1 ∈ ψ :: Γ, Pf Δ ψ_1
      rcases Γ_from_T ψ (byT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
⊢ ψ ∈ ψ :: Γ simp) with ⟨Δψ, Δψ_in_T, pf_ψ⟩
      have Γ_T : ∀ ξ ∈ Γ , ProvableFrom T ξ := byT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ_1 ∈ ψ :: Γ, Pf Δ ψ_1
        intro ξ ξ_in_ΓT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
⊢ ProvableFrom T ξ
        apply Γ_from_TaT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
⊢ ξ ∈ ψ :: Γ
        simp [ξ_in_Γ]
      rcases provable_merge Γ Γ_T with ⟨Δ, Δ_in_T, pf_Γ⟩T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ_1 ∈ ψ :: Γ, Pf Δ ψ_1
      -- Δψ is a context from which we can prove φ
      -- Δ is a context from which we can prove each of Γ
      -- so the concatenation should be able to prove φ :: Γ
      set tot_Γ : Ctxt := Δψ ++ ΔT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
⊢ ∃ Δ, (∀ ξ ∈ Δ, ξ ∈ T) ∧ ∀ ψ_1 ∈ ψ :: Γ, Pf Δ ψ_1
      refine ⟨tot_Γ, ?_, ?_⟩refine_1T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
⊢ ∀ ξ ∈ tot_Γ, ξ ∈ T
refine_2T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
⊢ ∀ ψ_1 ∈ ψ :: Γ, Pf tot_Γ ψ_1
      ·refine_1T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
⊢ ∀ ξ ∈ tot_Γ, ξ ∈ T intro ξ ξ_in_totrefine_1T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ tot_Γ
⊢ ξ ∈ T
        simp [tot_Γ] at ξ_in_totrefine_1T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
⊢ ξ ∈ T
        apply ξ_in_tot.elimrefine_1.leftT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
⊢ ξ ∈ Δψ → ξ ∈ T
refine_1.rightT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
⊢ ξ ∈ Δ → ξ ∈ T
        ·refine_1.leftT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
⊢ ξ ∈ Δψ → ξ ∈ T intro ξ_in_Δψrefine_1.leftT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
ξ_in_Δψ : ξ ∈ Δψ
⊢ ξ ∈ T; exact Δψ_in_T ξ ξ_in_Δψ
        ·refine_1.rightT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
⊢ ξ ∈ Δ → ξ ∈ T intro ξ_in_Δrefine_1.rightT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_tot : ξ ∈ Δψ ∨ ξ ∈ Δ
ξ_in_Δ : ξ ∈ Δ
⊢ ξ ∈ T; exact Δ_in_T ξ ξ_in_Δ
      ·refine_2T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
⊢ ∀ ψ_1 ∈ ψ :: Γ, Pf tot_Γ ψ_1 intro ξ ξ_in_Γ'refine_2T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_Γ' : ξ ∈ ψ :: Γ
⊢ Pf tot_Γ ξ
        simp at ξ_in_Γ'refine_2T : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
ξ_in_Γ' : ξ = ψ ∨ ξ ∈ Γ
⊢ Pf tot_Γ ξ
        rcases ξ_in_Γ' with rfl | hξrefine_2.inlT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ Pf tot_Γ ξ
refine_2.inrT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ Pf tot_Γ ξ
        ·refine_2.inlT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ Pf tot_Γ ξ apply Pf.monotone_mem Δψ (Δψ ++ Δ)refine_2.inl.hmemT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ ∀ Q ∈ Δψ, Q ∈ Δψ ++ Δ
refine_2.inl.aT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ Pf Δψ ξ
          ·refine_2.inl.hmemT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ ∀ Q ∈ Δψ, Q ∈ Δψ ++ Δ intro tm tm_in_Δψrefine_2.inl.hmemT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
tm : Tm
tm_in_Δψ : tm ∈ Δψ
⊢ tm ∈ Δψ ++ Δ
            simp [tm_in_Δψ]
          ·refine_2.inl.aT : Theory
Γ : List Tm
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
Γ_from_T : ∀ ψ ∈ ξ :: Γ, ProvableFrom T ψ
pf_ψ : Pf Δψ ξ
⊢ Pf Δψ ξ exact pf_ψ
        ·refine_2.inrT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ Pf tot_Γ ξ apply Pf.monotone_mem Δ (Δψ ++ Δ)refine_2.inr.hmemT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ ∀ Q ∈ Δ, Q ∈ Δψ ++ Δ
refine_2.inr.aT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ Pf Δ ξ
          ·refine_2.inr.hmemT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ ∀ Q ∈ Δ, Q ∈ Δψ ++ Δ intro tm tm_in_Δrefine_2.inr.hmemT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
tm : Tm
tm_in_Δ : tm ∈ Δ
⊢ tm ∈ Δψ ++ Δ
            simp [tm_in_Δ]
          ·refine_2.inr.aT : Theory
ψ : Tm
Γ : List Tm
Γ_from_T : ∀ ψ_1 ∈ ψ :: Γ, ProvableFrom T ψ_1
Δψ : Ctxt
Δψ_in_T : ∀ ψ ∈ Δψ, ψ ∈ T
pf_ψ : Pf Δψ ψ
Γ_T : ∀ ξ ∈ Γ, ProvableFrom T ξ
Δ : Ctxt
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
pf_Γ : ∀ ψ ∈ Γ, Pf Δ ψ
tot_Γ : Ctxt := Δψ ++ Δ
ξ : Tm
hξ : ξ ∈ Γ
⊢ Pf Δ ξ exact (pf_Γ ξ hξ)



lemma provableFrom_of_pf {T : Theory} {Γ : Ctxt} {φ : Tm}
    (hΓ : ∀ ψ ∈ Γ, ProvableFrom T ψ) (hpf : Pf Γ φ) : ProvableFrom T φ := byT : Theory
Γ : Ctxt
φ : Tm
hΓ : ∀ ψ ∈ Γ, ProvableFrom T ψ
hpf : Pf Γ φ
⊢ ProvableFrom T φ
  rcases provable_merge Γ hΓ with ⟨Δ, hΔ, hproofs⟩T : Theory
Γ : Ctxt
φ : Tm
hΓ : ∀ ψ ∈ Γ, ProvableFrom T ψ
hpf : Pf Γ φ
Δ : Ctxt
hΔ : ∀ ξ ∈ Δ, ξ ∈ T
hproofs : ∀ ψ ∈ Γ, Pf Δ ψ
⊢ ProvableFrom T φ
  exact ⟨Δ, hΔ, Pf.multicut hpf hproofs⟩



lemma closure_closed (T : Theory) : Closed (closure T) := byT : Theory
⊢ Closed (closure T)
  intro φ hφT : Theory
φ : Tm
hφ : ProvableFrom (closure T) φ
⊢ φ ∈ closure T
  rcases hφ with ⟨Γ, hΓ, hpf⟩T : Theory
φ : Tm
Γ : Ctxt
hΓ : ∀ ψ ∈ Γ, ψ ∈ closure T
hpf : Pf Γ φ
⊢ φ ∈ closure T
  exact provableFrom_of_pf hΓ hpf



def contextSet (Γ : Ctxt) : Theory := {φ | φ ∈ Γ}



def theoryOf (Γ : Ctxt) : Theory := closure (contextSet Γ)



lemma mem_theoryOf {Γ : Ctxt} {φ : Tm} : φ ∈ theoryOf Γ ↔ Pf Γ φ := byΓ : Ctxt
φ : Tm
⊢ φ ∈ theoryOf Γ ↔ Pf Γ φ
  constructormpΓ : Ctxt
φ : Tm
⊢ φ ∈ theoryOf Γ → Pf Γ φ
mprΓ : Ctxt
φ : Tm
⊢ Pf Γ φ → φ ∈ theoryOf Γ
  ·mpΓ : Ctxt
φ : Tm
⊢ φ ∈ theoryOf Γ → Pf Γ φ intro φ_in_Γ_ThmpΓ : Ctxt
φ : Tm
φ_in_Γ_Th : φ ∈ theoryOf Γ
⊢ Pf Γ φ
    rcases φ_in_Γ_Th with ⟨Δ, Δ_in_Γ, φ_pf⟩mpΓ : Ctxt
φ : Tm
Δ : Ctxt
Δ_in_Γ : ∀ ψ ∈ Δ, ψ ∈ contextSet Γ
φ_pf : Pf Δ φ
⊢ Pf Γ φ
    apply Pf.multicut φ_pfmpΓ : Ctxt
φ : Tm
Δ : Ctxt
Δ_in_Γ : ∀ ψ ∈ Δ, ψ ∈ contextSet Γ
φ_pf : Pf Δ φ
⊢ ∀ Q ∈ Δ, Pf Γ Q
    intro ψ ψ_in_ΔmpΓ : Ctxt
φ : Tm
Δ : Ctxt
Δ_in_Γ : ∀ ψ ∈ Δ, ψ ∈ contextSet Γ
φ_pf : Pf Δ φ
ψ : Tm
ψ_in_Δ : ψ ∈ Δ
⊢ Pf Γ ψ
    exact Pf.of_mem (Δ_in_Γ ψ ψ_in_Δ)
  ·mprΓ : Ctxt
φ : Tm
⊢ Pf Γ φ → φ ∈ theoryOf Γ intro pf_ΨmprΓ : Ctxt
φ : Tm
pf_Ψ : Pf Γ φ
⊢ φ ∈ theoryOf Γ
    simp [theoryOf, closure, ProvableFrom]mprΓ : Ctxt
φ : Tm
pf_Ψ : Pf Γ φ
⊢ ∃ Γ_1, (∀ ψ ∈ Γ_1, ψ ∈ contextSet Γ) ∧ Pf Γ_1 φ
    exists ΓmprΓ : Ctxt
φ : Tm
pf_Ψ : Pf Γ φ
⊢ (∀ ψ ∈ Γ, ψ ∈ contextSet Γ) ∧ Pf Γ φ
    aesop




lemma contextSet_mem {Γ : Ctxt} {φ : Tm} (φ_in_Γ : φ ∈ Γ) : φ ∈ theoryOf Γ :=
  subset_closure φ_in_Γ



-- if a context is provably from a union of a chain of theories,
-- then there is some theory that proves everything in the context
lemma chain_member_for_ctxt
   {c : Set Theory} (hc : IsChain (· ⊆ ·) c) (hne : c.Nonempty) :
    ∀ Γ : Ctxt, (∀ ψ ∈ Γ, ψ ∈ sUnion c) → ∃ T ∈ c, ∀ ψ ∈ Γ, ψ ∈ T
  | [], hΓ =>c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hΓ : ∀ ψ ∈ [], ψ ∈ ⋃₀ c
⊢ ∃ T ∈ c, ∀ ψ ∈ [], ψ ∈ T byc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hΓ : ∀ ψ ∈ [], ψ ∈ ⋃₀ c
⊢ ∃ T ∈ c, ∀ ψ ∈ [], ψ ∈ T
      rcases hne with ⟨T, T_in_c⟩c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hΓ : ∀ ψ ∈ [], ψ ∈ ⋃₀ c
T : Theory
T_in_c : T ∈ c
⊢ ∃ T ∈ c, ∀ ψ ∈ [], ψ ∈ T
      exists Tc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hΓ : ∀ ψ ∈ [], ψ ∈ ⋃₀ c
T : Theory
T_in_c : T ∈ c
⊢ T ∈ c ∧ ∀ ψ ∈ [], ψ ∈ T
      aesop
  | ψ :: Γ, Γ_in =>c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T byc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
      rcases Γ_in ψ (byc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
⊢ ψ ∈ ψ :: Γ simp) with ⟨Tψ, Tψ_in_c, ψ_in_Tψ⟩
      have : ∃ T ∈ c, ∀ ψ ∈ Γ, ψ ∈ T := byc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
        apply chain_member_for_ctxt hc hne Γc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
⊢ ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
        aesop
      rcases this with ⟨TΓ, TΓ_in_c, Γ_in_TΓ⟩c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
      by_cases hEq : Tψ = TΓposc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : Tψ = TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
negc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
      ·posc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : Tψ = TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T refine ⟨TΓ, TΓ_in_c, ?_⟩posc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : Tψ = TΓ
⊢ ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ TΓ
        aesop
      ·negc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T rcases hc Tψ_in_c TΓ_in_c hEq with hsub | hsubneg.inlc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : Tψ ⊆ TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
neg.inrc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : TΓ ⊆ Tψ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T
        ·neg.inlc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : Tψ ⊆ TΓ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T refine ⟨TΓ, TΓ_in_c, ?_⟩neg.inlc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : Tψ ⊆ TΓ
⊢ ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ TΓ
          aesop
        ·neg.inrc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : TΓ ⊆ Tψ
⊢ ∃ T ∈ c, ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ T refine ⟨Tψ, Tψ_in_c, ?_⟩neg.inrc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
ψ : Tm
Γ : List Tm
Γ_in : ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ ⋃₀ c
Tψ : Set Tm
Tψ_in_c : Tψ ∈ c
ψ_in_Tψ : ψ ∈ Tψ
TΓ : Theory
TΓ_in_c : TΓ ∈ c
Γ_in_TΓ : ∀ ψ ∈ Γ, ψ ∈ TΓ
hEq : ¬Tψ = TΓ
hsub : TΓ ⊆ Tψ
⊢ ∀ ψ_1 ∈ ψ :: Γ, ψ_1 ∈ Tψ
          aesop



lemma sUnion_closed {c : Set Theory} (hc : IsChain (· ⊆ ·) c) (hne : c.Nonempty)
    (hclosed : ∀ T ∈ c, Closed T) : Closed (sUnion c) := byc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
⊢ Closed (⋃₀ c)
  intro φ φ_provc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
φ_prov : ProvableFrom (⋃₀ c) φ
⊢ φ ∈ ⋃₀ c
  rcases φ_prov with ⟨Γ, Γ_in_union, φ_pf⟩c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
⊢ φ ∈ ⋃₀ c
  rcases chain_member_for_ctxt hc hne Γ Γ_in_union with ⟨T, T_in_c, φ_in_T⟩c : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ φ ∈ ⋃₀ c
  apply mem_sUnion_of_memhxc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ φ ∈ ?t
htc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ ?t ∈ c
tc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ Set Tm
  ·hxc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ φ ∈ ?t apply hclosed T T_in_chx.ac : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ ProvableFrom T φ
    exact ⟨Γ, φ_in_T, φ_pf⟩
  ·htc : Set Theory
hc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hne : c.Nonempty
hclosed : ∀ T ∈ c, Closed T
φ : Tm
Γ : Ctxt
Γ_in_union : ∀ ψ ∈ Γ, ψ ∈ ⋃₀ c
φ_pf : Pf Γ φ
T : Theory
T_in_c : T ∈ c
φ_in_T : ∀ ψ ∈ Γ, ψ ∈ T
⊢ ?t ∈ c exact T_in_c



lemma closure_insert_imp {T : Theory} {φ tm : Tm} (T_closed : Closed T)
    (htm : tm ∈ closure (Set.insert φ T)) : (φ ⇒ tm) ∈ T := byT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
htm : tm ∈ closure (Set.insert φ T)
⊢ (φ ⇒ tm) ∈ T
  rcases htm with ⟨Γ, Γ_in_T', pf_tm⟩T : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
⊢ (φ ⇒ tm) ∈ T
  let Δ : Ctxt := Γ.filter (· ∈ T)T : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
⊢ (φ ⇒ tm) ∈ T
  have Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T := byT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
htm : tm ∈ closure (Set.insert φ T)
⊢ (φ ⇒ tm) ∈ T
    intro ξ hξT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
ξ : Tm
hξ : ξ ∈ Δ
⊢ ξ ∈ T
    simp [Δ] at hξT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
ξ : Tm
hξ : ξ ∈ Γ ∧ ξ ∈ T
⊢ ξ ∈ T
    exact hξ.2
  have tm_ass_φ : Pf (φ :: Δ) tm := byT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
htm : tm ∈ closure (Set.insert φ T)
⊢ (φ ⇒ tm) ∈ T
    apply Pf.multicut pf_tmT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
⊢ ∀ Q ∈ Γ, Pf (φ :: Δ) Q
    intro ξ ξ_in_ΓT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
⊢ Pf (φ :: Δ) ξ
    have ξ_in_T' := Γ_in_T' ξ ξ_in_ΓT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
ξ_in_T' : ξ ∈ Set.insert φ T
⊢ Pf (φ :: Δ) ξ
    rcases ξ_in_T' with rfl | ξ_in_TinlT : Theory
tm : Tm
T_closed : Closed T
Γ : Ctxt
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert ξ T
⊢ Pf (ξ :: Δ) ξ
inrT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
ξ_in_T : ξ ∈ T
⊢ Pf (φ :: Δ) ξ
    ·inlT : Theory
tm : Tm
T_closed : Closed T
Γ : Ctxt
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert ξ T
⊢ Pf (ξ :: Δ) ξ exact Pf.assume
    ·inrT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
ξ : Tm
ξ_in_Γ : ξ ∈ Γ
ξ_in_T : ξ ∈ T
⊢ Pf (φ :: Δ) ξ have ξ_in_Δ' : ξ ∈ φ :: Δ := byT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
htm : tm ∈ closure (Set.insert φ T)
⊢ (φ ⇒ tm) ∈ T
        simp [Δ, ξ_in_Γ, ξ_in_T]
      exact Pf.of_mem ξ_in_Δ'
  apply T_closedaT : Theory
φ : Tm
tm : Tm
T_closed : Closed T
Γ : Ctxt
Γ_in_T' : ∀ ψ ∈ Γ, ψ ∈ Set.insert φ T
pf_tm : Pf Γ tm
Δ : Ctxt := List.filter (fun x => decide (x ∈ T)) Γ
Δ_in_T : ∀ ξ ∈ Δ, ξ ∈ T
tm_ass_φ : Pf (φ :: Δ) tm
⊢ ProvableFrom T (φ ⇒ tm)
  exact ⟨Δ, Δ_in_T, Pf.imp_I tm_ass_φ⟩





lemma closure_insert_failure {S T : Theory} {A φ : Tm}
    (hbase : S ⊆ T) (hnot :
      ¬ Admissible S A (closure (Set.insert φ T))) : A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T) := byS : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
⊢ A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T)
  by_contra hfailS : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ False
  apply hnotS : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ Admissible S A (closure (Set.insert φ T))
  refine ⟨?_, closure_closed _, ?_, ?_⟩refine_1S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ S ⊆ closure (Set.insert φ T)
refine_2S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ Consistent (closure (Set.insert φ T))
refine_3S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ A ∉ closure (Set.insert φ T)
  ·refine_1S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ S ⊆ closure (Set.insert φ T) intro χ hχrefine_1S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
χ : Tm
hχ : χ ∈ S
⊢ χ ∈ closure (Set.insert φ T)
    exact subset_closure (Or.inr (hbase hχ))
  ·refine_2S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ Consistent (closure (Set.insert φ T)) intro hffrefine_2S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
hff : Tm.ff ∈ closure (Set.insert φ T)
⊢ False
    exact hfail (Or.inr hff)
  ·refine_3S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
⊢ A ∉ closure (Set.insert φ T) intro hArefine_3S : Theory
T : Theory
A : Tm
φ : Tm
hbase : S ⊆ T
hnot : ¬Admissible S A (closure (Set.insert φ T))
hfail : ¬(A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T))
hA : A ∈ closure (Set.insert φ T)
⊢ False
    exact hfail (Or.inl hA)



lemma imp_target_of_failure {T : Theory} {φ A : Tm} (T_closed : Closed T)
    (ext_with : A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T)) :
    (φ ⇒ A) ∈ T := byT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ext_with : A ∈ closure (Set.insert φ T) ∨ Tm.ff ∈ closure (Set.insert φ T)
⊢ (φ ⇒ A) ∈ T
  rcases ext_with with A_in_T' | ff_in_T'inlT : Theory
φ : Tm
A : Tm
T_closed : Closed T
A_in_T' : A ∈ closure (Set.insert φ T)
⊢ (φ ⇒ A) ∈ T
inrT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
⊢ (φ ⇒ A) ∈ T
  ·inlT : Theory
φ : Tm
A : Tm
T_closed : Closed T
A_in_T' : A ∈ closure (Set.insert φ T)
⊢ (φ ⇒ A) ∈ T exact closure_insert_imp T_closed A_in_T'
  ·inrT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
⊢ (φ ⇒ A) ∈ T have neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T := closure_insert_imp T_closed ff_in_T'inrT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ (φ ⇒ A) ∈ T
    apply T_closedinr.aT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ ProvableFrom T (φ ⇒ A)
    exists [φ ⇒ Tm.ff]inr.aT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ (∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ T) ∧ Pf [φ ⇒ Tm.ff] (φ ⇒ A)
    constructorinr.a.leftT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ ∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ T
inr.a.rightT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ Pf [φ ⇒ Tm.ff] (φ ⇒ A)
    ·inr.a.leftT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ ∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ T simpa using neg_φ_in_T
    ·inr.a.rightT : Theory
φ : Tm
A : Tm
T_closed : Closed T
ff_in_T' : Tm.ff ∈ closure (Set.insert φ T)
neg_φ_in_T : (φ ⇒ Tm.ff) ∈ T
⊢ Pf [φ ⇒ Tm.ff] (φ ⇒ A) exact Pf.quodlibet φ A




theorem prime_extension_avoiding {S : Theory} {A : Tm}
    (S_closed : Closed S) (S_consistent : Consistent S) (not_A_in_S : A ∉ S) :
    ∃ T, Admissible S A T ∧ Prime T := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
  let candidates : Set Theory := {T | Admissible S A T}S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
⊢ ∃ T, Admissible S A T ∧ Prime T
  have S_in_candidates : S ∈ candidates :=
    ⟨subset_rfl, S_closed, S_consistent, not_A_in_S⟩S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ ∃ T, Admissible S A T ∧ Prime T
  obtain ⟨M, hSM, M_maximal⟩ : ∃ m, S ⊆ m ∧ Maximal (· ∈ candidates) m := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ ∃ m, S ⊆ m ∧ Maximal (fun x => x ∈ candidates) m
    -- if we for any non-empty chain c in candidates, we have an upper bound (also in candidates),
    -- then for any candidate we can find a maximal candidate set containing it
    apply zorn_subset_nonempty candidatesHS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ ∀ c ⊆ candidates, IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ candidates, ∀ s ∈ c, s ⊆ ub
hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates
    intro c c_in_CHS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
⊢ IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ candidates, ∀ s ∈ c, s ⊆ ub
hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates hcChainHS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
⊢ c.Nonempty → ∃ ub ∈ candidates, ∀ s ∈ c, s ⊆ ub
hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates c_neHS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
⊢ ∃ ub ∈ candidates, ∀ s ∈ c, s ⊆ ub
hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates
    refine ⟨sUnion c, ?_, ?_⟩H.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
⊢ ⋃₀ c ∈ candidates
H.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates
    -- show that the union of a chain is a candidate
    have union_closed : Closed (⋃₀ c) := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ ∃ m, S ⊆ m ∧ Maximal (fun x => x ∈ candidates) m
      apply sUnion_closed hcChain c_neS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
⊢ ∀ T ∈ c, Closed T
      intro T T_in_cS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
T : Theory
T_in_c : T ∈ c
⊢ Closed T
      apply (c_in_C T_in_c).closed
    ·H.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ ⋃₀ c ∈ candidates refine ⟨?_, union_closed , ?_, ?_⟩H.refine_1.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ S ⊆ ⋃₀ c
H.refine_1.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ Consistent (⋃₀ c)
H.refine_1.refine_3S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ A ∉ ⋃₀ c
      ·H.refine_1.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ S ⊆ ⋃₀ c intro φ φ_in_SH.refine_1.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
φ : Tm
φ_in_S : φ ∈ S
⊢ φ ∈ ⋃₀ c
        rcases c_ne with ⟨tms, tms_in_c⟩H.refine_1.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
union_closed : Closed (⋃₀ c)
φ : Tm
φ_in_S : φ ∈ S
tms : Set Tm
tms_in_c : tms ∈ c
⊢ φ ∈ ⋃₀ c
        -- φ is in S and so in any candidate admissible theory
        have φ_in_tms : φ ∈ tms := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ ∃ m, S ⊆ m ∧ Maximal (fun x => x ∈ candidates) m
          apply (c_in_C tms_in_c).baseaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
union_closed : Closed (⋃₀ c)
φ : Tm
φ_in_S : φ ∈ S
tms : Set Tm
tms_in_c : tms ∈ c
⊢ φ ∈ S
          exact φ_in_S
        apply mem_sUnion_of_mem φ_in_tmsH.refine_1.refine_1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
union_closed : Closed (⋃₀ c)
φ : Tm
φ_in_S : φ ∈ S
tms : Set Tm
tms_in_c : tms ∈ c
φ_in_tms : φ ∈ tms
⊢ tms ∈ c
        exact tms_in_c
      ·H.refine_1.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ Consistent (⋃₀ c) intro ff_in_UcH.refine_1.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
ff_in_Uc : Tm.ff ∈ ⋃₀ c
⊢ False
        rcases ff_in_Uc with ⟨T, T_in_c, ff_in_T⟩H.refine_1.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
T : Set Tm
T_in_c : T ∈ c
ff_in_T : Tm.ff ∈ T
⊢ False
        exact (c_in_C T_in_c).consistent ff_in_T
      ·H.refine_1.refine_3S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
⊢ A ∉ ⋃₀ c intro A_in_UcH.refine_1.refine_3S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
A_in_Uc : A ∈ ⋃₀ c
⊢ False
        rcases A_in_Uc with ⟨T, T_in_c, A_in_T⟩H.refine_1.refine_3S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
union_closed : Closed (⋃₀ c)
T : Set Tm
T_in_c : T ∈ c
A_in_T : A ∈ T
⊢ False
        exact (c_in_C T_in_c).avoids A_in_T
    ·H.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c intro s s_in_cH.refine_2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
c : Set (Set Tm)
c_in_C : c ⊆ candidates
hcChain : IsChain (fun x1 x2 => x1 ⊆ x2) c
c_ne : c.Nonempty
s : Set Tm
s_in_c : s ∈ c
⊢ s ⊆ ⋃₀ c
      exact subset_sUnion_of_mem s_in_c
    ·hxS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
⊢ S ∈ candidates exact S_in_candidates
  have M_admissible : Admissible S A M := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    apply M_maximal.1
  refine ⟨M, M_admissible, ?_⟩S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
⊢ Prime M
  -- prove that M = ⋃₀ c is prime:
  intro φ ψS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
⊢ (φ ∨ ψ) ∈ M → φ ∈ M ∨ ψ ∈ M or_in_MS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
⊢ φ ∈ M ∨ ψ ∈ M
  by_contra hPrimeS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : ¬(φ ∈ M ∨ ψ ∈ M)
⊢ False
  push Not at hPrimeS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
⊢ False
  have not_φ_in_M : φ ∉ M := hPrime.1S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
⊢ False
  have not_ψ_in_M : ψ ∉ M := hPrime.2S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
⊢ False
  let Mφ : Theory := closure (Set.insert φ M)S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
⊢ False
  let Mψ : Theory := closure (Set.insert ψ M)S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
⊢ False
  have hMφ : M ⊆ Mφ := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    intro tm tm_in_MS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
tm : Tm
tm_in_M : tm ∈ M
⊢ tm ∈ Mφ
    apply subset_closureaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
tm : Tm
tm_in_M : tm ∈ M
⊢ tm ∈ Set.insert φ M
    exact Or.inr tm_in_M
  have hMψ : M ⊆ Mψ := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    intro tm tm_in_MS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
tm : Tm
tm_in_M : tm ∈ M
⊢ tm ∈ Mψ
    apply subset_closureaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
tm : Tm
tm_in_M : tm ∈ M
⊢ tm ∈ Set.insert ψ M
    exact Or.inr tm_in_M
  -- neither Mφ not Mψ are admissible as then they would be equal to M
  -- by maximality, but then either φ or ψ would be in M
  have Mφ_not_addmissble : ¬ Admissible S A Mφ := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    intro Mφ_admissibleS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
⊢ False
    have hEq : M = Mφ := M_maximal.eq_of_subset Mφ_admissible hMφS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
hEq : M = Mφ
⊢ False
    apply not_φ_in_MS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
hEq : M = Mφ
⊢ φ ∈ M
    rw [hEq]S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
hEq : M = Mφ
⊢ φ ∈ Mφ
    apply subset_closureaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
hEq : M = Mφ
⊢ φ ∈ Set.insert φ M
    apply Or.inla.hS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_admissible : Admissible S A Mφ
hEq : M = Mφ
⊢ φ = φ
    rfl
  have Mψ_not_admissible : ¬ Admissible S A Mψ := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    intro Mψ_admissibleS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
⊢ False
    have hEq : M = Mψ := M_maximal.eq_of_subset Mψ_admissible hMψS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
hEq : M = Mψ
⊢ False
    apply not_ψ_in_MS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
hEq : M = Mψ
⊢ ψ ∈ M
    rw [hEq]S : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
hEq : M = Mψ
⊢ ψ ∈ Mψ
    apply subset_closureaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
hEq : M = Mψ
⊢ ψ ∈ Set.insert ψ M
    apply Or.inla.hS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_admissible : Admissible S A Mψ
hEq : M = Mψ
⊢ ψ = ψ
    rfl
  have φ_imp_A_in_M : (φ ⇒ A) ∈ M := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    apply imp_target_of_failureT_closedS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
⊢ Closed M
ext_withS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
⊢ A ∈ closure (Set.insert φ M) ∨ Tm.ff ∈ closure (Set.insert φ M)
    apply M_admissible.closedext_withS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
⊢ A ∈ closure (Set.insert φ M) ∨ Tm.ff ∈ closure (Set.insert φ M)
    apply (closure_insert_failure M_admissible.base Mφ_not_addmissble)
  have ψ_imp_A_in_M : (ψ ⇒ A) ∈ M := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    apply imp_target_of_failureT_closedS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
⊢ Closed M
ext_withS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
⊢ A ∈ closure (Set.insert ψ M) ∨ Tm.ff ∈ closure (Set.insert ψ M)
    apply M_admissible.closedext_withS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
⊢ A ∈ closure (Set.insert ψ M) ∨ Tm.ff ∈ closure (Set.insert ψ M)
    apply closure_insert_failure M_admissible.base Mψ_not_admissible
  have hA : A ∈ M := byS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
⊢ ∃ T, Admissible S A T ∧ Prime T
    apply M_admissible.closedaS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ ProvableFrom M A
    ·aS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ ProvableFrom M A exists [φ ∨ ψ, φ ⇒ A, ψ ⇒ A]aS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (∀ ψ_1 ∈ [φ ∨ ψ, φ ⇒ A, ψ ⇒ A], ψ_1 ∈ M) ∧ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A
      constructora.leftS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ ∀ ψ_1 ∈ [φ ∨ ψ, φ ⇒ A, ψ ⇒ A], ψ_1 ∈ M
a.rightS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A
      ·a.leftS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ ∀ ψ_1 ∈ [φ ∨ ψ, φ ⇒ A, ψ ⇒ A], ψ_1 ∈ M intro tm tm_in_ctxta.leftS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
tm : Tm
tm_in_ctxt : tm ∈ [φ ∨ ψ, φ ⇒ A, ψ ⇒ A]
⊢ tm ∈ M
        simp at tm_in_ctxta.leftS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
tm : Tm
tm_in_ctxt : tm = (φ ∨ ψ) ∨ tm = (φ ⇒ A) ∨ tm = (ψ ⇒ A)
⊢ tm ∈ M
        rcases tm_in_ctxt with rfl | rfl | rfla.left.inlS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (φ ∨ ψ) ∈ M
a.left.inr.inlS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (φ ⇒ A) ∈ M
a.left.inr.inrS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (ψ ⇒ A) ∈ M
        ·a.left.inlS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (φ ∨ ψ) ∈ M exact or_in_M
        ·a.left.inr.inlS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (φ ⇒ A) ∈ M exact φ_imp_A_in_M
        ·a.left.inr.inrS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ (ψ ⇒ A) ∈ M exact ψ_imp_A_in_M
      ·a.rightS : Theory
A : Tm
S_closed : Closed S
S_consistent : Consistent S
not_A_in_S : A ∉ S
candidates : Set Theory := {T | Admissible S A T}
S_in_candidates : S ∈ candidates
M : Theory
hSM : S ⊆ M
M_maximal : Maximal (fun x => x ∈ candidates) M
M_admissible : Admissible S A M
φ : Tm
ψ : Tm
or_in_M : (φ ∨ ψ) ∈ M
hPrime : φ ∉ M ∧ ψ ∉ M
not_φ_in_M : φ ∉ M
not_ψ_in_M : ψ ∉ M
Mφ : Theory := closure (Set.insert φ M)
Mψ : Theory := closure (Set.insert ψ M)
hMφ : M ⊆ Mφ
hMψ : M ⊆ Mψ
Mφ_not_addmissble : ¬Admissible S A Mφ
Mψ_not_admissible : ¬Admissible S A Mψ
φ_imp_A_in_M : (φ ⇒ A) ∈ M
ψ_imp_A_in_M : (ψ ⇒ A) ∈ M
⊢ Pf [φ ∨ ψ, φ ⇒ A, ψ ⇒ A] A exact Pf.or_cases_to φ ψ A
  exact M_admissible.avoids hA



structure World where
  carrier : Theory
  closed : Closed carrier
  consistent : Consistent carrier
  prime : Prime carrier



instance : LE World where
  le w v := w.carrier ⊆ v.carrier



instance : Preorder World where
  le := (· ≤ ·)
  le_refl _ := subset_rfl
  le_trans _ _ _ := Set.Subset.trans



instance : Frame World where
  val w i := Tm.var i ∈ w.carrier
  le_val := by⊢ ∀ {w w' : World} {i : ℕ}, w ≤ w' → Tm.var i ∈ w.carrier → Tm.var i ∈ w'.carrier aesop




theorem truth_lemma (w : World) : ∀ φ : Tm, at_world w φ ↔ φ ∈ w.carrier
  | Tm.var i => Iff.rfl
  | Tm.and φ ψ =>w : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier
      constructormpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) → (φ ∧ ψ) ∈ w.carrier
mprw : World
φ : Tm
ψ : Tm
⊢ (φ ∧ ψ) ∈ w.carrier → at_world w (φ ∧ ψ)
      ·mpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) → (φ ∧ ψ) ∈ w.carrier intro at_w_andmpw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
⊢ (φ ∧ ψ) ∈ w.carrier
        have hφ : φ ∈ w.carrier := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier
          rw [<- truth_lemma w φ]w : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
⊢ at_world w φ
          apply And.leftselfw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
⊢ at_world w φ ∧ ?b
bw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
⊢ Prop
          apply at_w_and
        have hψ : ψ ∈ w.carrier := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier
          rw [<- truth_lemma w ψ]w : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
⊢ at_world w ψ
          apply And.rightselfw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
⊢ ?a ∧ at_world w ψ
aw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
⊢ Prop
          apply at_w_and
        -- use that w is deductively closed
        apply w.closedmp.aw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ ProvableFrom w.carrier (φ ∧ ψ)
        exists [φ, ψ]mp.aw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ (∀ ψ_1 ∈ [φ, ψ], ψ_1 ∈ w.carrier) ∧ Pf [φ, ψ] (φ ∧ ψ)
        constructormp.a.leftw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ, ψ], ψ_1 ∈ w.carrier
mp.a.rightw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ Pf [φ, ψ] (φ ∧ ψ)
        ·mp.a.leftw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ, ψ], ψ_1 ∈ w.carrier aesop
        ·mp.a.rightw : World
φ : Tm
ψ : Tm
at_w_and : at_world w (φ ∧ ψ)
hφ : φ ∈ w.carrier
hψ : ψ ∈ w.carrier
⊢ Pf [φ, ψ] (φ ∧ ψ) have hφmem : φ ∈ [φ, ψ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier simp
          have hψmem : ψ ∈ [φ, ψ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier simp
          exact Pf.and_I (Pf.of_mem hφmem) (Pf.of_mem hψmem)
      ·mprw : World
φ : Tm
ψ : Tm
⊢ (φ ∧ ψ) ∈ w.carrier → at_world w (φ ∧ ψ) intro both_in_wmprw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ at_world w (φ ∧ ψ)
        constructormpr.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ at_world w φ
mpr.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ at_world w ψ
        ·mpr.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ at_world w φ rw [truth_lemma w φ]mpr.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ φ ∈ w.carrier
          apply w.closedmpr.left.aw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ProvableFrom w.carrier φ
          exists [φ ∧ ψ]mpr.left.aw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ (∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier) ∧ Pf [φ ∧ ψ] φ
          constructormpr.left.a.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier
mpr.left.a.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ Pf [φ ∧ ψ] φ
          ·mpr.left.a.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier simpa using both_in_w
          ·mpr.left.a.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ Pf [φ ∧ ψ] φ have hmem : (φ ∧ ψ) ∈ [φ ∧ ψ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier simp
            exact Pf.and_E₁ (Pf.of_mem hmem)
        ·mpr.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ at_world w ψ rw [truth_lemma w ψ]mpr.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ψ ∈ w.carrier
          apply w.closedmpr.right.aw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ProvableFrom w.carrier ψ
          exists [φ ∧ ψ]mpr.right.aw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ (∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier) ∧ Pf [φ ∧ ψ] ψ
          constructormpr.right.a.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier
mpr.right.a.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ Pf [φ ∧ ψ] ψ
          ·mpr.right.a.leftw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ ∀ ψ_1 ∈ [φ ∧ ψ], ψ_1 ∈ w.carrier simpa using both_in_w
          ·mpr.right.a.rightw : World
φ : Tm
ψ : Tm
both_in_w : (φ ∧ ψ) ∈ w.carrier
⊢ Pf [φ ∧ ψ] ψ have hmem : (φ ∧ ψ) ∈ [φ ∧ ψ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∧ ψ) ↔ (φ ∧ ψ) ∈ w.carrier simp
            exact Pf.and_E₂ (Pf.of_mem hmem)
  | Tm.or φ ψ =>w : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) ↔ (φ ∨ ψ) ∈ w.carrier byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) ↔ (φ ∨ ψ) ∈ w.carrier
      constructormpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) → (φ ∨ ψ) ∈ w.carrier
mprw : World
φ : Tm
ψ : Tm
⊢ (φ ∨ ψ) ∈ w.carrier → at_world w (φ ∨ ψ)
      ·mpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) → (φ ∨ ψ) ∈ w.carrier intro or_at_wmpw : World
φ : Tm
ψ : Tm
or_at_w : at_world w (φ ∨ ψ)
⊢ (φ ∨ ψ) ∈ w.carrier
        rcases or_at_w with φ_at_w | ψ_at_wmp.inlw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ (φ ∨ ψ) ∈ w.carrier
mp.inrw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ (φ ∨ ψ) ∈ w.carrier
        ·mp.inlw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ (φ ∨ ψ) ∈ w.carrier apply w.closedmp.inl.aw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ ProvableFrom w.carrier (φ ∨ ψ)
          exists [φ]mp.inl.aw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ (∀ ψ ∈ [φ], ψ ∈ w.carrier) ∧ Pf [φ] (φ ∨ ψ)
          constructormp.inl.a.leftw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ ∀ ψ ∈ [φ], ψ ∈ w.carrier
mp.inl.a.rightw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ Pf [φ] (φ ∨ ψ)
          ·mp.inl.a.leftw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ ∀ ψ ∈ [φ], ψ ∈ w.carrier simpmp.inl.a.leftw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ φ ∈ w.carrier
            rw [<- truth_lemma w φ]mp.inl.a.leftw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ at_world w φ
            exact φ_at_w
          ·mp.inl.a.rightw : World
φ : Tm
ψ : Tm
φ_at_w : at_world w φ
⊢ Pf [φ] (φ ∨ ψ) have hmem : φ ∈ [φ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) ↔ (φ ∨ ψ) ∈ w.carrier simp
            exact Pf.or_I₁ (Pf.of_mem hmem)

        ·mp.inrw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ (φ ∨ ψ) ∈ w.carrier apply w.closedmp.inr.aw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ ProvableFrom w.carrier (φ ∨ ψ)
          exists [ψ]mp.inr.aw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ (∀ ψ_1 ∈ [ψ], ψ_1 ∈ w.carrier) ∧ Pf [ψ] (φ ∨ ψ)
          constructormp.inr.a.leftw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ ∀ ψ_1 ∈ [ψ], ψ_1 ∈ w.carrier
mp.inr.a.rightw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ Pf [ψ] (φ ∨ ψ)
          ·mp.inr.a.leftw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ ∀ ψ_1 ∈ [ψ], ψ_1 ∈ w.carrier simpmp.inr.a.leftw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ ψ ∈ w.carrier
            rw [<- truth_lemma w ψ]mp.inr.a.leftw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ at_world w ψ
            exact ψ_at_w
          ·mp.inr.a.rightw : World
φ : Tm
ψ : Tm
ψ_at_w : at_world w ψ
⊢ Pf [ψ] (φ ∨ ψ) have hmem : ψ ∈ [ψ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ∨ ψ) ↔ (φ ∨ ψ) ∈ w.carrier simp
            exact Pf.or_I₂ (Pf.of_mem hmem)

      ·mprw : World
φ : Tm
ψ : Tm
⊢ (φ ∨ ψ) ∈ w.carrier → at_world w (φ ∨ ψ) intro or_in_wmprw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
⊢ at_world w (φ ∨ ψ)
        rcases w.prime or_in_w with φ_in_w | ψ_in_wmpr.inlw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
φ_in_w : φ ∈ w.carrier
⊢ at_world w (φ ∨ ψ)
mpr.inrw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
ψ_in_w : ψ ∈ w.carrier
⊢ at_world w (φ ∨ ψ)
        ·mpr.inlw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
φ_in_w : φ ∈ w.carrier
⊢ at_world w (φ ∨ ψ) simpmpr.inlw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
φ_in_w : φ ∈ w.carrier
⊢ at_world w φ ∨ at_world w ψ
          rw [truth_lemma w φ]mpr.inlw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
φ_in_w : φ ∈ w.carrier
⊢ φ ∈ w.carrier ∨ at_world w ψ
          apply Or.inlmpr.inl.hw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
φ_in_w : φ ∈ w.carrier
⊢ φ ∈ w.carrier
          assumption
        ·mpr.inrw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
ψ_in_w : ψ ∈ w.carrier
⊢ at_world w (φ ∨ ψ) simpmpr.inrw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
ψ_in_w : ψ ∈ w.carrier
⊢ at_world w φ ∨ at_world w ψ
          rw [truth_lemma w ψ]mpr.inrw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
ψ_in_w : ψ ∈ w.carrier
⊢ at_world w φ ∨ ψ ∈ w.carrier
          apply Or.inrmpr.inr.hw : World
φ : Tm
ψ : Tm
or_in_w : (φ ∨ ψ) ∈ w.carrier
ψ_in_w : ψ ∈ w.carrier
⊢ ψ ∈ w.carrier
          assumption

  | Tm.imp φ ψ =>w : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
      constructormpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) → (φ ⇒ ψ) ∈ w.carrier
mprw : World
φ : Tm
ψ : Tm
⊢ (φ ⇒ ψ) ∈ w.carrier → at_world w (φ ⇒ ψ)
      ·mpw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) → (φ ⇒ ψ) ∈ w.carrier intro imp_at_wmpw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
⊢ (φ ⇒ ψ) ∈ w.carrier
        by_contra imp_not_in_wmpw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
⊢ False
        have ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier) := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          intro ψ_in_closw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_in_clos : ψ ∈ closure (Set.insert φ w.carrier)
⊢ False
          apply imp_not_in_ww : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_in_clos : ψ ∈ closure (Set.insert φ w.carrier)
⊢ (φ ⇒ ψ) ∈ w.carrier
          apply closure_insert_impT_closedw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_in_clos : ψ ∈ closure (Set.insert φ w.carrier)
⊢ Closed w.carrier
htmw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_in_clos : ψ ∈ closure (Set.insert φ w.carrier)
⊢ ψ ∈ closure (Set.insert φ w.carrier)
          apply w.closedhtmw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_in_clos : ψ ∈ closure (Set.insert φ w.carrier)
⊢ ψ ∈ closure (Set.insert φ w.carrier)
          exact ψ_in_clos
        have w'_consistent : Consistent (closure (Set.insert φ w.carrier)) := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          intro ff_in_w'w : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
⊢ False
          have not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier :=
            closure_insert_imp w.closed ff_in_w'w : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ False
          apply imp_not_in_ww : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ (φ ⇒ ψ) ∈ w.carrier
          apply  w.closedaw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ ProvableFrom w.carrier (φ ⇒ ψ)
          exists
          [φ ⇒ Tm.ff]aw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ (∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ w.carrier) ∧ Pf [φ ⇒ Tm.ff] (φ ⇒ ψ)
          constructora.leftw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ ∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ w.carrier
a.rightw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ Pf [φ ⇒ Tm.ff] (φ ⇒ ψ)
          ·a.leftw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ ∀ ψ ∈ [φ ⇒ Tm.ff], ψ ∈ w.carrier simpa using not_φ_in_w
          ·a.rightw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
ff_in_w' : Tm.ff ∈ closure (Set.insert φ w.carrier)
not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier
⊢ Pf [φ ⇒ Tm.ff] (φ ⇒ ψ) exact Pf.quodlibet φ ψ
        -- construct a world containing w and φ, which extends w, and where
        -- φ holds but ψ doesn't
        obtain ⟨T, T_adm, T_prime⟩ :=
          prime_extension_avoiding (closure_closed _) w'_consistent ψ_not_in_closmpw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
⊢ False
        let v : World :=
          ⟨T, T_adm.closed, T_adm.consistent, T_prime⟩mpw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
v : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
⊢ False
        have w_le_v : w ≤ v := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          intro χ hχw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
v : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
χ : Tm
hχ : χ ∈ w.carrier
⊢ χ ∈ v.carrier
          exact T_adm.base (subset_closure (Or.inr hχ))
        have φ_at_v : at_world v φ := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          apply (truth_lemma v φ).2w : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
v : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
w_le_v : w ≤ v
⊢ φ ∈ v.carrier
          exact T_adm.base (subset_closure (Or.inl rfl))
        have not_ψ_at_v : ¬ at_world v ψ := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          intro hψvw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
v : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
w_le_v : w ≤ v
φ_at_v : at_world v φ
hψv : at_world v ψ
⊢ False
          exact T_adm.avoids ((truth_lemma v ψ).1 hψv)
        apply not_ψ_at_vmpw : World
φ : Tm
ψ : Tm
imp_at_w : at_world w (φ ⇒ ψ)
imp_not_in_w : (φ ⇒ ψ) ∉ w.carrier
ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier)
w'_consistent : Consistent (closure (Set.insert φ w.carrier))
T : Theory
T_adm : Admissible (closure (Set.insert φ w.carrier)) ψ T
T_prime : Prime T
v : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
w_le_v : w ≤ v
φ_at_v : at_world v φ
not_ψ_at_v : ¬at_world v ψ
⊢ at_world v ψ
        apply imp_at_w v w_le_v φ_at_v
      ·mprw : World
φ : Tm
ψ : Tm
⊢ (φ ⇒ ψ) ∈ w.carrier → at_world w (φ ⇒ ψ) intro imp_in_w vmprw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
⊢ w ≤ v → at_world v φ → at_world v ψ w_le_vmprw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
⊢ at_world v φ → at_world v ψ φ_at_vmprw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
⊢ at_world v ψ
        have imp_in_v : (φ ⇒ ψ) ∈ v.carrier := w_le_v imp_in_wmprw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
⊢ at_world v ψ
        have φ_in_v : φ ∈ v.carrier := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          rw [<- truth_lemma v φ]w : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
⊢ at_world v φ
          exact φ_at_v
        have ψ_in_v : ψ ∈ v.carrier := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier
          apply v.closedaw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ ProvableFrom v.carrier ψ
          exists [φ ⇒ ψ, φ]aw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ (∀ ψ_1 ∈ [φ ⇒ ψ, φ], ψ_1 ∈ v.carrier) ∧ Pf [φ ⇒ ψ, φ] ψ
          constructora.leftw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ ∀ ψ_1 ∈ [φ ⇒ ψ, φ], ψ_1 ∈ v.carrier
a.rightw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ Pf [φ ⇒ ψ, φ] ψ
          ·a.leftw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ ∀ ψ_1 ∈ [φ ⇒ ψ, φ], ψ_1 ∈ v.carrier intro tm tm_in_ctxa.leftw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
tm : Tm
tm_in_ctx : tm ∈ [φ ⇒ ψ, φ]
⊢ tm ∈ v.carrier
            simp at tm_in_ctxa.leftw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
tm : Tm
tm_in_ctx : tm = (φ ⇒ ψ) ∨ tm = φ
⊢ tm ∈ v.carrier
            rcases tm_in_ctx with rfl | rfla.left.inlw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ (φ ⇒ ψ) ∈ v.carrier
a.left.inrw : World
ψ : Tm
v : World
w_le_v : w ≤ v
tm : Tm
imp_in_w : (tm ⇒ ψ) ∈ w.carrier
φ_at_v : at_world v tm
imp_in_v : (tm ⇒ ψ) ∈ v.carrier
φ_in_v : tm ∈ v.carrier
⊢ tm ∈ v.carrier
            ·a.left.inlw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ (φ ⇒ ψ) ∈ v.carrier exact imp_in_v
            ·a.left.inrw : World
ψ : Tm
v : World
w_le_v : w ≤ v
tm : Tm
imp_in_w : (tm ⇒ ψ) ∈ w.carrier
φ_at_v : at_world v tm
imp_in_v : (tm ⇒ ψ) ∈ v.carrier
φ_in_v : tm ∈ v.carrier
⊢ tm ∈ v.carrier exact φ_in_v
          ·a.rightw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
⊢ Pf [φ ⇒ ψ, φ] ψ have imp_mem : (φ ⇒ ψ) ∈ [φ ⇒ ψ, φ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier simp
            have φ_mem: φ ∈ [φ ⇒ ψ, φ] := byw : World
φ : Tm
ψ : Tm
⊢ at_world w (φ ⇒ ψ) ↔ (φ ⇒ ψ) ∈ w.carrier simp
            exact Pf.imp_E (Pf.of_mem imp_mem) (Pf.of_mem φ_mem)
        rw [truth_lemma v ψ]mprw : World
φ : Tm
ψ : Tm
imp_in_w : (φ ⇒ ψ) ∈ w.carrier
v : World
w_le_v : w ≤ v
φ_at_v : at_world v φ
imp_in_v : (φ ⇒ ψ) ∈ v.carrier
φ_in_v : φ ∈ v.carrier
ψ_in_v : ψ ∈ v.carrier
⊢ ψ ∈ v.carrier
        exact ψ_in_v
  | Tm.tt =>w : World
⊢ at_world w Tm.tt ↔ Tm.tt ∈ w.carrier byw : World
⊢ at_world w Tm.tt ↔ Tm.tt ∈ w.carrier
      constructormpw : World
⊢ at_world w Tm.tt → Tm.tt ∈ w.carrier
mprw : World
⊢ Tm.tt ∈ w.carrier → at_world w Tm.tt
      ·mpw : World
⊢ at_world w Tm.tt → Tm.tt ∈ w.carrier intro _mpw : World
a✝ : at_world w Tm.tt
⊢ Tm.tt ∈ w.carrier
        exact w.closed ⟨[], byw : World
a✝ : at_world w Tm.tt
⊢ ∀ ψ ∈ [], ψ ∈ w.carrier simp, Pf.tt_I⟩
      ·mprw : World
⊢ Tm.tt ∈ w.carrier → at_world w Tm.tt aesop
  | Tm.ff =>w : World
⊢ at_world w Tm.ff ↔ Tm.ff ∈ w.carrier byw : World
⊢ at_world w Tm.ff ↔ Tm.ff ∈ w.carrier
      constructormpw : World
⊢ at_world w Tm.ff → Tm.ff ∈ w.carrier
mprw : World
⊢ Tm.ff ∈ w.carrier → at_world w Tm.ff
      ·mpw : World
⊢ at_world w Tm.ff → Tm.ff ∈ w.carrier intro ff_at_wmpw : World
ff_at_w : at_world w Tm.ff
⊢ Tm.ff ∈ w.carrier
        exact False.elim ff_at_w
      ·mprw : World
⊢ Tm.ff ∈ w.carrier → at_world w Tm.ff intro ff_in_wmprw : World
ff_in_w : Tm.ff ∈ w.carrier
⊢ at_world w Tm.ff
        exfalsomprw : World
ff_in_w : Tm.ff ∈ w.carrier
⊢ False
        exact w.consistent ff_in_w



end Canonical



open Canonical



theorem countermodel {Γ : Ctxt} {tm : Tm} (neg_pf : ¬ Pf Γ tm) :
    ¬ Kripke.SemEntails.{0} Γ tm := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
  have tm_avoids_T : tm ∉ theoryOf Γ := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
    intro htmΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
htm : tm ∈ theoryOf Γ
⊢ False
    apply neg_pfΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
htm : tm ∈ theoryOf Γ
⊢ Pf Γ tm
    rw [<- mem_theoryOf]Γ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
htm : tm ∈ theoryOf Γ
⊢ tm ∈ theoryOf Γ
    assumption
  have ΓT_Cons : Consistent (theoryOf Γ) := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
    intro hffΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
hff : Tm.ff ∈ theoryOf Γ
⊢ False
    apply neg_pfΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
hff : Tm.ff ∈ theoryOf Γ
⊢ Pf Γ tm
    apply Pf.ff_EaΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
hff : Tm.ff ∈ theoryOf Γ
⊢ Pf Γ Tm.ff
    rw [<- mem_theoryOf]aΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
hff : Tm.ff ∈ theoryOf Γ
⊢ Tm.ff ∈ theoryOf Γ
    assumption
  obtain ⟨T, T_admissible, T_prime⟩ :=
    prime_extension_avoiding (closure_closed _) ΓT_Cons tm_avoids_TΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
⊢ ¬SemEntails Γ tm
  let w : World := ⟨T, T_admissible.closed, T_admissible.consistent, T_prime⟩Γ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
⊢ ¬SemEntails Γ tm
  have all_in_T : ∀ Δ : Ctxt, (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
    intro Δ hΔΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
Δ : Ctxt
hΔ : ∀ φ ∈ Δ, φ ∈ T
⊢ all_at_world w Δ
    induction Δ with
    | nil =>nilΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
hΔ : ∀ φ ∈ [], φ ∈ T
⊢ all_at_world w []
        simp
    | cons φ Δ ih =>consΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ all_at_world w (φ :: Δ)
        constructorcons.leftΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ at_world w φ
cons.rightΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ all_at_world w Δ
        ·cons.leftΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ at_world w φ rw [truth_lemma w φ]cons.leftΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ φ ∈ w.carrier
          apply hΔ φcons.leftΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ φ ∈ φ :: Δ
          simp
        ·cons.rightΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ all_at_world w Δ apply ihcons.rightΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
⊢ ∀ φ ∈ Δ, φ ∈ T
          intro ψ hψcons.rightΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
ψ : Tm
hψ : ψ ∈ Δ
⊢ ψ ∈ T
          apply hΔ ψcons.rightΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
φ : Tm
Δ : List Tm
ih : (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
hΔ : ∀ φ_1 ∈ φ :: Δ, φ_1 ∈ T
ψ : Tm
hψ : ψ ∈ Δ
⊢ ψ ∈ φ :: Δ
          simp [hψ]
  have all_at_Γ : all_at_world w Γ := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
    apply all_in_T ΓΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
⊢ ∀ φ ∈ Γ, φ ∈ T
    intro φ φ_in_ΓΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
φ : Tm
φ_in_Γ : φ ∈ Γ
⊢ φ ∈ T
    apply T_admissible.base (contextSet_mem φ_in_Γ)
  have not_tm_at_w : ¬ at_world w tm := byΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
⊢ ¬SemEntails Γ tm
    intro tm_at_wΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
tm_at_w : at_world w tm
⊢ False
    apply T_admissible.avoidsΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
tm_at_w : at_world w tm
⊢ tm ∈ T
    rw [<- truth_lemma w tm]Γ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
tm_at_w : at_world w tm
⊢ at_world w tm
    apply tm_at_w
  intro sem_tmΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
not_tm_at_w : ¬at_world w tm
sem_tm : SemEntails Γ tm
⊢ False
  apply not_tm_at_wΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
not_tm_at_w : ¬at_world w tm
sem_tm : SemEntails Γ tm
⊢ at_world w tm
  apply sem_tmaΓ : Ctxt
tm : Tm
neg_pf : ¬Pf Γ tm
tm_avoids_T : tm ∉ theoryOf Γ
ΓT_Cons : Consistent (theoryOf Γ)
T : Theory
T_admissible : Admissible (Canonical.closure (contextSet Γ)) tm T
T_prime : Canonical.Prime T
w : World := { carrier := T, closed := ⋯, consistent := ⋯, prime := T_prime }
all_in_T : ∀ (Δ : Ctxt), (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ
all_at_Γ : all_at_world w Γ
not_tm_at_w : ¬at_world w tm
sem_tm : SemEntails Γ tm
⊢ all_at_world w Γ
  apply all_at_Γ



theorem completeness {Γ : Ctxt} {tm : Tm} : Kripke.SemEntails.{0} Γ tm → Pf Γ tm := byΓ : Ctxt
tm : Tm
⊢ SemEntails Γ tm → Pf Γ tm
  contrapose!Γ : Ctxt
tm : Tm
⊢ ¬Pf Γ tm → ¬SemEntails Γ tm
  exact countermodel



end Kripke