用于可废止疑问推理的无切割相继式演算

近年来，形式化疑问推理——即指向问题及由问题出发的推理——已成为疑问逻辑研究者的核心关切。然而，鲜有人尝试为这些推理建立证明论。为填补此空白，我们针对推理疑问逻辑（IEL）所研究的两类疑问推理——疑问引发与疑问蕴涵——构造了一个对（各类）相继式可靠且完备的演算。尽管已有工作尝试在相继式系统中公理化前者，但目前尚无后者的证明论。此外，既有的疑问引发公理化未能刻画其可废止特性，也未提供引入或消去问题形成算子的规则。相反，我们的演算对相继式编码了可废止条件，并提供了支配疑问公式引入与消去的规则。我们证明了一种适用于陈述句与疑问公式的切割规则版本的消去定理在我们的系统中成立，且 IEL 中问题引发的公理刻画规则在我们的系统中可容许。