Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. This pattern is especially common amongst logicians and set theorists, but workaday mathematicians also commonly do this too, witnessed by narrative notes accompanying a proof -- "the following proof is constructive", or "the following proof does not use choice", for example. Yet, current proof assistants provide poor support for capturing these narrative notes formally, an observation that is especially true of systems based on Gordon's HOL, a classical higher-order logic. Consequently, HOL and its many implementations seem ironically more committed to classical reasoning than mainstream mathematicians are themselves, limiting the mathematical content that one may easily formalise. To facilitate these context switches, we propose that mathematicians mentally employ a simple tainting system when temporarily working subclassically -- an idea not currently explored in proof assistants. We introduce a series of modest but far-reaching changes to HOL, extending the standard two-place Natural Deduction relation to incorporate a taint-label, taken from a particular lattice, and which describes or limits the "amount" of classical reasoning used within a proof. Taint can be seen either as a simple typing system on HOL proofs, or as a form of static analysis on proof trees, and partitions our logic into various fragments of differing expressivity, sitting side-by-side. Results may pass from a "less classical" fragment into a "more classical" fragment of the logic without modification, but not vice versa, with the flow of results between worlds controlled by an inference rule akin to a subtyping or subsumption rule.

翻译：尽管数学家默认采用经典推理原则，但他们在实际工作中常会切换上下文，将自身限制于各种次经典推理形式。这种模式在逻辑学家和集合论研究者中尤为常见，但普通数学家也频繁如此——这从伴随证明的叙述性附注中可见一斑，例如"以下证明是构造性的"或"以下证明未使用选择公理"。然而，当前证明助手对这些叙述性附注的形式化捕获支持不足，这一点在以基于Gordon的高阶逻辑（经典高阶逻辑）的系统上表现得尤为突出。因此，HOL及其众多实现似乎比主流数学家本身更执着于经典推理，从而限制了可轻松形式化的数学内容。为促进这些上下文切换，我们提出数学家在进行临时次经典工作时会采用一种简单的污染标注系统——这一思路在现有证明助手中尚未被探索。我们对HOL进行了一系列适度但影响深远的改造，将标准的两元自然演绎关系扩展为包含一个来自特定格结构的污染标签，该标签描述或限制证明中使用的"经典推理量"。污染既可被视作HOL证明上的简单类型系统，也可看作对证明树的静态分析形式，它将我们的逻辑划分为不同表达力的片段，使其并排共存。结果可从"较少经典性"片段无修改地流向"更多经典性"片段，反之则不可行，世界间的结果流向受控于类似子类型或包含规则的推理规则。