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. 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.