# 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 *P*_{1}, *P*_{2}, … 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`

:

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

):

There is also a playground mode:

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:

`→I`

, which justifies an assertion of the form*φ*→*ψ*by citing a subproof beginning with the assumption*φ*and ending with the conclusion*ψ*;`¬I`

, which justifies an assertion of the form ¬*φ*by citing a subproof beginning with the assumption*φ*and ending with a pair of lines*ψ*,¬*ψ*.`¬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.