Using Carnap

General introduction

Carnap is, as the project page describes it, “a free and open software framework written in Haskell for teaching and studying formal logic.” It can be customized to use many symbolization and proof systems, including the one we are using in this course (from forall x: Calgary). It allows you to type and structure symbolizations, natural deduction proofs, and truth tables, and it is capable of checking proofs for errors and giving you a heads-up that there’s a problem.

The system is named after Rudolf Carnap, a twentieth century philosopher who made major contributions to philosophy of science and logic.

I have not used the Carnap system in a course before. So, for us it is a bit of an experiment. I hope you will give me feedback on where you could use clearer guidance, what you like, and what you don’t like (if anywhere/anything). There are ways for me to set it up differently for our use, that I would be happy to try, for example.

Accessing Carnap

I posted a login link to Blackboard. It should allow you to create a login to work on Carnap. Let me know if you have any problems.

Typing Truth-functional Logic in Carnap

Here are the different ways you can type the logical connectives and symbols of TFL. For almost all of them, there is more than one way to type it!

So, for example, “If P then not Q” can be typed into symbols using P > ~Q (or also P -> -Q). For TFL, you can probably leave your caps-lock key on!

Typing natural deduction proofs in Carnap

To write a proof, you just need to write each inference on its own line.

Justifications are introduced by a colon, like :R 2 for “reiteration from line 2”, and can typed be typed using the symbol set above (as needed). Further examples: :/\E 4 for “Conjunction Elimination from line 4,” or :->I 2–6 for Conditional Introduction from lines 2 through 6.

You can flag that a sentence is a premise by justifying it with :PR. Of course, when we write proofs by hand using our system, we usually leave the justification space blank for premises, but adding that helps the interpreter understand that you haven’t just forgotten the justification.

So, a very simple proof might look like:

A /\ B :PR
B > ~A :PR
B :/\E 1
~A :->E 2,3

Try to read through that to see if you can understand it.

Typing subproofs

In Carnap, you can make a subproof by indenting the lines that make up the subproof, and by justifying its first line (the assumption of the subproof) with :AS (for “assumption”) to the right of the sentence. You can indent any number of spaces; I think two spaces is easy to read.

Sentences not in a subproof must not be indented at all, and sentences in the same subproof must be indented the same number of spaces.

Questions

Contact me if you have any questions and I can add any missing information here!