def Model.World.ForcesSequent {κ : Type u} [Nonempty κ] {α : Type v} (M : Model κ α) (x : M.World) (S : Sequent α) : Prop

Equations

• x ⊩[M] S = ((∀ C ∈ S.ant, x ⊩[M] C) → ∃ D ∈ S.suc, x ⊩[M] D)

def Model.World.«term_⊩[_]__1» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Model.World.forces_ctx_singleton_sequent {κ : Type u} [Nonempty κ] {α : Type v} {A : Formula α} {Γ : FormulaFinset α} {M : Model κ α} {x : M.World} : x ⊩[M] (Γ ⟹ {A}) ↔ (∀ C ∈ Γ, x ⊩[M] C) → x ⊩[M] A

theorem Model.World.forces_singleton_sequent {κ : Type u} [Nonempty κ] {α : Type v} {A : Formula α} {M : Model κ α} {x : M.World} : x ⊩[M] (∅ ⟹ {A}) ↔ x ⊩[M] A

theorem Model.World.forces_sequent_axm {κ : Type u} [Nonempty κ] {α : Type v} {A : Formula α} {M : Model κ α} {x : M.World} : x ⊩[M] ({A} ⟹ {A})

theorem Model.World.forces_sequent_botL {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {x : M.World} : x ⊩[M] ({⊥} ⟹ ∅)

theorem Model.World.forces_sequent_wkL {κ : Type u} [Nonempty κ] {α : Type v} {Γ Γ' Δ : FormulaFinset α} {M : Model κ α} {x : M.World} (h : x ⊩[M] (Γ ⟹ Δ)) (hΓ : Γ ⊆ Γ' := by grind) : x ⊩[M] (Γ' ⟹ Δ)

theorem Model.World.forces_sequent_wkR {κ : Type u} [Nonempty κ] {α : Type v} {Γ Δ Δ' : FormulaFinset α} {M : Model κ α} {x : M.World} (h : x ⊩[M] (Γ ⟹ Δ)) (hΔ : Δ ⊆ Δ' := by grind) : x ⊩[M] (Γ ⟹ Δ')

theorem Model.World.forces_sequent_impL {κ : Type u} [Nonempty κ] {α : Type v} [DecidableEq α] {A B : Formula α} {Γ Δ : FormulaFinset α} {M : Model κ α} {x : M.World} (h₁ : x ⊩[M] (Γ ⟹ insert A Δ)) (h₂ : x ⊩[M] (insert B Γ ⟹ Δ)) : x ⊩[M] (insert (A 🡒 B) Γ ⟹ Δ)

theorem Model.World.forces_sequent_impR {κ : Type u} [Nonempty κ] {α : Type v} [DecidableEq α] {A B : Formula α} {Γ Δ : FormulaFinset α} {M : Model κ α} {x : M.World} (h : x ⊩[M] (insert A Γ ⟹ insert B Δ)) : x ⊩[M] (Γ ⟹ insert (A 🡒 B) Δ)

theorem Model.World.forces_sequent_cut {κ : Type u} [Nonempty κ] {α : Type v} [DecidableEq α] {A : Formula α} {M : Model κ α} {x : M.World} {Γ₁ Γ₂ Δ₁ Δ₂ : FormulaFinset α} (h₁ : x ⊩[M] (Γ₁ ⟹ insert A Δ₁)) (h₂ : x ⊩[M] (insert A Γ₂ ⟹ Δ₂)) : x ⊩[M] (Γ₁ ∪ Γ₂ ⟹ Δ₁ ∪ Δ₂)

def Model.ValidateSequent {κ : Type u} [Nonempty κ] {α : Type v} (M : Model κ α) (S : Sequent α) : Prop

Equations

• (M ⊧ S) = ∀ (x : M.World), x ⊩[M] S

def Model.«term_⊧__1» : Lean.TrailingParserDescr

Equations

• Model.«term_⊧__1» = Lean.ParserDescr.trailingNode `Model.«term_⊧__1» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ ") (Lean.ParserDescr.cat `term 51))

theorem Model.validateSequent_singleton_iff {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {A : Formula α} : M ⊧ (∅ ⟹ {A}) ↔ M ⊧ A

Validity of the singleton sequent ∅ ⟹ {A} is exactly validity of A.

theorem Model.validate_gentzen_axm {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {A : Formula α} : M ⊧ ({A} ⟹ {A})

theorem Model.validate_gentzen_botL {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} : M ⊧ ({⊥} ⟹ ∅)

theorem Model.validate_gentzen_wkL {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {Γ Γ' Δ : FormulaFinset α} (h : M ⊧ (Γ ⟹ Δ)) (hΓ : Γ ⊆ Γ' := by grind) : M ⊧ (Γ' ⟹ Δ)

theorem Model.validate_gentzen_wkR {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {Γ Δ Δ' : FormulaFinset α} (h : M ⊧ (Γ ⟹ Δ)) (hΔ : Δ ⊆ Δ' := by grind) : M ⊧ (Γ ⟹ Δ')

theorem Model.validate_gentzen_impL {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {Γ Δ : FormulaFinset α} {A B : Formula α} [DecidableEq α] (hA : M ⊧ (Γ ⟹ insert A Δ)) (hB : M ⊧ (insert B Γ ⟹ Δ)) : M ⊧ (insert (A 🡒 B) Γ ⟹ Δ)

theorem Model.validate_gentzen_impR {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {Γ Δ : FormulaFinset α} {A B : Formula α} [DecidableEq α] (h : M ⊧ (insert A Γ ⟹ insert B Δ)) : M ⊧ (Γ ⟹ insert (A 🡒 B) Δ)

theorem Model.validate_gentzen_boxGL {κ : Type u} [Nonempty κ] {α : Type v} {M : Model κ α} {Γ : FormulaFinset α} {A : Formula α} [DecidableEq α] [M.IsGL] (h : M ⊧ (insert (□A) (Γ ∪ Γ.box) ⟹ {A})) : M ⊧ (Γ.box ⟹ {□A})

theorem LogicGL.ProvableGentzen.Kripke.soundness {α : Type v} [DecidableEq α] {S : Sequent α} (h : ⊢ᵍ[GL] S) {κ : Type u_1} [Nonempty κ] (M : Model κ α) [M.IsGL] : M ⊧ S

theorem LogicGL.ProvableGentzen.Kripke.finite_soundness {α : Type v} [DecidableEq α] {S : Sequent α} (h : ⊢ᵍ[GL] S) {κ : Type u_1} [Nonempty κ] (M : Model κ α) [M.IsFiniteGL] : M ⊧ S

@[simp]

theorem LogicGL.ProvableGentzen.not_provable_empty {α : Type v} [DecidableEq α] : ¬⊢ᵍ[GL] (∅ ⟹ ∅)

structure LogicGL.ExpandedSequent {α : Type v} [DecidableEq α] (BS : Sequent α) extends Sequent α : Type v

• ant : FormulaFinset α
• suc : FormulaFinset α
• saturated : self.Saturated
• subset_subfmls : self.ant ∪ self.suc ⊆ BS.subfmls
• unprovable : ¬⊢ᵍ[GL] self.toSequent

def LogicGL.ExpandedSequent.widen {α : Type v} [DecidableEq α] {BS₀ BS₁ : Sequent α} (S : ExpandedSequent BS₀) (hBS : BS₀ ⊆ BS₁) : ExpandedSequent BS₁

Equations

• S.widen hBS = { toSequent := S.toSequent, saturated := ⋯, subset_subfmls := ⋯, unprovable := ⋯ }

theorem LogicGL.ExpandedSequent.not_mem_both {α : Type v} [DecidableEq α] {BS : Sequent α} {S : ExpandedSequent BS} {A : Formula α} : ¬(A ∈ S.ant ∧ A ∈ S.suc)

theorem LogicGL.ExpandedSequent.not_mem_bot_ant {α : Type v} [DecidableEq α] {BS : Sequent α} {S : ExpandedSequent BS} : ⊥ ∉ S.ant

theorem LogicGL.ExpandedSequent.of_mem_imp_ant {α : Type v} [DecidableEq α] {B : Formula α} {BS : Sequent α} {S : ExpandedSequent BS} {A : Formula α} (h : A 🡒 B ∈ S.ant := by grind) : A ∈ S.suc ∨ B ∈ S.ant

theorem LogicGL.ExpandedSequent.of_mem_imp_suc {α : Type v} [DecidableEq α] {B : Formula α} {BS : Sequent α} {S : ExpandedSequent BS} {A : Formula α} (h : A 🡒 B ∈ S.suc := by grind) : A ∈ S.ant ∧ B ∈ S.suc

noncomputable def LogicGL.ExpandedSequent.lindenbaum_indexed {α : Type v} [DecidableEq α] (BS : Sequent α) (BS_unprovable : ¬⊢ᵍ[GL] BS) (S₀ : Sequent α) (S₀_unprovable : ¬⊢ᵍ[GL] S₀) : FormulaList α → { S : Sequent α // ¬⊢ᵍ[GL] S }

Equations

• One or more equations did not get rendered due to their size.
• LogicGL.ExpandedSequent.lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable [] = ⟨S₀, S₀_unprovable⟩
• LogicGL.ExpandedSequent.lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (head :: Γ) = LogicGL.ExpandedSequent.lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ

theorem LogicGL.ExpandedSequent.subset_lindenbaum_indexed {α : Type v} [DecidableEq α] {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} : S₀ ⊆ ↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)

theorem LogicGL.ExpandedSequent.subfmls_lindenbaum_indexed {α : Type v} [DecidableEq α] {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} (S₀sub : S₀.ant ∪ S₀.suc ⊆ BS.subfmls) {Γ : FormulaList α} (hΓ : ∀ C ∈ Γ, C ∈ BS.subfmls) : (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).ant ∪ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).suc ⊆ BS.subfmls

theorem LogicGL.ExpandedSequent.saturated_lindenbaum_indexed {α : Type v} [DecidableEq α] {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} (hΓ : (List.map (fun (x : Formula α) => x.complexity) Γ).SortedLE) : have S := lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ; (∀ {A B : Formula α}, A 🡒 B ∈ Γ → A 🡒 B ∈ (↑S).ant → A ∈ (↑S).suc ∨ B ∈ (↑S).ant) ∧ ∀ {A B : Formula α}, A 🡒 B ∈ Γ → A 🡒 B ∈ (↑S).suc → A ∈ (↑S).ant ∧ B ∈ (↑S).suc

theorem LogicGL.ExpandedSequent.lindenbaum_indexed_saturated_impL_of_sorted_complexity {α : Type v} [DecidableEq α] {B A : Formula α} {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} (hΓ : (List.map (fun (x : Formula α) => x.complexity) Γ).SortedLE) (h₁ : A 🡒 B ∈ Γ) (h₂ : A 🡒 B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).ant) : A ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).suc ∨ B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).ant

theorem LogicGL.ExpandedSequent.lindenbaum_indexed_saturated_impL {α : Type v} [DecidableEq α] {B A : Formula α} {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} (h : A 🡒 B ∈ Γ) : A 🡒 B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).ant → A ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).suc ∨ B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).ant

theorem LogicGL.ExpandedSequent.lindenbaum_indexed_saturated_impR_of_sorted_complexity {α : Type v} [DecidableEq α] {B A : Formula α} {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} (hΓ : (List.map (fun (x : Formula α) => x.complexity) Γ).SortedLE) (h₁ : A 🡒 B ∈ Γ) (h₂ : A 🡒 B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).suc) : A ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).ant ∧ B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable Γ)).suc

