Research

The Principia Rewrite Project

Most of my current research as a Killam Postdoctoral Fellow focuses on the Principia Rewrite project, which is my long-term, open-source, digital humanities project of rewriting Whitehead and Russell's Principia Mathematica. What I am actually doing is best summarized in a picture:

Rewriting Principia is a three-step process: first, I take Whitehead and Russell’s original Principia proof on the left. However, the original "proof" is in most cases really a proof sketch omitting a lot of steps. So the second step involves filling out the missing steps. For this I am using the interactive theorem prover Coq to ensure each proof step is a valid step according to Principia’s axioms and that no steps are skipped, even by accident. Finally, I am taking the Coq encoding to reconstruct and typeset the full, gap-free proof as it would appear in Principia’s notation. Below is a sample screenshot of the encoding of *4.4 in Coq.

So far, the Principia Rewrite project has, for the first time, computer verified all of Principia's Section A (propositional logic, or *1-*5) in a historically accurate way. By "historically accurate," I mean that all 189 proofs in Principia's propositional logic have been reconstructed fully in Coq such that each full proof cites all propositions mentioned in Whitehead and Russell's proof sketch. In the next year, I plan to complete a rewrite of Section B (quantification theory, reducibility, identity, and descriptions, or *9-*14) that is similarly faithful to the original text's proof sketches.

The Principia Rewrite project has methodological interest as suggesting a way for historians of philosophy to deploy computational tools in reconstructing arguments in texts. Interactive theorem provers like Coq allow us to encode and computer check reconstructions of texts, and to cross-check and compare them with other reconstructions throughout a corpus. Some interactive theorem provers can even offer hints and suggestions as to what to do next in constructing a proof. This is suggestive of one way in which modern digital tools can be useful to scholars doing traditional scholarship in the history of philosophy.

The Principia Rewrite project also has historical interest. It helps us rethink Principia's reputation as a "step backwards" from Gottlob Frege's Grundgesetze. This sort of evaluation of Principia was defended by notable logicians like Kurt Gödel, who especially complained about its proof sketches and syntax. The Principia Rewrite is revealing, firstly, that the proof sketches are actually quite methodical, so that what is omitted are almost always simple applications of commutativity or association. So this project gives us insight into the logical structure of Principia, as might be visualized using a subway-style map. Below is a sample of from the propositional logic proofs in *2.

Secondly, the Principia Rewrite project can serve as a tool to settle longstanding scholarly disputes concerning Principia's syntax: scholars debate whether the syntax is ramified or not. This will allow one to automatically verify whether the proofs stand on each rival reading and to survey whether proofs are preserved on the competing interpretations. It would also bear on Gödel's and others' criticism of the omitted type indices and scope conventions: it would stand to reason that the omissions are not so severe if they can be reconstructed faithfully and fully in Coq.

Finally, the Principia Rewrite project also bears on the philosophy of mathematics: this coding of Principia will function as a tool for rigorously extending Principia's logical framework to areas of mathematics not covered in the original work, like group theory, topology, and geometry, providing further support for the Logicist view of mathematics, which I am also concerned to defend in other papers.

Funding. This project was first undertaken with the support of an Izaak Walton Killam Memorial Postdoctoral Fellowship with the University of Alberta's Philosophy Department. Thanks are due to the Killam Trusts for their support of this research.

Digitizing Russell's pocket diaries

Bertrand Russell's pocket diaries are currently held in the Bertrand Russell Archives. These 64 diaries, spanning 1902-1905 and 1908-1969, are entirely contained in Series 240, Box Numbers 9.18-9.20. They span a good deal of Russell's 97-year life. They have not yet been published in an edited collection for scholarly use, nor digitized so as to make them easily searchable or readily viewable online.

However, Russell's pocket diaries shed valuable light on not only who Russell met and when—which is manifestly valuable for historical and scholarly work on Russell's life and philosophy—but also how Russell viewed certain things. For example, in one pocket diary Russell described his famous lectures on logical atomism as "LL" - logic lectures. This is evidence that Russell saw his lectures as logic-oriented rather than, as many scholars have argued, as epistemology-oriented. This is quite a nugget of information contained in one of these diaries.

The goal of this project is to digitize the pocket diaries so as to make them searchable and viewable online, and also to publish a scholarly edition of these diaries as an edited collection.

Other paper projects

• Carnap's marginal notes on Manley H. Thompson's term paper for Russell's U. Chicago seminar
• Computer verification for historians of philosophy
• Dot notation in Principia: its forerunners, its descendants, and its near-demise
• Dorothy Wrinch's work on set theory and the axiom of choice in the 1920s
• Logical atomism in Wittgenstein's pre-Tractatus 1913 Notes and 1914 Notes
• Making anti-exceptionalism about logic consistent with logic's basic epistemic role

Past Projects

The University of Iowa Tractatus Map

I contributed to The University of Iowa Tractatus Map, a project led by David G. Stern and Phillip Ricks. My main contribution was to convert the text of the Prototractatus into a digital format that allowed us to generate a digital, subway-style map of the Prototractatus and compare it to the Tractatus. The project is described in Daily Nous. Here is a brief summary, and a picture of the University of Iowa Tractatus Map:

Thanks to Luciano Bazzochi's work on Wittgenstein's Tractatus, we have a new and illuminating way to read the Tractatus. We may arrange the Tractatus' numbered propositions 'tree-wise', as opposed to arranging them in the usual linear manner. This produces a subway-style map of the Tractatus and of the earlier Prototractatus.

So there has been much fruitful activity in producing survey-able, 'tree-wise' arrangements of the Tractatus. Though we now have subway-style maps, we are still missing a public-domain, tree-wise textual arrangement of the Prototractatus. One of my ongoing projects is to produce such an edition of the Prototractus using LaTeX. This would be a readable and illuminating re-arrangement of an important text for both Wittgenstein scholars and students of the history of philosophy.

Dissertation

The Search for Logical Forms: In Defense of Logical Atomism

In my dissertation, I defend a new version logical atomism. I first criticize the standard interpretation of Russell's logical atomism as a search for logical atoms, and then I reinterpret it as a search for logical forms. I argue that logical atomists are term-busters, and they search for logical forms by taking apparent terms and busting them into non-term parts of formulas, just as is done in Principia Mathematica.

I split my dissertation into two parts: in the first part, I support my interpretation of logical atomism using its history. In the second part, I develop my own brand of logical atomism. So in the first part, I reinterpret the logical atomism genus; in the second part, I create my own species of logical atomism.

A public abstract is available here. The chapter titles are as follows:

1. The Logical Atomism of Russell
2. The Archetype for Logical Atomism: Principia Mathematica
3. The Logical Atomism of Wittgenstein
4. A Philosophy of Logic for Logical Atomism: Pure Logic
5. A Formal Logic for Pure Logic: Z-Types
6. A Metaphysics for Z-Types: Logical Concepts and Logical Facts