2.2.s. Summary
One way of combining principles of entailment uses the graphical idea of a tree. This provides a natural notation for the patterns of argument conjunction and extraction. The adequacy of this approach to entailment concerning conjunction can be shown by considering principles of entailment that state conditions for the validity of arguments that have conjunctions as conclusions or as premises. And patterns of argument, also with Latin names, can be added to capture the properties of ⊤ (ex nihilo verum) and ⊥ (ex falso quodlibet).
In fact, we will use a different, more compact notation for combining principles of entailment—a kind of natural deduction system that we will refer as a system of derivations. This notation presents the project of showing that an entailment holds as the task of closing a gap between its conclusion, which serves as a goal, and its premises, which serve as resources. As we narrow the initial gap (and others that result from it), we develop the derivation. The branching structure of tree-form proofs is represented in part by a system of vertical scope lines and in part by numerical annotations.
The laws of entailment appear as rules for exploiting resources, planning for goals, and closing gaps. There are rules for each of the patterns of argument that figure in tree-form proofs. The key rules for conjunction are Extraction (Ext) and Conjunction (Cnj). Quod Erat Demonstrandum (QED) is used to close a gap when its goal is among its resources, and the symbol ● (a black circle) marks a closed gap.
When a derivation is developed, numbers are used along with the labels for rules to record both the order of the development and the connection between the premises and conclusions of the rules.
Principles of entailment for other logical forms will be associated with further rules. Those for ⊤ and ⊥ are the rules Ex Nihilo Verum (ENV) and Ex Falso Quodlibet (EFQ).