# Natural Deduction in the Carnap Book

This document gives a short description of the systems of natural deduction used in the Carnap book, and the two available second-order extensions of these systems. At least some prior familiarity with Montague-style proof systems is assumed.

## The Propositional System

### Notation

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

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

The available sentence letters are P through W, and 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, a show line consisting of the word `show` followed by a formula, or a QED line containing a `:` followed by a rule for an indirect inference.

A subproof begins a new show line. The next line 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 with a QED line at the same level of indentation as the containing proof.

For example:

Playground
Show P -> (P -> P) P:AS Show: P->P P:AS :CD 4 :CD 3

### Basic Rules

The propositional part of the system (the system used in a proofchecker constructed with `.Prop` in Carnap's Pandoc Markup) has the following set of rules for direct inferences:

Rule Abbreviation Premises Conclusion
Simplification `S` φ ∧ ψ φ/ψ
Adjunction `ADJ` φ, ψ φ ∧ ψ
Modus Ponens `MP` φ, φ → ψ ψ
Modus Tollens `MT` ¬ψ, φ → ψ ¬φ
Modus Tollendo Ponens `MTP` ¬ψφ, φ ∨ ψ φ/ψ
Addition `ADD` φ/ψ φ ∨ ψ
Conditional to Bicond. `CB` ψ → φ, φ → ψ ψ ↔ φ
Biconditional to Cond. `BC` ψ ↔ φ ψ → φ/φ → ψ
Double Negation Intro. `DNI` φ ¬¬φ
Double Negation Elem. `DNE` ¬¬φ φ
Double Negation `DN` φ/¬¬φ ¬¬φ/φ

We also have three rules for indirect inferences: `DD`, which closes a show line of the form Show : φ by citing an available line containing φ , `CD` which closes a show line of the form Show : φ → ψ by citing an available line containing ψ, and cancels the assumption φ if it is used to support this line, and `ID`, which choses a show line of the form Show : ¬φ by citing two available lines containing ψ and ¬ψ, canceling the assumption φ if it is used to support these 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.

### Derived Rules

Additional rules previously derived by users are allowed. These are regular rules of direct inference, and use abbreviations of the form `D-NAME`, where `NAME` is chosen by the user.

## The First Order System

### Notation

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

Connective Keyboard
`A`
`E`
= `=`

Sentence letters are as in the propositional system.

Application of a function or relation symbol is indicated by wrapping a comma-separated list of arguments in parentheses, and appending this to the symbol.

The available relation symbols are F through O, with the infinitely many subscripted letters F1, F2, … written `F_1, F_2,…`. The arity of a relation symbol is determined from context.

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

The available function symbols are f through h, with the infinitely many subscripted letters f1, f2, … written `f_1, f_2,…`. The arity of a function symbol is determined from context.

The available variables are v through z, with the infinitely many subscripted letters x1, x2, … written `x_1, x_2,…`.

### Basic Rules

The first-order part of the system (the system used in a proofchecker constructed with `.FirstOrder`) extends the propositional part of the system with the following set of new basic rules:

Rule Abbreviation Premises Conclusion
Leibniz's Law `LL` τ = σ, φ(τ)/φ(σ) φ(σ)/φ(τ)
Leibniz's Law (negative) `LL` φ(τ), ¬φ(σ) ¬(τ = σ)
Euclid's Law `EL` τ = σ θ(τ) = θ(σ)
Universal Instantiation `UI` xφ(x) φ(τ)
Existential Generalization `EG` φ(τ) xφ(x)
Quantifier Negation `QN` ¬∀xφ(x)/¬∃xφ(x)/∃¬xφ(x)/∀¬xφ(x) x¬φ(x)/∀x¬φ(x)/¬∀xφ(x)/¬∃xφ(x)
Symmetry `Sm` τ = σ σ = τ
Reflexivity `ID` τ = τ

It also adds two new rules for indirect derivations: `UD`, which closes a show line of the form Show : ∀xφ(x) by citing an available line φ(a), where a is a fresh constant1 , and `ED` which closes a show line of the form Show : ψ by citing an assertion of the form xφ(x), an assumption of the form φ(a) and an assertion of the form ψ, and cancels the assumption φ(a), where a is a fresh constant.2

### Traditional Kalish and Montague Rules

The basic rules for first-order logic listed above are not precisely the same as the rules given by Kalish and Montague in Formal Logic. In particular, universal derivations work differently, and existential derivations are replaced by a rule of existential instantiation.

Universal Derivations in Formal Logic closing a show line of the form Show : ∀xφ(x) are required to end by citing an available line ϕ(x) in which ϕ occurs with precisely the same variable free as we see bound in xϕ(x). Furthermore, the variable x must not occur free on any line available from the salient show line.

The rule of `EI` of existential instantiation allows one to infer from a premise of the form xϕ(x) that ϕ(y) for some variable not occurring free or bound on any earlier line in the proof.

These rules can be activated by using `.MontagueQC` (for "Quantifier Calculus") instead of `.FirstOrder` in the construction of the proof-checker.

## The Monadic Second-Order System

### Notation

The different admissible keyboard abbreviations for monadic second-order lambdas is as follows:

Connective Keyboard
λ \

First order syntax is as in the first-order system.

The available second-order variables are X through Z, with the infinitely many subscripted variables X1, X2, … written `X_1, X_2,…`.

A lambda abstract has the form λx[φ(x)], and can be applied like a predicate. Lambdas can only be applied to formulas, so the only abstracts that can be produced are for monadic relations.

### Basic Rules

The monadic second-order system (the system used in a proofchecker constructed with `.SecondOrder`) extends the first-order part of the system with the following set of new basic rules:

Rule Abbreviation Premises Conclusion
Abstraction `ABS` φ(σ) λx[φ(x)](σ)
Application `APP` λx[φ(x)](σ) φ(σ)
Monadic Univ. Instantiation `UI` XΦ(X) Φ(ζ)
Monadic Ex. Generalization `EG` Φ(ζ) XΦ(X)

Where ζ is schematic for a unary lambda term.

And with rules for indirect derivation UD and EG exactly analogous to the first-order case, except that a fresh second-order variable is used rather than a fresh constant.

## The Polyadic Second-Order System

### Notation

First order syntax is as in the first-order system.

The available 2nd-order n-ary variables are XN through ZN (where N is replaced by the arity of the variable), with the infinitely many subscripted variables XN1, XN2, … written `XN_1, XN_2,…`.

A lambda abstract has the form λx1λxn[φ(x1, …, xn)], and can be applied like an n-ary relation symbol.

### Basic Rules

The polyadic second-order system (the system used in a proofchecker constructed with `.PolySecondOrder`) extends the first-order part of the system with the following set of new basic rules:

Rule Abbreviation Premises Conclusion
n-Abstraction `ABSN` φ(σ1, …, σn) λx1xn[φ(x1, …, xn)](σ1, …σn)
n-Application `APPN` λx1xn[φ(x1, …, xn)](σ1, …σn) φ(σ1, …, σn)
n-ary Univ. Instantiation `UIN` XNΦ(XN) Φ(ζn)
n-ary Ex. Generalization `EGN` Φ(ζn) XNΦ(XN)

Where ζn is schematic for an n-ary lambda term.

And with rules of n-ary universal and existential derivation `UDN` and `EGN` exactly analogous to the first-order case, except that a fresh second-order variable is used rather than a fresh constant.

1. A fresh constant is one not appearing in the statement on the show line or in any assumption or premise on which the justifications for the show line depends, other than assumptions cancelled by the inference rule in question. For pedagogical purposes, it's easiest to say that a constant is fresh if it does not appear outside of the given subproof.

2. The fact that φ(a) needs to be cited as a premise is undesirable, and will be changed relatively soon, pending some improvements to the proof checking algorithm.