Synthese 200 (3):1-28 (2022)
Authors |
|
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.
|
Keywords | Formal methods Formalization History of philosophy Interactive theorem provers Metaphilosophy |
Categories | (categorize this paper) |
ISBN(s) | |
DOI | 10.1007/s11229-022-03678-y |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Principia mathematica.A. N. Whitehead & B. Russell - 1910-1913 - Revue de Métaphysique et de Morale 19 (2):19-19.
View all 38 references / Add more references
Citations of this work BETA
No citations found.
Similar books and articles
Voting Theory in the Lean Theorem Prover.Wesley H. Holliday, Chase Norman & Eric Pacuit - 2021 - In Sujata Ghosh & Thomas Icard (eds.), Logic, Rationality, and Interaction: 8th International Workshop, Lori 2021, Xi’an, China, October 16–18, 2021, Proceedings. Springer Verlag. pp. 111-127.
How to Avoid the Formal Verification of a Theorem Prover.A. Avellone, M. Benini & U. Moscato - 2001 - Logic Journal of the IGPL 9 (1):1-25.
Speedith: A Reasoner for Spider Diagrams.Matej Urbas, Mateja Jamnik & Gem Stapleton - 2015 - Journal of Logic, Language and Information 24 (4):487-540.
Program Verification, Defeasible Reasoning, and Two Views of Computer Science.Timothy R. Colburn - 1991 - Minds and Machines 1 (1):97-116.
On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification.Nicola Angius - 2020 - Philosophy and Technology 33 (2):349-355.
About Some New Methods of Analytical Philosophy. Formalization, De-Formalization and Topological Hermeneutics.Janusz Kaczmarek - 2020 - Studia Humana 9 (3-4):140-153.
Philosophical Aspects of Program Verification.James H. Fetzer - 1991 - Minds and Machines 1 (2):197-216.
A Parametric, Resource-Bounded Generalization of Löb’s Theorem, and a Robust Cooperation Criterion for Open-Source Game Theory.Andrew Critch - 2019 - Journal of Symbolic Logic 84 (4):1368-1381.
A Finitely Axiomatized Formalization of Predicate Calculus with Equality.Norman D. Megill - 1995 - Notre Dame Journal of Formal Logic 36 (3):435-453.
The Triumph of Types: Principia Mathematica's Impact on Computer Science.Robert L. Constable - unknown
Hermeneutics, Logic and Reconstruction.Friedrich Reinmuth - 2014 - History of Philosophy & Logical Analysis 17 (1):152–190.
Analytics
Added to PP index
2022-03-26
Total views
114 ( #104,127 of 2,520,771 )
Recent downloads (6 months)
114 ( #5,978 of 2,520,771 )
2022-03-26
Total views
114 ( #104,127 of 2,520,771 )
Recent downloads (6 months)
114 ( #5,978 of 2,520,771 )
How can I increase my downloads?
Downloads