A Proof-Theoretic Interpolation Theorem for Inquisitive Propositional Logic

Abstract

This paper presents a sequent calculus for Inquisitive Propositional Logic obtained by expanding the sequent calculus g3ip for intuitionistic propositional logic with suitable rules for double negation elimination for atoms and the Split Property. A suitable rule for the Split Property is obtained by taking advantage of the connection between the truth-conditional fragment in Inquisitive Logic and Harrop formulas. The paper proves admissibility of cut for the sequent calculus and uses the sequent calculus to prove interpolation for Inquisitive Propositional Logic. Interpolation is obtained using Maehara’s lemma.