3.5.s. Summary

1

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 those rules may not bring a derivation any closer to is final state.

2

Although insight or foresight can help to shorten a derivation, all that is needed to complete a derivation is an understanding of what rules may be applied at any given stage. This is illustrated in the commentary on an extended example.

3

Derivations can be approached systematically through a 5-step procedure that is applied repeatedly until all gaps close or the derviation reaches a dead end.


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)
Glen Helman 23 Sep 2009