Natural Deduction in the forall x: Pittsburgh systems
This document gives a short description of how Carnap presents the systems of natural deduction from forall x: Pittsburgh, the remix by Dimitri Gallow of Aaron Thomas-Bolduc and Richard Zach's Calgary version of P.D. Magnus's forall x.
The syntax of formulas accepted is described in the Systems Reference.
The different admissible keyboard abbreviations for the different connectives are as follows:
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 the system
.GallowSLPlus with a Fitch-style guides overlay (activated with
Simple indent guides overlay (activated with
The SL systems
.GallowSLPlus allows all rules below.
.GallowSL is like
.GallowSLPlus except it disallows all derived rules, i.e., the
only allowed rules are
R, and the I and E rules for the connectives
and for ⊥.
It has the following set of rules for direct inferences:
||φ ∧ ψ||φ/ψ|
||φ, ψ||φ ∧ ψ|
||φ/ψ||φ ∨ ψ|
||φ/ψ, φ ↔︎ ψ||ψ/φ|
||¬ψ/¬φ, φ ∨ ψ||φ/ψ|
||φ → ψ, ¬ψ||¬φ|
|Double Negation Elim.||
||¬(φ∧ψ)||¬φ ∨ ¬ψ|
|¬(φ∨ψ)||¬φ ∧ ¬ψ|
|¬φ ∨ ¬ψ||¬(φ∧ψ)|
|¬φ ∧ ¬ψ||¬(φ∨ψ)|
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 φ.
¬E(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 ψ. LEM is a derived rule.
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
A/NOTETEXTHERE rather than
AS for an assumption.
Assumptions are only allowed on the first line of a subproof.
There are two proof systems corresponding to the Pittsburgh remix of
forall x. All of them allow sentence letters in first-order
formulas. The available relation symbols are the same as for SL: A
through Z, together with the infinitely many subscripted letters
F1, F2, … written
F_1, F_2 etc. However, the available
constants and function symbols are only a through v, together with
the infinitely many subscripted letters c1, c2, … written
c_1, c_2,…. The available variables are w through z, with the
infinitely many subscripted letters x1, x2, … written
The predicate logic system
.GallowPL of forall x: Pittsburgh extend the
rules of the system
.GallowSL with the following set of new
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
There is 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 proof system
.GallowPLPlus for the Pittsburgh version of forall x
adds, in addition to the (basic and derived) rules of
|Conversion of Quantifiers||
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.↩︎