Soundness of GL-proof system.

noncomputable def chain {𝕏 : Proof} {x : 𝕏.X} {Γ : Sequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSeq (M, w) Γ) (n : ℕ) : (y : 𝕏.X) × { u : W // ¬evaluateSeq (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.
• chain prop w_prop 0 = ⟨x, ⟨w, ⋯⟩⟩

theorem chain_proof_prop {𝕏 : Proof} {x : 𝕏.X} {Γ : Sequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSeq (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 chain_model_prop {𝕏 : Proof} {x : 𝕏.X} {Γ : Sequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSeq (M, w) Γ) (n : ℕ) : (¬(r 𝕏.α (chain prop w_prop n).fst).isBox = true → ↑(chain prop w_prop n).snd = ↑(chain prop w_prop (n + 1)).snd) ∧ ((r 𝕏.α (chain prop w_prop n).fst).isBox = true → 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 has_children_of_chain_model {𝕏 : Proof} {x : 𝕏.X} {Γ : Sequent} (prop : f (r 𝕏.α x) = Γ) {W : Type} {M : Model W} {w : W} (w_prop : ¬evaluateSeq (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 incChainEventualIncChain {β : 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

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

theorem incChainEventualIncChain_prop {β : Sort u_1} {Q : β → β → Prop} {g : ℕ → β} (Q_prop : ∀ (n : ℕ), ∃ (m : ℕ), Q (g n) (g m)) (n : ℕ) : Q ↑(incChainEventualIncChain Q_prop n) ↑(incChainEventualIncChain Q_prop (n + 1))

An eventually progressing chain has an progressing subchain.

theorem soundness_seq (Γ : Sequent) : ⊢Γ → ⊨Γ

Soundness theorem for the GL-proof system.