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

A LogicGrz.ProofGentzen-unprovable sequent saturated for impL/impR, closed under the reflexivity rule boxT on its antecedent, and bounded by the subformula closure of a base sequent BS. The bound is deliberately asymmetric: the antecedent may range over the enlarged BS.subfmlsGrz but the succedent stays within the plain BS.subfmls, so that a boxed formula □A in the succedent is guaranteed to have 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 }

One step of the Lindenbaum-style saturation for LogicGrz.ProofGentzen: process the given list of formulas, saturating the sequent for impL, impR and boxT while preserving LogicGrz.ProofGentzen-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 Γ)

Every step of lindenbaum_indexed only ever extends S₀.

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

Two-sided invariant of lindenbaum_indexed: if the antecedent of S₀ stays inside BS.subfmlsGrz and its succedent inside BS.subfmls, so do those of the resulting sequent. The bound is asymmetric like ExpandedSequent itself; each membership is derived from the invariant already established for the shorter list together with the closure lemmas for Sequent.subfmlsGrz, so no side condition on Γ is needed.

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

impL-saturation part of saturated_lindenbaum_indexed: the antecedent of the saturated sequent is closed under the impL rule for implications from Γ.

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

impR-saturation part of saturated_lindenbaum_indexed: the succedent of the saturated sequent is closed under the impR rule for implications from Γ.

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

boxT-saturation part of saturated_lindenbaum_indexed: the antecedent of the saturated sequent is closed under the boxT rule for boxed formulas from Γ.

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

Saturation of the Lindenbaum construction: the resulting sequent is simultaneously impL-, impR- and boxT-saturated for the formulas listed in Γ.

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

Lindenbaum-style saturation for LogicGrz.ProofGentzen: every unprovable sequent bounded by the subformula closure of BS extends to a saturated, boxT-closed, unprovable sequent whose bounds against BS are still asymmetric. Runs lindenbaum_indexed once over BS.subfmlsGrz sorted by complexity.

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

Two ExpandedSequents agree once their underlying antecedent and succedent agree.

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: worlds are the expanded sequents built over BS, an atom holds at a world exactly when it sits in its antecedent, and one world precedes another when its □-preimage antecedent is contained in the other's, with the containment forced into equality once it also holds in the reverse direction. Unlike the GL countermodel this relation is reflexive; the reversed-containment clause is exactly 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)

Truth lemma for the Grz countermodel: membership in the antecedent of an expanded sequent forces the formula, and membership in the succedent refutes it.

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

Kripke completeness of the cut-free LogicGrz.ProofGentzen: a sequent valid in every finite Grz model is provable.

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

Kripke soundness of the cut-free LogicGrz.ProofGentzen: every provable sequent is valid in every Grz model.

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})