# Natural Deduction in Logic Book Systems

This document gives a short description of how Carnap presents the systems of
natural deduction from Bergmann Moore and Nelson's *Logic Book*. At least some
prior familiarity with Fitch-style proof systems is assumed.

## Propositional Systems

### Notation

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

Connective | Keyboard |
---|---|

⊃ | `->` , `=>` ,`>` |

& | `/\` , `&` , `and` |

∨ | `\/` , `|` , `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: `--`

.^{1} A
justification consists of 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), followed by the name of a rule being applied.

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 system SD from the *Logic Book*

and here is one using system PD

### Basic Rules

#### Logic Book System SD

The minimal system SD from the *Logic Book* (the system used in a proofchecker
constructed with `.LogicBookSD`

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` |
φ/ψ |
φ ∨ ψ |

Condtional-Elim | `->E` .`CE` |
φ, φ ⊃ ψ |
ψ |

Biconditional-Elim | `<->E` ,`BE` |
φ/ψ, φ ↔ ψ |
ψ/φ |

Reiteration | `R` |
φ |
φ |

We also have four rules for indirect inferences:

`->I`

(also denoted`CI`

), which justifies an assertion of the form*φ*⊃*ψ*by citing a subproof beginning with the assumption*φ*and ending with the conclusion*ψ*;`<->I`

, (also denoted`BI`

) which justifies an assertion of the form φ↔ψ by citing two subproofs, beginning with assuptions*φ*,*ψ*, respectively, and ending with conclusions*ψ*,*φ*, respectively;`~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`

or `Assumption`

(to keep with the *Logic Book* terminology) can
be used to justify a line asserting a premise, and `AS`

can be used to justify
a line making an assumption. `A/SOMEADDITIONALTEXT`

(where
`SOMEADDITIONALTEXT`

indicates some additional text to be included alongside
the assumption in the rendered proof) can also be used to justify an
assumption. Assumptions are only allowed on the first line of a subproof.

#### Logic Book System SD Plus

The extended system SD Plus (the system used in a proofchecker constructed with
`.LogicBookSDPlus`

in Carnap's Pandoc
Markup) also adds the
following rules:

Rule | Abbreviation | Premises | Conclusion |
---|---|---|---|

Modus Tollens | `MT` |
φ ⊃ ψ, ∼ ψ |
∼ φ |

Hypothetical Syllogism | `HS` |
φ ⊃ ψ, ψ ⊃ χ |
φ ⊃ χ |

Disjunctive Syllogism | `DS` |
φ ∨ ψ, φ ⊃ χ, ψ ⊃ χ |
χ |

As well as the following exchange rules, which can be used within a propositional context Φ:

Rule | Abbreviation | Premises | Conclusion |
---|---|---|---|

Commutation | `Comm` |
Φ(φ&ψ) |
Φ(ψ&φ) |

Φ(φ ∨ ψ) |
Φ(ψ ∨ φ) |
||

Association | `Assoc` |
Φ(φ&(ψ&χ)) |
Φ((φ&ψ)&χ) |

Φ((φ&ψ)&χ) |
Φ(φ&(ψ&χ)) |
||

Φ(φ ∨ (ψ ∨ χ)) |
Φ((φ ∨ ψ) ∨ χ) |
||

Φ((φ ∨ ψ) ∨ χ) |
Φ(φ ∨ (ψ ∨ χ)) |
||

Implication | `Impl` |
Φ(φ ⊃ ψ)/Φ( ∼ φ ∨ ψ) |
Φ(φ ⊃ ψ)/Φ( ∼ φ ∨ ψ) |

Double Negation | `DN` |
Φ(φ)/Φ( ∼ ∼ φ) |
Φ( ∼ ∼ φ)/Φ(φ) |

Idempotence | `Idem` |
Φ(φ) |
Φ(φ&φ) |

Φ(φ&φ) |
Φ(φ) |
||

Φ(φ) |
Φ(φ ∨ φ) |
||

Φ(φ ∨ φ) |
Φ(φ) |
||

DeMorgan's Laws | `DeM` |
Φ( ∼ (φ&ψ)) |
Φ( ∼ φ ∨ ∼ ψ) |

Φ( ∼ (φ ∨ ψ)) |
Φ( ∼ φ& ∼ ψ) |
||

Φ( ∼ φ ∨ ∼ ψ) |
Φ( ∼ (φ&ψ)) |
||

Φ( ∼ φ& ∼ ψ) |
Φ( ∼ (φ ∨ ψ)) |
||

Transposition | `Trans` |
Φ(φ ⊃ ψ) |
Φ( ∼ ψ ⊃ ∼ φ)) |

Φ( ∼ ψ ⊃ ∼ φ)) |
Φ(φ ⊃ ψ) |
||

Exportation | `Exp` |
Φ(φ ⊃ (ψ ⊃ χ)) |
Φ(φ&ψ ⊃ χ) |

Φ(φ&ψ ⊃ χ) |
Φ(φ ⊃ (ψ ⊃ χ)) |
||

Distribution | `Dist` |
Φ(φ&(ψ ∨ χ)) |
Φ((φ&ψ) ∨ (φ&χ)) |

Φ((φ&ψ) ∨ (φ&χ)) |
Φ(φ&(ψ ∨ χ)) |
||

Φ(φ ∨ (ψ&χ)) |
Φ((φ ∨ ψ)&(φ ∨ χ)) |
||

Φ((φ ∨ ψ)&(φ ∨ χ)) |
Φ(φ ∨ (ψ&χ)) |
||

Equivalence | `Equiv` |
Φ(φ ↔ ψ) |
Φ(φ ⊃ ψ&ψ ⊃ φ) |

Φ(φ ⊃ ψ&ψ ⊃ φ) |
Φ(φ ↔ ψ) |
||

Φ(φ ↔ ψ) |
Φ((φ&ψ) ∨ ( ∼ ψ& ∼ φ)) |
||

Φ((φ&ψ) ∨ ( ∼ ψ& ∼ φ)) |
Φ(φ ↔ ψ) |

## First-Order Systems

### Notation

The different admissible keyboard abbreviations for quantifiers are as follows:

Connective | Keyboard |
---|---|

∀ | `A` |

∃ | `E` |

The Logic Book first order systems contain sentence letters *A* through *Z*,
together with the infinitely many subscripted letters *P*_{1}, *P*_{2}, … written
`P_1, P_2`

and so on.

Application of a relation symbol is indicated by directly appending the arguments to the symbol.

The available relation symbols are *A* through *Z*, together with the
infinitely many subscripted letters *F*_{1}, *F*_{2}, … written `F_1, F_2,…`

. The
arity of a relation symbol is determined from context.

The available constants are *a* through *v*, with the infinitely many
subscripted letters *c*_{1}, *c*_{2}, … written `c_1, c_2,…`

.

The available variables are *w* through *z*, with the infinitely many
subscripted letters *x*_{1}, *x*_{2}, … written `x_1, x_2,…`

.

Quantificational phrases are formed by appending a variable to a quantifier, and wrapping the result in parentheses.

### Basic Rules

The first-order *Logic Book* systems PD and PD+ (the systems used in
proofcheckers constructed with `.LogicBookPD`

, and `LogicBookPDPlus`

respectively) extend the rules of the system SD and SD+ respectively with the
following set of new basic rules:

Rule | Abbreviation | Premises | Conclusion |
---|---|---|---|

Existential Introduction | `EI` |
φ(σ) |
(∃x)φ(x) |

Universal Elimination | `AE` |
(∀x)φ(x) |
φ(σ) |

Universal Introduction | `AI` |
φ(σ) |
(∀x)φ(x) |

Where Universal Introduction is subject to the restriction that *σ* must not
appear in *φ*(*x*), or any undischarged assumption or in any premise of the
proof.^{2}

It also adds one new rule for indirect derivations: `EE`

, which justifies an
assertion *ψ* by citing an assertion of the form (∃*x*)*φ*(*x*) and a subproof
beginning with the assumption *φ*(*σ*) and ending with the conclusion *ψ*, where
*σ* does not appear in *ψ*, (∃*x*)*φ*(*x*), or in any of the undischarged assumptions
or premises of the proof.

To these rules, PD+ also adds the exchange rule:

Rule | Abbreviation | Premises | Conclusion |
---|---|---|---|

Quantifier Negation | `QN` |
Φ( ∼ (∀xφ)(x)) |
Φ((∃x) ∼ φ(x)) |

Φ((∃x) ∼ φ(x)) |
Φ( ∼ (∀x)φ(x)) |
||

Φ( ∼ (∃xφ)(x)) |
Φ((∀x) ∼ φ(x)) |
||

Φ((∀x) ∼ φ(x)) |
Φ( ∼ (∃x)φ(x)) |

These are intended for use when you have two contiguous subproofs and need to separate them - since they're at the same level of indentation, you need some extra indication to show that they're distinct subproofs.↩

Technically, Carnap checks only the assumptions and premises that are used in the derivation of

*φ*(*σ*). This has the same effect in terms of what's derivable, but is a little more lenient.↩