A “Propositions as Types” Interpretation of Classical Logic

This paper presents a theorem–proof style account of a “propositions as types” interpretation of classical logic. Inhabited and uninhabited types are represented by \(\top\) and \(\bot\), and a small family of type-level reductions is used to evaluate logical types at the level of truth values. When a type reduces to the canonical inhabited form \(\bot\rightarrow\bot\), its canonical reduced witness is the identity inhabitant \(i_{\bot{\rightarrow\bot}}:\bot\rightarrow\bot\). A witness of the original type is then treated as an induced witness, read from this reduced identity form and interpreted schematically, and in general contextually, at the original type. The resulting framework is applied to first-order classical propositional logic and to first-, second-, and higher-order classical predicate logic. The emphasis is on a uniform formal presentation while retaining the motivating idea that classical reasoning may be represented without introducing explicit control operators into the term language.