theorem LogicGL.ExpandedSequent.lindenbaum_indexed_saturated_impR {α : Type v} [DecidableEq α] {B A : Formula α} {BS : Sequent α} {BS_unprovable : ¬⊢ᵍ[GL] BS} {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {Γ : FormulaList α} (h : A 🡒 B ∈ Γ) : A 🡒 B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).suc → A ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).ant ∧ B ∈ (↑(lindenbaum_indexed BS BS_unprovable S₀ S₀_unprovable (List.insertionSort (fun (x1 x2 : Formula α) => x1.complexity ≤ x2.complexity) Γ))).suc

noncomputable def LogicGL.ExpandedSequent.lindenbaum {α : Type v} [DecidableEq α] {BS : Sequent α} [BS_unprovable : Fact ¬⊢ᵍ[GL] BS] (S₀ : Sequent α) (S₀_unprovable : ¬⊢ᵍ[GL] S₀) (S₀sub : S₀.ant ∪ S₀.suc ⊆ BS.subfmls) : ExpandedSequent BS

Equations

• One or more equations did not get rendered due to their size.

theorem LogicGL.ExpandedSequent.subset_lindenbaum {α : Type v} [DecidableEq α] {BS : Sequent α} [BS_unprovable : Fact ¬⊢ᵍ[GL] BS] {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[GL] S₀} {S₀sub : S₀.ant ∪ S₀.suc ⊆ BS.subfmls} : S₀ ⊆ (lindenbaum S₀ S₀_unprovable S₀sub).toSequent

