What question did this study set out to answer?

This research aims to establish a proof-theoretic framework for interpolation in inquisitive propositional logic.

May 4, 2026Open Access

A Proof-Theoretic Interpolation Theorem for Inquisitive Propositional Logic

Key Points

This research aims to establish a proof-theoretic framework for interpolation in inquisitive propositional logic.
Developed a sequent calculus for inquisitive propositional logic by extending g3ip for intuitionistic logic.
Introduced rules for double negation elimination and the Split Property.
Utilized Maehara's lemma to achieve interpolation.
Proved admissibility of cut in the sequent calculus.
Demonstrated interpolation 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.

Mark Helpful

Bookmark

Relay

View Full Paper