THE LOGIC NOTES

Natural deduction calculus Rules

The following are the logical rules for connectives in the standard natural deduction calculus:

A AND B ANDE
A
A AND B ANDE
B
A B ANDI
A AND B
A IMP B A IMPE
B
X, A  ⊢  B IMPI
X  ⊢  A IMP B
X  ⊢  A OR B Y, A  ⊢  C Z, B  ⊢  C ORE
X, Y, Z  ⊢  C
A ORI
A OR B
B ORI
A OR B
A NOT A NOTE
BAD
X, A  ⊢  BAD NOTI
X  ⊢  NOT A
X, A  ⊢  NOT B Y, A  ⊢  B RAA
X, Y  ⊢  NOT A
A NOTNOTI
NOTNOTA
NOTNOTA NOTNOTE
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:

A NOT A NOTEabs
B

For unrestricted quantifiers, as found in standard treatments of first order logic, we have:

ALLv A ALLE
Atv
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
Atv SOMEI
SOMEv A

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:

Atm t = u =E
Aum
  =I
t = t

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:

ALLv A EST(t) ALLEF
Atv
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