New Free Open-Source Multi-Purpose Multi-System Logic Software


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: a New Free Open-Source Multi-Purpose Multi-System Logic Software
by Graham Leach-Krouse

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:

  1. Carnap is free. My students don’t have to pay to use it, and don’t need to buy a textbook to access it.
  2. Carnap simplifies my teaching. It handles almost all of my logic grading, and gives my students lots of immediate feedback on their work.
  3. 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.
  4. Carnap’s applications can be deployed on the web. That means they’re accessible, without installation, on any device that can run a web
    browser.
  5. 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.
  6. 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:

Carnap – sample problem 1
Carnap – sample problem 2
Carnap – sample problem 3
Carnap – sample problem 4
Carnap – sample problem 5

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.

Disputed Moral Issues - Mark Timmons - Oxford University Press
Subscribe
Notify of
guest

8 Comments
Oldest
Newest Most Voted
Inline Feedbacks
View all comments
Andrew P Mills
Andrew P Mills
5 years ago

This is fantastic! I’ve been looking for ways to have my students get instant feedback on homework while they are doing it, and have been developing some clunky ways of doing that. This seems (potentially) much better. I’m about to email you to find out more!

Patricia A Blanchette
Patricia A Blanchette
5 years ago

Way cool.

Jay Carlson
Jay Carlson
5 years ago

https://www.harryhiker.com/lc/

Harry Gensler has written a logic software that he’s used in his courses. It looks a bit outdated (and has some odd quirks to it as well), but I’ve heard good things from people who’ve used it in teaching a logic course.

Curtis Franks
Curtis Franks
5 years ago

This is great. Just the fact that the justification of steps 6 and 10 of sample problem #1 is called “negation elimination” instead of “falsum introduction” is a huge conceptual advantage over the infinitely more expensive software I’ve been teaching with the past 15 years.

Richard Zach (@RrrichardZach)
Richard Zach (@RrrichardZach)
Reply to  Curtis Franks
5 years ago

I did a roundup last year of free logic courseware http://richardzach.org/2017/09/21/logic-courseware/
I think Carnap is the most promising of the bunch. I look forward to using it.
BTW the forall x books are linked to their Amazon pages, but they are also open source: https://www.fecundity.com/logic/ for the original and http://forallx.openlogicproject.org/ for the Calgary version. I suspect the reason for the “conceptual advance” Curtis mentioned in Carnap may be the fact that the Calgary version of forallx switched to Gentzen’s original natural deduction rules.

Curtis Franks
Curtis Franks
Reply to  Richard Zach (@RrrichardZach)
5 years ago

I did not have forallx in mind at all. But I am heartened by what you report about it and what I see in Carnap: natural deduction presented as a characterization of logical operators as universal properties, not as a ramshackle collection of rules that happens to work.

Matt Weiner
Matt Weiner
5 years ago

This looks fantastic!

Jill Rusin
Jill Rusin
3 years ago

Two years later!: Now with remote delivery happening, the promise of instant feedback, accessible on the web (and not needing to run software), seems like it will be so helpful to students. What a fantastic project.