The AllenSL system in Carnap

Carnap.io is logic software that runs in a browser. It supports the formal systems that are in a number of different textbooks. (There’s a list here: https://carnap.io/shared/gleachkr@gmail.com/carnap-derivations.pandoc.) I use a system for propositional logic that is similar to the one found in Allen and Hand’s Logic Primer, and I will explain it here for anyone who has used the Logic Primer and might be interested in using Carnap.

The system is called AllenSL, and an extension that includes some derived rules is called AllenSLPlus. First, AllenSL uses Fitch notation, not the Lemmon-style system that is in the Logic Primer. There are also a few other differences explained below, but most importantly, any proof using the primitive rules of proof in the Logic Primer can be done in roughly the same number of steps and will be the same level of difficulty for students (with maybe one small exception that is noted below).


These are the rules of derivation in AllenSL:

conjunction-introduction (&Ⅰ): P, Q ⊢ P & Q

conjunction-elimination (&E): P & Q ⊢ P or P & Q ⊢ Q

disjunction-introduction (∨Ⅰ): P ⊢ P ∨ Q or P ⊢ Q ∨ P

disjunction-elimination (∨E): P ∨ Q, ¬P ⊢ Q

conditional-elimination (→E): P → Q, P ⊢ Q

biconditional-introduction (↔Ⅰ): P → Q, Q → P ⊢ P ↔ Q

biconditional-elimination (↔E): P ↔ Q, P ⊢ Q or P ↔ Q, Q ⊢ P

double-negation (DN): ¬¬P ⊢ P or P ⊢ ¬¬P

reiteration (R): P ⊢ P

conditional-introduction (→Ⅰ): from a subproof beginning with the assumption A and ending with B, infer A → B.

negation-introduction (¬Ⅰ or RAA): from a subproof beginning with the assumption A and ending with B and ¬B (or ¬B and B) on consecutive lines, infer ¬A.

negation-elimination (¬E or RAA): from a subproof beginning with the assumption ¬A and ending with B and ¬B (or ¬B and B) on consecutive lines, infer A.

The symbols for the logical operators are ¬, &, ∨, →, and ↔, and they are typed with ~, &, v, ->, and <->. Premises are labeled with ‘PR’. Other assumptions are labeled with ‘AS’. The parentheses dropping conventions are close to those given on p. 9 in the Logic Primer. The only differences are that ∨ binds more strongly than &, and → and ↔ bind equally strongly.


Besides using Fitch notation, the rules of derivation differ from those in the Logic Primer in the following ways.

(1) The disjunction-elimination rule requires the negation, not merely the denial, of one of the disjuncts. Consequently, to derive P from P v ¬Q and Q, the double-negation rule has to be used—for example, as shown here:

(2) Allen and Hand’s reductio ad absurdum rule (RAA) can be used as it is explained on p. 24 in the Logic Primer (with the necessary adjustments for Fitch notation). Alternatively, that rule can be split into a negation-introduction rule and a negation-elimination rule, which is what I use. (Probably, students should only be told about the availability of one or the other.)

(3) The reiteration rule is included to facilitate using RAA or ¬I/¬E with Fitch notation. (Not always, but often, one line of the contradiction will need to be moved down from somewhere else in the proof.)

In this example, the reiteration rule is used to get the contradiction on consecutive lines at the end of the subproof. ‘¬I’ in line 6 can be replaced with ‘RAA’ (while keeping everything else the same).

(4) The biconditional-elimination rule in AllenSL is the “modus ponens for the biconditional,” not the one on pp. 25 – 26 in the Logic Primer. I think that, in most cases, this difference won’t have much effect, although, depending on what else is available in the proof and what the goal is, a derivation with the AllenSL biconditional-elimination rule could be more difficult for students.

You can try Carnap out here: https://carnap.io/shared/gregory.s.johnson@gmail.com/playground-AllenSL.txt (Put a colon before the PR, AS or rule, and put the lines numbers being cited after the abbreviation for the rule.) For example, like this:

Derived Rules

I don’t use any derived rules in my 1000-level logic course, but the following five are included in AllenSLPlus.

Hypothetical syllogism (HYP), which is S16 on p. 29 in the Logic Primer.

Dilemma (DIL), which is S25 on p. 29 in the Logic Primer.

Modus tollens (MT), but only S12 on p. 29 in the Logic Primer.

Material conditional (MC), which is Allen and Hand’s “wedge-arrow” but only S21 and S22 (in both directions).

DeMorgan’s laws (DeM), but only S28 and S29.

You can try these out here: https://carnap.io/shared/gregory.s.johnson@gmail.com/playground-AllenSLPlus.txt

Truth Tables

For truth table problems, use system=”magnusSL”. That will display ¬, &, ∨, →, and ↔ for the logical operators, and it will assign the truth values for the operators in the standard way.

Textbook

For further information about using Carnap, go here: https://carnap.io/shared/Documentation (and probably start with 1, 2, 3, and 4).

If you’ve been using the Logic Primer and you want to use AllenSL in Carnap, you, perhaps, don’t need a textbook at all. This one, however, is freely available to use: forall x: The Mississippi State edition (and can be modified if you’re familiar with LaTeX). You can also just use the two pages listing the propositional logic rules in the appendix if that’s all that you need.

First-order Logic

Although I used to cover first-order logic in my 1000-level logic course, I’ve stopped (and I don’t ever teach any other logic courses). I may go back to including it at some point, but, as it is, I haven’t used Carnap for first-order logic. Using the ForallxQL system in Carnap will work, however, at least to an extent. The universal-elim, universal-intro, existential-intro, existential-elim, identity-intro, and identity-elim rules are, essentially, the same as those in the Logic Primer (with the necessary adjustments for Fitch notation). The only issue is that the biconditional-introduction, double negation, and RAA rules will not available. Perhaps that can be changed in the future, but if you’re primarily focused on the FOL rules, maybe it won’t matter.

For reference, here are some proofs using ForallxQL in Carnap. You can try it out yourself here: https://carnap.io/shared/gregory.s.johnson@gmail.com/playground-ForallxQL.txt (use ‘A’ for ‘∀’ and ‘E’ for ‘∃’.)

The second example on p. 81 in the Logic Primer, ∀x(Fx → Gx), ∀xFx ⊢ ∀xGx, becomes

The example at the bottom of p. 83, ∃xFx ⊢ ∃x(Fx ∨ Gx), becomes

The example at the top of p. 84, ∀xFxx, ∃x(Fxx → Pb) ⊢ Pb, becomes

And S88 on p. 87, ∀x(Fx → ¬Hx), ∃x(Gx & Fx) ⊢ ∃x¬Hx, is