theorem LogicGL.provable_imp_iff_provableGentzen_seqent {α : Type u} [DecidableEq α] {A B : Formula α} : A 🡒 B ∈ LogicGL ↔ ⊢ᵍ[GL] ({A} ⟹ {B})

noncomputable def LogicGL.interpolant {α : Type u} [DecidableEq α] {A B : Formula α} (h : A 🡒 B ∈ LogicGL) : Formula α

Equations

• LogicGL.interpolant h = LogicGL.ProvableGentzen.interpolant (LogicGL.PartitionOf.ss A B) ⋯

theorem LogicGL.interpolant_provable_ant {α : Type u} [DecidableEq α] {A B : Formula α} {h : A 🡒 B ∈ LogicGL} : A 🡒 interpolant h ∈ LogicGL

theorem LogicGL.interpolant_provable_suc {α : Type u} [DecidableEq α] {A B : Formula α} {h : A 🡒 B ∈ LogicGL} : interpolant h 🡒 B ∈ LogicGL

theorem LogicGL.interpolant_atoms {α : Type u} [DecidableEq α] {A B : Formula α} {h : A 🡒 B ∈ LogicGL} : (interpolant h).atoms ⊆ A.atoms ∩ B.atoms

theorem LogicGL.CIP {α : Type u} [DecidableEq α] {A B : Formula α} (h : A 🡒 B ∈ LogicGL) : ∃ (C : Formula α), A 🡒 C ∈ LogicGL ∧ C 🡒 B ∈ LogicGL ∧ C.atoms ⊆ A.atoms ∩ B.atoms

Craig interpolation property of LogicGL.