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

Playground
P:AS P:AS P:R 2 P->P:->I 2-3 P->(P->P):->I 1-4

### 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:

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 two subproofs, beginning with assuptions φ, ψ, respectively, and ending with conclusions ψ, φ, respectively;
3. `¬I`, which justifies an assertion of the form ¬φ by citing a subproof beginning with the assumption φ and ending with a pair of lines ψ,¬ψ.
4. `¬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.

#### 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) allows the propositional constant (`!?`, `_|_`). It 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:

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 two subproofs, beginning with assumptions φ, ψ, respectively, and ending with conclusions ψ, φ, respectively;
3. `¬I`, which justifies an assertion of the form ¬φ by citing a subproof beginning with the assumption φ and ending with a conclusion .
4. `∨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 φ.
5. `IP` (indirect proof), which justifies an assertion of the form φ by citing a subproof beginning with the assumption ¬φ and ending with a conclusion .
6. `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.

The system `.ZachTFL2019` is like `.ZachTFL` except it disallows all derived rules, i.e., the only allowed rules are `R`, `X`, `IP`, and the I and E rules for the connectives.

Because the Calgary FOL systems treat v as a variable, `v` is not allowed as a keyboard shortcut for .

## First-Order System QL

The proof system for Magnus's forall x, QL, is activated using `.ForallxQL`.

### 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 F1, F2, … written `F1, F2. The arity of a relation symbol is determined from context.

The available constants are a through w, with the infinitely many subscripted letters c1, c2, … written `c_1, c_2,…`.

The available variables are x through z, with the infinitely many subscripted letters x1, x2, … 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 `∃I` φ(σ) 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.

### Calgary FOL Systems

There are three systems corresponding to the Calgary remix of forall x. All of them allow sentence letters in first-order formulas. The available relation symbols are the same as for QL: A through Z, together with the infinitely many subscripted letters F1, F2, … written `F_1, F_2` etc. However, the available constants are only a through r, together with the infinitely many subscripted letters c1, c2, … written `c_1, c_2,…`. The available variables are s through z, with the infinitely many subscripted letters x1, x2, … written `x_1, x_2,…`.

Again, because the Calgary systems treat v as a variable, `v` is not allowed as a keyboard shortcut for . However, the Calgary systems also allow `@` for and `3` for .

Connective Keyboard
`A`, `@`
`E`, `3`
= `=`

As of the Fall 2019 edition of forall x: Calgary, the syntax for first-order formulas has arguments to predicates in parentheses and with commas (e.g., F(a, b)); prior to that edition, the convention was the same as in the original and Cambridge editions of forall x (e.g., Fab).

The original proof system for the Calgary version of forall x, `.ZachFOL` adds, in addition to the basic rules of `ForallxQL`, the rules

Rule Abbreviation Premises Conclusion
Conversion of Quantifiers `CQ` ¬∀xφ(x) x¬φ(x)
x¬φ(x) ¬∀xφ(x)
¬∃xφ(x) x¬φ(x)
x¬φ(x) ¬∃xφ(x)

The 2019 versions of the FOL systems use the new syntax, i.e., F(a, b) instead of Fab. The system `.ZachFOL2019` allows only the basic rules of the TFL system and the basic rules of QL. The system `.ZachFOLPlus2019` allows the basic and derived rules of `.ZachTFL` and the CQ rules listed above.

In summary:

System TFL Rules FOL Syntax FOL Rules
`.ZachTFL` Basic + Derived
`.ZachFOL` Basic + Derived Fab Basic + CQ
`.ZachTFL2019` Basic
`.ZachFOL2019` Basic F(a,b) Basic
`.ZachFOLPlus2019` Basic + Derived F(a,b) Basic + CQ

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