3.5.s. Summary
Any step in a derivation that is allowed by the basic rules (that is, for now, all rules except LFR and Adj) is safe and will take the derivation some way towards completion. We call the system of derivations limited to those rules the basic system. There will often be different orders in which the basic rules can be applied, and such differences may lead to longer or shorter derivations. The use of non-basic rules can sometimes shorten derivations still further, but they may not bring a derivation any closer to is final state.
The following table collects all rules we have now seen (and, as with the table of 2.4.s, the rule labels are links to the original statements of the rules):
|
Rules for developing gaps
|
|
|
for resources
|
for goals
|
atomic
sentence
|
|
IP
|
negation
¬ φ
|
CR
(if φ is not atomic
and the goal is ⊥)
|
RAA
|
conjunction
φ ∧ ψ
|
Ext
|
Cnj
|
|
|
|
Rules for closing gaps
|
|
when to close
|
rule
|
the goal is also
a resource
|
QED
|
sentences φ and ¬ φ are
resources & the goal is ⊥
|
Nc
|
|
⊤ is the goal
|
ENV
|
|
⊥ is a resource
|
EFQ
|
|
Basic system
|
|
|
|
|
Attachment rule
|
|
added resource
|
rule
|
|
φ ∧ ψ
|
Adj
|
|
Rule for lemmas
|
|
prerequisite
|
rule
|
|
the goal is ⊥
|
LFR
|
|
Added rules
(optional)
|