# Natural Deduction in forall x systems

This document gives a short description of how Carnap presents the systems of natural deduction from P.D. Magnus' *forall x* and from the Calgary remix of *forall x*. 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: `--`

. 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 system SL of P.D. Magnus forall x:

### Basic Rules

#### forall x System SL

The minimal system SL for P.D. Magnus' forall x (the system used in a proofchecker constructed with `.ForallxSL`

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` | φ, φ → ψ | ψ |

Biconditional-Elim | `↔E` | φ/ψ, φ ↔ ψ | ψ/φ |

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 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`

can be used to justify a line asserting a premise, and `AS`

can be used to justify a line making an assumption. Assumptions are only allowed on the first line of a subproof.

#### forall x System SL Plus

The extended system SL Plus for P.D. Magnus' forall x (the system used in a proofchecker constructed with `.ForallxSLPlus`

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

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

Dilemma | `DIL` | φ ∨ ψ, φ → χ, ψ → χ | χ |

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

Modus Tollens | `MT` | φ → ψ, ¬ψ | ¬φ |

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

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

Commutativity | `Comm` | Φ(φ ∧ ψ) | Φ(ψ ∧ φ) |

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

Φ(φ ↔ ψ) | Φ(ψ ↔ φ) | ||

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

Material Conditional | `MC` | Φ(φ → ψ) | Φ(¬φ ∨ ψ) |

Φ(¬φ ∨ ψ) | Φ(φ → ψ) | ||

Φ(φ ∨ ψ) | Φ(¬φ → ψ) | ||

Φ(¬φ → ψ) | Φ(φ ∨ ψ) | ||

BiConditional Exchange | `↔ex` | Φ(φ ↔ ψ) | Φ(φ → ψ ∧ ψ → φ) |

Φ(φ → ψ ∧ ψ → φ) | Φ(φ ↔ ψ) | ||

DeMorgan's Laws | `DeM` | Φ(¬(φ ∧ ψ)) | Φ(¬φ ∨ ¬ψ) |

Φ(¬(φ ∨ ψ)) | Φ(¬φ ∧ ¬ψ) | ||

Φ(¬φ ∨ ¬ψ) | Φ(¬(φ ∧ ψ)) | ||

Φ(¬φ ∧ ¬ψ) | Φ(¬(φ ∨ ψ)) |

#### Calgary TFL

The system TFL from the Calgary Remix of forall x (the system used in a proofchecker constructed with `.ZachTFL`

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

Negation-Elim | `¬E` | φ, ¬φ | ⊥ |

Explosion | `X` | ⊥ | ψ |

Biconditional-Elim | `↔E` | φ/ψ, φ ↔ ψ | ψ/φ |

Reiteration | `R` | φ | φ |

Disjunctive Syllogism | `DS` | ¬ψ/¬φ, φ ∨ ψ | φ/ψ |

Modus Tollens | `MT` | φ → ψ, ¬ψ | ¬φ |

Double Negation Elim. | `DNE` | ¬¬φ | φ |

DeMorgan's Laws | `DeM` | ¬(φ ∧ ψ) | ¬φ ∨ ¬ψ |

¬(φ ∨ ψ) | ¬φ ∧ ¬ψ | ||

¬φ ∨ ¬ψ | ¬(φ ∧ ψ) | ||

¬φ ∧ ¬ψ | ¬(φ ∨ ψ) |

We also have five 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 two subproofs, beginning with assumptions*φ*,*ψ*, 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 conclusion ⊥.`∨E`

, which justifies an assertion of the form φ by citing a disjunction*ψ*∨*χ*and two subproofs beginning with assumptions*ψ*,*χ*respectively and each ending with the conclusion*φ*.`IP`

(indirect proof), which justifies an assertion of the form*φ*by citing a subproof beginning with the assumption ¬*φ*and ending with a conclusion ⊥.`LEM`

(Law of the Excluded Middle), which justifies an assertion of the form*ψ*by citing two subproofs beginning with assumptions*φ*, ¬*φ*respectively and each ending with the conclusion*ψ*.

As above, `PR`

can be used to justify a line asserting a premise, and `AS`

can be used to justify a line making an assumption. Assumptions are only allowed on the first line of a subproof.

## First-Order Systems

### Notation

The different admissible keyboard abbreviations for quantifiers and equality is as follows:

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

∀ | `A` |

∃ | `E` |

= | `=` |

The forall x first-order systems do not contain sentence letters.

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 *w*, with the infinitely many subscripted letters *c*_{1}, *c*_{2}, … written `c_1, c_2,…`

.

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

.

### Basic Rules

The first-order forall x systems QL and FOL (the systems used in proofcheckers constructed with `.ForallxQL`

, and `ZachFOL`

respectively) extend the rules of the system SL and TFL respectively with the following set of new basic rules:

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

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

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

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

Equality Introduction | `=I` | σ = σ | |

Equality Elimination | `=E` | σ = τ, φ(σ)/φ(τ) | φ(τ)/φ(σ) |

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.^{1}

It also adds one new rule for indirect derivations: `∃E`

, 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.

The Calgary remix system FOL adds, in addition to these rules, the rule

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

Conversion of Quantifiers | `CQ` | ¬∀xφ(x) | ∃x¬φ(x) |

∃x¬φ(x) | ¬∀xφ(x) | ||

¬∃xφ(x) | ∀x¬φ(x) | ||

∀x¬φ(x) | ¬∃xφ(x) |

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.↩