instance LogicGL.ExpandedSequent.instSubsingletonSaturated {α : Type v} {S : Sequent α} : Subsingleton S.Saturated

theorem LogicGL.ExpandedSequent.ext {α : Type v} [DecidableEq α] {BS : Sequent α} {S T : ExpandedSequent BS} (ha : S.ant = T.ant) (hs : S.suc = T.suc) : S = T

instance LogicGL.ExpandedSequent.instFinite {α : Type v} [DecidableEq α] {BS : Sequent α} : Finite (ExpandedSequent BS)

instance LogicGL.ExpandedSequent.instNonemptyOfFactNotProvableGentzen {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[GL] BS] : Nonempty (ExpandedSequent BS)

def LogicGL.ProvableGentzen.Kripke.countermodelOf {α : Type v} [DecidableEq α] (BS : Sequent α) [Fact ¬⊢ᵍ[GL] BS] : Model (ExpandedSequent BS) α

Equations

• One or more equations did not get rendered due to their size.

instance LogicGL.ProvableGentzen.Kripke.instIsFiniteGLExpandedSequentCountermodelOf {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[GL] BS] : (countermodelOf BS).IsFiniteGL

theorem LogicGL.ProvableGentzen.Kripke.truthlemma {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[GL] BS] {x : (countermodelOf BS).World} {A : Formula α} : (A ∈ x.ant → x ⊩[countermodelOf BS] A) ∧ (A ∈ x.suc → ¬x ⊩[countermodelOf BS] A)

