theorem Model.validate_gentzen_boxT {κ : Type u} [Nonempty κ] {α : Type v} [DecidableEq α] {M : Model κ α} {B : Formula α} {Γ Δ : FormulaFinset α} [Std.Refl Rel] (h : M ⊧ (insert B Γ ⟹ Δ)) : M ⊧ (insert (□B) Γ ⟹ Δ)

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

@[reducible, inline]

abbrev LogicGrz.trivial_Grz_model {α : Type u_1} : Model (Fin 1) α

Equations

• LogicGrz.trivial_Grz_model = { Rel' := fun (x x_1 : Fin 1) => True, Val' := fun (x : Fin 1) (x_1 : α) => False }

instance LogicGrz.instIsFiniteGrzFinOfNatNatTrivial_Grz_model {α : Type v} : trivial_Grz_model.IsFiniteGrz

noncomputable def Sequent.subfmlsGrz {α : Type v} [DecidableEq α] (S : Sequent α) : FormulaFinset α

Equations

• S.subfmlsGrz = S.subfmls ∪ Finset.image (fun (C : Formula α) => C 🡒 □C) (FormulaFinset.prebox S.subfmls) ∪ Finset.image (fun (C : Formula α) => □(C 🡒 □C)) (FormulaFinset.prebox S.subfmls)

theorem LogicGrz.subfmls_subset_subfmlsGrz {α : Type v} [DecidableEq α] {S : Sequent α} : S.subfmls ⊆ S.subfmlsGrz

theorem LogicGrz.imp_mem_subfmlsGrz {α : Type v} [DecidableEq α] {A B : Formula α} {S : Sequent α} (h : A 🡒 B ∈ S.subfmlsGrz) : A ∈ S.subfmls ∧ B ∈ S.subfmls

theorem LogicGrz.box_mem_subfmlsGrz {α : Type v} [DecidableEq α] {A : Formula α} {S : Sequent α} (h : □A ∈ S.subfmlsGrz) : A ∈ S.subfmlsGrz

theorem LogicGrz.grzCompanions_mem_subfmlsGrz {α : Type v} [DecidableEq α] {A : Formula α} {S : Sequent α} (h : □A ∈ S.subfmls) : A 🡒 □A ∈ S.subfmlsGrz ∧ □(A 🡒 □A) ∈ S.subfmlsGrz

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

An unprovable sequent, saturated and boxT-closed, bounded by the subformula closure of a base sequent BS. The bound is asymmetric: the antecedent ranges over the enlarged BS.subfmlsGrz while the succedent stays within BS.subfmls, so that □A in the succedent has its Grz companion A 🡒 □A inside BS.subfmlsGrz.

• ant : FormulaFinset α
• suc : FormulaFinset α
• saturated : self.Saturated
• boxT_closed {A : Formula α} : □A ∈ self.ant → A ∈ self.ant
• ant_subset : self.ant ⊆ BS.subfmlsGrz
• suc_subset : self.suc ⊆ BS.subfmls
• unprovable : ¬⊢ᵍ[Grz] self.toSequent

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

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

theorem LogicGrz.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 LogicGrz.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 LogicGrz.ExpandedSequent.lindenbaum_indexed {α : Type v} [DecidableEq α] (S₀ : Sequent α) (S₀_unprovable : ¬⊢ᵍ[Grz] S₀) : FormulaList α → { S : Sequent α // ¬⊢ᵍ[Grz] S }

Lindenbaum-style saturation: runs through a list of formulas, saturating the sequent for impL, impR and boxT while preserving unprovability.

Equations

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

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

theorem LogicGrz.ExpandedSequent.bounds_lindenbaum_indexed {α : Type v} [DecidableEq α] {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[Grz] S₀} {Γ : FormulaList α} {BS : Sequent α} (S₀_ant : S₀.ant ⊆ BS.subfmlsGrz) (S₀_suc : S₀.suc ⊆ BS.subfmls) : (↑(lindenbaum_indexed S₀ S₀_unprovable Γ)).ant ⊆ BS.subfmlsGrz ∧ (↑(lindenbaum_indexed S₀ S₀_unprovable Γ)).suc ⊆ BS.subfmls

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

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

theorem LogicGrz.ExpandedSequent.saturated_boxT_lindenbaum_indexed {α : Type v} [DecidableEq α] {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[Grz] S₀} {Γ : FormulaList α} (hΓ : (List.map (fun (x : Formula α) => x.complexity) Γ).SortedLE) : have S := lindenbaum_indexed S₀ S₀_unprovable Γ; ∀ {A : Formula α}, □A ∈ Γ → □A ∈ (↑S).ant → A ∈ (↑S).ant

theorem LogicGrz.ExpandedSequent.saturated_lindenbaum_indexed {α : Type v} [DecidableEq α] {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[Grz] S₀} {Γ : FormulaList α} (hΓ : (List.map (fun (x : Formula α) => x.complexity) Γ).SortedLE) : have S := lindenbaum_indexed 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) ∧ ∀ {A : Formula α}, □A ∈ Γ → □A ∈ (↑S).ant → A ∈ (↑S).ant

noncomputable def LogicGrz.ExpandedSequent.lindenbaum {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[Grz] BS] (S₀ : Sequent α) (S₀_unprovable : ¬⊢ᵍ[Grz] S₀) (S₀_ant : S₀.ant ⊆ BS.subfmlsGrz) (S₀_suc : S₀.suc ⊆ BS.subfmls) : ExpandedSequent BS

Equations

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

theorem LogicGrz.ExpandedSequent.subset_lindenbaum {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[Grz] BS] {S₀ : Sequent α} {S₀_unprovable : ¬⊢ᵍ[Grz] S₀} {S₀_ant : S₀.ant ⊆ BS.subfmlsGrz} {S₀_suc : S₀.suc ⊆ BS.subfmls} : S₀ ⊆ (lindenbaum S₀ S₀_unprovable S₀_ant S₀_suc).toSequent

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

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

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

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

The canonical finite countermodel of an unprovable Grz sequent BS. Unlike the GL countermodel its accessibility relation is reflexive, and the reversed-containment clause is what forces antisymmetry.

Equations

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

instance LogicGrz.ProvableGentzen.Kripke.instIsFiniteGrzExpandedSequentCountermodelOf {α : Type v} [DecidableEq α] {BS : Sequent α} [Fact ¬⊢ᵍ[Grz] BS] : (countermodelOf BS).IsFiniteGrz

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

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

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

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

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

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

@[simp]

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

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

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

Alias of LogicGrz.ProvableGentzen.of_with_cut.

theorem LogicGrz.ProvableGentzen.modalGrz {α : Type v} [DecidableEq α] {A : Formula α} : ⊢ᵍ[Grz] (∅ ⟹ {□(□(A 🡒 □A) 🡒 A) 🡒 A})

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