  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.
