A modest proposal: explicit support for foundational pluralism

**Abstract.** 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. As such, 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 bounded 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. Denizens of all worlds reason over
the same set of definitions, and to maximise reuse users
are therefore given incentive to phrase results in the
weakest possible world that will suffice, eschewing
needlessly-classical reasoning.

**Downloads:** Paper (draft). Implementation (Github). BibTeX