Graham Leach-Krouse, assistant professor of philosophy at Kansas State University, has created some remarkable new logic software and has made it free for everyone to use and develop. He has named the software Carnap and describes it in the guest post* below.
Carnap is a software framework for creating and manipulating languages. You can use it to write programs (and, in particular, web-apps) for dealing with formal languages and logics.
(Why “Carnap”? Roughly, because of Rudolph Carnap’s Principle of Tolerance. Loosely paraphrased: “everyone is (or should be) at liberty to build up their own logic (i.e. their own form of language). All that’s required is to state your methods clearly and give your syntactical rules.”)
I created Carnap because I wasn’t really happy with the computer support available to me for my logic teaching. Here are some things that are nice about teaching logic with Carnap:
- Carnap is free. My students don’t have to pay to use it, and don’t need to buy a textbook to access it.
- Carnap simplifies my teaching. It handles almost all of my logic grading, and gives my students lots of immediate feedback on their work.
- Carnap is extensible. It’s designed to work with many different formal systems (I’ve implemented more than two dozen) and to make it easy to add more. Because of this, I’m not tied to the system of any one textbook, and I can even teach topics like higher-order or modal logic, for which there’s almost no pedagogical software support right now.
- Carnap’s applications can be deployed on the web. That means they’re accessible, without installation, on any device that can run a web
- Carnap is libre software (GPL3-licensed). Anybody can add to the software or improve it, as long as they’re willing to share their improvements with everyone. You can find the source-code and put in requests for changes here.
- Carnap is actively developed. I’m using it in my own teaching, and I plan to continue improving and extending it.
I’ve used Carnap to build a website for class management. I use this site in my own teaching. Several other instructors have also been using it over last two semesters. Here’s what some homework problems might look like:
And here’s a video of using Carnap to derive the law of the excluded middle:
Right now, the Carnap website supports natural deduction for about 30 formal systems, including: the propositional and first-order logics of Montague’s Logic, of Bergmann and Moor’s The Logic Book, and of both P.D. Magnus’ original forall x and the Calgary Remix of that text. It also supports the propositional logic of Tomassi’s Logic, and the first-order systems presented by Goldfarb in Deductive Logic. It supports quite a few modal logics: in particular, Hardegree’s natural deduction systems for modal logics K, D, T, B, 4, 5, and S5, Hardegree’s “world theory” WTL, and Hardegree’s presentation MPL of naive possibilist quantified modal logic (all of these can be found in Hardegree’s Modal Logic text). Finally, it supports a system of second-order logic, and two systems of elementary set theory.
The site also supports truth-tables, syntactical parsing exercises, and translations from English to propositional and first-order logic. The site includes an interactive textbook with some ready-made problem sets. But you can also use the site without the textbook by creating custom assignments, which your students can then access on the web.
Why am I telling you all this? Well, I think it’d be great if the project were to continue to grow.
I’d like to find more users, since the more people who are using the software, the greater the contribution to the profession, the more feedback I get, and the more of an excuse I have to spend time on it. Ultimately, I’d also like to find some folks who would like to help on the development end. The dream, with an open-source piece of software like this, is that you can get a community of people to work together and make something really great. There are lots of you out there who know a thing or two about web-design, about pedagogy, and certainly about logic. It would be wonderful if we could put all that expertise to work, and build a fantastic new set of tools for philosophers.
There are still a million things left to do (first-order counterexamples, semantic tableaux, sequent calculi…) But Carnap has already been a great help to me, and has gotten positive reviews from the kind folks who have volunteered to beta-test. So I think it’s time to invite everyone to try it out. If you’d like to learn more, take a look the Carnap “about” page, where you can find additional information, interactive examples, and links to documentation.
If you’re interested in using Carnap for your logic course, please send me an email at [email protected], and I’ll let you know how to get an instructor account set up on carnap.io. I’d also be happy to talk to you about adding your favorite formal system, if it isn’t already supported. And if you’re interested in using Carnap in some other way (bespoke proof assistant for a large-scale formalization project? formally verified wiki of proofs? development of interactive online teaching materials for topics in philosophical logic?) let me know and I’ll do my best to help out.