Papers › A modest proposal: explicit support for foundational pluralism
A modest proposal: explicit support for foundational pluralism
Martin Berger, Dominic P. Mulligan
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
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.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections