the JohnsonSL system in Carnap
Carnap.io is logic software that runs in a browser. JohnsonSL is a propositional logic system for forallx: Mississippi State that can be use in Carnap.
These are the rules of derivation in JohnsonSL:

conjunctionintroduction (&I): P, Q \(\vdash\) P & Q

conjunctionelimination (&E): P & Q \(\vdash\) P or P & Q \(\vdash\) Q

disjunctionintroduction (\(\vee\)I): P \(\vdash\) P \(\vee\) Q or P \(\vdash\) Q \(\vee\) P

disjunctionelimination (\(\vee\)E): P \(\vee\) Q, \(\neg\)P \(\vdash\) Q

conditionalelimination (\(\rightarrow\)E): P \(\rightarrow\) Q, P \(\vdash\) Q

biconditionalintroduction (\(\leftrightarrow\)I): P \(\rightarrow\) Q, Q \(\rightarrow\) P \(\vdash\) P \(\leftrightarrow\) Q

biconditionalelimination (\(\leftrightarrow\)E): P \(\leftrightarrow\) Q, P \(\vdash\) Q or P \(\leftrightarrow\) Q, Q \(\vdash\) P

doublenegation (DN): \(\neg\neg\)P \(\vdash\) P or P \(\vdash\) \(\neg\neg\)P

reiteration (R): P \(\vdash\) P

conditionalintroduction (\(\rightarrow\)I): from a subproof beginning with the assumption A and ending with B, infer A \(\rightarrow\) B.

negationintroduction (\(\neg\)I or RAA): from a subproof beginning with the assumption A and ending with B and \(\neg\)B (or \(\neg\)B and B) on consecutive lines, infer \(\neg\)A.

negationelimination (\(\neg\)E or RAA): from a subproof beginning with the assumption \(\neg\)A and ending with B and \(\neg\)B (or \(\neg\)B and B) on consecutive lines, infer A.
The symbols for the logical operators are \(\neg\), &, \(\vee\), \(\rightarrow\), and \(\leftrightarrow\), and they are typed with ~, &, v, >, and <>. Premises are labeled with â€˜PRâ€™. Other assumptions are labeled with â€˜ASâ€™. The parentheses dropping conventions are as follows. \(\vee\) binds more strongly than &; & binds more strongly than \(\rightarrow\) and \(\leftrightarrow\); \(\rightarrow\) and \(\leftrightarrow\) bind equally strongly.
Some further details
The disjunctionelimination rule requires the negation, not merely the denial, of one of the disjuncts. Consequently, to derive P from P \(\vee\) \(\neg\)Q and Q, the doublenegation rule has to be usedâ€”for example, as shown below on the left.
Following Allen and Hand, a reductio ad absurdum rule (RAA) can be used to derive the denial of an assumption. Alternatively, two different rules can be used, a negationintroduction rule and a negationelimination rule. (Probably, students should only be told about the availability of one or the other.)
The reiteration rule is included to facilitate using RAA or \(\neg\)I/\(\neg\)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 the example on the right, the reiteration rule is used to get the contradiction on consecutive lines at the end of the subproof. â€˜\(\neg\)Iâ€™ in line 6 can be replaced with â€˜RAAâ€™ (while keeping everything else the same).
Carnap requires a colon before the PR, AS, or rule. Put the lines numbers being cited after the abbreviation for the rule. For example, as is shown here.
Derived Rules
I donâ€™t use any derived rules in my 1000level logic course, but the following five are included in JohnsonSLPlus.

Hypothetical syllogism (HYP): P \(\rightarrow\) Q, Q \(\rightarrow\) R \(\vdash\) P \(\rightarrow\) R

Dilemma (DIL): P \(\vee\) Q, P \(\rightarrow\) R, Q \(\rightarrow\) R \(\vdash\) R

Modus tollens (MT): P \(\rightarrow\) Q, \(\neg\)Q \(\vdash\) \(\neg\)P

Material conditional (MC): \(\neg\)P \(\vee\) Q \(\dashv\vdash\) P \(\rightarrow\) Q and P v Q \(\dashv\vdash\) \(\neg\)P \(\rightarrow\) Q

DeMorganâ€™s laws (DeM): \(\neg\)(P \(\vee\) Q) \(\dashv\vdash\) \(\neg\)P & \(\neg\)Q and \(\neg\)(P & Q) \(\dashv\vdash\) \(\neg\)P \(\vee\) \(\neg\)Q
Truth Tables
For truth table problems, use system="magnusSL"
. It will display \(\neg\), &, âˆ¨, \(\rightarrow\), and \(\leftrightarrow\) for the logical operators, and will assign the truth values for the operators in the standard way.
Firstorder Logic
Although I used to cover firstorder logic in my 1000level 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 firstorder logic.