Soundness of GL-split proof system.

noncomputable def SplitCut.chain {𝕏 : Proof} {x : 𝕏.X} {Γ : SplitSequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSSeq (M, w) Γ) (n : ℕ) : (y : 𝕏.X) × { u : W // ¬evaluateSSeq (M, u) (f (r 𝕏.α y)) }

Helper for soundness, Given a proof of Γ and a countermodel of Γ, find a path in the proof and the model

Equations

• One or more equations did not get rendered due to their size.
• SplitCut.chain prop w_prop 0 = ⟨x, ⟨w, ⋯⟩⟩

theorem SplitCut.chain_proof_prop {𝕏 : Proof} {x : 𝕏.X} {Γ : SplitSequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSSeq (M, w) Γ) (n : ℕ) : edge 𝕏.α (chain prop w_prop n).fst (chain prop w_prop (n + 1)).fst

The left projection of chain is a chain in the proof.

theorem SplitCut.chain_model_prop {𝕏 : Proof} {x : 𝕏.X} {Γ : SplitSequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSSeq (M, w) Γ) (n : ℕ) : (¬(r 𝕏.α (chain prop w_prop n).fst).isBox → ↑(chain prop w_prop n).snd = ↑(chain prop w_prop (n + 1)).snd) ∧ ((r 𝕏.α (chain prop w_prop n).fst).isBox → M.R ↑(chain prop w_prop n).snd ↑(chain prop w_prop (n + 1)).snd)

The right projection of chain makes progress in the model on box nodes.

theorem SplitCut.has_children_of_chain_model {𝕏 : Proof} {x : 𝕏.X} {Γ : SplitSequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSSeq (M, w) Γ) (n : ℕ) : ∃ (m : ℕ), M.R ↑(chain prop w_prop n).snd ↑(chain prop w_prop (n + m)).snd

The right projection of chain eventually progresses.

noncomputable def SplitCut.inc_chain_eventual_inc_chain {β : Sort u_1} {Q : β → β → Prop} {g : ℕ → β} (Q_prop : ∀ (n : ℕ), ∃ (m : ℕ), Q (g n) (g m)) (n : ℕ) : { b : β // ∃ (n : ℕ), b = g n }

Progressing subchain of an eventually increasing chain

Equations

• SplitCut.inc_chain_eventual_inc_chain Q_prop 0 = ⟨g ⋯.choose, ⋯⟩
• SplitCut.inc_chain_eventual_inc_chain Q_prop n_2.succ = match SplitCut.inc_chain_eventual_inc_chain Q_prop n_2 with | ⟨ih, ih_prop⟩ => ⟨g ⋯.choose, ⋯⟩

theorem SplitCut.inc_chain_eventual_inc_chain_prop {β : Sort u_1} {Q : β → β → Prop} {g : ℕ → β} (Q_prop : ∀ (n : ℕ), ∃ (m : ℕ), Q (g n) (g m)) (n : ℕ) : Q ↑(inc_chain_eventual_inc_chain Q_prop n) ↑(inc_chain_eventual_inc_chain Q_prop (n + 1))

An eventually progressing chain has an progressing subchain.

theorem SplitCut.soundness_sseq (Γ : SplitSequent) : ⊢Γ → ⊨Γ

Soundness theorem for the GL-split proof system.

Soundness of GL-split cut proof system.

This soundness theorem follows by converting any GL-split proof into a GL-split cut proof.

def α_conv (𝕏 : Split.Proof) : 𝕏.X → SplitCut.T.obj 𝕏.X

Converts structure morphism for GL-split proof into a structure morphism for GL-split cut proofs.

Equations

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

theorem SplitProofIsSplitCutProof (Γ : SplitSequent) : ⊢Γ → ⊢Γ

If there is a GL-split proof of Γ then there is a GL-split cut proof of Γ.

theorem Split.soundness_sseq (Γ : SplitSequent) : ⊢Γ → ⊨Γ

Soundness theorem for the GL-split cut proof system.