theorem LogicGL.ProvableGentzen.Kripke.truthlemma_ant {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[GL] BS] {x : (countermodelOf BS).World} {A : Formula α} : A ∈ x.ant → x ⊩[countermodelOf BS] A

theorem LogicGL.ProvableGentzen.Kripke.truthlemma_suc {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[GL] BS] {x : (countermodelOf BS).World} {A : Formula α} : A ∈ x.suc → ¬x ⊩[countermodelOf BS] A

theorem LogicGL.ProvableGentzen.Kripke.completeness {α : Type v} [DecidableEq α] {S : Sequent α} (h : ∀ {κ : Type v} [inst : Nonempty κ] (M : Model κ α) [M.IsFiniteGL], M ⊧ S) : ⊢ᵍ[GL] S

theorem LogicGL.ProvableGentzen.of_with_cut {α : Type v} [DecidableEq α] {S : Sequent α} : ⊢ᵍᶜ[GL] S → ⊢ᵍ[GL] S

Cut-elimination: any sequent provable with the cut rule (⊢ᵍᶜ[GL]) is also provable without it (⊢ᵍ[GL]).

theorem LogicGL.GentzenWithCutProvable.cut_elimination {α : Type v} [DecidableEq α] {S : Sequent α} : ⊢ᵍᶜ[GL] S → ⊢ᵍ[GL] S

Alias of LogicGL.ProvableGentzen.of_with_cut.

---

Cut-elimination: any sequent provable with the cut rule (⊢ᵍᶜ[GL]) is also provable without it (⊢ᵍ[GL]).

theorem LogicGL.ProvableGentzen.mdp {α : Type v} [DecidableEq α] {A B : Formula α} : ⊢ᵍ[GL] (∅ ⟹ {A 🡒 B}) → ⊢ᵍ[GL] (∅ ⟹ {A}) → ⊢ᵍ[GL] (∅ ⟹ {B})

theorem LogicGL.ProvableGentzen.ruleLöb {α : Type v} [DecidableEq α] {A : Formula α} {Γ : FormulaFinset α} (h : ⊢ᵍ[GL] (insert (□A) (Γ ∪ Γ.box) ⟹ {A})) : ⊢ᵍ[GL] (Γ ∪ Γ.box ⟹ {A})

Löb's rule is admissible in ProofGentzen. Proved via cut.