Computer verification for historians of philosophy
Published in Synthese, 2022
Recommended citation: Elkind, Landon D.C. "Computer verification for historians of philosophy". *Synthese*, First View, Special Issue: Metaphilosophy of Formal Methods, 1(3). https://doi.org/10.1007/s11229-022-03678-y
Abstract
Interactive theorem provers might seem particularly impractical in the history of philosophy. Journal articles in this discipline are generally not formalized. Interactive theorem provers involve a learning curve for which the payoffs might seem minimal. In this article I argue that interactive theorem provers have already demonstrated their potential as a useful tool for historians of philosophy; I do this by highlighting examples of work where this has already been done. Further, I argue that interactive theorem provers can continue to be useful tools for historians of philosophy in the future; this claim is defended through a more conceptual analysis of what historians of philosophy do that identifies argument reconstruction as a core activity of such practitioners. It is then shown that interactive theorem provers can assist in this core practice by a description of what interactive theorem provers are and can do. If this is right, then computer verification for historians of philosophy is in the offing. <\details> 