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. 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:
→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.
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 F_{1}, F_{2}, … 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 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 | ∃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 F_{1}, F_{2}, … written F_1, F_2
etc. However, the available constants
are only a through r, together with the infinitely many subscripted letters
c_{1}, c_{2}, … written c_1, c_2,…
. The available variables are
s through z, with the infinitely many subscripted letters x_{1}, x_{2}, … 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 |
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.↩