**Coding the Proofs of ****Principia Mathematica**** in Coq**

**Coding the Proofs of**

**Principia Mathematica**

In this ongoing, long-term digital scholarship project, I use the computer proof-assistant Coq to computer check the proofs in *Principia Mathematica* under rival interpretations. This has historical interest 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.

This 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.

My work on this project is presently supported by an Izaak Walton Killam Memorial Postdoctoral Fellowship with the University of Alberta’s Philosophy Department. Many thanks to the Killam Trusts for their support of this fellowship.

**Digitizing and Publishing Bertrand 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.

**A Public-Domain ***Prototractatus*

*Prototractatus*

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.

**The Search for Logical Forms: In Defense of Logical Atomism**

**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 longer dissertation abstract is available here. The chapter titles are as follows:

- The Logical Atomism of Russell
- The Archetype for Logical Atomism:
*Principia Mathematica* - The Logical Atomism of Wittgenstein
- A Philosophy of Logic for Logical Atomism: Pure Logic
- A Formal Logic for Pure Logic:
**Z**-Types - A Metaphysics for
**Z**-Types: Logical Concepts and Logical Facts