The following are the logical rules for connectives in the
standard natural deduction calculus:
|
|
|
|
|
X, A
⊢ B |
IMPI |
X ⊢ A
IMP B |
|
|
X ⊢ A OR B |
Y, A
⊢ C |
Z, B
⊢ C |
ORE |
X, Y, Z
⊢ C |
|
|
|
|
|
|
X, A
⊢ BAD |
NOTI |
X ⊢
NOT A |
|
|
X, A ⊢
NOT B |
Y, A
⊢ B |
RAA |
X, Y ⊢ NOT
A |
|
|
|
|
|
Where there is no discharge, the sets of premises
(assumptions) do not change, so they have been omitted
from the notation in the interests of clarity. Discharged
assumptions need not actually be present, as vacuous
discharge is allowed. In the rule RAA, the
discharged A will typically be present on one
side at most, though it is allowed to occur on both.
The rule NOTNOTI is redundant, but is included in the
set as it is one of the primitive rules given by Lemmon in
his original version of the system [8], and it matches the
NOTNOTE rule which is required for all proofs of
intuitionistically invalid sequents. RAA is equivalent in
the context of the rest to NOTI and NOTE.
To obtain intuitionistic (constructive) logic, omit the rule
NOTNOTE and strengthen NOTE to the "absurdity" rule:
For unrestricted quantifiers, as found in standard
treatments of first order logic, we have:
|
|
X
⊢ A |
ALLI |
m not in any formula
in X |
X ⊢
ALLv
Avm |
|
|
X
⊢ SOMEv
Avm |
Y, A ⊢ B |
SOMEE |
m not in B or in
any formula in Y |
X, Y ⊢
B |
|
|
|
|
|
Here t is any term, m any name
and v any variable. It is assumed that all
formulae are
well-formed. Aφψis
the result of substituting expression φ for all
occurrences of expression ψ in A.
The relation of identity is given special status because
of its importance in reasoning and in knowledge
representation. It has its own introduction and
elimination rules:
The following versions of the quantifier rules govern
restricted quantifiers:
ALL( v: A ) B |
Atv |
ALLER |
Btv |
|
|
|
X, A
⊢ B |
ALLIR |
m not in any
formula in X |
X ⊢
ALL( v: Avm) Bvm |
|
|
X
⊢ SOME( v: Avm) Bvm |
Y, A, B
⊢ C |
SOMEER |
m not in C or in
any formula in Y |
X, Y ⊢
C |
|
|
|
Atv |
Btv |
SOMEIR |
SOME( v: A ) B |
|
|
|
The quantifier rules for free logic are somewhat similar
in form, with the assumption of existence playing the role
of the sort indicator:
|
|
X, EST(m)
⊢ A |
ALLIF |
m not in any
formula in X |
X ⊢
ALLv
Avm |
|
|
X
⊢ SOME Avm |
Y, EST(m), A
⊢ B |
SOMEEF |
m not in B or in
any formula in Y |
X, Y ⊢
B |
|
|
|
Atv |
EST(t) |
SOMEIF |
SOMEv A |
|
|
|