A modest proposal: explicit support for foundational pluralism

TL;DR

This paper proposes a novel extension to HOL proof systems that introduces a tainting mechanism to explicitly manage and switch between different levels of classical reasoning within proofs, enhancing formalization flexibility.

Contribution

It introduces a tainting system for HOL that allows explicit control over classical reasoning levels, enabling seamless context switching in formal proofs.

Findings

Enables formal distinction between classical and non-classical reasoning fragments

Allows flow of results from less classical to more classical fragments

Provides a static analysis tool for proof trees in HOL

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.