Classical Logic with Mendler Induction A Dual Calculus and Its Strong Normalization

摘要

We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering prepositional, second-order, and (co-)inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-)iterator that remains strongly normalizing under head reduction. We prove this using a non-constructive realizability argument.