# Natural deduction in the forall x: Mississippi State systems

This document gives a short description of how Carnap presents the systems of natural deduction from Greg Johnson's forall x: Mississippi State. At least some prior familiarity with Fitch-style proof systems is assumed.

The syntax of formulas accepted is described in the Systems Reference.

## Notation

The different admissible keyboard abbreviations for the different connectives are as follows:

Connective Keyboard
`->`, `=>`,`>`
& `/\`, `and`
`v`, `\/`, `|`, `or`
↔︎ `<->`, `<=>`
¬ `-`, `~`, `not`

The available sentence letters are A through Z, together with the infinitely many subscripted letters P1, P2, … written `P_1, P_2` and so on.

Proofs consist of a series of lines. A line is either an assertion line containing a formula followed by a `:` and then a justification for that formula, or a separator line containing two dashes, thus: `--`. A justification consists of a rule abbreviation followed by zero or more numbers (citations of particular lines) and pairs of numbers separated by a dash (citations of a subproof contained within the given line range).

A subproof is begun by increasing the indentation level. The first line of a subproof should be more indented than the containing proof, and the lines directly contained in this subproof should maintain this indentation level. (Lines indirectly contained, by being part of a sub-sub-proof, will need to be indented more deeply.) The subproof ends when the indentation level of the containing proof is resumed; hence, two contiguous sub-proofs of the same containing proof can be distinguished from one another by inserting a separator line between them at the same level of indentation as the containing proof. The final unindented line of a derivation will serve as the conclusion of the entire derivation.

Here's an example derivation, using the TFL system `.JohnsonSL`:

Ex
~P \/ (R & Q) :PR P :AS ~~P :DN 2 R & Q :\/E 1,3 Q :&E 4 P -> Q :->I 2-5

Or, with a Fitch-style guides overlay (activated with `guides="fitch"`):

Ex
~P \/ (R & Q) :PR P :AS ~~P :DN 2 R & Q :\/E 1,3 Q :&E 4 P -> Q :->I 2-5

There is also a playground mode:

Playground

The system for Johnson's forall x: Mississippi State (the system used in a proofchecker constructed with `.JohnsonSL` in Carnap's Pandoc Markup) has the following set of rules for direct inferences:

Rule Abbreviation Premises Conclusion
And-Elim `∧E` φ ∧ ψ φ/ψ
And-Intro `∧I` φ, ψ φ ∧ ψ
Or-Elim `∨E` ¬ψ, φ ∨ ψ φ
¬φ, φ ∨ ψ ψ
Or-Intro `∨I` φ φ ∨ ψ
ψ φ ∨ ψ
Conditional-Elim `→E` φ, φ → ψ ψ
Biconditional-Elim `↔︎E` φ, φ ↔︎ ψ ψ
ψ, φ ↔︎ ψ φ
Biconditional-Intro `↔︎I` φ → ψ, ψ → φ φ ↔︎ ψ
Double Negation `DN` φ ¬¬φ
Reiteration `R` φ φ

We also have four rules for indirect inferences:

1. `→I`, which justifies an assertion of the form φ → ψ by citing a subproof beginning with the assumption φ and ending with the conclusion ψ;
2. `¬I`, which justifies an assertion of the form ¬φ by citing a subproof beginning with the assumption φ and ending with a pair of lines ψ,¬ψ.
3. `¬E`, which justifies an assertion of the form φ by citing a subproof beginning with the assumption ¬φ and ending with a pair of lines ψ,¬ψ.

Finally, `PR` can be used to justify a line asserting a premise, and `AS` can be used to justify a line making an assumption. A note about the reason for an assumption can be included in the rendered proof by writing `A/NOTETEXTHERE` rather than `AS` for an assumption. Assumptions are only allowed on the first line of a subproof.